An interface for a decision procedure for satisfiability problems. More...
#include <decision_procedure.h>
Inheritance diagram for decision_proceduret:Public Types | |
| enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
| Result of running the decision procedure. More... | |
Public Member Functions | |
| 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'. | |
| void | set_to_true (const exprt &) |
For a Boolean expression expr, add the constraint 'expr'. | |
| void | set_to_false (const exprt &) |
For a Boolean expression expr, add the constraint 'not expr'. | |
| 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. | |
| resultt | operator() () |
| Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. | |
| resultt | operator() (const exprt &assumption) |
| Run the decision procedure to solve the problem under the given assumption. | |
| virtual exprt | get (const exprt &) 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 | |
| virtual resultt | dec_solve (const exprt &assumption)=0 |
| Implementation of the decision procedure. | |
Detailed Description
An interface for a decision procedure for satisfiability problems.
Definition at line 21 of file decision_procedure.h.
Member Enumeration Documentation
◆ resultt
Result of running the decision procedure.
| Enumerator | |
|---|---|
| D_SATISFIABLE | |
| D_UNSATISFIABLE | |
| D_ERROR | |
Definition at line 44 of file decision_procedure.h.
Constructor & Destructor Documentation
◆ ~decision_proceduret()
|
virtual |
Definition at line 16 of file decision_procedure.cpp.
Member Function Documentation
◆ dec_solve()
Implementation of the decision procedure.
Implemented in prop_conv_solvert, bv_refinementt, smt2_convt, smt2_dect, smt2_incremental_decision_proceduret, and string_refinementt.
◆ decision_procedure_text()
|
pure virtual |
Return a textual description of the decision procedure.
Implemented in prop_conv_solvert, bv_refinementt, smt2_convt, smt2_dect, smt2_incremental_decision_proceduret, and string_refinementt.
◆ get()
Return expr with variables replaced by values from satisfying assignment if available.
Return nil if not available
Implemented in boolbvt, prop_conv_solvert, smt2_convt, smt2_incremental_decision_proceduret, and string_refinementt.
◆ get_number_of_solver_calls()
|
pure virtual |
Return the number of incremental solver calls.
Implemented in prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.
◆ handle()
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.
Implemented in boolbvt, prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.
◆ operator()() [1/2]
| decision_proceduret::resultt decision_proceduret::operator() | ( | ) |
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
Definition at line 20 of file decision_procedure.cpp.
◆ operator()() [2/2]
| decision_proceduret::resultt decision_proceduret::operator() | ( | const exprt & | assumption | ) |
Run the decision procedure to solve the problem under the given assumption.
This corresponds to SMT-LIB's check-sat-assuming.
Definition at line 26 of file decision_procedure.cpp.
◆ print_assignment()
Print satisfying assignment to out.
Implemented in boolbvt, prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.
◆ set_to()
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Implemented in boolbvt, prop_conv_solvert, smt2_convt, smt2_incremental_decision_proceduret, and string_refinementt.
◆ set_to_false()
For a Boolean expression expr, add the constraint 'not expr'.
Definition at line 36 of file decision_procedure.cpp.
◆ set_to_true()
For a Boolean expression expr, add the constraint 'expr'.
Definition at line 31 of file decision_procedure.cpp.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/decision_procedure.h
- /home/runner/work/cbmc/cbmc/src/solvers/decision_procedure.cpp
