diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-17 10:50:49 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-17 17:50:49 +0100 |
| commit | 9b099b715cec0dc60048fdc64b4d61b977d14096 (patch) | |
| tree | d342bef4833946288c427a4d3d1c05b7df2a518f | |
| parent | db157ade422c4bc16750d2cb6db7643f1fd3dad6 (diff) | |
(proof-new) Minor updates to term conversion proof generator (#5691)
Minor updates to term conversion proof generator
| -rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 13 |
1 files 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<ProofNode> 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; |