#include <stack_decision_procedure.h>
Inheritance diagram for stack_decision_proceduret: Collaboration diagram for stack_decision_proceduret:Public Member Functions | |
| 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. More... | |
| virtual void | push ()=0 |
| Push a new context on the stack This context becomes a child context nested in the current context. More... | |
| virtual void | pop ()=0 |
| Pop whatever is on top of the stack. More... | |
| virtual | ~stack_decision_proceduret ()=default |
| Public Member Functions inherited from decision_proceduret | |
| virtual void | set_to (const exprt &, bool value)=0 |
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'. More... | |
| void | set_to_true (const exprt &) |
For a Boolean expression expr, add the constraint 'expr'. More... | |
| void | set_to_false (const exprt &) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| virtual exprt | handle (const exprt &)=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. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More... | |
| resultt | operator() (const exprt &assumption) |
| Run the decision procedure to solve the problem under the given assumption. More... | |
| virtual exprt | get (const exprt &) const =0 |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
| virtual void | print_assignment (std::ostream &out) const =0 |
Print satisfying assignment to out. More... | |
| virtual std::string | decision_procedure_text () const =0 |
| Return a textual description of the decision procedure. More... | |
| virtual std::size_t | get_number_of_solver_calls () const =0 |
| Return the number of incremental solver calls. More... | |
| virtual | ~decision_proceduret () |
Additional Inherited Members | |
| Public Types inherited from decision_proceduret | |
| enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
| Result of running the decision procedure. More... | |
| Protected Member Functions inherited from decision_proceduret | |
| virtual resultt | dec_solve (const exprt &assumption)=0 |
| Implementation of the decision procedure. More... | |
Detailed Description
Definition at line 57 of file stack_decision_procedure.h.
Constructor & Destructor Documentation
◆ ~stack_decision_proceduret()
|
virtualdefault |
Member Function Documentation
◆ pop()
|
pure virtual |
Pop whatever is on top of the stack.
Popping from the empty stack results in an invariant violation.
Implemented in smt2_incremental_decision_proceduret, smt2_convt, and prop_conv_solvert.
◆ push() [1/2]
|
pure virtual |
Push a new context on the stack This context becomes a child context nested in the current context.
Implemented in smt2_incremental_decision_proceduret, smt2_convt, and prop_conv_solvert.
◆ push() [2/2]
|
pure virtual |
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.
Implemented in smt2_incremental_decision_proceduret, prop_conv_solvert, and smt2_convt.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/stack_decision_procedure.h
