From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 5 Nov 2021 17:45:00 +0000 (-0300)
Subject: Minor changes to circuit propagator (#7584)
X-Git-Tag: cvc5-1.0.0~882
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a5cc46097fa1c7b601d4275f0cf0c5af9c3d97e;p=cvc5.git

Minor changes to circuit propagator (#7584)

Previously in a given part of the code a proof would be retrieved only so that it'd be printed. This commit guards that part of the code with whether the trace is on and gives more information in what is printed.

Also changes the style of a call.
---

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 741d35e9d..714dcfb01 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -87,14 +87,9 @@ void CircuitPropagator::assertTrue(TNode assertion)
     // Analyze the assertion for back-edges and all that
     computeBackEdges(assertion);
     // Assign the given assertion to true
-    if (isProofEnabled())
-    {
-      assignAndEnqueue(assertion, true, d_pnm->mkAssume(assertion));
-    }
-    else
-    {
-      assignAndEnqueue(assertion, true, nullptr);
-    }
+    assignAndEnqueue(assertion,
+                     true,
+                     isProofEnabled() ? d_pnm->mkAssume(assertion) : nullptr);
   }
 }
 
@@ -805,11 +800,11 @@ void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
                             << "\t" << *pf << std::endl;
       d_epg->setProofFor(f, std::move(pf));
     }
-    else
+    else if (Trace.isOn("circuit-prop"))
     {
       auto prf = d_epg->getProofFor(f);
-      Trace("circuit-prop") << "Ignoring proof, we already have" << std::endl
-                            << "\t" << *prf << std::endl;
+      Trace("circuit-prop") << "Ignoring proof\n\t" << *pf
+                            << "\nwe already have\n\t" << *prf << std::endl;
     }
   }
 }