cprover
|
#include <smt2_incremental_decision_procedure.h>
Classes | |
class | sequencet |
Public Member Functions | |
smt2_incremental_decision_proceduret (const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler) | |
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. | |
exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. | |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . | |
std::string | decision_procedure_text () const override |
Return a textual description of the decision procedure. | |
std::size_t | get_number_of_solver_calls () const override |
Return the number of incremental solver calls. | |
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'. | |
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 . | |
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. | |
![]() | |
virtual void | push (const std::vector< exprt > &assumptions)=0 |
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions . | |
virtual void | push ()=0 |
Push a new context on the stack This context becomes a child context nested in the current context. | |
virtual void | pop ()=0 |
Pop whatever is on top of the stack. | |
virtual | ~stack_decision_proceduret ()=default |
![]() | |
virtual void | set_to (const exprt &expr, bool value)=0 |
For a Boolean expression expr , add the constraint 'expr' if value is true , otherwise add 'not expr'. | |
void | set_to_true (const exprt &expr) |
For a Boolean expression expr , add the constraint 'expr'. | |
void | set_to_false (const exprt &expr) |
For a Boolean expression expr , add the constraint 'not expr'. | |
virtual exprt | handle (const exprt &expr)=0 |
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. | |
resultt | operator() () |
Run the decision procedure to solve the problem. | |
virtual exprt | get (const exprt &expr) const =0 |
Return expr with variables replaced by values from satisfying assignment if available. | |
virtual void | print_assignment (std::ostream &out) const =0 |
Print satisfying assignment to out . | |
virtual std::string | decision_procedure_text () const =0 |
Return a textual description of the decision procedure. | |
virtual std::size_t | get_number_of_solver_calls () const =0 |
Return the number of incremental solver calls. | |
virtual | ~decision_proceduret () |
Protected Member Functions | |
resultt | dec_solve () override |
Run the decision procedure to solve the problem. | |
void | define_dependent_functions (const exprt &expr) |
Defines any functions which expr depends on, which have not yet been defined, along with their dependencies in turn. | |
void | ensure_handle_for_expr_defined (const exprt &expr) |
virtual resultt | dec_solve ()=0 |
Run the decision procedure to solve the problem. | |
Protected Attributes | |
const namespacet & | ns |
size_t | number_of_solver_calls |
std::unique_ptr< smt_base_solver_processt > | solver_process |
messaget | log |
class smt2_incremental_decision_proceduret::sequencet | handle_sequence |
std::unordered_map< exprt, smt_identifier_termt, irep_hash > | expression_handle_identifiers |
std::unordered_map< exprt, smt_identifier_termt, irep_hash > | expression_identifiers |
Additional Inherited Members | |
![]() | |
enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
Result of running the decision procedure. More... | |
Definition at line 23 of file smt2_incremental_decision_procedure.h.
|
explicit |
_ns | Namespace for looking up the expressions which symbol_exprts relate to. |
solver_process | The smt2 solver process communication interface. |
message_handler | The messaging system to be used for logging purposes. |
Definition at line 128 of file smt2_incremental_decision_procedure.cpp.
|
overrideprotectedvirtual |
Run the decision procedure to solve the problem.
Implements decision_proceduret.
Definition at line 305 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Return a textual description of the decision procedure.
Implements decision_proceduret.
Definition at line 240 of file smt2_incremental_decision_procedure.cpp.
|
protected |
Defines any functions which expr
depends on, which have not yet been defined, along with their dependencies in turn.
Definition at line 75 of file smt2_incremental_decision_procedure.cpp.
|
protected |
Definition at line 143 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 183 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Return the number of incremental solver calls.
Implements decision_proceduret.
Definition at line 246 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 160 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 287 of file smt2_incremental_decision_procedure.cpp.
|
overridevirtual |
Print satisfying assignment to out
.
Implements decision_proceduret.
Definition at line 233 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 282 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 271 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 251 of file smt2_incremental_decision_procedure.cpp.
|
protected |
Definition at line 78 of file smt2_incremental_decision_procedure.h.
|
protected |
Definition at line 80 of file smt2_incremental_decision_procedure.h.
|
protected |
|
protected |
Definition at line 64 of file smt2_incremental_decision_procedure.h.
|
protected |
Definition at line 59 of file smt2_incremental_decision_procedure.h.
|
protected |
Definition at line 61 of file smt2_incremental_decision_procedure.h.
|
protected |
Definition at line 63 of file smt2_incremental_decision_procedure.h.