CBMC
prop_conv.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
11 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
12 
13 #include <solvers/stack_decision_procedure.h>
14 
15 class literalt;
16 class tvt;
17 
18 // API that provides a "handle" in the form of a literalt
19 // for expressions.
20 
21 class prop_convt : public stack_decision_proceduret
22 {
23 public:
24  virtual ~prop_convt() { }
25 
27  virtual literalt convert(const exprt &expr) = 0;
28 
31  virtual tvt l_get(literalt l) const = 0;
32 };
33 
34 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
exprt
Base class for all expressions.
Definition: expr.h:56
prop_convt
Definition: prop_conv.h:22
prop_convt::l_get
virtual tvt l_get(literalt l) const =0
Return value of literal l from satisfying assignment.
prop_convt::~prop_convt
virtual ~prop_convt()
Definition: prop_conv.h:24
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
Convert a Boolean expression and return the corresponding literal.
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
tvt
Definition: threeval.h:20
stack_decision_procedure.h
Decision procedure with incremental solving with contexts and assumptions.