diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 129 |
1 files changed, 120 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 21f2d9209..2cc606fa9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -52,6 +52,7 @@ #include "util/node_visitor.h" #include "util/configuration.h" #include "util/exception.h" +#include "util/nary_builder.h" #include "smt/command_list.h" #include "smt/boolean_terms.h" #include "smt/options.h" @@ -90,6 +91,19 @@ namespace CVC4 { namespace smt { +/** Useful for counting the number of recursive calls. */ +class ScopeCounter { +private: + unsigned& d_depth; +public: + ScopeCounter(unsigned& d) : d_depth(d) { + ++d_depth; + } + ~ScopeCounter(){ + --d_depth; + } +}; + /** * Representation of a defined function. We keep these around in * SmtEngine to permit expanding definitions late (and lazily), to @@ -150,6 +164,9 @@ struct SmtEngineStatistics { /** time spent in processAssertions() */ TimerStat d_processAssertionsTime; + /** Has something simplified to false? */ + IntStat d_simplifiedToFalse; + SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"), @@ -168,7 +185,10 @@ struct SmtEngineStatistics { d_checkModelTime("smt::SmtEngine::checkModelTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), - d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") { + d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) + + { StatisticsRegistry::registerStat(&d_definitionExpansionTime); StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime); @@ -188,6 +208,7 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_solveTime); StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); + StatisticsRegistry::registerStat(&d_simplifiedToFalse); } ~SmtEngineStatistics() { @@ -209,6 +230,7 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_solveTime); StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); + StatisticsRegistry::unregisterStat(&d_simplifiedToFalse); } };/* struct SmtEngineStatistics */ @@ -305,6 +327,10 @@ class SmtEnginePrivate : public NodeManagerListener { */ Node d_modZero; + /** Number of calls of simplify assertions active. + */ + unsigned d_simplifyAssertionsDepth; + public: /** * Map from skolem variables to index in d_assertionsToCheck containing @@ -353,11 +379,15 @@ private: void bvToBool(); // Simplify ITE structure - void simpITE(); + bool simpITE(); // Simplify based on unconstrained values void unconstrainedSimp(); + // Ensures the assertions asserted after before now + // effectively come before d_realAssertionsEnd + void compressBeforeRealAssertions(size_t before); + /** * Any variable in an assertion that is declared as a subtype type * (predicate subtype or integer subrange type) must be constrained @@ -402,6 +432,7 @@ public: d_divByZero(), d_intDivByZero(), d_modZero(), + d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext) @@ -869,12 +900,41 @@ void SmtEngine::setLogicInternal() throw() { } // Turn on ite simplification for QF_LIA and QF_AUFBV if(! options::doITESimp.wasSetByUser()) { - bool iteSimp = !d_logic.isQuantified() && - ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) || - (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV))); + bool qf_aufbv = !d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV); + bool qf_lia = !d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && + d_logic.isLinear() && + !d_logic.isDifferenceLogic() && + !d_logic.areRealsUsed(); + + bool iteSimp = (qf_aufbv || qf_lia); Trace("smt") << "setting ite simplification to " << iteSimp << endl; options::doITESimp.set(iteSimp); } + if(! options::compressItes.wasSetByUser() ){ + bool qf_lia = !d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && + d_logic.isLinear() && + !d_logic.isDifferenceLogic() && + !d_logic.areRealsUsed(); + + bool compressIte = qf_lia; + Trace("smt") << "setting ite compression to " << compressIte << endl; + options::compressItes.set(compressIte); + } + if(! options::simplifyWithCareEnabled.wasSetByUser() ){ + bool qf_aufbv = !d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV); + + bool withCare = qf_aufbv; + Trace("smt") << "setting ite simplify with care to " << withCare << endl; + options::simplifyWithCareEnabled.set(withCare); + } // Turn off array eager index splitting for QF_AUFLIA if(! options::arraysEagerIndexSplitting.wasSetByUser()) { if (not d_logic.isQuantified() && @@ -2031,16 +2091,56 @@ void SmtEnginePrivate::bvToBool() { } } -void SmtEnginePrivate::simpITE() { +bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; + unsigned numAssertionOnEntry = d_assertionsToCheck.size(); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); + Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); + d_assertionsToCheck[i] = result; + if(result.isConst() && !result.getConst<bool>()){ + return false; + } } + bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck); + if(numAssertionOnEntry < d_assertionsToCheck.size()){ + compressBeforeRealAssertions(numAssertionOnEntry); + } + return result; } +void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ + size_t curr = d_assertionsToCheck.size(); + if(before >= curr || + d_realAssertionsEnd <= 0 || + d_realAssertionsEnd >= curr){ + return; + } + + // assertions + // original: [0 ... d_realAssertionsEnd) + // can be modified + // ites skolems [d_realAssertionsEnd, before) + // cannot be moved + // added [before, curr) + // can be modified + Assert(0 < d_realAssertionsEnd); + Assert(d_realAssertionsEnd <= before); + Assert(before < curr); + + std::vector<Node> intoConjunction; + for(size_t i = before; i<curr; ++i){ + intoConjunction.push_back(d_assertionsToCheck[i]); + } + d_assertionsToCheck.resize(before); + size_t lastBeforeItes = d_realAssertionsEnd - 1; + intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]); + Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + d_assertionsToCheck[lastBeforeItes] = newLast; + Assert(d_assertionsToCheck.size() == before); +} void SmtEnginePrivate::unconstrainedSimp() { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); @@ -2490,11 +2590,13 @@ void SmtEnginePrivate::doMiplibTrick() { d_realAssertionsEnd = d_assertionsToCheck.size(); } + // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() throw(TypeCheckingException, LogicException) { Assert(d_smt.d_pendingPops == 0); try { + ScopeCounter depth(d_simplifyAssertionsDepth); Trace("simplify") << "SmtEnginePrivate::simplify()" << endl; @@ -2560,9 +2662,14 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; // ITE simplification - if(options::doITESimp()) { + if(options::doITESimp() && + (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) { Chat() << "...doing ITE simplification..." << endl; - simpITE(); + bool noConflict = simpITE(); + if(!noConflict){ + Chat() << "...ITE simplification found unsat..." << endl; + return false; + } } dumpAssertions("post-itesimp", d_assertionsToCheck); @@ -2916,6 +3023,9 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); + if(!noConflict){ + ++(d_smt.d_stats->d_simplifiedToFalse); + } dumpAssertions("post-simplify", d_assertionsToCheck); dumpAssertions("pre-static-learning", d_assertionsToCheck); @@ -2954,6 +3064,7 @@ void SmtEnginePrivate::processAssertions() { if(options::repeatSimp()) { d_assertionsToCheck.swap(d_assertionsToPreprocess); Chat() << "re-simplifying assertions..." << endl; + ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); if (noConflict) { // Need to fix up assertion list to maintain invariants: |