GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_algorithm_black.cpp Lines: 93 93 100.0 %
Date: 2021-03-22 Branches: 311 886 35.1 %

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