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)
--- /dev/null
+/********************* */
+/*! \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 <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/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<Node, NodeHashFunction> 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<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, NodeHashFunction> 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<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
+
+ // 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>(BitVectorExtract(1, 0));
+ Node extractOp2 =
+ d_nodeManager->mkConst<BitVectorExtract>(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<Node, Node, NodeHashFunction> 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
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#include <string>
-#include <vector>
-
-#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<Node, NodeHashFunction> 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<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, NodeHashFunction> 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<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
-
- // 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>(BitVectorExtract(1, 0));
- Node extractOp2 = d_nodeManager->mkConst<BitVectorExtract>(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<Node, Node, NodeHashFunction> 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;
-};
** 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
--- /dev/null
+/********************* */
+/*! \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<NodeManagerScope> d_scope;
+ std::unique_ptr<NodeManager> d_nodeManager;
+ std::unique_ptr<TypeNode> d_intTypeNode;
+ std::unique_ptr<TypeNode> d_boolTypeNode;
+ std::unique_ptr<TypeNode> d_bvTypeNode;
+};
+
+} // namespace test
+} // namespace CVC4
+#endif
projects / cvc5.git / commitdiff