From: Alex Ozdemir Date: Sat, 20 Jun 2020 05:45:32 +0000 (-0700) Subject: Use traversal iterators in IntToBv (#4169) X-Git-Tag: cvc5-1.0.0~3187 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bc4a541b6c3a35fae987cc068e0e01937d5c4b1;p=cvc5.git Use traversal iterators in IntToBv (#4169) This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators. Also, cleaned `childrenTypesChanged` a bit. While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes). --- diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp index 0d207b302..5968c4348 100644 --- a/src/expr/node_traversal.cpp +++ b/src/expr/node_traversal.cpp @@ -63,8 +63,11 @@ TNode& NodeDfsIterator::operator*() return d_current; } -bool NodeDfsIterator::operator==(const NodeDfsIterator& other) const +bool NodeDfsIterator::operator==(NodeDfsIterator& other) { + // Unitialize this node, and the other, before comparing. + initializeIfUninitialized(); + other.initializeIfUninitialized(); // The stack and current node uniquely represent traversal state. We need not // use the scheduled node set. // @@ -74,7 +77,7 @@ bool NodeDfsIterator::operator==(const NodeDfsIterator& other) const return d_stack == other.d_stack && d_current == other.d_current; } -bool NodeDfsIterator::operator!=(const NodeDfsIterator& other) const +bool NodeDfsIterator::operator!=(NodeDfsIterator& other) { return !(*this == other); } diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 1398f6485..586cbb64d 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -67,9 +67,13 @@ class NodeDfsIterator // Dereference reference operator*(); // Equals - bool operator==(const NodeDfsIterator&) const; + // It is not constant, because an unitilized node must be initialized before + // comparison + bool operator==(NodeDfsIterator&); // Not equals - bool operator!=(const NodeDfsIterator&) const; + // It is not constant, because an unitilized node must be initialized before + // comparison + bool operator!=(NodeDfsIterator&); private: // While we're not at an appropriate visit (see d_postorder), advance. diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 2740cb771..e30c03f26 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -23,6 +23,7 @@ #include #include "expr/node.h" +#include "expr/node_traversal.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -36,107 +37,58 @@ using NodeMap = std::unordered_map; namespace { -// TODO: clean this up -struct intToBV_stack_element -{ - TNode d_node; - bool d_children_added; - intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {} -}; /* struct intToBV_stack_element */ - bool childrenTypesChanged(Node n, NodeMap& cache) { - bool result = false; for (Node child : n) { TypeNode originalType = child.getType(); TypeNode newType = cache[child].getType(); if (! newType.isSubtypeOf(originalType)) { - result = true; - break; + return true; } } - return result; + return false; } Node intToBVMakeBinary(TNode n, NodeMap& cache) { - // Do a topological sort of the subexpressions and substitute them - vector toVisit; - toVisit.push_back(n); - - while (!toVisit.empty()) + for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER, + [&cache](TNode nn) { return cache.count(nn) > 0; })) { - // The current node we are processing - intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.d_node; - - NodeMap::iterator find = cache.find(current); - if (find != cache.end()) + Node result; + NodeManager* nm = NodeManager::currentNM(); + if (current.getNumChildren() == 0) { - toVisit.pop_back(); - continue; + result = current; } - if (stackHead.d_children_added) + else if (current.getNumChildren() > 2 + && (current.getKind() == kind::PLUS + || current.getKind() == kind::MULT)) { - // Children have been processed, so rebuild this node - Node result; - NodeManager* nm = NodeManager::currentNM(); - if (current.getNumChildren() > 2 - && (current.getKind() == kind::PLUS - || current.getKind() == kind::MULT)) - { - Assert(cache.find(current[0]) != cache.end()); - result = cache[current[0]]; - for (unsigned i = 1; i < current.getNumChildren(); ++i) - { - Assert(cache.find(current[i]) != cache.end()); - Node child = current[i]; - Node childRes = cache[current[i]]; - result = nm->mkNode(current.getKind(), result, childRes); - } - } - else + Assert(cache.find(current[0]) != cache.end()); + result = cache[current[0]]; + for (unsigned i = 1; i < current.getNumChildren(); ++i) { - NodeBuilder<> builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); - } - - for (unsigned i = 0; i < current.getNumChildren(); ++i) - { - Assert(cache.find(current[i]) != cache.end()); - builder << cache[current[i]]; - } - result = builder; + Assert(cache.find(current[i]) != cache.end()); + Node child = current[i]; + Node childRes = cache[current[i]]; + result = nm->mkNode(current.getKind(), result, childRes); } - cache[current] = result; - toVisit.pop_back(); } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) - { - stackHead.d_children_added = true; - // We need to add the children - for (TNode::iterator child_it = current.begin(); - child_it != current.end(); - ++child_it) - { - TNode childNode = *child_it; - NodeMap::iterator childFind = cache.find(childNode); - if (childFind == cache.end()) - { - toVisit.push_back(childNode); - } - } + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); } - else + + for (unsigned i = 0; i < current.getNumChildren(); ++i) { - cache[current] = current; - toVisit.pop_back(); + Assert(cache.find(current[i]) != cache.end()); + builder << cache[current[i]]; } + result = builder; } + cache[current] = result; } return cache[n]; } @@ -147,30 +99,16 @@ Node intToBV(TNode n, NodeMap& cache) AlwaysAssert(size > 0); AlwaysAssert(!options::incrementalSolving()); - vector toVisit; NodeMap binaryCache; Node n_binary = intToBVMakeBinary(n, binaryCache); - toVisit.push_back(TNode(n_binary)); - while (!toVisit.empty()) + for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER, + [&cache](TNode nn) { return cache.count(nn) > 0; })) { - // The current node we are processing - intToBV_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.d_node; - - // If node is already in the cache we're done, pop from the stack - NodeMap::iterator find = cache.find(current); - if (find != cache.end()) - { - toVisit.pop_back(); - continue; - } - - // Not yet substituted, so process NodeManager* nm = NodeManager::currentNM(); - if (stackHead.d_children_added) + if (current.getNumChildren() > 0) { - // Children have been processed, so rebuild this node + // Not a leaf vector children; unsigned max = 0; for (unsigned i = 0; i < current.getNumChildren(); ++i) @@ -258,73 +196,51 @@ Node intToBV(TNode n, NodeMap& cache) result = Rewriter::rewrite(result); cache[current] = result; - toVisit.pop_back(); } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) + // It's a leaf: could be a variable or a numeral + Node result = current; + if (current.isVar()) { - stackHead.d_children_added = true; - // We need to add the children - for (TNode::iterator child_it = current.begin(); - child_it != current.end(); - ++child_it) + if (current.getType() == nm->integerType()) { - TNode childNode = *child_it; - NodeMap::iterator childFind = cache.find(childNode); - if (childFind == cache.end()) - { - toVisit.push_back(childNode); - } + result = nm->mkSkolem("__intToBV_var", + nm->mkBitVectorType(size), + "Variable introduced in intToBV pass"); } } - else + else if (current.isConst()) { - // It's a leaf: could be a variable or a numeral - Node result = current; - if (current.isVar()) + switch (current.getKind()) { - if (current.getType() == nm->integerType()) + case kind::CONST_RATIONAL: { - result = nm->mkSkolem("__intToBV_var", - nm->mkBitVectorType(size), - "Variable introduced in intToBV pass"); - } - } - else if (current.isConst()) - { - switch (current.getKind()) - { - case kind::CONST_RATIONAL: - { - Rational constant = current.getConst(); - if (constant.isIntegral()) { - AlwaysAssert(constant >= 0); - BitVector bv(size, constant.getNumerator()); - if (bv.toSignedInteger() != constant.getNumerator()) - { - throw TypeCheckingException( - current.toExpr(), - string("Not enough bits for constant in intToBV: ") - + current.toString()); - } - result = nm->mkConst(bv); + Rational constant = current.getConst(); + if (constant.isIntegral()) { + AlwaysAssert(constant >= 0); + BitVector bv(size, constant.getNumerator()); + if (bv.toSignedInteger() != constant.getNumerator()) + { + throw TypeCheckingException( + current.toExpr(), + string("Not enough bits for constant in intToBV: ") + + current.toString()); } - break; + result = nm->mkConst(bv); } - default: break; + break; } + default: break; } - else - { - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate to BV: ") + current.toString()); - } - cache[current] = result; - toVisit.pop_back(); } + else + { + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to BV: ") + current.toString()); + } + cache[current] = result; } } return cache[n_binary]; diff --git a/test/unit/expr/node_traversal_black.h b/test/unit/expr/node_traversal_black.h index 02f8db6a3..6f5dfaf04 100644 --- a/test/unit/expr/node_traversal_black.h +++ b/test/unit/expr/node_traversal_black.h @@ -177,6 +177,22 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); TS_ASSERT_EQUALS(actual, expected); } + + void testSkipAll() + { + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector expected = {}; + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER, + [](TNode n) { return true; }); + + std::vector actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + TS_ASSERT_EQUALS(actual, expected); + } }; class NodePreorderTraversalBlack : public CxxTest::TestSuite