diff options
author | Tim King <taking@cs.nyu.edu> | 2017-07-22 20:02:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-22 20:02:44 -0700 |
commit | 7785045ede376f7ee5a540ded9afdd7d3f57c47d (patch) | |
tree | 7e3a900e96330a07b65bc2ce71409dbb4289ee85 /test/unit | |
parent | 4cab39bd4f166716cd3d357a175c346afb838137 (diff) |
Deprecating the unused convenience_node_builders.h (#203)
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/node_builder_black.h | 77 | ||||
-rw-r--r-- | test/unit/expr/node_self_iterator_black.h | 3 |
2 files changed, 1 insertions, 79 deletions
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 88b229ab6..2aa6f402d 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -21,7 +21,6 @@ #include <sstream> #include "base/cvc4_assert.h" -#include "expr/convenience_node_builders.h" #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" @@ -622,80 +621,4 @@ public: TS_ASSERT_EQUALS(nexpected, n); } - - void testConvenienceBuilders() { - Node a = d_nm->mkSkolem("a", *d_booleanType); - - Node b = d_nm->mkSkolem("b", *d_booleanType); - Node c = d_nm->mkSkolem("c", *d_booleanType); - - Node d = d_nm->mkSkolem("d", *d_realType); - Node e = d_nm->mkSkolem("e", *d_realType); - Node f = d_nm->mkSkolem("f", *d_realType); - - Node m = a && b; - TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); - - Node n = (a && b) || c; - TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); - - Node p = (a && m) || n; - TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, m), n)); - - Node w = d + e - f; - TS_ASSERT_EQUALS(w, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f))); - - Node x = d + e + w - f; - TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, w, d_nm->mkNode(UMINUS, f))); - - Node y = f - x - e + w; - TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS, - f, - d_nm->mkNode(UMINUS, x), - d_nm->mkNode(UMINUS, e), - w)); - - Node q = a && b && c; - TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c)); - - Node r = (c && b && a) || (m && n) || p || (a && p); - TS_ASSERT_EQUALS(r, d_nm->mkNode(OR, - d_nm->mkNode(AND, c, b, a), - d_nm->mkNode(AND, m, n), - p, - d_nm->mkNode(AND, a, p))); - - TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c)); - TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); - TS_ASSERT_EQUALS(Node((a || b) || c), d_nm->mkNode(OR, a, b, c)); - TS_ASSERT_EQUALS(Node(a || (b || c)), d_nm->mkNode(OR, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(Node((a && b) || c), d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); - TS_ASSERT_EQUALS(Node(a && (b || c)), d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); - TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); - - TS_ASSERT_EQUALS(Node((d + e) + f), d_nm->mkNode(PLUS, d, e, f)); - TS_ASSERT_EQUALS(Node(d + (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, f))); - TS_ASSERT_EQUALS(Node((d - e) - f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d - (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))))); - TS_ASSERT_EQUALS(Node((d * e) * f), d_nm->mkNode(MULT, d, e, f)); - TS_ASSERT_EQUALS(Node(d * (e * f)), d_nm->mkNode(MULT, d, d_nm->mkNode(MULT, e, f))); - TS_ASSERT_EQUALS(Node((d + e) - f), d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d + (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))); - TS_ASSERT_EQUALS(Node((d - e) + f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), f)); - TS_ASSERT_EQUALS(Node(d - (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, f)))); - TS_ASSERT_EQUALS(Node((d + e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, e), f)); - TS_ASSERT_EQUALS(Node(d + (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(MULT, e, f))); - TS_ASSERT_EQUALS(Node((d - e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e)), f)); - TS_ASSERT_EQUALS(Node(d - (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, e, f)))); - TS_ASSERT_EQUALS(Node((d * e) + f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), f)); - TS_ASSERT_EQUALS(Node(d * (e + f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, f))); - TS_ASSERT_EQUALS(Node((d * e) - f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d * (e - f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))); - - TS_ASSERT_EQUALS(Node(-d), d_nm->mkNode(UMINUS, d)); - TS_ASSERT_EQUALS(Node(- d - e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), d_nm->mkNode(UMINUS, e))); - TS_ASSERT_EQUALS(Node(- d + e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), e)); - TS_ASSERT_EQUALS(Node(- d * e), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, d), e)); - } }; diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 271c4eadc..a1dc7aacf 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "expr/node_builder.h" -#include "expr/convenience_node_builders.h" using namespace CVC4; using namespace CVC4::kind; @@ -52,7 +51,7 @@ public: void testSelfIteration() { Node x = d_nodeManager->mkSkolem("x", *d_booleanType); Node y = d_nodeManager->mkSkolem("y", *d_booleanType); - Node x_and_y = x && y; + Node x_and_y = x.andNode(y); NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); TS_ASSERT(i != x_and_y.end()); TS_ASSERT(j != x_and_y.end()); |