summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/int_to_bv.cpp208
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];
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback