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