|
| equalityt (propt &_prop, message_handlert &message_handler) |
|
virtual literalt | equality (const exprt &e1, const exprt &e2) |
|
void | post_process () override |
|
| prop_conv_solvert (propt &_prop, message_handlert &message_handler) |
|
virtual | ~prop_conv_solvert ()=default |
|
decision_proceduret::resultt | dec_solve () override |
| Run the decision procedure to solve the problem. 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...
|
|
exprt | get (const exprt &expr) const override |
| Return expr with variables replaced by values from satisfying assignment if available. More...
|
|
tvt | l_get (literalt a) const override |
| Return value of literal l from satisfying assignment. More...
|
|
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...
|
|
void | set_frozen (literalt) |
|
void | set_frozen (const bvt &) |
|
void | set_all_frozen () |
|
literalt | convert (const exprt &expr) override |
| Convert a Boolean expression and return the corresponding literal. More...
|
|
bool | is_in_conflict (const exprt &expr) const override |
| Returns true if an expression is in the final conflict leading to UNSAT. More...
|
|
void | set_to (const exprt &expr, bool value) override |
| For a Boolean expression expr , add the constraint 'current_context => expr' if value is true , otherwise add 'current_context => not expr'. More...
|
|
void | push () override |
| Push a new context on the stack This context becomes a child context nested in the current context. More...
|
|
void | push (const std::vector< exprt > &assumptions) override |
| Push assumptions in form of literal_exprt More...
|
|
void | pop () override |
| Pop whatever is on top of the stack. More...
|
|
bool | literal (const symbol_exprt &expr, literalt &literal) const |
|
virtual void | clear_cache () |
|
const cachet & | get_cache () const |
|
const symbolst & | get_symbols () const |
|
void | set_time_limit_seconds (uint32_t lim) override |
| Set the limit for the solver to time out in seconds. More...
|
|
std::size_t | get_number_of_solver_calls () const override |
| Return the number of incremental solver calls. More...
|
|
void | with_solver_hardness (handlert handler) override |
|
void | enable_hardness_collection () override |
|
virtual | ~conflict_providert ()=default |
|
virtual | ~prop_convt () |
|
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 () |
|
virtual | ~solver_resource_limitst ()=default |
|
virtual | ~hardness_collectort ()=default |
|
Definition at line 19 of file equality.h.