diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-06-19 22:45:32 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 22:45:32 -0700 |
commit | 3bc4a541b6c3a35fae987cc068e0e01937d5c4b1 (patch) | |
tree | 56f19ac241b31904cf52f46c60c1798fadc4c18f /src/preprocessing | |
parent | 3d44636a3080831bd8ea4c6b2d4f60adf6b37e9d (diff) |
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).
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 208 |
1 files changed, 62 insertions, 146 deletions
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 <vector> #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<Node, Node, NodeHashFunction>; 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<intToBV_stack_element> 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<intToBV_stack_element> 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<Node> 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<Rational>(); - 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<Rational>(); + 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]; |