From d2bc889a6df05f0c984983192ed1aca129931df7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Feb 2022 10:55:18 -0600 Subject: [PATCH] Distinguish proof mode from unsat core mode (#8062) Previously, we were making unsat cores mode the source of our configuration for unsat cores and proofs at the same time. This led to a lot of unnecessary complication in the logic, and would allow bugs e.g. if produce-difficulty but not produce-unsat-cores was enabled. Fixes cvc5/cvc5-projects#406. --- src/options/smt_options.toml | 20 ++++- src/prop/minisat/core/Solver.cc | 3 +- src/prop/theory_proxy.cpp | 2 +- src/smt/env.cpp | 10 +-- src/smt/set_defaults.cpp | 80 ++++++++++++------- src/smt/solver_engine.cpp | 6 +- test/regress/CMakeLists.txt | 1 + .../proj-issue406-diff-unsat-core.smt2 | 12 +++ 8 files changed, 86 insertions(+), 48 deletions(-) create mode 100644 test/regress/regress1/proj-issue406-diff-unsat-core.smt2 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 0af1d703b..842cf046f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -164,15 +164,27 @@ name = "SMT Layer" help = "Do not produce unsat cores." [[option.mode.SAT_PROOF]] name = "sat-proof" - help = "Produce unsat cores from SAT and preprocessing proofs." -[[option.mode.FULL_PROOF]] - name = "full-proof" - help = "Produce unsat cores from full proofs." + help = "Produce unsat cores from the SAT proof and prepocessing proofs." [[option.mode.ASSUMPTIONS]] name = "assumptions" help = "Produce unsat cores using solving under assumptions and preprocessing proofs." + +[[option]] + name = "proofMode" + category = "expert" + long = "proof-mode=MODE" + type = "ProofMode" + default = "OFF" + help = "choose proof mode, see --proof-mode=help" + help_mode = "proof modes." +[[option.mode.OFF]] + name = "off" [[option.mode.PP_ONLY]] name = "pp-only" +[[option.mode.SAT]] + name = "sat-proof" +[[option.mode.FULL]] + name = "full-proof" [[option]] name = "minimalUnsatCores" diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 9715fc9a7..c0e524cde 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -2190,8 +2190,7 @@ bool Solver::isProofEnabled() const { return d_pfManager != nullptr; } bool Solver::needProof() const { return isProofEnabled() - && options().smt.unsatCoresMode != options::UnsatCoresMode::ASSUMPTIONS - && options().smt.unsatCoresMode != options::UnsatCoresMode::PP_ONLY; + && options().smt.proofMode != options::ProofMode::PP_ONLY; } } // namespace Minisat diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 58a7fb666..357248726 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -167,7 +167,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { Node theoryExplanation = tte.getNode(); if (d_env.isSatProofProducing()) { - Assert(options().smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF + Assert(options().smt.proofMode != options::ProofMode::FULL || tte.getGenerator()); d_propEngine->getProofCnfStream()->convertPropagation(tte); } diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 55beaed75..41bf8a482 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -93,19 +93,13 @@ ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } bool Env::isSatProofProducing() const { return d_proofNodeManager != nullptr - && (!d_options.smt.unsatCores - || (d_options.smt.unsatCoresMode - != options::UnsatCoresMode::ASSUMPTIONS - && d_options.smt.unsatCoresMode - != options::UnsatCoresMode::PP_ONLY)); + && d_options.smt.proofMode != options::ProofMode::PP_ONLY; } bool Env::isTheoryProofProducing() const { return d_proofNodeManager != nullptr - && (!d_options.smt.unsatCores - || d_options.smt.unsatCoresMode - == options::UnsatCoresMode::FULL_PROOF); + && d_options.smt.proofMode == options::ProofMode::FULL; } theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 8e993d376..12cf15346 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -62,12 +62,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) void SetDefaults::setDefaultsPre(Options& opts) { - // internal-only options - if (opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY) - { - throw OptionException( - std::string("Unsat core mode pp-only is for internal use only.")); - } // implied options if (opts.smt.debugCheckModels) { @@ -86,13 +80,6 @@ void SetDefaults::setDefaultsPre(Options& opts) { opts.smt.produceDifficulty = true; } - if (opts.smt.produceDifficulty) - { - if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) - { - opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY; - } - } if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) @@ -109,37 +96,72 @@ void SetDefaults::setDefaultsPre(Options& opts) } opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } - - if (opts.smt.checkProofs || opts.driver.dumpProofs) + // if check-proofs, dump-proofs, or proof-mode=full, then proofs being fully + // enabled is implied + if (opts.smt.checkProofs || opts.driver.dumpProofs + || opts.smt.proofMode == options::ProofMode::FULL) { opts.smt.produceProofs = true; } - if (opts.smt.produceProofs - && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) + // this check assumes the user has requested *full* proofs + if (opts.smt.produceProofs) { - if (opts.smt.unsatCoresModeWasSetByUser) + // if the user requested proofs, proof mode is full + opts.smt.proofMode = options::ProofMode::FULL; + // unsat cores are available due to proofs being enabled + if (opts.smt.unsatCoresMode != options::UnsatCoresMode::SAT_PROOF) { - notifyModifyOption("unsatCoresMode", "full-proof", "enabling proofs"); + if (opts.smt.unsatCoresModeWasSetByUser) + { + notifyModifyOption("unsatCoresMode", "full-proof", "enabling proofs"); + } + opts.smt.unsatCores = true; + opts.smt.unsatCoresMode = options::UnsatCoresMode::SAT_PROOF; } - // enable unsat cores, because they are available as a consequence of proofs - opts.smt.unsatCores = true; - opts.smt.unsatCoresMode = options::UnsatCoresMode::FULL_PROOF; } - - // set proofs on if not yet set - if (opts.smt.unsatCores && !opts.smt.produceProofs) + if (!opts.smt.produceProofs) { - if (opts.smt.produceProofsWasSetByUser) + if (opts.smt.proofMode != options::ProofMode::OFF) { - notifyModifyOption("produceProofs", "true", "enabling unsat cores"); + // if (expert) user set proof mode to something other than off, enable + // proofs + opts.smt.produceProofs = true; + } + // if proofs weren't enabled by user, and we are producing difficulty + if (opts.smt.produceDifficulty) + { + opts.smt.produceProofs = true; + // ensure at least preprocessing proofs are enabled + if (opts.smt.proofMode == options::ProofMode::OFF) + { + opts.smt.proofMode = options::ProofMode::PP_ONLY; + } + } + // if proofs weren't enabled by user, and we are producing unsat cores + if (opts.smt.unsatCores) + { + opts.smt.produceProofs = true; + if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF) + { + // if requested to be based on proofs, we produce (preprocessing +) SAT + // proofs + opts.smt.proofMode = options::ProofMode::SAT; + } + else if (opts.smt.proofMode == options::ProofMode::OFF) + { + // otherwise, we always produce preprocessing proofs + opts.smt.proofMode = options::ProofMode::PP_ONLY; + } } - opts.smt.produceProofs = true; } - // if unsat cores are disabled, then unsat cores mode should be OFF + // if unsat cores are disabled, then unsat cores mode should be OFF. Similarly + // for proof mode. Assert(opts.smt.unsatCores == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); + Assert(opts.smt.produceProofs + == (opts.smt.proofMode != options::ProofMode::OFF)); // if we requiring disabling proofs, disable them now if (opts.smt.produceProofs) diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 9e8d4703a..68cdf2780 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1528,10 +1528,8 @@ void SolverEngine::printInstantiations(std::ostream& out) // Second, extract and print the instantiations std::map rinsts; - if (d_env->getOptions().smt.produceProofs - && (!d_env->getOptions().smt.unsatCores - || d_env->getOptions().smt.unsatCoresMode - == options::UnsatCoresMode::FULL_PROOF) + if ((d_env->getOptions().smt.produceProofs + && d_env->getOptions().smt.proofMode == options::ProofMode::FULL) && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ad5918ee8..3e98a01ad 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1925,6 +1925,7 @@ set(regress_1_tests regress1/nl/zero-subset.smt2 regress1/non-fatal-errors.smt2 regress1/proj-issue175.smt2 + regress1/proj-issue406-diff-unsat-core.smt2 regress1/proof00.smt2 regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 diff --git a/test/regress/regress1/proj-issue406-diff-unsat-core.smt2 b/test/regress/regress1/proj-issue406-diff-unsat-core.smt2 new file mode 100644 index 000000000..db234dc8d --- /dev/null +++ b/test/regress/regress1/proj-issue406-diff-unsat-core.smt2 @@ -0,0 +1,12 @@ +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof +; EXPECT: unsat +; EXPECT: (error "Cannot get unsat core unless explicitly enabled (try --produce-unsat-cores)") +; EXIT: 1 +(set-logic ALL) +(set-option :global-declarations true) +(set-option :produce-difficulty true) +(declare-const _x0 String) +(assert (let ((_let0 (str.suffixof _x0 _x0)))(and (and (not _let0) (= _let0 _let0)) _let0))) +(check-sat) +(get-unsat-core) \ No newline at end of file -- 2.30.2