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 741d35e9d89d081a11ccaf1cc0b59ac612606d57..714dcfb01d721ceaafdd551c5544ea370616dc63 100644 (file)
--- 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;
     }
   }
 }