38 typedef std::pair<z3::expr, Type> Z3ExprTypePair;
42 std::vector<std::vector<z3::expr> > z3Stack_;
47 CommonSubexpressions ctxCses_;
49 VariableDeclarations ctxVarDecls_;
52 std::vector<SymbolicExpression::Ptr> holdingExprs_;
56#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
57 friend class boost::serialization::access;
60 void serialize(S &s,
const unsigned ) {
61 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
SmtSolver);
75 , ctx_(NULL), solver_(NULL)
79 ctx_ =
new z3::context;
80 solver_ =
new z3::solver(*ctx_);
81 z3Stack_.push_back(std::vector<z3::expr>());
114 explicit Z3Solver(
const boost::filesystem::path &exe,
const std::string &shellArgs =
"")
114 explicit Z3Solver(
const boost::filesystem::path &exe,
const std::string &shellArgs =
"") {
…}
132 virtual z3::context *z3Context()
const;
142 virtual z3::solver *z3Solver()
const;
152 virtual std::vector<z3::expr> z3Assertions()
const;
153 virtual std::vector<z3::expr> z3Assertions(
size_t level)
const;
166 SExprTypePair outputList(
const std::string &
name,
const std::vector<SExprTypePair>&,
Type rettype = NO_TYPE);
174 virtual void pop()
override;
176 virtual void timeout(boost::chrono::duration<double>)
override;
185 virtual Type mostType(
const std::vector<Z3ExprTypePair>&);
186 using SmtlibSolver::mostType;
187 Z3ExprTypePair ctxCast(
const Z3ExprTypePair&,
Type toType);
188 std::vector<Z3Solver::Z3ExprTypePair> ctxCast(
const std::vector<Z3ExprTypePair>&,
Type toType);
191 std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(
const std::vector<SymbolicExpression::Ptr>&);