From 4be746589d4f456f772d4c8c524a1d34ab3b75c8 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 3 Apr 2018 20:43:37 -0700 Subject: [PATCH] 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). --- src/Makefile.am | 2 + src/preprocessing/passes/int_to_bv.cpp | 339 +++++++++++++++++++++++++ src/preprocessing/passes/int_to_bv.h | 45 ++++ src/smt/smt_engine.cpp | 254 +----------------- 4 files changed, 396 insertions(+), 244 deletions(-) create mode 100644 src/preprocessing/passes/int_to_bv.cpp create mode 100644 src/preprocessing/passes/int_to_bv.h diff --git a/src/Makefile.am b/src/Makefile.am index 8aa06e82f..b33c0586f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -62,6 +62,8 @@ libcvc4_la_SOURCES = \ 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 \ 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 +#include +#include + +#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; + +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 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 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 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(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(); + 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 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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2f6832089..abefaf215 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,12 +18,13 @@ #include #include -#include -#include #include +#include #include #include #include +#include +#include #include #include @@ -67,6 +68,7 @@ #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" @@ -116,6 +118,7 @@ using namespace std; 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; @@ -2542,7 +2545,10 @@ bool SmtEngine::isDefinedFunction( Expr func ){ 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(new IntToBV(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -2703,244 +2709,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map NodeMap; -Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) { - // Do a topological sort of the subexpressions and substitute them - vector 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 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 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(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(); - 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); @@ -4317,11 +4087,7 @@ void SmtEnginePrivate::processAssertions() { } if (options::solveIntAsBV() > 0) { - Chat() << "converting ints to bit-vectors..." << endl; - unordered_map 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 && -- 2.30.2