diff options
Diffstat (limited to 'src/theory/strings/infer_proof_cons.cpp')
| -rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 5eba8663a..5090b15cb 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -217,18 +217,35 @@ void InferProofCons::convert(InferenceId infer, Node src = ps.d_children[ps.d_children.size() - 1]; std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1); // start with a default rewrite + Trace("strings-ipc-core") + << "Generate proof for STRINGS_EXTF_EQ_REW, starting with " << src + << std::endl; Node mainEqSRew = psb.applyPredElim(src, expe); + Trace("strings-ipc-core") + << "...after pred elim: " << mainEqSRew << std::endl; if (mainEqSRew == conc) { + Trace("strings-ipc-core") << "...success" << std::endl; useBuffer = true; break; } + else if (mainEqSRew.getKind() != EQUAL) + { + // Note this can happen in rare cases where substitution+rewriting + // is more powerful than congruence+rewriting. We fail to reconstruct + // the proof in this case. + Trace("strings-ipc-core") + << "...failed, not equality after rewriting" << std::endl; + break; + } // may need the "extended equality rewrite" Node mainEqSRew2 = psb.applyPredElim(mainEqSRew, {}, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, MethodId::RW_REWRITE_EQ_EXT); + Trace("strings-ipc-core") + << "...after extended equality rewrite: " << mainEqSRew2 << std::endl; if (mainEqSRew2 == conc) { useBuffer = true; |