diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 13:36:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 18:36:15 +0000 |
commit | 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch) | |
tree | 03b1a5792f2f6ca5537353b86682f427090668da /test | |
parent | 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff) |
Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/node/attribute_black.cpp | 10 | ||||
-rw-r--r-- | test/unit/node/node_algorithm_black.cpp | 13 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 89 | ||||
-rw-r--r-- | test/unit/node/node_builder_black.cpp | 26 | ||||
-rw-r--r-- | test/unit/node/node_manager_black.cpp | 50 | ||||
-rw-r--r-- | test/unit/node/node_manager_white.cpp | 4 | ||||
-rw-r--r-- | test/unit/node/node_self_iterator_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/test_node.h | 3 | ||||
-rw-r--r-- | test/unit/test_smt.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_bags_rewriter_white.cpp | 27 | ||||
-rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.cpp | 10 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_skolem_cache_black.cpp | 10 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.cpp | 16 |
13 files changed, 141 insertions, 126 deletions
diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp index 880bb85e4..0ec1c5e56 100644 --- a/test/unit/node/attribute_black.cpp +++ b/test/unit/node/attribute_black.cpp @@ -55,7 +55,7 @@ class TestNodeBlackAttribute : public TestNode TEST_F(TestNodeBlackAttribute, ints) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; uint64_t data1 = 0; @@ -72,9 +72,9 @@ TEST_F(TestNodeBlackAttribute, ints) TEST_F(TestNodeBlackAttribute, tnodes) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); - Node val(d_nodeManager->mkSkolem("b", booleanType)); + Node val(d_skolemManager->mkDummySkolem("b", booleanType)); TNode data0; TNode data1; @@ -90,7 +90,7 @@ TEST_F(TestNodeBlackAttribute, tnodes) TEST_F(TestNodeBlackAttribute, strings) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); std::string val("63489"); std::string data0; @@ -108,7 +108,7 @@ TEST_F(TestNodeBlackAttribute, strings) TEST_F(TestNodeBlackAttribute, bools) { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType)); bool val = true; bool data0 = false; diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index b9cac2169..1a739cf1b 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -39,7 +39,7 @@ class TestNodeBlackNodeAlgorithm : public TestNode TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1) { // The only symbol in ~x (x is a boolean varible) should be x - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, x); std::unordered_set<Node, NodeHashFunction> syms; getSymbols(n, syms); @@ -53,8 +53,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) // "var" is bound. // left conjunct - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->integerType()); Node left = d_nodeManager->mkNode(EQUAL, x, y); // right conjunct @@ -87,12 +87,13 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >(); // create test formula - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); Node plus = d_nodeManager->mkNode(PLUS, x, x); Node mul = d_nodeManager->mkNode(MULT, x, x); Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4)); + Node y = + d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4)); Node ext1 = theory::bv::utils::mkExtract(y, 1, 0); Node ext2 = theory::bv::utils::mkExtract(y, 3, 2); Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2); @@ -143,7 +144,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) Node two = d_nodeManager->mkConst(Rational(2)); Node x = d_nodeManager->mkBoundVar(integer); - Node a = d_nodeManager->mkSkolem("a", integer); + Node a = d_skolemManager->mkDummySkolem("a", integer); Node n1 = d_nodeManager->mkNode(MULT, two, x); std::unordered_map<Node, Node, NodeHashFunction> subs; diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 87121c1c2..cfe008ec0 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -26,6 +26,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node_value.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "test_node.h" #include "theory/rewriter.h" @@ -43,10 +44,11 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, TypeNode type) { std::vector<Node> skolems; + SkolemManager* sm = nodeManager->getSkolemManager(); for (uint32_t i = 0; i < n; i++) { - skolems.push_back(nodeManager->mkSkolem( - "skolem_", type, "Created by makeNSkolemNodes()")); + skolems.push_back( + sm->mkDummySkolem("skolem_", type, "Created by makeNSkolemNodes()")); } return skolems; } @@ -119,12 +121,12 @@ TEST_F(TestNodeBlackNode, operator_equals) { Node a, b, c; - b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); ASSERT_TRUE(a == a); ASSERT_TRUE(a == b); @@ -154,12 +156,12 @@ TEST_F(TestNodeBlackNode, operator_not_equals) { Node a, b, c; - b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); /*structed assuming operator == works */ ASSERT_TRUE(iff(a != a, !(a == a))); @@ -215,7 +217,7 @@ TEST_F(TestNodeBlackNode, operator_assign) { Node a, b; Node c = d_nodeManager->mkNode( - NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); + NOT, d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType())); b = c; ASSERT_EQ(b, c); @@ -232,8 +234,8 @@ TEST_F(TestNodeBlackNode, operator_less_than) // We don't have access to the ids so we can't test the implementation // in the black box tests. - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); ASSERT_TRUE(a < b || b < a); ASSERT_TRUE(!(a < b && b < a)); @@ -275,8 +277,8 @@ TEST_F(TestNodeBlackNode, operator_less_than) TEST_F(TestNodeBlackNode, eqNode) { TypeNode t = d_nodeManager->mkSort(); - Node left = d_nodeManager->mkSkolem("left", t); - Node right = d_nodeManager->mkSkolem("right", t); + Node left = d_skolemManager->mkDummySkolem("left", t); + Node right = d_skolemManager->mkDummySkolem("right", t); Node eq = left.eqNode(right); ASSERT_EQ(EQUAL, eq.getKind()); @@ -325,8 +327,8 @@ TEST_F(TestNodeBlackNode, orNode) TEST_F(TestNodeBlackNode, iteNode) { - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); Node cnd = d_nodeManager->mkNode(OR, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -382,8 +384,8 @@ TEST_F(TestNodeBlackNode, xorNode) TEST_F(TestNodeBlackNode, getKind) { - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, a); ASSERT_EQ(NOT, n.getKind()); @@ -391,8 +393,8 @@ TEST_F(TestNodeBlackNode, getKind) n = d_nodeManager->mkNode(EQUAL, a, b); ASSERT_EQ(EQUAL, n.getKind()); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType()); n = d_nodeManager->mkNode(PLUS, x, y); ASSERT_EQ(PLUS, n.getKind()); @@ -407,8 +409,8 @@ TEST_F(TestNodeBlackNode, getOperator) TypeNode booleanType = d_nodeManager->booleanType(); TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); - Node f = d_nodeManager->mkSkolem("f", predType); - Node a = d_nodeManager->mkSkolem("a", sort); + Node f = d_skolemManager->mkDummySkolem("f", predType); + Node a = d_skolemManager->mkDummySkolem("a", sort); Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); ASSERT_TRUE(fa.hasOperator()); @@ -460,9 +462,9 @@ TEST_F(TestNodeBlackNode, getNumChildren) TEST_F(TestNodeBlackNode, iterator) { NodeBuilder b; - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); - Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); + Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType()); Node n = b << x << y << z << kind::AND; { // iterator @@ -487,9 +489,9 @@ TEST_F(TestNodeBlackNode, kinded_iterator) { TypeNode integerType = d_nodeManager->integerType(); - Node x = d_nodeManager->mkSkolem("x", integerType); - Node y = d_nodeManager->mkSkolem("y", integerType); - Node z = d_nodeManager->mkSkolem("z", integerType); + Node x = d_skolemManager->mkDummySkolem("x", integerType); + Node y = d_skolemManager->mkDummySkolem("y", integerType); + Node z = d_skolemManager->mkDummySkolem("z", integerType); Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); @@ -510,13 +512,13 @@ TEST_F(TestNodeBlackNode, toString) { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem( + Node w = d_skolemManager->mkDummySkolem( "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem( + Node y = d_skolemManager->mkDummySkolem( "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem( + Node z = d_skolemManager->mkDummySkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << w << x << kind::OR; Node n = NodeBuilder() << m << y << z << kind::AND; @@ -528,13 +530,13 @@ TEST_F(TestNodeBlackNode, toStream) { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem( + Node w = d_skolemManager->mkDummySkolem( "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem( + Node y = d_skolemManager->mkDummySkolem( "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem( + Node z = d_skolemManager->mkDummySkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder() << x << y << kind::OR; Node n = NodeBuilder() << w << m << z << kind::AND; @@ -597,14 +599,14 @@ TEST_F(TestNodeBlackNode, dagifier) TypeNode intType = d_nodeManager->integerType(); TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType); - Node x = - d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = - d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node f = - d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); - Node g = - d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node x = d_skolemManager->mkDummySkolem( + "x", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node y = d_skolemManager->mkDummySkolem( + "y", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node f = d_skolemManager->mkDummySkolem( + "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node g = d_skolemManager->mkDummySkolem( + "g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); Node fx = d_nodeManager->mkNode(APPLY_UF, f, x); Node fy = d_nodeManager->mkNode(APPLY_UF, f, y); Node gx = d_nodeManager->mkNode(APPLY_UF, g, x); @@ -702,7 +704,7 @@ TEST_F(TestNodeBlackNode, isConst) listType.getDType().getConstructors(); Node cons = lcons[0]->getConstructor(); Node nil = lcons[1]->getConstructor(); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); Node cons_x_nil = d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, @@ -764,8 +766,9 @@ TEST_F(TestNodeBlackNode, isConst) namespace { Node level0(NodeManager* nm) { + SkolemManager* sm = nm->getSkolemManager(); NodeBuilder nb(kind::AND); - Node x = nm->mkSkolem("x", nm->booleanType()); + Node x = sm->mkDummySkolem("x", nm->booleanType()); nb << x; nb << x; return Node(nb.constructNode()); diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 8c6145940..2b8ef7a04 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -92,7 +92,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) NodeBuilder noKind; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); - Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode)); noKind << x << x; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); @@ -112,7 +112,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) TEST_F(TestNodeBlackNodeBuilder, getNumChildren) { - Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode)); NodeBuilder nb; #ifdef CVC4_ASSERTIONS @@ -300,16 +300,16 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node) TEST_F(TestNodeBlackNodeBuilder, append) { - Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); - Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); - Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode); + Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode); + Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode); Node m = d_nodeManager->mkNode(AND, y, z, x); Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z); Node o = d_nodeManager->mkNode(XOR, y, x); - Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode); - Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode); - Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode); + Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode); + Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode); + Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode); Node p = d_nodeManager->mkNode( EQUAL, @@ -389,13 +389,13 @@ TEST_F(TestNodeBlackNodeBuilder, leftist_building) { NodeBuilder nb; - Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode); + Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode); - Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode); - Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode); + Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode); + Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode); - Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode); - Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode); + Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode); + Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode); nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE; diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index 5d21ff734..6ad6f583c 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -37,7 +37,7 @@ class TestNodeBlackNodeManager : public TestNode TEST_F(TestNodeBlackNodeManager, mkNode_not) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, x); ASSERT_EQ(n.getNumChildren(), 1u); ASSERT_EQ(n.getKind(), NOT); @@ -46,8 +46,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_not) TEST_F(TestNodeBlackNodeManager, mkNode_binary) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(IMPLIES, x, y); ASSERT_EQ(n.getNumChildren(), 2u); ASSERT_EQ(n.getKind(), IMPLIES); @@ -57,9 +57,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_binary) TEST_F(TestNodeBlackNodeManager, mkNode_three_children) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); - Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); + Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType()); + Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x, y, z); ASSERT_EQ(n.getNumChildren(), 3u); ASSERT_EQ(n.getKind(), AND); @@ -70,10 +70,10 @@ TEST_F(TestNodeBlackNodeManager, mkNode_three_children) TEST_F(TestNodeBlackNodeManager, mkNode_four_children) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); - Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4); ASSERT_EQ(n.getNumChildren(), 4u); ASSERT_EQ(n.getKind(), AND); @@ -85,11 +85,11 @@ TEST_F(TestNodeBlackNodeManager, mkNode_four_children) TEST_F(TestNodeBlackNodeManager, mkNode_five_children) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); - Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); - Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType()); + Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5); ASSERT_EQ(n.getNumChildren(), 5u); ASSERT_EQ(n.getKind(), AND); @@ -102,9 +102,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_five_children) TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); std::vector<Node> args; args.push_back(x1); args.push_back(x2); @@ -120,9 +120,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node) TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) { - Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); - Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); - Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType()); std::vector<TNode> args; args.push_back(x1); args.push_back(x2); @@ -138,7 +138,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name) { - Node x = d_nodeManager->mkSkolem( + Node x = d_skolemManager->mkDummySkolem( "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME); ASSERT_EQ(x.getKind(), SKOLEM); ASSERT_EQ(x.getNumChildren(), 0u); @@ -303,7 +303,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType) TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children) { #ifdef CVC4_ASSERTIONS - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); ASSERT_DEATH(d_nodeManager->mkNode(AND, x), "Nodes with kind AND must have at least 2 children"); #endif @@ -316,8 +316,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) std::vector<Node> vars; const uint32_t max = metakind::getMaxArityForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); - Node skolem_i = d_nodeManager->mkSkolem("i", boolType); - Node skolem_j = d_nodeManager->mkSkolem("j", boolType); + Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType); + Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType); Node andNode = skolem_i.andNode(skolem_j); Node orNode = skolem_i.orNode(skolem_j); while (vars.size() <= max) diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index 66ac65cb5..a13e76d03 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -64,8 +64,8 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) TEST_F(TestNodeWhiteNodeManager, topological_sort) { TypeNode boolType = d_nodeManager->booleanType(); - Node i = d_nodeManager->mkSkolem("i", boolType); - Node j = d_nodeManager->mkSkolem("j", boolType); + Node i = d_skolemManager->mkDummySkolem("i", boolType); + Node j = d_skolemManager->mkDummySkolem("j", boolType); Node n1 = d_nodeManager->mkNode(kind::AND, j, j); Node n2 = d_nodeManager->mkNode(kind::AND, i, n1); diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp index 43eebcda9..fa4889540 100644 --- a/test/unit/node/node_self_iterator_black.cpp +++ b/test/unit/node/node_self_iterator_black.cpp @@ -32,8 +32,8 @@ class TestNodeBlackNodeSelfIterator : public TestNode TEST_F(TestNodeBlackNodeSelfIterator, iteration) { - Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); - Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode); + Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode); Node x_and_y = x.andNode(y); NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); ASSERT_NE(i, x_and_y.end()); diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 359cc0b6f..dacc1f543 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -16,6 +16,7 @@ #define CVC4__TEST__UNIT__TEST_NODE_H #include "expr/node_manager.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -29,6 +30,7 @@ class TestNode : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); @@ -38,6 +40,7 @@ class TestNode : public TestInternal std::unique_ptr<NodeManagerScope> d_scope; std::unique_ptr<NodeManager> d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr<TypeNode> d_boolTypeNode; std::unique_ptr<TypeNode> d_bvTypeNode; std::unique_ptr<TypeNode> d_intTypeNode; diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index f26bd0ff6..9be954059 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -19,6 +19,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "expr/proof_checker.h" +#include "expr/skolem_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" @@ -43,6 +44,7 @@ class TestSmt : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); @@ -50,6 +52,7 @@ class TestSmt : public TestInternal std::unique_ptr<NodeManagerScope> d_nmScope; std::unique_ptr<NodeManager> d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr<SmtEngine> d_smtEngine; }; @@ -59,12 +62,14 @@ class TestSmtNoFinishInit : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager()); + d_skolemManager = d_nodeManager->getSkolemManager(); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); } std::unique_ptr<NodeManagerScope> d_nmScope; std::unique_ptr<NodeManager> d_nodeManager; + SkolemManager* d_skolemManager; std::unique_ptr<SmtEngine> d_smtEngine; }; diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 586afd8b5..10a606d11 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -41,7 +41,8 @@ class TestTheoryWhiteBagsRewriter : public TestSmt std::vector<Node> elements(n); for (size_t i = 0; i < n; i++) { - elements[i] = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + elements[i] = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); } return elements; } @@ -63,8 +64,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) std::vector<Node> elements = getNStrings(2); Node x = elements[0]; Node y = elements[1]; - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType()); - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->integerType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType()); Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d); Node emptyBag = d_nodeManager->mkConst( @@ -129,7 +130,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element) TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) { - Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node skolem = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(-1))); @@ -160,7 +162,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) TEST_F(TestTheoryWhiteBagsRewriter, bag_count) { int n = 3; - Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node skolem = + d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); Node bag = d_nodeManager->mkBag( @@ -181,7 +184,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node bag = d_nodeManager->mkBag( d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); @@ -585,7 +588,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) TEST_F(TestTheoryWhiteBagsRewriter, choose) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node c = d_nodeManager->mkConst(Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); @@ -598,7 +601,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose) TEST_F(TestTheoryWhiteBagsRewriter, bag_card) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node zero = d_nodeManager->mkConst(Rational(0)); @@ -640,8 +643,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) { Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); // TODO(projects#223): complete this function @@ -662,7 +665,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) TEST_F(TestTheoryWhiteBagsRewriter, from_set) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) @@ -676,7 +679,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) TEST_F(TestTheoryWhiteBagsRewriter, to_set) { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType()); + Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node bag = d_nodeManager->mkBag( d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 64ba39e7f..92e76d5f5 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -41,7 +41,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4)); - d_sk = d_nodeManager->mkSkolem("sk", d_t.getType()); + d_sk = d_skolemManager->mkDummySkolem("sk", d_t.getType()); d_x = d_nodeManager->mkBoundVar(d_t.getType()); d_bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {d_x}); } @@ -139,7 +139,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit { s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s2.getType()); - sk = d_nodeManager->mkSkolem("sk", s2.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s2.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, x, s2); sc = getICBvConcat(pol, litk, 0, sk, sv_t, t); @@ -148,7 +148,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit { s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s1.getType()); - sk = d_nodeManager->mkSkolem("sk", s1.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s1.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x); sc = getICBvConcat(pol, litk, 1, sk, sv_t, t); @@ -159,7 +159,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4)); s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4)); x = d_nodeManager->mkBoundVar(s2.getType()); - sk = d_nodeManager->mkSkolem("sk", s1.getType()); + sk = d_skolemManager->mkDummySkolem("sk", s1.getType()); t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(12)); sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x, s2); sc = getICBvConcat(pol, litk, 1, sk, sv_t, t); @@ -195,7 +195,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit unsigned w = 8; Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(wx)); - Node sk = d_nodeManager->mkSkolem("sk", x.getType()); + Node sk = d_skolemManager->mkDummySkolem("sk", x.getType()); x = d_nodeManager->mkBoundVar(x.getType()); Node t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(w)); diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 33543cc42..920075674 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -33,11 +33,11 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) { Node zero = d_nodeManager->mkConst(Rational(0)); - Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType()); - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType()); - Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType()); - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType()); + Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType()); + Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType()); + Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType()); + Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->stringType()); + Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->stringType()); Node sa = d_nodeManager->mkNode( kind::STRING_SUBSTR, a, diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 97bbb1bcf..2e266ce58 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -36,20 +36,20 @@ class TestUtilBlackBooleanSimplification : public TestNode { TestNode::SetUp(); - d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()); - d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); - d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType()); - d_f = d_nodeManager->mkSkolem( + d_a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType()); + d_b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType()); + d_c = d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType()); + d_d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType()); + d_e = d_skolemManager->mkDummySkolem("e", d_nodeManager->booleanType()); + d_f = d_skolemManager->mkDummySkolem( "f", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); - d_g = d_nodeManager->mkSkolem( + d_g = d_skolemManager->mkDummySkolem( "g", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); - d_h = d_nodeManager->mkSkolem( + d_h = d_skolemManager->mkDummySkolem( "h", d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), d_nodeManager->booleanType())); |