From: Aina Niemetz Date: Thu, 10 Dec 2020 15:47:43 +0000 (-0800) Subject: google test: expr: Migrate node_algorithm_black. (#5643) X-Git-Tag: cvc5-1.0.0~2458 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a20e8855be20f2cb4a8f43e03df35ff7caf31f96;p=cvc5.git google test: expr: Migrate node_algorithm_black. (#5643) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 8494064fb..440874166 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -16,7 +16,7 @@ cvc4_add_unit_test_white(attribute_white expr) cvc4_add_unit_test_black(kind_black expr) cvc4_add_unit_test_black(kind_map_black expr) cvc4_add_cxx_unit_test_black(node_black expr) -cvc4_add_cxx_unit_test_black(node_algorithm_black expr) +cvc4_add_unit_test_black(node_algorithm_black expr) cvc4_add_cxx_unit_test_black(node_builder_black expr) cvc4_add_cxx_unit_test_black(node_manager_black expr) cvc4_add_cxx_unit_test_white(node_manager_white expr) diff --git a/test/unit/expr/node_algorithm_black.cpp b/test/unit/expr/node_algorithm_black.cpp new file mode 100644 index 000000000..dd1982b1c --- /dev/null +++ b/test/unit/expr/node_algorithm_black.cpp @@ -0,0 +1,202 @@ +/********************* */ +/*! \file node_algorithm_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Black box testing of utility functions in node_algorithm.{h,cpp} + ** + ** Black box testing of node_algorithm.{h,cpp} + **/ + +#include +#include + +#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/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace expr; +using namespace kind; + +namespace test { + +class TestNodeBlackNodeAlgorithm : public TestNodeBlack +{ +}; + +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 n = d_nodeManager->mkNode(NOT, x); + std::unordered_set syms; + getSymbols(n, syms); + EXPECT_EQ(syms.size(), 1); + EXPECT_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_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType()); + Node left = d_nodeManager->mkNode(EQUAL, x, y); + + // right conjunct + Node var = d_nodeManager->mkBoundVar(*d_intTypeNode); + std::vector 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 syms; + getSymbols(res, syms); + + // assertions + EXPECT_EQ(syms.size(), 2); + EXPECT_NE(syms.find(x), syms.end()); + EXPECT_NE(syms.find(y), syms.end()); + EXPECT_EQ(syms.find(var), syms.end()); +} + +TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) +{ + // map to store result + std::map > result = + std::map >(); + + // create test formula + Node x = d_nodeManager->mkSkolem("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 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 + EXPECT_EQ(result.size(), 3); + EXPECT_NE(result.find(*d_intTypeNode), result.end()); + EXPECT_NE(result.find(*d_boolTypeNode), result.end()); + EXPECT_NE(result.find(*d_bvTypeNode), result.end()); + + // in integers, we should only have plus and mult as operators + EXPECT_EQ(result[*d_intTypeNode].size(), 2); + EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)), + result[*d_intTypeNode].end()); + EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)), + result[*d_intTypeNode].end()); + + // in booleans, we should only have "=" and "and" as an operator. + EXPECT_EQ(result[*d_boolTypeNode].size(), 2); + EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)), + result[*d_boolTypeNode].end()); + EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)), + result[*d_boolTypeNode].end()); + + // in bv, we should only have "extract" as an operator. + EXPECT_EQ(result[*d_boolTypeNode].size(), 2); + Node extractOp1 = + d_nodeManager->mkConst(BitVectorExtract(1, 0)); + Node extractOp2 = + d_nodeManager->mkConst(BitVectorExtract(3, 2)); + EXPECT_NE(result[*d_bvTypeNode].find(extractOp1), + result[*d_bvTypeNode].end()); + EXPECT_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_nodeManager->mkSkolem("a", integer); + + Node n1 = d_nodeManager->mkNode(MULT, two, x); + std::unordered_map subs; + + // check reflexivity + ASSERT_TRUE(match(n1, n1, subs)); + EXPECT_EQ(subs.size(), 0); + + Node n2 = d_nodeManager->mkNode(MULT, two, a); + subs.clear(); + + // check instance + ASSERT_TRUE(match(n1, n2, subs)); + EXPECT_EQ(subs.size(), 1); + EXPECT_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)); + EXPECT_EQ(subs.size(), 1); + EXPECT_EQ(subs[x], a); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h deleted file mode 100644 index 56a2f6e8c..000000000 --- a/test/unit/expr/node_algorithm_black.h +++ /dev/null @@ -1,220 +0,0 @@ -/********************* */ -/*! \file node_algorithm_black.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Abdalrhman Mohamed, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief Black box testing of utility functions in node_algorithm.{h,cpp} - ** - ** Black box testing of node_algorithm.{h,cpp} - **/ - -#include - -#include -#include - -#include "base/output.h" -#include "expr/node_algorithm.h" -#include "expr/node_manager.h" -#include "util/integer.h" -#include "util/rational.h" -#include "theory/bv/theory_bv_utils.h" - -using namespace CVC4; -using namespace CVC4::expr; -using namespace CVC4::kind; - -class NodeAlgorithmBlack : public CxxTest::TestSuite -{ - public: - void setUp() override - { - d_nodeManager = new NodeManager(NULL); - d_scope = new NodeManagerScope(d_nodeManager); - d_intTypeNode = new TypeNode(d_nodeManager->integerType()); - d_boolTypeNode = new TypeNode(d_nodeManager->booleanType()); - d_bvTypeNode = new TypeNode(d_nodeManager->mkBitVectorType(2)); - } - - void tearDown() override - { - delete d_bvTypeNode; - delete d_boolTypeNode; - delete d_intTypeNode; - delete d_scope; - delete d_nodeManager; - } - - // The only symbol in ~x (x is a boolean varible) should be x - void testGetSymbols1() - { - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node n = d_nodeManager->mkNode(NOT, x); - std::unordered_set syms; - getSymbols(n, syms); - TS_ASSERT_EQUALS(syms.size(), 1); - TS_ASSERT(syms.find(x) != syms.end()); - } - - // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because - // "var" is bound. - void testGetSymbols2() - { - // left conjunct - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType()); - Node left = d_nodeManager->mkNode(EQUAL, x, y); - - // right conjunct - Node var = d_nodeManager->mkBoundVar(*d_intTypeNode); - std::vector 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 syms; - getSymbols(res, syms); - - // assertions - TS_ASSERT_EQUALS(syms.size(), 2); - TS_ASSERT(syms.find(x) != syms.end()); - TS_ASSERT(syms.find(y) != syms.end()); - TS_ASSERT(syms.find(var) == syms.end()); - } - - void testGetOperatorsMap() - { - // map to store result - std::map > result = - std::map >(); - - // create test formula - Node x = d_nodeManager->mkSkolem("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 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 - TS_ASSERT(result.size() == 3); - TS_ASSERT(result.find(*d_intTypeNode) != result.end()); - TS_ASSERT(result.find(*d_boolTypeNode) != result.end()); - TS_ASSERT(result.find(*d_bvTypeNode) != result.end()); - - // in integers, we should only have plus and mult as operators - TS_ASSERT(result[*d_intTypeNode].size() == 2); - TS_ASSERT(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)) - != result[*d_intTypeNode].end()); - TS_ASSERT(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)) - != result[*d_intTypeNode].end()); - - // in booleans, we should only have "=" and "and" as an operator. - TS_ASSERT(result[*d_boolTypeNode].size() == 2); - TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)) - != result[*d_boolTypeNode].end()); - TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)) - != result[*d_boolTypeNode].end()); - - //in bv, we should only have "extract" as an operator. - TS_ASSERT(result[*d_boolTypeNode].size() == 2); - Node extractOp1 = d_nodeManager->mkConst(BitVectorExtract(1, 0)); - Node extractOp2 = d_nodeManager->mkConst(BitVectorExtract(3, 2)); - TS_ASSERT(result[*d_bvTypeNode].find(extractOp1) - != result[*d_bvTypeNode].end()); - TS_ASSERT(result[*d_bvTypeNode].find(extractOp2) - != result[*d_bvTypeNode].end()); - } - - void testMatch() - { - 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_nodeManager->mkSkolem("a", integer); - - Node n1 = d_nodeManager->mkNode(MULT, two, x); - std::unordered_map subs; - - // check reflexivity - TS_ASSERT(match(n1, n1, subs)); - TS_ASSERT_EQUALS(subs.size(), 0); - - Node n2 = d_nodeManager->mkNode(MULT, two, a); - subs.clear(); - - // check instance - TS_ASSERT(match(n1, n2, subs)); - TS_ASSERT_EQUALS(subs.size(), 1); - TS_ASSERT_EQUALS(subs[x], a); - - // should return false for flipped arguments (match is not symmetric) - TS_ASSERT(!match(n2, n1, subs)); - - n2 = d_nodeManager->mkNode(MULT, one, a); - - // should return false since n2 is not an instance of n1 - TS_ASSERT(!match(n1, n2, subs)); - - n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a); - - // should return false for similar operators - TS_ASSERT(!match(n1, n2, subs)); - - n2 = d_nodeManager->mkNode(MULT, two, a, one); - - // should return false for different number of arguments - TS_ASSERT(!match(n1, n2, subs)); - - n1 = x; - n2 = d_nodeManager->mkConst(true); - - // should return false for different types - TS_ASSERT(!match(n1, n2, subs)); - - n1 = d_nodeManager->mkNode(MULT, x, x); - n2 = d_nodeManager->mkNode(MULT, two, a); - - // should return false for contradictory substitutions - TS_ASSERT(!match(n1, n2, subs)); - - n2 = d_nodeManager->mkNode(MULT, a, a); - subs.clear(); - - // implementation: check if the cache works correctly - TS_ASSERT(match(n1, n2, subs)); - TS_ASSERT_EQUALS(subs.size(), 1); - TS_ASSERT_EQUALS(subs[x], a); - } - - private: - NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_intTypeNode; - TypeNode* d_boolTypeNode; - TypeNode* d_bvTypeNode; -}; diff --git a/test/unit/test_expr.h b/test/unit/test_expr.h index a6757a506..8c81f5902 100644 --- a/test/unit/test_expr.h +++ b/test/unit/test_expr.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Common header for Expr unit test. + ** \brief Common header for Expr unit tests. **/ #ifndef CVC4__TEST__UNIT__TEST_EXPR_H diff --git a/test/unit/test_node.h b/test/unit/test_node.h new file mode 100644 index 000000000..774c9e4d0 --- /dev/null +++ b/test/unit/test_node.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file test_expr.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Common header for Node unit tests. + **/ + +#ifndef CVC4__TEST__UNIT__TEST_NODE_H +#define CVC4__TEST__UNIT__TEST_NODE_H + +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test.h" +#include "test_api.h" + +namespace CVC4 { +namespace test { + +class TestNodeBlack : public TestInternal +{ + protected: + void SetUp() override + { + d_nodeManager.reset(new NodeManager(nullptr)); + d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType())); + d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); + d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); + } + + std::unique_ptr d_scope; + std::unique_ptr d_nodeManager; + std::unique_ptr d_intTypeNode; + std::unique_ptr d_boolTypeNode; + std::unique_ptr d_bvTypeNode; +}; + +} // namespace test +} // namespace CVC4 +#endif