diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-03 20:43:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-03 20:43:37 -0700 |
commit | 4be746589d4f456f772d4c8c524a1d34ab3b75c8 (patch) | |
tree | edef4179d1c7d2a666a6195b07fb55e71eb77b30 /src/preprocessing | |
parent | eaebc10c50ca44644edd430ed3f555092a0fb27a (diff) |
Refactor IntToBV preprocessing pass (#1716)
This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 339 | ||||
-rw-r--r-- | src/preprocessing/passes/int_to_bv.h | 45 |
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 */ |