[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.

1 files changed, 49 insertions, 9 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 0a8819c4b..cf5fc267b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -70,13 +70,36 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl;
     options::dumpUnsatCores.set(true);
   }
-  if (options::checkUnsatCores() || options::checkUnsatCoresNew()
-      || options::dumpUnsatCores() || options::unsatAssumptions())
+  if ((options::unsatCores() && options::unsatCoresNew())
+      || (options::checkUnsatCores() && options::checkUnsatCoresNew()))
+  {
+    AlwaysAssert(false) << "Can't have both unsat cores modes, pick one.\n";
+  }
+  if (options::checkUnsatCores())
   {
-    Notice() << "SmtEngine: setting unsatCores" << std::endl;
     options::unsatCores.set(true);
   }
-  if (options::checkProofs() || options::checkUnsatCoresNew()
+  if (options::checkUnsatCoresNew())
+  {
+    options::unsatCoresNew.set(true);
+  }
+  if (options::dumpUnsatCores() || options::unsatAssumptions())
+  {
+    if (!options::unsatCoresNew())
+    {
+      Notice() << "SmtEngine: setting unsatCores" << std::endl;
+      options::unsatCores.set(true);
+    }
+  }
+  if (options::unsatCoresNew()
+      && ((options::produceProofs() && options::produceProofs.wasSetByUser())
+          || (options::checkProofs() && options::checkProofs.wasSetByUser())
+          || (options::dumpProofs() && options::dumpProofs.wasSetByUser())))
+  {
+    AlwaysAssert(false) << "Can't properly produce proofs and have the new "
+                           "unsat cores simultaneously.\n";
+  }
+  if (options::checkProofs() || options::unsatCoresNew()
       || options::dumpProofs())
   {
     Notice() << "SmtEngine: setting proof" << std::endl;
@@ -278,11 +301,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   // !!! must disable proofs if using the old unsat core infrastructure
   // TODO (#project 37) remove this
-  if (options::unsatCores() && !options::checkUnsatCoresNew())
+  if (options::unsatCores())
   {
     disableProofs = true;
   }
 
+  // new unsat core specific restrictions for proofs
+  if (options::unsatCoresNew())
+  {
+    // no fine-graininess
+    if (!options::proofGranularityMode.wasSetByUser())
+    {
+      options::proofGranularityMode.set(options::ProofGranularityMode::OFF);
+    }
+  }
+
   if (options::arraysExp())
   {
     if (!logic.isQuantified())
@@ -335,6 +368,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // if we requiring disabling proofs, disable them now
   if (disableProofs && options::produceProofs())
   {
+    if (options::unsatCoresNew())
+    {
+      Notice() << "SmtEngine: turning off new unsat cores." << std::endl;
+    }
+    options::unsatCoresNew.set(false);
+    options::checkUnsatCoresNew.set(false);
     if (options::produceProofs())
     {
       Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
@@ -366,7 +405,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
   // with arithmetic, force the option off.
-  if (options::incrementalSolving() || options::unsatCores())
+  if (options::incrementalSolving() || options::unsatCores()
+      || options::unsatCoresNew())
   {
     if (options::unconstrainedSimp())
     {
@@ -428,7 +468,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // Disable options incompatible with unsat cores or output an error if enabled
   // explicitly
-  if (options::unsatCores())
+  if (options::unsatCores() || options::unsatCoresNew())
   {
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
@@ -707,7 +747,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
                        && !options::incrementalSolving()
-                       && !options::unsatCores();
+                       && !options::unsatCores() && !options::unsatCoresNew();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
     options::ufSymmetryBreaker.set(qf_uf_noinc);
@@ -756,7 +796,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
                           && logic.isTheoryEnabled(THEORY_UF)
                           && logic.isTheoryEnabled(THEORY_BV))
-                      && !options::unsatCores();
+                      && !options::unsatCores() && !options::unsatCoresNew();
     Trace("smt") << "setting repeat simplification to " << repeatSimp
                  << std::endl;
     options::repeatSimp.set(repeatSimp);