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.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 0af1d703b6af07733817b71207d8d6bf7e098449..842cf046f285dd216effc6fc469af2ff2b711ed4 100644 (file)
--- 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 9715fc9a7fc431ef89d0c8a04aefdf7de85fad4a..c0e524cde915df0307d053af209f33c4d648fbc8 100644 (file)
--- 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 58a7fb6669f07d830b78cd93a18c266324ff52ea..35724872672439c0437ba56079845a9396680137 100644 (file)
--- 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 55beaed75ea38eae927a87c382a3005c65d219d1..41bf8a482ab59f95dc772336a5c74eb02635b602 100644 (file)
--- 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 8e993d376e05eacd8e58fb106bdd0d9d853fe9f4..12cf15346d461b8f8f657dbcc20578b78d33a3b4 100644 (file)
--- 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 9e8d4703a1e58177e8053ffa533f8df90c44e733..68cdf27806f993ac9a6f6ad0cc66ab16fb4fbded 100644 (file)
--- 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<Node, InstantiationList> 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 ad5918ee8457277c5e440bb4596d8d91d2d7dc41..3e98a01adc15ba4c23d6ba67c934c07b137bb649 100644 (file)
--- 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 (file)
index 0000000..db234dc
--- /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