From 4be746589d4f456f772d4c8c524a1d34ab3b75c8 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 3 Apr 2018 20:43:37 -0700 Subject: 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/smt/smt_engine.cpp | 254 ++----------------------------------------------- 1 file changed, 10 insertions(+), 244 deletions(-) (limited to 'src/smt') 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 && -- cgit v1.2.3