[proof-new] Only use old proofs for unsat cores if no proof new (#5725)

Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.

This also does some minor refactoring in some preprocessing. No behavior is changed.

7 files changed, 33 insertions, 65 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 3b304c8b9..4bc3323e5 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -96,19 +96,19 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
   }
   Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
                            << n << std::endl;
-  if (options::unsatCores())
-  {
-    ProofManager::currentPM()->addDependence(n, d_nodes[i]);
-  }
   if (isProofEnabled())
   {
     d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
   }
+  else if (options::unsatCores())
+  {
+    ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+  }
   d_nodes[i] = n;
 }
 
 void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
-{  
+{
   if (trn.isNull())
   {
     // null trust node denotes no change, nothing to do
@@ -201,7 +201,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       d_pppg->notifyNewAssert(newConjr, lcp);
     }
   }
-  if (options::unsatCores())
+  if (options::unsatCores() && !isProofEnabled())
   {
     ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
   }
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 92f31b0b8..c93895e79 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -33,32 +33,28 @@ ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult ApplySubsts::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  if (!options::unsatCores())
-  {
-    Chat() << "applying substitutions..." << std::endl;
-    Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
-                      << "applying substitutions" << std::endl;
-    // TODO(#1255): Substitutions in incremental mode should be managed with a
-    // proper data structure.
+  Chat() << "applying substitutions..." << std::endl;
+  Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+                        << "applying substitutions" << std::endl;
+  // TODO(#1255): Substitutions in incremental mode should be managed with a
+  // proper data structure.
 
-    theory::TrustSubstitutionMap& tlsm =
-        d_preprocContext->getTopLevelSubstitutions();
-    unsigned size = assertionsToPreprocess->size();
-    for (unsigned i = 0; i < size; ++i)
+  theory::TrustSubstitutionMap& tlsm =
+      d_preprocContext->getTopLevelSubstitutions();
+  unsigned size = assertionsToPreprocess->size();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (assertionsToPreprocess->isSubstsIndex(i))
     {
-      if (assertionsToPreprocess->isSubstsIndex(i))
-      {
-        continue;
-      }
-      Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
-                        << std::endl;
-      d_preprocContext->spendResource(
-          ResourceManager::Resource::PreprocessStep);
-      assertionsToPreprocess->replaceTrusted(
-          i, tlsm.apply((*assertionsToPreprocess)[i]));
-      Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
-                        << std::endl;
+      continue;
     }
+    Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
+                          << std::endl;
+    d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+    assertionsToPreprocess->replaceTrusted(
+        i, tlsm.apply((*assertionsToPreprocess)[i]));
+    Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
+                          << std::endl;
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index d2f053379..91af2a5b8 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -50,7 +50,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
       // process
       assertions->replaceTrusted(i, trn);
       // rewritten assertion has a dependence on the node (old pf architecture)
-      if (options::unsatCores())
+      if (options::unsatCores() && !options::proofNew())
       {
         ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
       }
@@ -61,7 +61,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
       imap[newSkolems[j]] = assertions->size();
       assertions->pushBackTrusted(newAsserts[j]);
       // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCores())
+      if (options::unsatCores() && !options::proofNew())
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 5568dcad0..746bf33bd 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -114,13 +114,7 @@ ITESimp::Statistics::~Statistics()
 
 bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 {
-  // This pass does not support dependency tracking yet
-  // (learns substitutions from all assertions so just
-  // adding addDependence is not enough)
-  if (options::unsatCores())
-  {
-    return true;
-  }
+  Assert(!options::unsatCores());
   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 4ed2aede9..0bb386697 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -180,6 +180,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          == assertionsToPreprocess->size());
   Assert(!options::incrementalSolving());
+  Assert(!options::unsatCores());
 
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
@@ -527,10 +528,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
 
               Node n = Rewriter::rewrite(geq.andNode(leq));
               assertionsToPreprocess->push_back(n);
-              if (options::unsatCores())
-              {
-                ProofManager::currentPM()->addDependence(n, Node::null());
-              }
               TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
               CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get();
               Theory::PPAssertStatus status CVC4_UNUSED;  // just for assertions
@@ -599,11 +596,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           Debug("miplib") << "  " << newAssertion << endl;
 
           assertionsToPreprocess->push_back(newAssertion);
-          if (options::unsatCores())
-          {
-            ProofManager::currentPM()->addDependence(newAssertion,
-                                                     Node::null());
-          }
           Debug("miplib") << "  assertions to remove: " << endl;
           for (vector<TNode>::const_iterator k = asserts[pos_var].begin(),
                                              k_end = asserts[pos_var].end();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 7ace55c0a..656822299 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -66,7 +66,8 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult NonClausalSimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(!options::unsatCores());
+  Assert(!options::unsatCores() || isProofEnabled())
+      << "Unsat cores with non-clausal simp only supported with new proofs";
 
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
@@ -111,13 +112,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
     // If in conflict, just return false
     Trace("non-clausal-simplify")
         << "conflict in non-clausal propagation" << std::endl;
-    Assert(!options::unsatCores());
     assertionsToPreprocess->clear();
     assertionsToPreprocess->pushBackTrusted(conf);
-    if (options::unsatCores())
-    {
-      ProofManager::currentPM()->addDependence(conf.getNode(), Node::null());
-    }
     propagator->setNeedsFinish(true);
     return PreprocessingPassResult::CONFLICT;
   }
@@ -177,14 +173,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         // If the learned literal simplifies to false, we're in conflict
         Trace("non-clausal-simplify")
             << "conflict with " << learned_literals[i].getNode() << std::endl;
-        Assert(!options::unsatCores());
         assertionsToPreprocess->clear();
         Node n = NodeManager::currentNM()->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
-        if (options::unsatCores())
-        {
-          ProofManager::currentPM()->addDependence(n, Node::null());
-        }
         propagator->setNeedsFinish(true);
         return PreprocessingPassResult::CONFLICT;
       }
@@ -216,14 +207,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         // If in conflict, we return false
         Trace("non-clausal-simplify")
             << "conflict while solving " << learnedLiteral << std::endl;
-        Assert(!options::unsatCores());
         assertionsToPreprocess->clear();
         Node n = NodeManager::currentNM()->mkConst<bool>(false);
         assertionsToPreprocess->push_back(n);
-        if (options::unsatCores())
-        {
-          ProofManager::currentPM()->addDependence(n, Node::null());
-        }
         propagator->setNeedsFinish(true);
         return PreprocessingPassResult::CONFLICT;
       }
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 604f8719c..028bfede5 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -80,7 +80,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
     for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
-        if (options::unsatCores()
+        if (options::unsatCores() && !options::proofNew()
             && std::find(macro_assertions.begin(),
                          macro_assertions.end(),
                          assertions[i])
@@ -106,7 +106,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
           // is an over-approximation. a more fine-grained unsat core
           // computation would require caching dependencies for each subterm of
           // the formula, which is expensive.
-          if (options::unsatCores())
+          if (options::unsatCores() && !options::proofNew())
           {
             ProofManager::currentPM()->addDependence(curr, assertions[i]);
             for (unsigned j = 0; j < macro_assertions.size(); j++)