cvc4-1.4
pickler.h
Go to the documentation of this file.
1 /********************* */
19 #include "cvc4_public.h"
20 
21 #ifndef __CVC4__PICKLER_H
22 #define __CVC4__PICKLER_H
23 
24 #include "expr/variable_type_map.h"
25 #include "expr/expr.h"
26 #include "util/exception.h"
27 
28 #include <exception>
29 #include <stack>
30 
31 namespace CVC4 {
32 
33 class ExprManager;
34 
35 namespace expr {
36 namespace pickle {
37 
38 class Pickler;
39 class PicklerPrivate;
40 
41 class PickleData;// CVC4-internal representation
42 
44  PickleData* d_data;
45  friend class Pickler;
46  friend class PicklerPrivate;
47 public:
48  Pickle();
49  Pickle(const Pickle& p);
50  ~Pickle();
51  Pickle& operator=(const Pickle& other);
52 };/* class Pickle */
53 
55 public:
57  Exception("Pickling failed") {
58  }
59 };/* class PicklingException */
60 
62  PicklerPrivate* d_private;
63 
64  friend class PicklerPrivate;
65 
66 protected:
67  virtual uint64_t variableToMap(uint64_t x) const
68  throw(PicklingException) {
69  return x;
70  }
71  virtual uint64_t variableFromMap(uint64_t x) const {
72  return x;
73  }
74 
75 public:
76  Pickler(ExprManager* em);
77  ~Pickler();
78 
88  void toPickle(Expr e, Pickle& p) throw(PicklingException);
89 
96  Expr fromPickle(Pickle& p);
97 
98  static void debugPickleTest(Expr e);
99 
100 };/* class Pickler */
101 
103 private:
104  const VarMap& d_toMap;
105  const VarMap& d_fromMap;
106 
107 public:
108  MapPickler(ExprManager* em, const VarMap& to, const VarMap& from):
109  Pickler(em),
110  d_toMap(to),
111  d_fromMap(from) {
112  }
113 
114  virtual ~MapPickler() throw() {}
115 
116 protected:
117 
118  virtual uint64_t variableToMap(uint64_t x) const
119  throw(PicklingException) {
120  VarMap::const_iterator i = d_toMap.find(x);
121  if(i != d_toMap.end()) {
122  return i->second;
123  } else {
124  throw PicklingException();
125  }
126  }
127 
128  virtual uint64_t variableFromMap(uint64_t x) const;
129 };/* class MapPickler */
130 
131 }/* CVC4::expr::pickle namespace */
132 }/* CVC4::expr namespace */
133 }/* CVC4 namespace */
134 
135 #endif /* __CVC4__PICKLER_H */
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
__gnu_cxx::hash_map< uint64_t, uint64_t > VarMap
[[ Add one-line brief description here ]]
Definition: expr.h:106
void * ExprManager
virtual uint64_t variableToMap(uint64_t x) const
Definition: pickler.h:67
CVC4&#39;s exception base class and some associated utilities.
virtual uint64_t variableToMap(uint64_t x) const
Definition: pickler.h:118
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
virtual uint64_t variableFromMap(uint64_t x) const
Definition: pickler.h:71
MapPickler(ExprManager *em, const VarMap &to, const VarMap &from)
Definition: pickler.h:108
expr.h