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
|
/*
* expr_manager.cpp
*
* Created on: Dec 10, 2009
* Author: dejan
*/
#include "expr/node.h"
#include "expr/expr.h"
#include "expr/node_manager.h"
#include "expr/expr_manager.h"
using namespace std;
namespace CVC4 {
ExprManager::ExprManager()
: d_nm(new NodeManager()) {
}
ExprManager::~ExprManager() {
delete d_nm;
}
Expr ExprManager::mkExpr(Kind kind) {
return Expr(this, new Node(d_nm->mkNode(kind)));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3) {
return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4) {
return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode(),
child4.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4,
const Expr& child5) {
return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode(),
child5.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
vector<Node> nodes;
vector<Expr>::const_iterator it = children.begin();
vector<Expr>::const_iterator it_end = children.end();
while(it != it_end) {
nodes.push_back(it->getNode());
++it;
}
return Expr(this, new Node(d_nm->mkNode(kind, nodes)));
}
Expr ExprManager::mkVar() {
return Expr(this, new Node(d_nm->mkVar()));
}
NodeManager* ExprManager::getNodeManager() const {
return d_nm;
}
} // End namespace CVC4
|
