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 23377cb0c8dc7716ab156c03a5522b96712603a3..5903c1606a4670a96ff04bf72b90ded34ebbc375 100644 (file)
--- 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 43f91f73289adfe57bef2879cb6e1e018922ff1f..090b44b90f068aa077322503248b791c244dd654 100644 (file)
--- 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());