resultt operator()()
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
void set_to_false(const exprt &)
For a Boolean expression expr, add the constraint 'not expr'.
virtual resultt dec_solve(const exprt &assumption)=0
Implementation of the decision procedure.
resultt
Result of running the decision procedure.
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual ~decision_proceduret()
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Base class for all expressions.
Decision Procedure Interface.
API to expression classes.