cprover
prop_conv_store.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_STORE_H
11 #define CPROVER_SOLVERS_PROP_PROP_CONV_STORE_H
12 
13 #include "prop_conv.h"
14 
16 {
17 public:
18  explicit prop_conv_storet(const namespacet &_ns):prop_convt(_ns)
19  {
20  }
21 
22  struct constraintt
23  {
24  enum class typet { NONE, CONVERT, SET_TO };
26 
28 
29  // for set_to
30  bool value;
31 
32  // for convert
34 
35  void replay(prop_convt &dest) const;
36  void print(std::ostream &out) const;
37  };
38 
40  {
41  public:
42  typedef std::list<constraintt> constraint_listt;
43  constraint_listt constraint_list;
44 
46  {
47  constraint_list.push_back(constraintt());
48  return constraint_list.back();
49  }
50 
51  void replay(prop_convt &dest) const;
52  void print(std::ostream &out) const;
53  };
54 
56  {
57  return constraints;
58  }
59 
60  // overloading
61  virtual void set_to(const exprt &expr, bool value);
62  virtual literalt convert(const exprt &expr);
63 
64 protected:
66 };
67 
68 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_STORE_H
The type of an expression.
Definition: type.h:20
void print(std::ostream &out) const
constraintst constraints
virtual void set_to(const exprt &expr, bool value)
void replay(prop_convt &dest) const
TO_BE_DOCUMENTED.
Definition: namespace.h:62
prop_conv_storet(const namespacet &_ns)
std::list< constraintt > constraint_listt
Base class for all expressions.
Definition: expr.h:46
const constraintst & get_constraints() const
virtual literalt convert(const exprt &expr)