blob: f1cdd1c65fd4fa9f3d0e9d72eb99d526c3e6e572 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
/********************* */
/*! \file pickler.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Kshitij Bansal
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief This is a "pickler" for expressions
**
** This is a "pickler" for expressions. It produces a binary
** serialization of an expression that can be converted back
** into an expression in the same or another ExprManager.
**/
#include "cvc4_public.h"
#ifndef __CVC4__PICKLER_H
#define __CVC4__PICKLER_H
#include "expr/variable_type_map.h"
#include "expr/expr.h"
#include "util/exception.h"
#include <exception>
#include <stack>
namespace CVC4 {
class ExprManager;
namespace expr {
namespace pickle {
class Pickler;
class PicklerPrivate;
class PickleData;// CVC4-internal representation
class CVC4_PUBLIC Pickle {
PickleData* d_data;
friend class Pickler;
friend class PicklerPrivate;
public:
Pickle();
Pickle(const Pickle& p);
~Pickle();
Pickle& operator=(const Pickle& other);
};/* class Pickle */
class CVC4_PUBLIC PicklingException : public Exception {
public:
PicklingException() :
Exception("Pickling failed") {
}
};/* class PicklingException */
class CVC4_PUBLIC Pickler {
PicklerPrivate* d_private;
friend class PicklerPrivate;
protected:
virtual uint64_t variableToMap(uint64_t x) const
throw(PicklingException) {
return x;
}
virtual uint64_t variableFromMap(uint64_t x) const {
return x;
}
public:
Pickler(ExprManager* em);
~Pickler();
/**
* Constructs a new Pickle of the node n.
* n must be a node allocated in the node manager specified at initialization
* time. The new pickle has variables mapped using the VariableIDMap provided
* at initialization.
* TODO: Fix comment
*
* @return the pickle, which should be dispose()'d when you're done with it
*/
void toPickle(Expr e, Pickle& p) throw(PicklingException);
/**
* Constructs a node from a Pickle.
* This destroys the contents of the Pickle.
* The node is created in the NodeManager getNM();
* TODO: Fix comment
*/
Expr fromPickle(Pickle& p);
static void debugPickleTest(Expr e);
};/* class Pickler */
class CVC4_PUBLIC MapPickler : public Pickler {
private:
const VarMap& d_toMap;
const VarMap& d_fromMap;
public:
MapPickler(ExprManager* em, const VarMap& to, const VarMap& from):
Pickler(em),
d_toMap(to),
d_fromMap(from) {
}
virtual ~MapPickler() throw() {}
protected:
virtual uint64_t variableToMap(uint64_t x) const
throw(PicklingException) {
VarMap::const_iterator i = d_toMap.find(x);
if(i != d_toMap.end()) {
return i->second;
} else {
throw PicklingException();
}
}
virtual uint64_t variableFromMap(uint64_t x) const;
};/* class MapPickler */
}/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PICKLER_H */
|
