resultt operator()()
Run the decision procedure to solve the problem.
resultt
Result of running the decision procedure.
virtual ~decision_proceduret()
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
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'.
virtual resultt dec_solve()=0
Run the decision procedure to solve the problem.
Base class for all expressions.
Decision Procedure Interface.