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).
decision/decision_strategy.h \
decision/justification_heuristic.cpp \
decision/justification_heuristic.h \
+ preprocessing/passes/int_to_bv.cpp \
+ preprocessing/passes/int_to_bv.h \
preprocessing/preprocessing_pass.cpp \
preprocessing/preprocessing_pass.h \
preprocessing/preprocessing_pass_context.cpp \
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#include <algorithm>
#include <cctype>
-#include <unordered_map>
-#include <unordered_set>
#include <iterator>
+#include <memory>
#include <sstream>
#include <stack>
#include <string>
+#include <unordered_map>
+#include <unordered_set>
#include <utility>
#include <vector>
#include "options/strings_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "preprocessing/preprocessing_pass_registry.h"
using namespace CVC4;
using namespace CVC4::smt;
using namespace CVC4::preprocessing;
+using namespace CVC4::preprocessing::passes;
using namespace CVC4::prop;
using namespace CVC4::context;
using namespace CVC4::theory;
void SmtEnginePrivate::finishInit() {
d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
- //TODO: register passes here
+ // TODO: register passes here (this will likely change when we add support for
+ // actually assembling preprocessing pipelines).
+ std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
+ d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
}
Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
return result.top();
}
-//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 */
-
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-Node SmtEnginePrivate::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 SmtEnginePrivate::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];
-}
-
Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) {
Trace("real-as-int-debug") << "Convert : " << n << std::endl;
NodeMap::iterator find = cache.find(n);
}
if (options::solveIntAsBV() > 0) {
- Chat() << "converting ints to bit-vectors..." << endl;
- unordered_map<Node, Node, NodeHashFunction> cache;
- for(unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.replace(i, intToBV(d_assertions[i], cache));
- }
+ d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions);
}
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
projects / cvc5.git / commitdiff