From 4a5cc46097fa1c7b601d4275f0cf0c5af9c3d97e Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 5 Nov 2021 14:45:00 -0300 Subject: [PATCH] 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. --- src/theory/booleans/circuit_propagator.cpp | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) 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 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; } } } -- 2.30.2