Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

7 files changed, 4 insertions, 74 deletions

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 7dc2e915d..504dce71e 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -23,7 +23,6 @@
 #include "options/expr_options.h"
 #include "options/language.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 #include "smt/abstract_values.h"
 #include "smt/env.h"
 #include "smt/smt_engine.h"
@@ -193,25 +192,6 @@ void Assertions::addFormula(TNode n,
     }
   }
 
-  // Give it to the old proof manager
-  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    if (inInput)
-    {  // n is an input assertion
-      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
-          || options::checkUnsatCores())
-      {
-        ProofManager::currentPM()->addCoreAssertion(n);
-      }
-    }
-    else
-    {
-      // n is the result of an unknown preprocessing step, add it to dependency
-      // map to null
-      ProofManager::currentPM()->addDependence(n, Node::null());
-    }
-  }
-
   // Add the normalized formula to the queue
   d_assertions.push_back(n, isAssumption, true);
 }
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index be19923af..e7870e4d7 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -104,8 +104,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // set proofs on if not yet set
-  if (options::unsatCores() && !options::produceProofs()
-      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
+  if (options::unsatCores() && !options::produceProofs())
   {
     if (opts.wasSetByUser(options::produceProofs))
     {
@@ -318,7 +317,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // new unsat core specific restrictions for proofs
   if (options::unsatCores()
-      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
@@ -413,12 +411,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.set(options::produceAssertions, true);
   }
 
-  // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
-  // unsat core mode or ASSUMPTIONS, the new default, since other ones are
-  // experimental
+  // whether we want to force safe unsat cores, i.e., if we are in the default
+  // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =
-      options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-      || options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS;
+      options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS;
 
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0e1ff8878..bd38f630d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -33,7 +33,6 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
-#include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
@@ -91,7 +90,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
-      d_proofManager(nullptr),
       d_model(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
@@ -140,15 +138,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // make the quantifier elimination solver
   d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
 
-  // The ProofManager is constructed before any other proof objects such as
-  // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
-  // initialized in TheoryEngine and PropEngine respectively.
-  Assert(d_proofManager == nullptr);
-
-  // d_proofManager must be created before Options has been finished
-  // being parsed from the input file. Because of this, we cannot trust
-  // that d_env->getOption(options::unsatCores) is set correctly yet.
-  d_proofManager.reset(new ProofManager(getUserContext()));
 }
 
 bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
@@ -317,15 +306,6 @@ SmtEngine::~SmtEngine()
     //destroy all passes before destroying things that they refer to
     d_pp->cleanup();
 
-    // d_proofManager is always created when proofs are enabled at configure
-    // time.  Because of this, this code should not be wrapped in PROOF() which
-    // additionally checks flags such as
-    // d_env->getOption(options::produceProofs).
-    //
-    // Note: the proof manager must be destroyed before the theory engine.
-    // Because the destruction of the proofs depends on contexts owned be the
-    // theory solvers.
-    d_proofManager.reset(nullptr);
     d_pfManager.reset(nullptr);
     d_ucManager.reset(nullptr);
 
@@ -1403,12 +1383,6 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
         "Cannot get an unsat core unless immediately preceded by "
         "UNSAT/ENTAILED response.");
   }
-  // use old proof infrastructure
-  if (!d_pfManager)
-  {
-    d_proofManager->traceUnsatCore();  // just to trigger core creation
-    return UnsatCore(d_proofManager->extractUnsatCore());
-  }
   // generate with new proofs
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 924e3c974..b8cd1c3d7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -41,7 +41,6 @@ class TypeNode;
 class Env;
 class NodeManager;
 class TheoryEngine;
-class ProofManager;
 class UnsatCore;
 class LogicRequest;
 class StatisticsRegistry;
@@ -99,7 +98,6 @@ class SmtScope;
 class PfManager;
 class UnsatCoreManager;
 
-ProofManager* currentProofManager();
 }  // namespace smt
 
 /* -------------------------------------------------------------------------- */
@@ -858,12 +856,6 @@ class CVC5_EXPORT SmtEngine
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
   prop::PropEngine* getPropEngine();
 
-  /**
-   * Get a pointer to the ProofManager owned by this SmtEngine.
-   * TODO (project #37): this is the old proof manager and will be deleted
-   */
-  ProofManager* getProofManager() { return d_proofManager.get(); };
-
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager() const;
 
@@ -1076,8 +1068,6 @@ class CVC5_EXPORT SmtEngine
   /** The SMT solver */
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
-  /** The (old) proof manager TODO (project #37): delete this */
-  std::unique_ptr<ProofManager> d_proofManager;
   /**
    * The SMT-level model object, which contains information about how to
    * print the model, as well as a pointer to the underlying TheoryModel
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 962529924..98f4c8d70 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -35,11 +35,6 @@ SmtEngine* currentSmtEngine() {
 
 bool smtEngineInScope() { return s_smtEngine_current != NULL; }
 
-ProofManager* currentProofManager() {
-  Assert(s_smtEngine_current != NULL);
-  return s_smtEngine_current->getProofManager();
-}
-
 ResourceManager* currentResourceManager()
 {
   return s_smtEngine_current->getResourceManager();
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 76bc5c641..cc231fa3c 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -27,7 +27,6 @@
 
 namespace cvc5 {
 
-class ProofManager;
 class SmtEngine;
 class StatisticsRegistry;
 
@@ -36,9 +35,6 @@ namespace smt {
 SmtEngine* currentSmtEngine();
 bool smtEngineInScope();
 
-// FIXME: Maybe move into SmtScope?
-ProofManager* currentProofManager();
-
 /** get the current resource manager */
 ResourceManager* currentResourceManager();
 
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 34ef53194..eaf5cf82f 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -23,7 +23,6 @@
 #include "expr/term_context_stack.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 
 using namespace std;