1 #ifndef Rose_BinaryAnalysis_Z3Solver_H
2 #define Rose_BinaryAnalysis_Z3Solver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <BinarySmtlibSolver.h>
10 #ifdef ROSE_HAVE_Z3_VERSION_H
11 #include <z3_version.h>
18 #include <boost/serialization/access.hpp>
36 typedef std::pair<z3::expr, Type> Z3ExprTypePair;
40 std::vector<std::vector<z3::expr> > z3Stack_;
42 CommonSubexpressions ctxCses_;
44 VariableDeclarations ctxVarDecls_;
48 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
49 friend class boost::serialization::access;
52 void serialize(S &s,
const unsigned ) {
53 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
SmtSolver);
67 , ctx_(NULL), solver_(NULL)
71 ctx_ =
new z3::context;
72 solver_ =
new z3::solver(*ctx_);
73 z3Stack_.push_back(std::vector<z3::expr>());
108 explicit Z3Solver(
const boost::filesystem::path &exe,
const std::string &shellArgs =
"")
126 virtual z3::context *z3Context()
const;
136 virtual z3::solver *z3Solver()
const;
146 virtual std::vector<z3::expr> z3Assertions()
const;
147 virtual std::vector<z3::expr> z3Assertions(
size_t level)
const;
160 SExprTypePair outputList(
const std::string &
name,
const std::vector<SExprTypePair>&,
Type rettype = NO_TYPE);
165 virtual
void reset() ROSE_OVERRIDE;
168 virtual
void pop() ROSE_OVERRIDE;
169 virtual
void selfTest() ROSE_OVERRIDE;
170 virtual
void timeout(
boost::chrono::duration<
double>) ROSE_OVERRIDE;
174 virtual SExprTypePair outputExpression(const SymbolicExpr::
Ptr&) ROSE_OVERRIDE;
175 virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
179 virtual Type mostType(
const std::vector<Z3ExprTypePair>&);
180 using SmtlibSolver::mostType;
181 Z3ExprTypePair ctxCast(
const Z3ExprTypePair&,
Type toType);
182 std::vector<Z3Solver::Z3ExprTypePair> ctxCast(
const std::vector<Z3ExprTypePair>&,
Type toType);
185 std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(
const std::vector<SymbolicExpr::Ptr>&);
211 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
virtual void selfTest() ROSE_OVERRIDE
Unit tests.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Interface to the Z3 SMT solver.
virtual void pop() ROSE_OVERRIDE
Pop a backtracking point.
virtual Satisfiable checkLib() ROSE_OVERRIDE
Check satisfiability using a library API.
virtual Ptr create() const ROSE_OVERRIDE
Virtual constructor.
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
const std::string & name() const
Property: Name of solver for debugging.
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
Generate definitions for bit-wise XOR functions.
Main namespace for the ROSE library.
Satisfiable
Satisfiability constants.
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Reference-counting intrusive smart pointer.
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
Wrapper around solvers that speak SMT-LIB.
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
Generate functions for comparison of bitvectors.
virtual void z3Update()
Updates the Z3 state to match the ROSE state.
virtual void reset() ROSE_OVERRIDE
Reset solver state.
Type
Type (sort) of expression.
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Interface to Satisfiability Modulo Theory (SMT) solvers.
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Container associating values with keys.
LinkMode linkage() const
Property: How ROSE communicates with the solver.