|
| equalityt (propt &_prop, message_handlert &message_handler) |
|
virtual literalt | equality (const exprt &e1, const exprt &e2) |
|
void | finish_eager_conversion () override |
|
| prop_conv_solvert (propt &_prop, message_handlert &message_handler) |
|
virtual | ~prop_conv_solvert ()=default |
|
virtual void | finish_eager_conversion () |
|
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...
|
|
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...
|
|
hardness_collectort * | get_hardness_collector () |
|
virtual bool | is_in_conflict (const exprt &) const =0 |
| Returns true if an expression is in the final conflict leading to UNSAT. More...
|
|
virtual | ~conflict_providert ()=default |
|
virtual | ~prop_convt () |
|
virtual literalt | convert (const exprt &expr)=0 |
| Convert a Boolean expression and return the corresponding literal. More...
|
|
virtual tvt | l_get (literalt l) const =0 |
| Return value of literal l from satisfying assignment. More...
|
|
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 |
|
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 () |
|
virtual void | set_time_limit_seconds (uint32_t)=0 |
| Set the limit for the solver to time out in seconds. More...
|
|
virtual | ~solver_resource_limitst ()=default |
|
Definition at line 19 of file equality.h.