CBMC
decision_procedure.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Decision Procedure Interface
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "decision_procedure.h"
13 
14 decision_proceduret::~decision_proceduret()
15 {
16 }
17 
18 decision_proceduret::resultt decision_proceduret::operator()()
19 {
20  return dec_solve();
21 }
22 
23 void decision_proceduret::set_to_true(const exprt &expr)
24 {
25  set_to(expr, true);
26 }
27 
28 void decision_proceduret::set_to_false(const exprt &expr)
29 {
30  set_to(expr, false);
31 }
exprt
Base class for all expressions.
Definition: expr.h:55
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Definition: decision_procedure.cpp:23
decision_proceduret::operator()
resultt operator()()
Run the decision procedure to solve the problem.
Definition: decision_procedure.cpp:18
decision_procedure.h
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
Definition: decision_procedure.cpp:28
decision_proceduret::set_to
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'.
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
Run the decision procedure to solve the problem.
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:43
decision_proceduret::~decision_proceduret
virtual ~decision_proceduret()
Definition: decision_procedure.cpp:14