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

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 3b304c8b9f9568a15b623383db10a2c8f2f9a093..4bc3323e5c982bac2cf59e9bedb972e16899c692 100644 (file)
--- 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 92f31b0b8f95d32569f41544e1e50da7a2aca84b..c93895e79885f9159f3906b3e3fdf7248c23fc12 100644 (file)
--- 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 d2f05337974b0ed04df7821e0d3bb60caef6bcbf..91af2a5b85b13b315557aa3743952ae1e4f5c836 100644 (file)
--- 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 5568dcad0ae22b8af9f86cf9029088279de96509..746bf33bde1134b27195acd08625fa10c13d1fee 100644 (file)
--- 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 4ed2aede97e75e6edb855a893ac62319efccfdf0..0bb386697cdfdd1522e0bccbcf068b424853f029 100644 (file)
--- 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 7ace55c0a149fa3c93cfc3ad9eff91f27b1de662..65682229952ccc83bf35cb63af5b04436abd1962 100644 (file)
--- 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 604f8719c8b7a0329738924494ba4e10cb1e25b4..028bfede56f5c8139b4759dae4f48c325ec51f0c 100644 (file)
--- 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++)

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 12246be419cf84edcd3bb452ee974a8aa1907bf2..ab3b0cfe7adbbcb0241e2e0de91ed9cfc08d997d 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -227,8 +227,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
     d_pfManager.reset(
         new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
   }
-
-  if (options::unsatCores() && !isProofEnabled())
+  else if (options::unsatCores())
   {
     ProofManager::currentPM()->initSatProof(this);
   }

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 8af73140e0c5c28b43d9a49f509f0b6cdc3d70cd..c48df499869fd2d9410026778a1bff4a43f79d13 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -159,7 +159,9 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
     return ClauseIdUndef;
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
-  Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError);
+  // FIXME: to be deleted when we kill old proof code for unsat cores
+  Assert(!options::unsatCores() || options::proofNew()
+         || clause_id != ClauseIdError);
   return clause_id;
 }
 

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5c8922360051729b547ccc5771c310ed852c820b..4649a67aa653e18e81f2019e086110caaedac8f8 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -58,7 +58,8 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
       subsumption_lim(opt_subsumption_lim),
       simp_garbage_frac(opt_simp_garbage_frac),
       use_asymm(opt_use_asymm),
-      use_rcheck(opt_use_rcheck),
+      // make sure this is not enabled if unsat cores or proofs are on
+      use_rcheck(opt_use_rcheck && !options::unsatCores() && !pnm),
       use_elim(options::minisatUseElim() && !enableIncremental),
       merges(0),
       asymm_lits(0),

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eeb879a2bc83c2d7e1347a12479aded59fb01361..81fadb709b38cd2a1f7f33dce2edf25225961234 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -117,7 +117,7 @@ PropEngine::PropEngine(TheoryEngine* te,
     d_ppm.reset(
         new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
   }
-  if (options::unsatCores())
+  else if (options::unsatCores())
   {
     ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
   }

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 23405675afd5e530a830eafe9e13b7c156c4aaa1..7559e4015dbe0c44b24fdfcf61e9c7e175a71c92 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -83,11 +83,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
-  if (options::unsatCores())
+  else if (options::unsatCores())
   {
     ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
   }
-  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
+                        << std::endl;
   explanation.push_back(l);
   if (theoryExplanation.getKind() == kind::AND)
   {

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index ab2c9ae5dfa4b83d0f7a6a977c172ecc86860322..6776b06e28de615f95aef355ac1427cad398a265 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -172,8 +172,8 @@ void Assertions::addFormula(
     }
   }
 
-  // Give it to proof manager
-  if (options::unsatCores())
+  // Give it to the old proof manager
+  if (options::unsatCores() && !isProofEnabled())
   {
     if (inInput)
     {  // n is an input assertion

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 7fd1db7971c0ef5fe5e659724dfc8687c5e2b083..5faa2a66c51182e63f29b8dd2137fbb8da738177 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -207,10 +207,7 @@ bool ProcessAssertions::apply(Assertions& as)
 
   // Since this pass is not robust for the information tracking necessary for
   // unsat cores, it's only applied if we are not doing unsat core computation
-  if (!options::unsatCores())
-  {
-    d_passes["apply-substs"]->apply(&assertions);
-  }
+  d_passes["apply-substs"]->apply(&assertions);
 
   // Assertions MUST BE guaranteed to be rewritten by this point
   d_passes["rewrite"]->apply(&assertions);
@@ -361,15 +358,12 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
 
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
-      if (!options::unsatCores())
+      // Perform non-clausal simplification
+      PreprocessingPassResult res =
+          d_passes["non-clausal-simp"]->apply(&assertions);
+      if (res == PreprocessingPassResult::CONFLICT)
       {
-        // Perform non-clausal simplification
-        PreprocessingPassResult res =
-            d_passes["non-clausal-simp"]->apply(&assertions);
-        if (res == PreprocessingPassResult::CONFLICT)
-        {
-          return false;
-        }
+        return false;
       }
 
       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
@@ -415,8 +409,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
     }
 
     if (options::repeatSimp()
-        && options::simplificationMode() != options::SimplificationMode::NONE
-        && !options::unsatCores())
+        && options::simplificationMode() != options::SimplificationMode::NONE)
     {
       PreprocessingPassResult res =
           d_passes["non-clausal-simp"]->apply(&assertions);

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index a781bc44b3bb48bd6fc6fe716c9c866d37ad914d..3c70d8a57a2489490473f14587c481ff2b12d833 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -484,6 +484,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       throw OptionException("bitblast-aig not supported with unsat cores");
     }
+
+    if (options::doITESimp())
+    {
+      throw OptionException("ITE simp not supported with unsat cores");
+    }
   }
   else
   {

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index fb622452eb091c578148a675303a129b7d2d9611..7592f22c77a1819c3a036afd9ef13c16618818c2 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -683,7 +683,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
 {
   // only if unsat core available
-  if (options::unsatCores())
+  if (options::unsatCores() && !isProofEnabled())
   {
     if (!ProofManager::currentPM()->unsatCoreAvailable())
     {

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 81cca34afa281d475edfdda7667d33b087a0a624..1a46b26f5346ed1c9e68d72c4edce6334b20c71a 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -1026,7 +1026,7 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
                    : NodeManager::currentNM()->mkNode(kind::AND, asserts);
     if( res!=vec_node[i] ){
       res = Rewriter::rewrite( res );
-      if (options::unsatCores())
+      if (options::unsatCores() && !options::proofNew())
       {
         ProofManager::currentPM()->addDependence(res, vec_node[i]);
       }