#include <decision_procedure.h>
Inheritance diagram for decision_proceduret:Public Types | |
| enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
| Result of running the decision procedure. More... | |
Public Member Functions | |
| 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'. More... | |
| 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... | |
| 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. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem. More... | |
| virtual exprt | get (const exprt &expr) 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 () |
Protected Member Functions | |
| virtual resultt | dec_solve ()=0 |
| Run the decision procedure to solve the problem. More... | |
Detailed Description
Definition at line 20 of file decision_procedure.h.
Member Enumeration Documentation
◆ resultt
|
strong |
Result of running the decision procedure.
| Enumerator | |
|---|---|
| D_SATISFIABLE | |
| D_UNSATISFIABLE | |
| D_ERROR | |
Definition at line 43 of file decision_procedure.h.
Constructor & Destructor Documentation
◆ ~decision_proceduret()
|
virtual |
Definition at line 14 of file decision_procedure.cpp.
Member Function Documentation
◆ dec_solve()
|
protectedpure virtual |
Run the decision procedure to solve the problem.
Implemented in smt2_convt, string_refinementt, smt2_incremental_decision_proceduret, prop_conv_solvert, bv_refinementt, and smt2_dect.
◆ decision_procedure_text()
|
pure virtual |
Return a textual description of the decision procedure.
Implemented in string_refinementt, smt2_convt, smt2_incremental_decision_proceduret, prop_conv_solvert, bv_refinementt, and smt2_dect.
◆ get()
Return expr with variables replaced by values from satisfying assignment if available.
Return nil if not available
Implemented in string_refinementt, smt2_convt, boolbvt, prop_conv_solvert, and smt2_incremental_decision_proceduret.
◆ 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 smt2_convt, prop_conv_solvert, and smt2_incremental_decision_proceduret.
◆ operator()()
| decision_proceduret::resultt decision_proceduret::operator() | ( | ) |
Run the decision procedure to solve the problem.
Definition at line 18 of file decision_procedure.cpp.
◆ print_assignment()
|
pure virtual |
Print satisfying assignment to out.
Implemented in smt2_convt, boolbvt, smt2_incremental_decision_proceduret, and prop_conv_solvert.
◆ set_to()
|
pure virtual |
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Implemented in string_refinementt, boolbvt, smt2_convt, prop_conv_solvert, and smt2_incremental_decision_proceduret.
◆ set_to_false()
| void decision_proceduret::set_to_false | ( | const exprt & | expr | ) |
For a Boolean expression expr, add the constraint 'not expr'.
Definition at line 28 of file decision_procedure.cpp.
◆ set_to_true()
| void decision_proceduret::set_to_true | ( | const exprt & | expr | ) |
For a Boolean expression expr, add the constraint 'expr'.
Definition at line 23 of file decision_procedure.cpp.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/decision_procedure.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/decision_procedure.cpp
