Remove old unsat cores (#6581)

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

6 files changed, 0 insertions, 23 deletions

diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 8c97aabc7..44dafefcb 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -21,7 +21,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 2b25098af..dc47c9c8e 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -21,7 +21,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
@@ -61,12 +60,6 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
     {
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
-      // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
-                                                 assertion);
-      }
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index f2724932f..e0a57ae5b 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -115,7 +115,6 @@ ITESimp::Statistics::Statistics()
 
 bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
   bool result = true;
   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
   if (simpDidALotOfWork)
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index fe515ed59..f27ff836a 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -188,7 +188,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          == assertionsToPreprocess->size());
   Assert(!options::incrementalSolving());
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
 
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index d88e901d7..921442f0e 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -69,12 +69,6 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult NonClausalSimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
-         || isProofEnabled())
-      << "Unsat cores with non-clausal simp only supported with new proofs. "
-         "Cores mode is "
-      << options::unsatCoresMode() << "\n";
-
   d_preprocContext->spendResource(Resource::PreprocessStep);
 
   theory::booleans::CircuitPropagator* propagator =
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 90a4b8240..1eb21cd96 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -20,7 +20,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -58,12 +57,6 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
     {
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
-      // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
-                                                 assertion);
-      }
     }
   }