|
| | 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.
|
| |
| void | print_assignment (std::ostream &out) const override |
| | Print satisfying assignment to out.
|
| |
| std::string | decision_procedure_text () const override |
| | Return a textual description of the decision procedure.
|
| |
| exprt | get (const exprt &expr) const override |
| | Return expr with variables replaced by values from satisfying assignment if available.
|
| |
| tvt | l_get (literalt a) const override |
| | Return value of literal l from satisfying assignment.
|
| |
| 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.
|
| |
| 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.
|
| |
| bool | is_in_conflict (const exprt &expr) const override |
| | Returns true if an expression is in the final conflict leading to UNSAT.
|
| |
| 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'.
|
| |
| void | push () override |
| | Push a new context on the stack This context becomes a child context nested in the current context.
|
| |
| void | push (const std::vector< exprt > &assumptions) override |
| | Push assumptions in form of literal_exprt
|
| |
| void | pop () override |
| | Pop whatever is on top of the stack.
|
| |
| 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.
|
| |
| std::size_t | get_number_of_solver_calls () const override |
| | Return the number of incremental solver calls.
|
| |
| 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.
|
| |
| virtual | ~conflict_providert ()=default |
| |
| virtual | ~prop_convt () |
| |
| virtual literalt | convert (const exprt &expr)=0 |
| | Convert a Boolean expression and return the corresponding literal.
|
| |
| virtual tvt | l_get (literalt l) const =0 |
| | Return value of literal l from satisfying assignment.
|
| |
| 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.
|
| |
| virtual void | push ()=0 |
| | Push a new context on the stack This context becomes a child context nested in the current context.
|
| |
| virtual void | pop ()=0 |
| | Pop whatever is on top of the stack.
|
| |
| 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'.
|
| |
| void | set_to_true (const exprt &expr) |
| | For a Boolean expression expr, add the constraint 'expr'.
|
| |
| void | set_to_false (const exprt &expr) |
| | For a Boolean expression expr, add the constraint 'not expr'.
|
| |
| 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.
|
| |
| resultt | operator() () |
| | Run the decision procedure to solve the problem.
|
| |
| virtual exprt | get (const exprt &expr) 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 () |
| |
| virtual void | set_time_limit_seconds (uint32_t)=0 |
| | Set the limit for the solver to time out in seconds.
|
| |
| virtual | ~solver_resource_limitst ()=default |
| |
Definition at line 19 of file equality.h.
Inheritance diagram for equalityt: