diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
commit | 7eb18a6c4b0ec6fcf4b6474d22307baa04f8f515 (patch) | |
tree | 8621e2e60756ec6770bc949877eef808e7e99d55 /src/expr | |
parent | 3b06265b82d48074b3b733d655efd6dab6481150 (diff) |
+ test infrastructure fixes
+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager.cpp | 14 | ||||
-rw-r--r-- | src/expr/node.cpp | 16 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 14 | ||||
-rw-r--r-- | src/expr/node_manager.h | 14 |
4 files changed, 29 insertions, 29 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 877ba9d3c..ea1649e12 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -23,27 +23,27 @@ ExprManager::~ExprManager() { } Expr ExprManager::mkExpr(Kind kind) { - return Expr(this, new Node(d_nm->mkExpr(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->mkExpr(kind, child1.getNode()))); + 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->mkExpr(kind, child1.getNode(), + 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->mkExpr(kind, child1.getNode(), + 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->mkExpr(kind, child1.getNode(), + return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode(), child3.getNode(), child4.getNode()))); } @@ -51,7 +51,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, 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->mkExpr(kind, child1.getNode(), + return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode(), child3.getNode(), child5.getNode()))); } @@ -64,7 +64,7 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) { nodes.push_back(it->getNode()); ++it; } - return Expr(this, new Node(d_nm->mkExpr(kind, nodes))); + return Expr(this, new Node(d_nm->mkNode(kind, nodes))); } Expr ExprManager::mkVar() { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 40dd70457..334cf1b0e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -87,35 +87,35 @@ uint64_t Node::hash() const { } Node Node::eqExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(EQUAL, *this, right); + return NodeManager::currentNM()->mkNode(EQUAL, *this, right); } Node Node::notExpr() const { - return NodeManager::currentNM()->mkExpr(NOT, *this); + return NodeManager::currentNM()->mkNode(NOT, *this); } Node Node::andExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(AND, *this, right); + return NodeManager::currentNM()->mkNode(AND, *this, right); } Node Node::orExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(OR, *this, right); + return NodeManager::currentNM()->mkNode(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { - return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart); + return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(IFF, *this, right); + return NodeManager::currentNM()->mkNode(IFF, *this, right); } Node Node::impExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right); + return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { - return NodeManager::currentNM()->mkExpr(XOR, *this, right); + return NodeManager::currentNM()->mkNode(XOR, *this, right); } }/* CVC4 namespace */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4b550ee3d..7e871d9c3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -101,32 +101,32 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { // general expression-builders -Node NodeManager::mkExpr(Kind kind) { +Node NodeManager::mkNode(Kind kind) { return NodeBuilder<>(this, kind); } -Node NodeManager::mkExpr(Kind kind, const Node& child1) { +Node NodeManager::mkNode(Kind kind, const Node& child1) { return NodeBuilder<>(this, kind) << child1; } -Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { +Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) { return NodeBuilder<>(this, kind) << child1 << child2; } -Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) { +Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) { return NodeBuilder<>(this, kind) << child1 << child2 << child3; } -Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { +Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; } -Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { +Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; } // N-ary version -Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) { +Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) { return NodeBuilder<>(this, kind).append(children); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8caa797fa..643f09f11 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -36,14 +36,14 @@ public: static NodeManager* currentNM() { return s_current; } // general expression-builders - Node mkExpr(Kind kind); - Node mkExpr(Kind kind, const Node& child1); - Node mkExpr(Kind kind, const Node& child1, const Node& child2); - Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3); - Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4); - Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5); + 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 mkExpr(Kind kind, const std::vector<Node>& children); + Node mkNode(Kind kind, const std::vector<Node>& children); // variables are special, because duplicates are permitted Node mkVar(); |