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
|
/********************* */
/** node_manager.h
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): taking
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** A manager for Nodes.
**/
/* circular dependency; force node.h first */
#include "expr/node.h"
#ifndef __CVC4__NODE_MANAGER_H
#define __CVC4__NODE_MANAGER_H
#include <vector>
#include <string>
#include <ext/hash_set>
#include "expr/kind.h"
namespace __gnu_cxx {
template<>
struct hash<CVC4::NodeValue*> {
size_t operator()(const CVC4::NodeValue* nv) const {
return (size_t)nv->hash();
}
};
}/* __gnu_cxx namespace */
namespace CVC4 {
class Type;
class NodeManager {
static __thread NodeManager* s_current;
template <unsigned> friend class CVC4::NodeBuilder;
typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
NodeValueSet d_nodeValueSet;
expr::AttributeManager d_am;
NodeValue* poolLookup(NodeValue* nv) const;
void poolInsert(NodeValue* nv);
friend class NodeManagerScope;
public:
NodeManager() : d_am(this) {
poolInsert( &NodeValue::s_null );
}
static NodeManager* currentNM() { return s_current; }
// general expression-builders
Node mkNode(Kind kind);
Node mkNode(Kind kind, const Node& child1);
Node mkNode(Kind kind, const Node& child1, const Node& child2);
Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
// N-ary version
Node mkNode(Kind kind, const std::vector<Node>& children);
// variables are special, because duplicates are permitted
Node mkVar(const Type* type, std::string name);
Node mkVar(const Type* type);
Node mkVar();
template <class AttrKind>
inline typename AttrKind::value_type getAttribute(const Node& n,
const AttrKind&) const;
template <class AttrKind>
inline bool hasAttribute(const Node& n,
const AttrKind&,
typename AttrKind::value_type* = NULL) const;
template <class AttrKind>
inline void setAttribute(const Node& n,
const AttrKind&,
const typename AttrKind::value_type& value);
};
class NodeManagerScope {
NodeManager *d_oldNodeManager;
public:
NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) {
NodeManager::s_current = nm;
Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
}
~NodeManagerScope() {
NodeManager::s_current = d_oldNodeManager;
Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
}
};
template <class AttrKind>
inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
const AttrKind&) const {
return d_am.getAttribute(n, AttrKind());
}
template <class AttrKind>
inline bool NodeManager::hasAttribute(const Node& n,
const AttrKind&,
typename AttrKind::value_type* ret) const {
return d_am.hasAttribute(n, AttrKind(), ret);
}
template <class AttrKind>
inline void NodeManager::setAttribute(const Node& n,
const AttrKind&,
const typename AttrKind::value_type& value) {
d_am.setAttribute(n, AttrKind(), value);
}
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_MANAGER_H */
|
