From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 4 May 2021 18:36:41 +0000 (-0300)
Subject: Do not use proof CNF stream with assumptions-based cores (#6488)
X-Git-Tag: cvc5-1.0.0~1795
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5018442120cb22e6f1923a97df7cd98c2d2b5a4a;p=cvc5.git

Do not use proof CNF stream with assumptions-based cores (#6488)

Previously using proof CNF stream together with assumptions-based unsat cores added unnecessary performance overhead.

Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
---

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 23377cb0c..5903c1606 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -111,11 +111,17 @@ PropEngine::PropEngine(TheoryEngine* te,
   // connect theory proxy
   d_theoryProxy->finishInit(d_cnfStream);
   // connect SAT solver
-  d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
+  d_satSolver->initialize(
+      d_context,
+      d_theoryProxy,
+      userContext,
+      options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
+          ? pnm
+          : nullptr);
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
-  if (pnm)
+  if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
   {
     d_pfCnfStream.reset(new ProofCnfStream(
         userContext,
@@ -261,21 +267,23 @@ void PropEngine::assertInternal(
     TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
 {
   // Assert as (possibly) removable
-  if (isProofEnabled())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
   {
-    if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS
-        && input)
+    if (input)
     {
       Assert(!negated);
-      d_pfCnfStream->ensureLiteral(node);
+      d_cnfStream->ensureLiteral(node);
       d_assumptions.push_back(node);
     }
     else
     {
-      d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+      d_cnfStream->convertAndAssert(node, removable, negated, input);
     }
-
-    // if input, register the assertion
+  }
+  else if (isProofEnabled())
+  {
+    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    // if input, register the assertion in the proof manager
     if (input)
     {
       d_ppm->registerAssertion(node);
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 43f91f732..090b44b90 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -98,7 +98,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (options::produceProofs())
+  if (options::produceProofs()
+      && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
   {
     Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
            || tte.getGenerator());