diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-16 09:36:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-16 14:36:40 +0000 |
commit | 6203bcb456d5450770c8ac6cdb775ec0f73e0325 (patch) | |
tree | b04a994369496c67e176acd15143d2ed09235fb6 /src/expr | |
parent | 87bc1447d59e36410feab768ea2bbb577e58fb7b (diff) |
Fix ONCE for post-rewrite (#6372)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 22e1309d2..2233dcc7b 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -533,6 +533,16 @@ Node TConvProofGenerator::getProofForRewriting(Node t, } else { + // If we changed due to congruence, and then rewrote, then we + // require a trans step to connect here + if (!rret.isNull() && childChanged) + { + std::vector<Node> pfChildren; + pfChildren.push_back(cur.eqNode(ret)); + pfChildren.push_back(ret.eqNode(rret)); + Node result = cur.eqNode(rret); + pf.addStep(result, PfRule::TRANS, pfChildren, {}); + } // take its rewrite if it rewrote and we have ONCE rewriting policy ret = rret.isNull() ? ret : rret; Trace("tconv-pf-gen-rewrite") |