blob: ae9f6d94fd77289f42f9896e637fc2d62f071b2d (
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
|
/********************* */
/*! \file pickler.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Tim King, Clark Barrett
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. 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 "base/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 { return x; }
virtual uint64_t variableFromMap(uint64_t x) const { return x; }
public:
Pickler(ExprManager* em);
virtual ~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);
/**
* 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) {
}
protected:
uint64_t variableToMap(uint64_t x) const override
{
VarMap::const_iterator i = d_toMap.find(x);
if (i != d_toMap.end())
{
return i->second;
}
else
{
throw PicklingException();
}
}
uint64_t variableFromMap(uint64_t x) const override;
};/* class MapPickler */
}/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PICKLER_H */
|
