1 #ifndef ROSE_BinaryAnalysis_Z3Solver_H
2 #define ROSE_BinaryAnalysis_Z3Solver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/SmtlibSolver.h>
10 #ifdef ROSE_HAVE_Z3_VERSION_H
11 #include <z3_version.h>
18 #include <boost/serialization/access.hpp>
21 namespace BinaryAnalysis {
36 typedef std::pair<z3::expr, Type> Z3ExprTypePair;
40 std::vector<std::vector<z3::expr> > z3Stack_;
45 CommonSubexpressions ctxCses_;
47 VariableDeclarations ctxVarDecls_;
50 std::vector<SymbolicExpression::Ptr> holdingExprs_;
54 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
55 friend class boost::serialization::access;
58 void serialize(S &s,
const unsigned ) {
59 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
SmtSolver);
73 , ctx_(NULL), solver_(NULL)
77 ctx_ =
new z3::context;
78 solver_ =
new z3::solver(*ctx_);
79 z3Stack_.push_back(std::vector<z3::expr>());
112 explicit Z3Solver(
const boost::filesystem::path &exe,
const std::string &shellArgs =
"")
130 virtual z3::context *z3Context()
const;
140 virtual z3::solver *z3Solver()
const;
150 virtual std::vector<z3::expr> z3Assertions()
const;
151 virtual std::vector<z3::expr> z3Assertions(
size_t level)
const;
164 SExprTypePair outputList(
const std::string &
name,
const std::vector<SExprTypePair>&,
Type rettype = NO_TYPE);
169 virtual void reset()
override;
172 virtual void pop()
override;
174 virtual void timeout(boost::chrono::duration<double>)
override;
176 virtual void outputBvxorFunctions(std::ostream&,
const std::vector<SymbolicExpression::Ptr>&)
override;
183 virtual Type mostType(
const std::vector<Z3ExprTypePair>&);
184 using SmtlibSolver::mostType;
185 Z3ExprTypePair ctxCast(
const Z3ExprTypePair&,
Type toType);
186 std::vector<Z3Solver::Z3ExprTypePair> ctxCast(
const std::vector<Z3ExprTypePair>&,
Type toType);
189 std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(
const std::vector<SymbolicExpression::Ptr>&);
215 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
virtual void reset() override
Reset solver state.
virtual void parseEvidence() override
Parses evidence of satisfiability.
Interface to the Z3 SMT solver.
Sawyer::Container::Set< SymbolicExpression::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override
Generate definitions for bit-wise XOR functions.
virtual void timeout(boost::chrono::duration< double >) override
Set the timeout for the solver.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override
Generate functions for comparison of bitvectors.
Base class for symbolic expression nodes.
virtual void pop() override
Pop a backtracking point.
const std::string & name() const
Property: Name of solver for debugging.
Main namespace for the ROSE library.
Satisfiable
Satisfiability constants.
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
Reference-counting intrusive smart pointer.
virtual void selfTest() override
Unit tests.
virtual Satisfiable checkLib() override
Check satisfiability using a library API.
Wrapper around solvers that speak SMT-LIB.
virtual void z3Update()
Updates the Z3 state to match the ROSE state.
Type
Type (sort) of expression.
Leaf node of an expression tree for instruction semantics.
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Interior node of an expression tree for instruction semantics.
Interface to Satisfiability Modulo Theory (SMT) solvers.
virtual void clearEvidence() override
Clears evidence information.
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Container associating values with keys.
virtual Ptr create() const override
Virtual constructor.