Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/node/node_algorithm_black.cpp	Lines:	93	93	100.0 %
Date:	2021-09-29	Branches:	310	884	35.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Black box testing of node_algorithm.{h,cpp}
 */

#include <string>
#include <vector>

#include "base/output.h"
#include "expr/node_algorithm.h"
#include "expr/node_manager.h"
#include "test_node.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/bitvector.h"
#include "util/integer.h"
#include "util/rational.h"

namespace cvc5 {

using namespace expr;
using namespace kind;

namespace test {

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_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
  Node n = d_nodeManager->mkNode(NOT, x);
  std::unordered_set<Node> syms;
  getSymbols(n, syms);
  ASSERT_EQ(syms.size(), 1);
  ASSERT_NE(syms.find(x), syms.end());
}

TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
{
  // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because
  // "var" is bound.

  // left conjunct
  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
  Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
  std::vector<Node> vars;
  vars.push_back(var);
  Node sum = d_nodeManager->mkNode(PLUS, var, var);
  Node qeq = d_nodeManager->mkNode(EQUAL, x, sum);
  Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars);
  Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq);

  // conjunction
  Node res = d_nodeManager->mkNode(AND, left, right);

  // symbols
  std::unordered_set<Node> syms;
  getSymbols(res, syms);

  // assertions
  ASSERT_EQ(syms.size(), 2);
  ASSERT_NE(syms.find(x), syms.end());
  ASSERT_NE(syms.find(y), syms.end());
  ASSERT_EQ(syms.find(var), syms.end());
}

TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
{
  // map to store result
  std::map<TypeNode, std::unordered_set<Node> > result =
      std::map<TypeNode, std::unordered_set<Node> >();

  // create test formula
  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_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);

  Node formula = d_nodeManager->mkNode(AND, eq1, eq2);

  // call function
  expr::getOperatorsMap(formula, result);

  // Verify result
  // We should have only integer, bv and boolean as types
  ASSERT_EQ(result.size(), 3);
  ASSERT_NE(result.find(*d_intTypeNode), result.end());
  ASSERT_NE(result.find(*d_boolTypeNode), result.end());
  ASSERT_NE(result.find(*d_bvTypeNode), result.end());

  // in integers, we should only have plus and mult as operators
  ASSERT_EQ(result[*d_intTypeNode].size(), 2);
  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
            result[*d_intTypeNode].end());
  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
            result[*d_intTypeNode].end());

  // in booleans, we should only have "=" and "and" as an operator.
  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
            result[*d_boolTypeNode].end());
  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
            result[*d_boolTypeNode].end());

  // in bv, we should only have "extract" as an operator.
  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
  Node extractOp1 =
      d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
  Node extractOp2 =
      d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
  ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
            result[*d_bvTypeNode].end());
  ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
            result[*d_bvTypeNode].end());
}

TEST_F(TestNodeBlackNodeAlgorithm, match)
{
  TypeNode integer = d_nodeManager->integerType();

  Node one = d_nodeManager->mkConst(Rational(1));
  Node two = d_nodeManager->mkConst(Rational(2));

  Node x = d_nodeManager->mkBoundVar(integer);
  Node a = d_skolemManager->mkDummySkolem("a", integer);

  Node n1 = d_nodeManager->mkNode(MULT, two, x);
  std::unordered_map<Node, Node> subs;

  // check reflexivity
  ASSERT_TRUE(match(n1, n1, subs));
  ASSERT_EQ(subs.size(), 0);

  Node n2 = d_nodeManager->mkNode(MULT, two, a);
  subs.clear();

  // check instance
  ASSERT_TRUE(match(n1, n2, subs));
  ASSERT_EQ(subs.size(), 1);
  ASSERT_EQ(subs[x], a);

  // should return false for flipped arguments (match is not symmetric)
  ASSERT_FALSE(match(n2, n1, subs));

  n2 = d_nodeManager->mkNode(MULT, one, a);

  // should return false since n2 is not an instance of n1
  ASSERT_FALSE(match(n1, n2, subs));

  n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);

  // should return false for similar operators
  ASSERT_FALSE(match(n1, n2, subs));

  n2 = d_nodeManager->mkNode(MULT, two, a, one);

  // should return false for different number of arguments
  ASSERT_FALSE(match(n1, n2, subs));

  n1 = x;
  n2 = d_nodeManager->mkConst(true);

  // should return false for different types
  ASSERT_FALSE(match(n1, n2, subs));

  n1 = d_nodeManager->mkNode(MULT, x, x);
  n2 = d_nodeManager->mkNode(MULT, two, a);

  // should return false for contradictory substitutions
  ASSERT_FALSE(match(n1, n2, subs));

  n2 = d_nodeManager->mkNode(MULT, a, a);
  subs.clear();

  // implementation: check if the cache works correctly
  ASSERT_TRUE(match(n1, n2, subs));
  ASSERT_EQ(subs.size(), 1);
  ASSERT_EQ(subs[x], a);
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
4		*
5		* This file is part of the cvc5 project.
6		*
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.
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 {
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_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
43	4	Node n = d_nodeManager->mkNode(NOT, x);
44	4	std::unordered_set<Node> 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_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
57	4	Node y = d_skolemManager->mkDummySkolem("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> 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> > result =
87	4	std::map<TypeNode, std::unordered_set<Node> >();
88
89		// create test formula
90	4	Node x = d_skolemManager->mkDummySkolem("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		Node y =
96	4	d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4));
97	4	Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
98	4	Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
99	4	Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
100
101	4	Node formula = d_nodeManager->mkNode(AND, eq1, eq2);
102
103		// call function
104	2	expr::getOperatorsMap(formula, result);
105
106		// Verify result
107		// We should have only integer, bv and boolean as types
108	2	ASSERT_EQ(result.size(), 3);
109	2	ASSERT_NE(result.find(*d_intTypeNode), result.end());
110	2	ASSERT_NE(result.find(*d_boolTypeNode), result.end());
111	2	ASSERT_NE(result.find(*d_bvTypeNode), result.end());
112
113		// in integers, we should only have plus and mult as operators
114	2	ASSERT_EQ(result[*d_intTypeNode].size(), 2);
115	2	ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
116	2	result[*d_intTypeNode].end());
117	2	ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
118	2	result[*d_intTypeNode].end());
119
120		// in booleans, we should only have "=" and "and" as an operator.
121	2	ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
122	2	ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
123	2	result[*d_boolTypeNode].end());
124	2	ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
125	2	result[*d_boolTypeNode].end());
126
127		// in bv, we should only have "extract" as an operator.
128	2	ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
129		Node extractOp1 =
130	4	d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
131		Node extractOp2 =
132	4	d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
133	2	ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
134	2	result[*d_bvTypeNode].end());
135	2	ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
136	2	result[*d_bvTypeNode].end());
137		}
138
139	13	TEST_F(TestNodeBlackNodeAlgorithm, match)
140		{
141	4	TypeNode integer = d_nodeManager->integerType();
142
143	4	Node one = d_nodeManager->mkConst(Rational(1));
144	4	Node two = d_nodeManager->mkConst(Rational(2));
145
146	4	Node x = d_nodeManager->mkBoundVar(integer);
147	4	Node a = d_skolemManager->mkDummySkolem("a", integer);
148
149	4	Node n1 = d_nodeManager->mkNode(MULT, two, x);
150	4	std::unordered_map<Node, Node> subs;
151
152		// check reflexivity
153	2	ASSERT_TRUE(match(n1, n1, subs));
154	2	ASSERT_EQ(subs.size(), 0);
155
156	4	Node n2 = d_nodeManager->mkNode(MULT, two, a);
157	2	subs.clear();
158
159		// check instance
160	2	ASSERT_TRUE(match(n1, n2, subs));
161	2	ASSERT_EQ(subs.size(), 1);
162	2	ASSERT_EQ(subs[x], a);
163
164		// should return false for flipped arguments (match is not symmetric)
165	2	ASSERT_FALSE(match(n2, n1, subs));
166
167	2	n2 = d_nodeManager->mkNode(MULT, one, a);
168
169		// should return false since n2 is not an instance of n1
170	2	ASSERT_FALSE(match(n1, n2, subs));
171
172	2	n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);
173
174		// should return false for similar operators
175	2	ASSERT_FALSE(match(n1, n2, subs));
176
177	2	n2 = d_nodeManager->mkNode(MULT, two, a, one);
178
179		// should return false for different number of arguments
180	2	ASSERT_FALSE(match(n1, n2, subs));
181
182	2	n1 = x;
183	2	n2 = d_nodeManager->mkConst(true);
184
185		// should return false for different types
186	2	ASSERT_FALSE(match(n1, n2, subs));
187
188	2	n1 = d_nodeManager->mkNode(MULT, x, x);
189	2	n2 = d_nodeManager->mkNode(MULT, two, a);
190
191		// should return false for contradictory substitutions
192	2	ASSERT_FALSE(match(n1, n2, subs));
193
194	2	n2 = d_nodeManager->mkNode(MULT, a, a);
195	2	subs.clear();
196
197		// implementation: check if the cache works correctly
198	2	ASSERT_TRUE(match(n1, n2, subs));
199	2	ASSERT_EQ(subs.size(), 1);
200	2	ASSERT_EQ(subs[x], a);
201		}
202		} // namespace test
203	15	} // namespace cvc5