diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-29 13:27:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-29 13:27:44 -0600 |
| commit | ce1b2f2fb06150599c231bf0d59b52a07e74c3f5 (patch) | |
| tree | 53fee982175e433e70ca5abe60a81b763c42f81f /src/smt/expand_definitions.cpp | |
| parent | 145b99d771e182fba70402398702ed12e3303682 (diff) | |
(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)
This is work towards resolving two kinds of failures on proof-new:
(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.
A followup PR will simplify and fix proofs for theory-preprocessing.
Diffstat (limited to 'src/smt/expand_definitions.cpp')
| -rw-r--r-- | src/smt/expand_definitions.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 4f49e1bbe..c2c4b6fd2 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -99,7 +99,7 @@ TrustNode ExpandDefs::expandDefinitions( // ------- ASSUME // n = f Node conc = n.eqNode(f); - tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}); + tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true); } // must recursively expand its definition TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg); @@ -236,7 +236,8 @@ TrustNode ExpandDefs::expandDefinitions( instance, PfRule::MACRO_SR_PRED_INTRO, pfExpChildren, - {conc}); + {conc}, + true); } } // now, call expand definitions again on the result @@ -260,7 +261,7 @@ TrustNode ExpandDefs::expandDefinitions( if (tpg != nullptr) { tpg->addRewriteStep( - n, node, trn.getGenerator(), PfRule::THEORY_EXPAND_DEF); + n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF); } } else |