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 #include <util/std_expr.h>
15 
17 {
18 }
19 
21 {
22  return dec_solve(nil_exprt());
23 }
24 
27 {
28  return dec_solve(assumption);
29 }
30 
32 {
33  set_to(expr, true);
34 }
35 
37 {
38  set_to(expr, false);
39 }
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 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.
Definition: expr.h:56
The NIL expression.
Definition: std_expr.h:3073
Decision Procedure Interface.
API to expression classes.