diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-27 15:33:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-27 13:33:12 -0700 |
| commit | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (patch) | |
| tree | 4e7f89713008787557ae1293c6d0149e185c9b66 /src/expr | |
| parent | faa97a6f1ee19760dfb0a79ad18c53afdff6b09a (diff) | |
(proof-new) Proof production for term formula removal (#4687)
This adds proof support in the term formula removal pass.
It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.cpp | 1 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index c51bfb3c7..7844dfccb 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -33,6 +33,7 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; case PfRule::PREPROCESS: return "PREPROCESS"; + case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index c76e907c7..62bc77cfb 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -183,6 +183,13 @@ enum class PfRule : uint32_t // based on some preprocessing pass, or otherwise F was added as a new // assertion by some preprocessing pass. PREPROCESS, + // ======== Remove Term Formulas Axiom + // Children: none + // Arguments: (t) + // --------------------------------------------------------------- + // Conclusion: RemoveTermFormulas::getAxiomFor(t). + REMOVE_TERM_FORMULA_AXIOM, + //================================================= Boolean rules // ======== Split // Children: none |