From ccd4500c03685952ebf571b3539bd9e29c829cb5 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 25 Jun 2020 19:36:59 -0700 Subject: [PATCH] fix and test (#4658) This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly. --- src/expr/node_algorithm.cpp | 8 ++++++- test/unit/expr/node_algorithm_black.h | 34 ++++++++++++++++++++++----- 2 files changed, 35 insertions(+), 7 deletions(-) diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 52c5165a6..be436bf8b 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -491,7 +491,13 @@ void getOperatorsMap( // add the current operator to the result if (cur.hasOperator()) { - ops[tn].insert(NodeManager::currentNM()->operatorOf(cur.getKind())); + Node o; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { + o = cur.getOperator(); + } else { + o = NodeManager::currentNM()->operatorOf(cur.getKind()); + } + ops[tn].insert(o); } // add children to visit in the future for (TNode cn : cur) diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h index dea5b1f37..1f799cd40 100644 --- a/test/unit/expr/node_algorithm_black.h +++ b/test/unit/expr/node_algorithm_black.h @@ -24,6 +24,7 @@ #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; @@ -36,6 +37,7 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite NodeManagerScope* d_scope; TypeNode* d_intTypeNode; TypeNode* d_boolTypeNode; + TypeNode* d_bvTypeNode; public: void setUp() override @@ -44,6 +46,7 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite 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 @@ -107,16 +110,24 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite 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); + 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(eq, result); + expr::getOperatorsMap(formula, result); // Verify result - // We should have only integer and boolean as types - TS_ASSERT(result.size() == 2); + // 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); @@ -125,10 +136,21 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite 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); + // 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() -- 2.30.2