From: Liana Hadarean Date: Thu, 23 Apr 2015 16:38:48 +0000 (+0100) Subject: Added option for --check-unsat-cores and various core bug fixes (merge of Morgan... X-Git-Tag: cvc5-1.0.0~6344^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0daf670d46ec2e781c2060b41449f2787b6e8f66;p=cvc5.git Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch). --- diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index def9308bb..bf0e57eca 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -228,6 +228,7 @@ void Smt2::addTheory(Theory theory) { case THEORY_STRINGS: defineType("String", getExprManager()->stringType()); + defineType("Int", getExprManager()->integerType()); addStringOperators(); break; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 0f9cfa710..2d8c4178a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -204,7 +204,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { Debug("cores") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); d_deps[Node::fromExpr(formula)]; // empty vector of deps - if(inUnsatCore || options::dumpUnsatCores()) { + if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) { Debug("cores") << "adding to input core forms: " << formula << std::endl; d_inputCoreFormulas.insert(formula); } @@ -221,6 +221,11 @@ void ProofManager::addDependence(TNode n, TNode dep) { } } +void ProofManager::addUnsatCore(Expr formula) { + Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); + d_outputCoreFormulas.insert(formula); +} + void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 43d6723fa..ee99b0159 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -171,6 +171,7 @@ public: void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); // note that n depends on dep (for cores) void addDependence(TNode n, TNode dep); + void addUnsatCore(Expr formula); assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } 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::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 @@ -185,6 +185,13 @@ class CVC4_PUBLIC SmtEngine { */ std::vector d_dumpCommands; + /** + *A vector of command definitions to be imported in the new + *SmtEngine when checking unsat-cores. + */ +#ifdef CVC4_PROOF + std::vector d_defineCommands; +#endif /** * The logic we're in. */ @@ -260,6 +267,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; diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 635262a1e..1df304061 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -223,13 +223,7 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc p += 2; } if(*p == 'S') { - // Strings requires arith for length constraints, - // and UF for equality (?) enableTheory(THEORY_STRINGS); - enableTheory(THEORY_UF); - enableTheory(THEORY_ARITH); - enableIntegers(); - arithOnlyLinear(); ++p; } if(!strncmp(p, "IDL", 3)) { diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h index 27cf86488..8f497688a 100644 --- a/src/util/unsat_core.h +++ b/src/util/unsat_core.h @@ -23,6 +23,7 @@ #include #include #include "expr/expr.h" +#include "util/output.h" namespace CVC4 { @@ -43,13 +44,17 @@ public: UnsatCore() : d_smt(NULL) {} template - UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {} + UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) { + Debug("core") << "UnsatCore size " << d_core.size() << std::endl; + } ~UnsatCore() {} /** get the smt engine that this unsat core is hooked up to */ SmtEngine* getSmtEngine() { return d_smt; } + size_t size() const { return d_core.size(); } + typedef std::vector::const_iterator iterator; typedef std::vector::const_iterator const_iterator; diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2 index acb6ffcdf..e1ca49ac5 100644 --- a/test/regress/regress0/arith/bug569.smt2 +++ b/test/regress/regress0/arith/bug569.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-unsat-cores +; EXPECT: unsat (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 5fe17b412..4f6320028 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -1,4 +1,4 @@ -% COMMAND-LINE: --no-check-proofs +% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores % OPTION "incremental"; diff --git a/test/regress/regress0/fmf/Makefile b/test/regress/regress0/fmf/Makefile new file mode 100644 index 000000000..1e68a1e9e --- /dev/null +++ b/test/regress/regress0/fmf/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/fmf + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index f0e53fc98..f3db78491 100644 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --no-check-proofs +; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. diff --git a/test/regress/run_regression b/test/regress/run_regression index 7b215dc2a..b6fb735fe 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -230,16 +230,28 @@ if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/d fi fi check_proofs=false +check_unsat_cores=false if [ "$proof" = yes ]; then # proofs not currently supported in incremental mode, turn it off if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && - ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-proofs on check_proofs=true fi + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-unsat-cores' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-unsat-cores' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then + # later on, we'll run another test with --check-unsat-cores on + check_unsat_cores=true + fi fi fi if [ -z "$expected_error" ]; then @@ -315,7 +327,7 @@ if [ "$exit_status" != "$expected_exit_status" ]; then exitcode=1 fi -if $check_models || $check_proofs; then +if $check_models || $check_proofs || $check_unsat_cores; then check_cmdline= if $check_models; then check_cmdline="$check_cmdline --check-models" @@ -323,7 +335,10 @@ if $check_models || $check_proofs; then if $check_proofs; then check_cmdline="$check_cmdline --check-proofs" fi - # at least one sat/invalid response: run an extra model/proof-checking pass + if $check_unsat_cores; then + check_cmdline="$check_cmdline --check-unsat-cores" + fi + # run an extra model/proof/core-checking pass if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then exitcode=1 fi