diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2019-07-22 22:39:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-22 22:39:59 -0700 |
commit | 5b494f33f146677386385fc7d055f95d9aae08d5 (patch) | |
tree | 603751d479cf69281d7c40658478e9bedda90048 /test | |
parent | 5d203980cb011ce0a9aa5007d4792c1f80dd1e4b (diff) |
Get operators in node (#3094)
This commit adds a function to node_algorithm.{h,cpp} that returns the operators that occur in a given node.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/expr/node_algorithm_black.h | 133 |
2 files changed, 134 insertions, 0 deletions
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 575268cae..d487bf560 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -8,6 +8,7 @@ cvc4_add_unit_test_black(expr_public expr) cvc4_add_unit_test_black(kind_black expr) cvc4_add_unit_test_black(kind_map_black expr) cvc4_add_unit_test_black(node_black expr) +cvc4_add_unit_test_black(node_algorithm_black expr) cvc4_add_unit_test_black(node_builder_black expr) cvc4_add_unit_test_black(node_manager_black expr) cvc4_add_unit_test_white(node_manager_white expr) diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h new file mode 100644 index 000000000..2151eef72 --- /dev/null +++ b/test/unit/expr/node_algorithm_black.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file node_algorithm_black.h + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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" + +using namespace CVC4; +using namespace CVC4::expr; +using namespace CVC4::kind; + +class NodeAlgorithmBlack : public CxxTest::TestSuite +{ + private: + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; + TypeNode* d_intTypeNode; + TypeNode* d_boolTypeNode; + + 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()); + } + + void tearDown() override + { + delete d_intTypeNode; + delete d_boolTypeNode; + 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 eq = d_nodeManager->mkNode(EQUAL, plus, mul); + + // call function + expr::getOperatorsMap(eq, result); + + // Verify result + // We should have only integer and boolean as types + TS_ASSERT(result.size() == 2); + TS_ASSERT(result.find(*d_intTypeNode) != result.end()); + TS_ASSERT(result.find(*d_boolTypeNode) != 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 "=" as an operator. + TS_ASSERT(result[*d_boolTypeNode].size() == 1); + TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)) + != result[*d_boolTypeNode].end()); + } +}; |