diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-15 09:35:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-15 09:35:27 -0600 |
commit | 829b3c2798c1f2c0bb313d7eff2c1e76f0184ae2 (patch) | |
tree | 6855fbf1b5bf7b11958a222f70e9301156931c0b /test/unit/node | |
parent | 9aeb23f2ae58e4f6dd2b53dbb47cf8c173e56d83 (diff) | |
parent | 94c4d5b54e7840fa36d76e7c3d52e19c31a1dbc1 (diff) |
Merge branch 'master' into refactorEagerSolverrefactorEagerSolver
Diffstat (limited to 'test/unit/node')
-rw-r--r-- | test/unit/node/node_algorithm_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 10 | ||||
-rw-r--r-- | test/unit/node/node_builder_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/node/node_manager_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/node/node_manager_white.cpp | 5 | ||||
-rw-r--r-- | test/unit/node/node_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/node/type_node_white.cpp | 3 |
7 files changed, 15 insertions, 13 deletions
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index df8fb9383..8dac2cfda 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -140,8 +140,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) { TypeNode integer = d_nodeManager->integerType(); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x = d_nodeManager->mkBoundVar(integer); Node a = d_skolemManager->mkDummySkolem("a", integer); diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index b170ccbb6..50e766e61 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -732,15 +732,15 @@ TEST_F(TestNodeBlackNode, isConst) Node cons_1_nil = d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); Node cons_1_cons_2_nil = d_nodeManager->mkNode( APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); ASSERT_FALSE(cons_x_nil.isConst()); @@ -749,8 +749,8 @@ TEST_F(TestNodeBlackNode, isConst) TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); ASSERT_TRUE(storeAll.isConst()); diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 05ccfc90c..779397e04 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -312,7 +312,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) Node p = d_nodeManager->mkNode( EQUAL, - d_nodeManager->mkConst<Rational>(0), + d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0), d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index b02790cb5..ad41155c3 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -140,7 +140,7 @@ TEST_F(TestNodeBlackNodeManager, mkConst_bool) TEST_F(TestNodeBlackNodeManager, mkConst_rational) { Rational r("3/2"); - Node n = d_nodeManager->mkConst(r); + Node n = d_nodeManager->mkConst(CONST_RATIONAL, r); ASSERT_EQ(n.getConst<Rational>(), r); } diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index fe06f85d3..64f6a70f5 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -23,6 +23,7 @@ namespace cvc5 { using namespace cvc5::expr; +using namespace cvc5::kind; namespace test { @@ -33,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode TEST_F(TestNodeWhiteNodeManager, mkConst_rational) { Rational i("3"); - Node n = d_nodeManager->mkConst(i); - Node m = d_nodeManager->mkConst(i); + Node n = d_nodeManager->mkConst(CONST_RATIONAL, i); + Node m = d_nodeManager->mkConst(CONST_RATIONAL, i); ASSERT_EQ(n.getId(), m.getId()); } diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index eb6f77bdc..8061526d5 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -49,7 +49,7 @@ TEST_F(TestNodeWhiteNode, iterators) Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y); - Node two = d_nodeManager->mkConst(Rational(2)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y); diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 9f93017f0..424fee989 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -50,7 +50,8 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) TypeNode bvType = d_nodeManager->mkBitVectorType(32); Node x = d_nodeManager->mkBoundVar("x", realType); - Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0))); + Node xPos = d_nodeManager->mkNode( + GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType); Node lambda = d_nodeManager->mkVar("lambda", funtype); std::vector<Node> formals; |