cprover
|
#include <smt2_incremental_decision_procedure.h>
Public Member Functions | |
smt2_incremental_decision_proceduret (std::string solver_command) | |
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 is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More... | |
exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . More... | |
std::string | decision_procedure_text () const override |
Return a textual description of the decision procedure. More... | |
std::size_t | get_number_of_solver_calls () const override |
Return the number of incremental solver calls. More... | |
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'. More... | |
void | push (const std::vector< exprt > &assumptions) override |
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions . More... | |
void | push () override |
Push a new context on the stack This context becomes a child context nested in the current context. More... | |
void | pop () override |
Pop whatever is on top of the stack. More... | |
![]() | |
virtual | ~stack_decision_proceduret ()=default |
![]() | |
void | set_to_true (const exprt &expr) |
For a Boolean expression expr , add the constraint 'expr'. More... | |
void | set_to_false (const exprt &expr) |
For a Boolean expression expr , add the constraint 'not expr'. More... | |
resultt | operator() () |
Run the decision procedure to solve the problem. More... | |
virtual | ~decision_proceduret () |
Protected Member Functions | |
resultt | dec_solve () override |
Run the decision procedure to solve the problem. More... | |
Protected Attributes | |
std::string | solver_command |
This is where we store the solver command for reporting the solver used. More... | |
size_t | number_of_solver_calls |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Result of running the decision procedure. More... | |
Definition at line 11 of file smt2_incremental_decision_procedure.h.
|
explicit |
solver_command | The command and arguments for invoking the smt2 solver. |
Definition at line 7 of file smt2_incremental_decision_procedure.cpp.
|
overrideprotectedvirtual |
Run the decision procedure to solve the problem.
Implements decision_proceduret.
Definition at line 69 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Return a textual description of the decision procedure.
Implements decision_proceduret.
Definition at line 30 of file smt2_incremental_decision_procedure.cpp.
Return expr
with variables replaced by values from satisfying assignment if available.
Return nil
if not available
Implements decision_proceduret.
Definition at line 18 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Return the number of incremental solver calls.
Implements decision_proceduret.
Definition at line 36 of file smt2_incremental_decision_procedure.cpp.
Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.
The returned expression may be the expression itself or a more compact but solver-specific representation.
Implements decision_proceduret.
Definition at line 13 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Pop whatever is on top of the stack.
Popping from the empty stack results in an invariant violation.
Implements stack_decision_proceduret.
Definition at line 64 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Print satisfying assignment to out
.
Implements decision_proceduret.
Definition at line 23 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Push a new context on the stack This context becomes a child context nested in the current context.
Implements stack_decision_proceduret.
Definition at line 59 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions
.
This context becomes a child context nested in the current context. An assumption is usually obtained by calling decision_proceduret::handle
. Thus it can be a Boolean expression or something more solver-specific such as literal_exprt
. An empty vector of assumptions counts as an element on the stack (and therefore needs to be popped), but has no effect beyond that.
Implements stack_decision_proceduret.
Definition at line 48 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
For a Boolean expression expr
, add the constraint 'expr' if value
is true
, otherwise add 'not expr'.
Implements decision_proceduret.
Definition at line 41 of file smt2_incremental_decision_procedure.cpp.
|
protected |
Definition at line 38 of file smt2_incremental_decision_procedure.h.
|
protected |
This is where we store the solver command for reporting the solver used.
Definition at line 37 of file smt2_incremental_decision_procedure.h.