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.cpp339
-rw-r--r--src/preprocessing/passes/int_to_bv.h45
2 files changed, 384 insertions, 0 deletions
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
new file mode 100644
index 000000000..997705835
--- /dev/null
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -0,0 +1,339 @@
+/********************* */
+/*! \file int_to_bv.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 The IntToBV preprocessing pass
+ **
+ ** Converts integer operations into bitvector operations. The width of the
+ ** bitvectors is controlled through the `--solve-int-as-bv` command line
+ ** option.
+ **/
+
+#include "preprocessing/passes/int_to_bv.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+namespace {
+
+// TODO: clean this up
+struct intToBV_stack_element
+{
+ TNode node;
+ bool children_added;
+ intToBV_stack_element(TNode node) : node(node), children_added(false) {}
+}; /* struct intToBV_stack_element */
+
+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())
+ {
+ // The current node we are processing
+ intToBV_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
+
+ NodeMap::iterator find = cache.find(current);
+ if (find != cache.end())
+ {
+ toVisit.pop_back();
+ continue;
+ }
+ if (stackHead.children_added)
+ {
+ // 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
+ {
+ NodeBuilder<> builder(current.getKind());
+ for (unsigned i = 0; i < current.getNumChildren(); ++i)
+ {
+ Assert(cache.find(current[i]) != cache.end());
+ builder << cache[current[i]];
+ }
+ result = builder;
+ }
+ cache[current] = result;
+ toVisit.pop_back();
+ }
+ else
+ {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0)
+ {
+ stackHead.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);
+ }
+ }
+ }
+ else
+ {
+ cache[current] = current;
+ toVisit.pop_back();
+ }
+ }
+ }
+ return cache[n];
+}
+
+Node intToBV(TNode n, NodeMap& cache)
+{
+ int size = options::solveIntAsBV();
+ 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())
+ {
+ // The current node we are processing
+ intToBV_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.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.children_added)
+ {
+ // Children have been processed, so rebuild this node
+ vector<Node> children;
+ unsigned max = 0;
+ for (unsigned i = 0; i < current.getNumChildren(); ++i)
+ {
+ Assert(cache.find(current[i]) != cache.end());
+ TNode childRes = cache[current[i]];
+ TypeNode type = childRes.getType();
+ if (type.isBitVector())
+ {
+ unsigned bvsize = type.getBitVectorSize();
+ if (bvsize > max)
+ {
+ max = bvsize;
+ }
+ }
+ children.push_back(childRes);
+ }
+
+ kind::Kind_t newKind = current.getKind();
+ if (max > 0)
+ {
+ switch (newKind)
+ {
+ case kind::PLUS:
+ Assert(children.size() == 2);
+ newKind = kind::BITVECTOR_PLUS;
+ max = max + 1;
+ break;
+ case kind::MULT:
+ Assert(children.size() == 2);
+ newKind = kind::BITVECTOR_MULT;
+ max = max * 2;
+ break;
+ case kind::MINUS:
+ Assert(children.size() == 2);
+ newKind = kind::BITVECTOR_SUB;
+ max = max + 1;
+ break;
+ case kind::UMINUS:
+ Assert(children.size() == 1);
+ newKind = kind::BITVECTOR_NEG;
+ max = max + 1;
+ break;
+ case kind::LT: newKind = kind::BITVECTOR_SLT; break;
+ case kind::LEQ: newKind = kind::BITVECTOR_SLE; break;
+ case kind::GT: newKind = kind::BITVECTOR_SGT; break;
+ case kind::GEQ: newKind = kind::BITVECTOR_SGE; break;
+ case kind::EQUAL:
+ case kind::ITE: break;
+ default:
+ if (Theory::theoryOf(current) == THEORY_BOOL)
+ {
+ break;
+ }
+ throw TypeCheckingException(
+ current.toExpr(),
+ string("Cannot translate to BV: ") + current.toString());
+ }
+ for (unsigned i = 0; i < children.size(); ++i)
+ {
+ TypeNode type = children[i].getType();
+ if (!type.isBitVector())
+ {
+ continue;
+ }
+ unsigned bvsize = type.getBitVectorSize();
+ if (bvsize < max)
+ {
+ // sign extend
+ Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
+ BitVectorSignExtend(max - bvsize));
+ children[i] = nm->mkNode(signExtendOp, children[i]);
+ }
+ }
+ }
+ NodeBuilder<> builder(newKind);
+ for (unsigned i = 0; i < children.size(); ++i)
+ {
+ builder << children[i];
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+
+ result = Rewriter::rewrite(result);
+ cache[current] = result;
+ toVisit.pop_back();
+ }
+ else
+ {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0)
+ {
+ stackHead.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);
+ }
+ }
+ }
+ else
+ {
+ // It's a leaf: could be a variable or a numeral
+ Node result = current;
+ if (current.isVar())
+ {
+ if (current.getType() == nm->integerType())
+ {
+ result = nm->mkSkolem("__intToBV_var",
+ nm->mkBitVectorType(size),
+ "Variable introduced in intToBV pass");
+ }
+ else
+ {
+ AlwaysAssert(current.getType() == nm->booleanType());
+ }
+ }
+ else if (current.isConst())
+ {
+ switch (current.getKind())
+ {
+ case kind::CONST_RATIONAL:
+ {
+ Rational constant = current.getConst<Rational>();
+ AlwaysAssert(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);
+ break;
+ }
+ case kind::CONST_BOOLEAN: break;
+ default:
+ throw TypeCheckingException(
+ current.toExpr(),
+ string("Cannot translate const to BV: ")
+ + current.toString());
+ }
+ }
+ else
+ {
+ throw TypeCheckingException(
+ current.toExpr(),
+ string("Cannot translate to BV: ") + current.toString());
+ }
+ cache[current] = result;
+ toVisit.pop_back();
+ }
+ }
+ }
+ return cache[n_binary];
+}
+} // namespace
+
+IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "int-to-bv"){};
+
+PreprocessingPassResult IntToBV::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+ {
+ assertionsToPreprocess->replace(
+ i, intToBV((*assertionsToPreprocess)[i], cache));
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
new file mode 100644
index 000000000..072e547c9
--- /dev/null
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -0,0 +1,45 @@
+/********************* */
+/*! \file int_to_bv.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 The IntToBV preprocessing pass
+ **
+ ** Converts integer operations into bitvector operations. The width of the
+ ** bitvectors is controlled through the `--solve-int-as-bv` command line
+ ** option.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
+#define __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class IntToBV : public PreprocessingPass
+{
+ public:
+ IntToBV(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback