cprover
decision_procedure.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Decision Procedure Interface
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "decision_procedure.h"
13
15{
16}
17
19{
20 return dec_solve();
21}
22
24{
25 set_to(expr, true);
26}
27
29{
30 set_to(expr, false);
31}
resultt operator()()
Run the decision procedure to solve the problem.
resultt
Result of running the decision procedure.
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.
Definition: expr.h:54
Decision Procedure Interface.