diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
commit | 0daf670d46ec2e781c2060b41449f2787b6e8f66 (patch) | |
tree | 7f1870bc621407a3c387ab6eb3dc77db529355dc /src/smt | |
parent | c604492260d0555bdb3cac5ba0863b7223f21777 (diff) |
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 126 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 12 | ||||
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 7 |
4 files changed, 136 insertions, 13 deletions
diff --git a/src/smt/options b/src/smt/options index 593fc4887..b23d73943 100644 --- a/src/smt/options +++ b/src/smt/options @@ -31,7 +31,7 @@ option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation -option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write after UNSAT/VALID, machine-check the generated proof option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response @@ -41,6 +41,8 @@ option dumpSynth --dump-synth bool :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation +option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write + after UNSAT/VALID, produce and check an unsat core (expensive) option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" output unsat cores after every UNSAT/VALID response diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 229cc7c7c..b2bdea13f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -199,6 +199,8 @@ struct SmtEngineStatistics { TimerStat d_checkModelTime; /** time spent in checkProof() */ TimerStat d_checkProofTime; + /** time spent in checkUnsatCore() */ + TimerStat d_checkUnsatCoreTime; /** time spent in PropEngine::checkSat() */ TimerStat d_solveTime; /** time spent in pushing/popping */ @@ -229,6 +231,7 @@ struct SmtEngineStatistics { d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_checkModelTime("smt::SmtEngine::checkModelTime"), d_checkProofTime("smt::SmtEngine::checkProofTime"), + d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), @@ -253,6 +256,7 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_numAssertionsPost); StatisticsRegistry::registerStat(&d_checkModelTime); StatisticsRegistry::registerStat(&d_checkProofTime); + StatisticsRegistry::registerStat(&d_checkUnsatCoreTime); StatisticsRegistry::registerStat(&d_solveTime); StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); @@ -278,6 +282,7 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_numAssertionsPost); StatisticsRegistry::unregisterStat(&d_checkModelTime); StatisticsRegistry::unregisterStat(&d_checkProofTime); + StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime); StatisticsRegistry::unregisterStat(&d_solveTime); StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); @@ -695,6 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_modelGlobalCommands(), d_modelCommands(NULL), d_dumpCommands(), +#ifdef CVC4_PROOF + d_defineCommands(), +#endif d_logic(), d_originalOptions(em->getOptions()), d_pendingPops(0), @@ -1029,6 +1037,14 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl; setOption("bv-intro-pow2", false); } + if(options::repeatSimp()) { + if(options::repeatSimp.wasSetByUser()) { + throw OptionException("repeat-simp not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl; + setOption("repeat-simp", false); + } + } if(options::produceAssignments() && !options::produceModels()) { @@ -1047,6 +1063,24 @@ void SmtEngine::setDefaults() { } } + // strings require LIA, UF; widen the logic + if(d_logic.isTheoryEnabled(THEORY_STRINGS)) { + LogicInfo log(d_logic.getUnlockedCopy()); + // Strings requires arith for length constraints, and also UF + if(!d_logic.isTheoryEnabled(THEORY_UF)) { + Trace("smt") << "because strings are enabled, also enabling UF" << endl; + log.enableTheory(THEORY_UF); + } + if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) { + Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl; + log.enableTheory(THEORY_ARITH); + log.enableIntegers(); + log.arithOnlyLinear(); + } + d_logic = log; + d_logic.lock(); + } + // by default, symmetry breaker is on only for QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified(); @@ -1133,16 +1167,25 @@ void SmtEngine::setDefaults() { // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! options::repeatSimp.wasSetByUser()) { bool repeatSimp = !d_logic.isQuantified() && - (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)); + (d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV)) && + !options::unsatCores(); Trace("smt") << "setting repeat simplification to " << repeatSimp << endl; options::repeatSimp.set(repeatSimp); } // Turn on unconstrained simplification for QF_AUFBV - if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) { + if(!options::unconstrainedSimp.wasSetByUser() || + options::incrementalSolving()) { // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() && - (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); + bool uncSimp = !options::incrementalSolving() && + !d_logic.isQuantified() && + !options::produceModels() && + !options::produceAssignments() && + !options::checkModels() && + !options::unsatCores() && + (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl; options::unconstrainedSimp.set(uncSimp); } @@ -1660,6 +1703,11 @@ void SmtEngine::defineFunction(Expr func, SmtScope smts(this); + PROOF( if (options::checkUnsatCores()) { + d_defineCommands.push_back(c.clone()); + }); + + // Substitute out any abstract values in formula Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr(); @@ -3033,7 +3081,7 @@ void SmtEnginePrivate::processAssertions() { Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - + if (d_assertions.size() == 0) { // nothing to do return; @@ -3331,8 +3379,7 @@ void SmtEnginePrivate::processAssertions() { d_iteSkolemMap.erase(toErase.back()); toErase.pop_back(); } - d_assertions[d_realAssertionsEnd - 1] = - Rewriter::rewrite(Node(builder)); + d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); } // For some reason this is needed for some benchmarks, such as // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 @@ -3442,6 +3489,12 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); } + // rewrite rules are by default in the unsat core because + // they need to be applied until saturation + if(options::unsatCores() && + n.getKind() == kind::REWRITE_RULE ){ + ProofManager::currentPM()->addUnsatCore(n.toExpr()); + } ); // Add the normalized formula to the queue @@ -3512,7 +3565,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE // Dump the query if requested if(Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << CheckSatCommand(); + Dump("benchmark") << CheckSatCommand(ex); } // Pop the context @@ -3539,6 +3592,13 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE checkProof(); } } + // Check that UNSAT results generate an unsat core correctly. + if(options::checkUnsatCores()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); + checkUnsatCore(); + } + } return r; } catch (UnsafeInterruptException& e) { @@ -3596,7 +3656,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce // Dump the query if requested if(Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << CheckSatCommand(); + Dump("benchmark") << QueryCommand(ex); } // Pop the context @@ -3623,6 +3683,13 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce checkProof(); } } + // Check that UNSAT results generate an unsat core correctly. + if(options::checkUnsatCores()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); + checkUnsatCore(); + } + } return r; } catch (UnsafeInterruptException& e) { @@ -3943,6 +4010,47 @@ Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) { return m; } +void SmtEngine::checkUnsatCore() { + Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off"); + + Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; + UnsatCore core = getUnsatCore(); + + SmtEngine coreChecker(d_exprManager); + coreChecker.setLogic(getLogicInfo()); + + PROOF( + std::vector<Command*>::const_iterator itg = d_defineCommands.begin(); + for (; itg != d_defineCommands.end(); ++itg) { + (*itg)->invoke(&coreChecker); + } + ); + + Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; + for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { + Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl; + coreChecker.assertFormula(*i); + } + const bool checkUnsatCores = options::checkUnsatCores(); + Result r; + try { + options::checkUnsatCores.set(false); + options::checkProofs.set(false); + r = coreChecker.checkSat(); + } catch(...) { + options::checkUnsatCores.set(checkUnsatCores); + throw; + } + Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; + if(r.asSatisfiabilityResult().isUnknown()) { + InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown."); + } + + if(r.asSatisfiabilityResult().isSat()) { + InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable."); + } +} + void SmtEngine::checkModel(bool hardFailure) { // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7c5c45e42..de9b8127d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -186,6 +186,13 @@ class CVC4_PUBLIC SmtEngine { std::vector<Command*> d_dumpCommands; /** + *A vector of command definitions to be imported in the new + *SmtEngine when checking unsat-cores. + */ +#ifdef CVC4_PROOF + std::vector<Command*> d_defineCommands; +#endif + /** * The logic we're in. */ LogicInfo d_logic; @@ -261,6 +268,11 @@ class CVC4_PUBLIC SmtEngine { void checkProof(); /** + * Check that an unsatisfiable core is indeed unsatisfiable. + */ + void checkUnsatCore(); + + /** * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 2080c772a..4c35bd863 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,9 +57,10 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if( ! ( d_logic.isPure(theory::THEORY_BOOL) || - ( d_logic.isPure(theory::THEORY_UF) && - ! d_logic.hasCardinalityConstraints() ) ) ) { + if( !(d_logic.isPure(theory::THEORY_BOOL) || + (d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints())) || + d_logic.isQuantified()) { // no checking for these yet Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; |