[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.

7 files changed, 101 insertions, 26 deletions

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index d873f31bb..aee7a2a86 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -178,7 +178,7 @@ void Assertions::addFormula(
   }
 
   // Give it to the old proof manager
-  if (options::unsatCores() && !isProofEnabled())
+  if (options::unsatCores())
   {
     if (inInput)
     {  // n is an input assertion
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index b06590918..f6c489055 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -131,9 +131,10 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
 
   Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
 
-  // Now make the final scope, which ensures that the only open leaves
-  // of the proof are the assertions.
-  d_finalProof = d_pnm->mkScope(pfn, assertions);
+  // Now make the final scope, which ensures that the only open leaves of the
+  // proof are the assertions, unless we are doing proofs to generate unsat
+  // cores, in which case we do not care.
+  d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCoresNew());
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 0345991d2..253dbecaf 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -38,6 +38,24 @@ class ProofPostproccess;
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
  * well as setting up the global proof checker and proof node manager.
+ *
+ * The proof production of an SmtEngine is directly impacted by whether, and
+ * how, we are producing unsat cores:
+ *
+ * - If we are producing unsat cores using the old proof infrastructure, then
+ *   SmtEngine will not have proofs in the sense of this proof manager.
+ *
+ * - If we are producing unsat cores using this proof infrastructure, then the
+ *   SmtEngine will have proofs using this proof manager (if --produce-proofs
+ *   was not passed by the user it will be activated), but these proofs will
+ *   only cover preprocessing and the prop engine, i.e., the theory engine will
+ *   not have proofs.
+ *
+ * - If we are not producing unsat cores then the SmtEngine will have proofs as
+ *   long as --produce-proofs was given.
+ *
+ * - If SmtEngine has been configured in a way that is incompatible with proofs
+ *   then unsat core production will be disabled.
  */
 class PfManager
 {
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);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3eedfdf53..3d38ba37b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -236,7 +236,10 @@ void SmtEngine::finishInit()
   }
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
-  d_smtSolver->finishInit(logic);
+  // if proofs and unsat cores, proofs are used solely for unsat core
+  // production, so we don't generate proofs in the theory engine, which is
+  // communicated via the second argument
+  d_smtSolver->finishInit(logic, options::unsatCoresNew());
 
   // now can construct the SMT-level model object
   TheoryEngine* te = d_smtSolver->getTheoryEngine();
@@ -1408,10 +1411,11 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!options::unsatCores())
+  if (!options::unsatCores() && !options::unsatCoresNew())
   {
     throw ModalException(
-        "Cannot get an unsat core when produce-unsat-cores option is off.");
+        "Cannot get an unsat core when produce-unsat-cores[-new] option is "
+        "off.");
   }
   if (d_state->getMode() != SmtMode::UNSAT)
   {
@@ -1437,7 +1441,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(options::unsatCores())
+  Assert(options::unsatCores() || options::unsatCoresNew())
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1449,7 +1453,10 @@ void SmtEngine::checkUnsatCore() {
   coreChecker->getOptions().set(options::checkUnsatCores, false);
   // disable all proof options
   coreChecker->getOptions().set(options::produceProofs, false);
+  coreChecker->getOptions().set(options::checkProofs, false);
   coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
+  coreChecker->getOptions().set(options::proofEagerChecking, false);
+
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;
   if (getSepHeapTypes(sepLocType, sepDataType))
@@ -1633,7 +1640,8 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::produceProofs() && getSmtMode() == SmtMode::UNSAT)
+  if (options::produceProofs() && !options::unsatCoresNew()
+      && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
     getRelevantInstantiationTermVectors(insts);
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ceec0619b..2847e5ee9 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -49,16 +49,18 @@ SmtSolver::SmtSolver(SmtEngine& smt,
 
 SmtSolver::~SmtSolver() {}
 
-void SmtSolver::finishInit(const LogicInfo& logicInfo)
+void SmtSolver::finishInit(const LogicInfo& logicInfo,
+                           bool proofForUnsatCoreMode)
 {
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
-                                        d_smt.getUserContext(),
-                                        d_rm,
-                                        logicInfo,
-                                        d_smt.getOutputManager(),
-                                        d_pnm));
+  d_theoryEngine.reset(
+      new TheoryEngine(d_smt.getContext(),
+                       d_smt.getUserContext(),
+                       d_rm,
+                       logicInfo,
+                       d_smt.getOutputManager(),
+                       proofForUnsatCoreMode ? nullptr : d_pnm));
 
   // Add the theories
   for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index e4493eedf..ae1cc2e40 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -71,8 +71,13 @@ class SmtSolver
   ~SmtSolver();
   /**
    * Create theory engine, prop engine based on the logic info.
+   *
+   * @param logicInfo the logic information
+   * @param proofForUnsatCoreMode whether this SmtSolver will operate in unsat
+   * core mode. If true, proofs will not be produced in the theory engine.
    */
-  void finishInit(const LogicInfo& logicInfo);
+  void finishInit(const LogicInfo& logicInfo,
+                  bool proofForUnsatCoreMode = false);
   /** Reset all assertions, global declarations, etc.  */
   void resetAssertions();
   /**
@@ -129,6 +134,7 @@ class SmtSolver
   /** Get a pointer to the preprocessor */
   Preprocessor* getPreprocessor();
   //------------------------------------------ end access methods
+
  private:
   /** Reference to the parent SMT engine */
   SmtEngine& d_smt;