8 std::string solver_command)
9 : solver_command{std::move(solver_command)}, number_of_solver_calls{0}
24 std::ostream &out)
const
44 "`set_to` (" + std::string{value ?
"true" :
"false"} +
"):\n " +
49 const std::vector<exprt> &assumptions)
51 for(
const auto &assumption : assumptions)
54 "pushing of assumption:\n " + assumption.pretty(2, 0));
resultt
Result of running the decision procedure.
Base class for all expressions.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
size_t number_of_solver_calls
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
resultt dec_solve() override
Run the decision procedure to solve the problem.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
void pop() override
Pop whatever is on top of the stack.
std::string solver_command
This is where we store the solver command for reporting the solver used.
smt2_incremental_decision_proceduret(std::string solver_command)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)