Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of node_algorithm.{h,cpp}
11 : : */
12 : :
13 : : #include <string>
14 : : #include <vector>
15 : :
16 : : #include "base/output.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "expr/node_manager.h"
19 : : #include "test_node.h"
20 : : #include "theory/bv/theory_bv_utils.h"
21 : : #include "util/bitvector.h"
22 : : #include "util/integer.h"
23 : : #include "util/rational.h"
24 : :
25 : : namespace cvc5::internal {
26 : :
27 : : using namespace expr;
28 : :
29 : : namespace test {
30 : :
31 : : class TestNodeBlackNodeAlgorithm : public TestNode
32 : : {
33 : : };
34 : :
35 : 4 : TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
36 : : {
37 : : // The only symbol in ~x (x is a boolean varible) should be x
38 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
39 : 1 : Node n = d_nodeManager->mkNode(Kind::NOT, x);
40 : 1 : std::unordered_set<Node> syms;
41 : 1 : getSymbols(n, syms);
42 [ - + ][ + - ]: 1 : ASSERT_EQ(syms.size(), 1);
43 [ - + ][ + - ]: 1 : ASSERT_NE(syms.find(x), syms.end());
44 [ + - ][ + - ]: 1 : }
[ + - ]
45 : :
46 : 4 : TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
47 : : {
48 : : // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because
49 : : // "var" is bound.
50 : :
51 : : // left conjunct
52 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
53 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->integerType());
54 : 2 : Node left = d_nodeManager->mkNode(Kind::EQUAL, x, y);
55 : :
56 : : // right conjunct
57 : 1 : Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
58 : 1 : std::vector<Node> vars;
59 : 1 : vars.push_back(var);
60 : 2 : Node sum = d_nodeManager->mkNode(Kind::ADD, var, var);
61 : 2 : Node qeq = d_nodeManager->mkNode(Kind::EQUAL, x, sum);
62 : 1 : Node bvl = d_nodeManager->mkNode(Kind::BOUND_VAR_LIST, vars);
63 : 2 : Node right = d_nodeManager->mkNode(Kind::EXISTS, bvl, qeq);
64 : :
65 : : // conjunction
66 : 2 : Node res = d_nodeManager->mkNode(Kind::AND, left, right);
67 : :
68 : : // symbols
69 : 1 : std::unordered_set<Node> syms;
70 : 1 : getSymbols(res, syms);
71 : :
72 : : // assertions
73 [ - + ][ + - ]: 1 : ASSERT_EQ(syms.size(), 2);
74 [ - + ][ + - ]: 1 : ASSERT_NE(syms.find(x), syms.end());
75 [ - + ][ + - ]: 1 : ASSERT_NE(syms.find(y), syms.end());
76 [ - + ][ + - ]: 1 : ASSERT_EQ(syms.find(var), syms.end());
77 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
78 : :
79 : 4 : TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
80 : : {
81 : : // map to store result
82 : : std::map<TypeNode, std::unordered_set<Node> > result =
83 : 1 : std::map<TypeNode, std::unordered_set<Node> >();
84 : :
85 : : // create test formula
86 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
87 : 2 : Node plus = d_nodeManager->mkNode(Kind::ADD, x, x);
88 : 2 : Node mul = d_nodeManager->mkNode(Kind::MULT, x, x);
89 : 2 : Node eq1 = d_nodeManager->mkNode(Kind::EQUAL, plus, mul);
90 : :
91 : : Node y =
92 : 2 : d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4));
93 : 1 : Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
94 : 1 : Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
95 : 2 : Node eq2 = d_nodeManager->mkNode(Kind::EQUAL, ext1, ext2);
96 : :
97 : 2 : Node formula = d_nodeManager->mkNode(Kind::AND, eq1, eq2);
98 : :
99 : : // call function
100 : 1 : expr::getOperatorsMap(formula, result);
101 : :
102 : : // Verify result
103 : : // We should have only integer, bv and boolean as types
104 [ - + ][ + - ]: 1 : ASSERT_EQ(result.size(), 3);
105 [ - + ][ + - ]: 1 : ASSERT_NE(result.find(*d_intTypeNode), result.end());
106 [ - + ][ + - ]: 1 : ASSERT_NE(result.find(*d_boolTypeNode), result.end());
107 [ - + ][ + - ]: 1 : ASSERT_NE(result.find(*d_bvTypeNode), result.end());
108 : :
109 : : // in integers, we should only have plus and mult as operators
110 [ - + ][ + - ]: 1 : ASSERT_EQ(result[*d_intTypeNode].size(), 2);
111 [ - + ]: 1 : ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(Kind::ADD)),
112 [ + - ]: 1 : result[*d_intTypeNode].end());
113 [ - + ]: 1 : ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(Kind::MULT)),
114 [ + - ]: 1 : result[*d_intTypeNode].end());
115 : :
116 : : // in booleans, we should only have "=" and "and" as an operator.
117 [ - + ][ + - ]: 1 : ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
118 [ - + ]: 1 : ASSERT_NE(
119 : : result[*d_boolTypeNode].find(d_nodeManager->operatorOf(Kind::EQUAL)),
120 [ + - ]: 1 : result[*d_boolTypeNode].end());
121 [ - + ]: 1 : ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(Kind::AND)),
122 [ + - ]: 1 : result[*d_boolTypeNode].end());
123 : :
124 : : // in bv, we should only have "extract" as an operator.
125 [ - + ][ + - ]: 1 : ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
126 : : Node extractOp1 =
127 : 1 : d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
128 : : Node extractOp2 =
129 : 1 : d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
130 [ - + ]: 1 : ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
131 [ + - ]: 1 : result[*d_bvTypeNode].end());
132 [ - + ]: 1 : ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
133 [ + - ]: 1 : result[*d_bvTypeNode].end());
134 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
135 : :
136 : 4 : TEST_F(TestNodeBlackNodeAlgorithm, match)
137 : : {
138 : 1 : TypeNode integer = d_nodeManager->integerType();
139 : :
140 : 1 : Node one = d_nodeManager->mkConstInt(Rational(1));
141 : 1 : Node two = d_nodeManager->mkConstInt(Rational(2));
142 : :
143 : 1 : Node x = d_nodeManager->mkBoundVar(integer);
144 : 2 : Node a = d_skolemManager->mkDummySkolem("a", integer);
145 : :
146 : 2 : Node n1 = d_nodeManager->mkNode(Kind::MULT, two, x);
147 : 1 : std::unordered_map<Node, Node> subs;
148 : :
149 : : // check reflexivity
150 [ - + ][ + - ]: 1 : ASSERT_TRUE(match(n1, n1, subs));
151 [ - + ][ + - ]: 1 : ASSERT_EQ(subs.size(), 0);
152 : :
153 : 2 : Node n2 = d_nodeManager->mkNode(Kind::MULT, two, a);
154 : 1 : subs.clear();
155 : :
156 : : // check instance
157 [ - + ][ + - ]: 1 : ASSERT_TRUE(match(n1, n2, subs));
158 [ - + ][ + - ]: 1 : ASSERT_EQ(subs.size(), 1);
159 [ - + ][ + - ]: 1 : ASSERT_EQ(subs[x], a);
160 : :
161 : : // should return false for flipped arguments (match is not symmetric)
162 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n2, n1, subs));
163 : :
164 : 1 : n2 = d_nodeManager->mkNode(Kind::MULT, one, a);
165 : :
166 : : // should return false since n2 is not an instance of n1
167 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n1, n2, subs));
168 : :
169 : 1 : n2 = d_nodeManager->mkNode(Kind::NONLINEAR_MULT, two, a);
170 : :
171 : : // should return false for similar operators
172 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n1, n2, subs));
173 : :
174 : 1 : n2 = d_nodeManager->mkNode(Kind::MULT, two, a, one);
175 : :
176 : : // should return false for different number of arguments
177 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n1, n2, subs));
178 : :
179 : 1 : n1 = x;
180 : 1 : n2 = d_nodeManager->mkConst(true);
181 : :
182 : : // should return false for different types
183 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n1, n2, subs));
184 : :
185 : 1 : n1 = d_nodeManager->mkNode(Kind::MULT, x, x);
186 : 1 : n2 = d_nodeManager->mkNode(Kind::MULT, two, a);
187 : :
188 : : // should return false for contradictory substitutions
189 [ - + ][ + - ]: 1 : ASSERT_FALSE(match(n1, n2, subs));
190 : :
191 : 1 : n2 = d_nodeManager->mkNode(Kind::MULT, a, a);
192 : 1 : subs.clear();
193 : :
194 : : // implementation: check if the cache works correctly
195 [ - + ][ + - ]: 1 : ASSERT_TRUE(match(n1, n2, subs));
196 [ - + ][ + - ]: 1 : ASSERT_EQ(subs.size(), 1);
197 [ - + ][ + - ]: 1 : ASSERT_EQ(subs[x], a);
198 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
199 : : } // namespace test
200 : : } // namespace cvc5::internal
|
