From 9b099b715cec0dc60048fdc64b4d61b977d14096 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Dec 2020 10:50:49 -0600 Subject: (proof-new) Minor updates to term conversion proof generator (#5691) Minor updates to term conversion proof generator --- src/expr/term_conversion_proof_generator.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 858ca9f64..d351d88b6 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -84,7 +84,6 @@ void TConvProofGenerator::addRewriteStep(Node t, Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { - AlwaysAssert(ps.d_rule != PfRule::ASSUME); d_proof.addStep(eq, ps); } } @@ -99,7 +98,6 @@ void TConvProofGenerator::addRewriteStep(Node t, Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { - AlwaysAssert(id != PfRule::ASSUME); d_proof.addStep(eq, id, children, args); } } @@ -180,16 +178,21 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) Node conc = getProofForRewriting(f[0], lpf, d_tcontext); if (conc != f) { + bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug"); Assert(conc.getKind() == EQUAL && conc[0] == f[0]); std::stringstream serr; serr << "TConvProofGenerator::getProofFor: " << toStringDebug() - << ": failed, mismatch (see -t tconv-pf-gen-debug for details)" - << std::endl; + << ": failed, mismatch"; + if (!debugTraceEnabled) + { + serr << " (see -t tconv-pf-gen-debug for details)"; + } + serr << std::endl; serr << " source: " << f[0] << std::endl; serr << "expected after rewriting: " << f[1] << std::endl; serr << " actual after rewriting: " << conc[1] << std::endl; - if (Trace.isOn("tconv-pf-gen-debug")) + if (debugTraceEnabled) { Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl; serr << "Rewrite steps: " << std::endl; -- cgit v1.2.3