diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options_handlers.h | 12 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 119 |
2 files changed, 110 insertions, 21 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 058a00f32..af8e8663c 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -121,7 +121,13 @@ t-explanations [non-stateful]\n\ bv-rewrites [non-stateful]\n\ + Output correctness queries for all bitvector rewrites\n\ \n\ -theory::fullcheck [non-stateful]\n\ +bv-abstraction [non-stateful]\n\ ++ Output correctness queries for all bv abstraction \n\ +\n\ +bv-algebraic [non-stateful]\n\ ++ Output correctness queries for bv algebraic solver. \n\ +\n\ +theory::fullcheck [non-stateful]\n \ + Output completeness queries for all full-check effort-level theory checks\n\ \n\ Dump modes can be combined with multiple uses of --dump. Generally you want\n\ @@ -237,6 +243,10 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { } else if(!strcmp(optargPtr, "help")) { puts(dumpHelp.c_str()); exit(1); + } else if(!strcmp(optargPtr, "bv-abstraction")) { + Dump.on("bv-abstraction"); + } else if(!strcmp(optargPtr, "bv-algebraic")) { + Dump.on("bv-algebraic"); } else { throw OptionException(std::string("unknown option for --dump: `") + optargPtr + "'. Try --dump help."); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 33496ac3b..6dbef4fe3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -361,11 +361,15 @@ private: // Lift bit-vectors of size 1 to booleans void bvToBool(); + // Abstract common structure over small domains to UF + // return true if changes were made. + void bvAbstraction(); + // Simplify ITE structure bool simpITE(); // Simplify based on unconstrained values - void unconstrainedSimp(); + void unconstrainedSimp(std::vector<Node>& assertions); // Ensures the assertions asserted after before now // effectively come before d_realAssertionsEnd @@ -896,11 +900,6 @@ void SmtEngine::setDefaults() { */ } - if(options::bitvectorEagerBitblast()) { - // Eager solver should use the internal decision strategy - options::decisionMode.set(DECISION_STRATEGY_INTERNAL); - } - if(options::checkModels()) { if(! options::interactive()) { Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; @@ -1069,6 +1068,27 @@ void SmtEngine::setDefaults() { setOption("check-models", SExpr("false")); } } + + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && + options::incrementalSolving()) { + if (options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ + Try --bitblast=lazy")); + } + Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl; + setOption("incremental", SExpr("false")); + } + + if (! options::bvEagerExplanations.wasSetByUser() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_BV)) { + Trace("smt") << "enabling eager bit-vector explanations " << endl; + options::bvEagerExplanations.set(true); + } + + + // Turn on arith rewrite equalities only for pure arithmetic if(! options::arithRewriteEq.wasSetByUser()) { bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified(); @@ -1971,13 +1991,29 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } +void SmtEnginePrivate::bvAbstraction() { + Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl; + std::vector<Node> new_assertions; + bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertionsToPreprocess, new_assertions); + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]); + } + // if we are using the lazy solver and the abstraction + // applies, then UF symbols were introduced + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && + changed) { + LogicRequest req(d_smt); + req.widenLogic(THEORY_UF); + } +} + void SmtEnginePrivate::bvToBool() { Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; std::vector<Node> new_assertions; - d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToPreprocess, new_assertions); + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]); } } @@ -2032,11 +2068,10 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ Assert(d_assertionsToCheck.size() == before); } -void SmtEnginePrivate::unconstrainedSimp() { +void SmtEnginePrivate::unconstrainedSimp(std::vector<Node>& assertions) { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); - Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; - d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck); + d_smt.d_theoryEngine->ppUnconstrainedSimp(assertions); } @@ -2533,6 +2568,9 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // before ppRewrite check if only core theory for BV theory + d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck); + // Theory preprocessing if (d_smt.d_earlyTheoryPP) { Chat() << "...doing early theory preprocessing..." << endl; @@ -2570,7 +2608,7 @@ bool SmtEnginePrivate::simplifyAssertions() // Unconstrained simplification if(options::unconstrainedSimp()) { Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(); + unconstrainedSimp(d_assertionsToCheck); } dumpAssertions("post-unconstrained", d_assertionsToCheck); @@ -2825,7 +2863,26 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && + !d_smt.d_logic.isPure(THEORY_BV)) { + throw ModalException("Eager bit-blasting does not currently support theory combination. " + "Note that in a QF_BV problem UF symbols can be introduced for division. " + "Try --bv-div-zero-const to interpret division by zero as a constant."); + } + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess); + } + + + if ( options::bvAbstraction() && + !options::incrementalSolving()) { + dumpAssertions("pre-bv-abstraction", d_assertionsToPreprocess); + bvAbstraction(); + dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess); + } + dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess); { Chat() << "rewriting Boolean terms..." << endl; @@ -2855,6 +2912,15 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + // Unconstrained simplification + if(options::unconstrainedSimp()) { + dumpAssertions("pre-unconstrained-simp", d_assertionsToPreprocess); + Chat() << "...doing unconstrained simplification..." << endl; + unconstrainedSimp(d_assertionsToPreprocess); + dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess); + } + dumpAssertions("pre-substitution", d_assertionsToPreprocess); // Apply the substitutions we already have, and normalize @@ -2871,6 +2937,15 @@ void SmtEnginePrivate::processAssertions() { // Assertions ARE guaranteed to be rewritten by this point + + // Lift bit-vectors of size 1 to bool + if(options::bitvectorToBool()) { + dumpAssertions("pre-bv-to-bool", d_assertionsToPreprocess); + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess); + } + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); CVC4::theory::strings::StringsPreprocess sp; @@ -2957,12 +3032,6 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); - // Lift bit-vectors of size 1 to bool - if(options::bvToBool()) { - Chat() << "...doing bvToBool..." << endl; - bvToBool(); - } - Trace("smt") << "POST bvToBool" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -3086,6 +3155,15 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-theory-preprocessing", d_assertionsToCheck); + // If we are using eager bit-blasting wrap assertions in fake atom so that + // everything gets bit-blasted to internal SAT solver + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { + Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]); + d_assertionsToCheck[i] = eager_atom; + } + } + // Push the formula to decision engine if(noConflict) { Chat() << "pushing to decision engine..." << endl; @@ -3099,7 +3177,6 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-everything", d_assertionsToCheck); - // Push the formula to SAT { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); @@ -3107,6 +3184,7 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); } } + d_assertionsProcessed = true; @@ -3380,6 +3458,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L hash_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); n = postprocess(n, TypeNode::fromType(e.getType())); + return n.toExpr(); } |