diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-02 09:41:31 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-02 09:41:31 -0600 |
| commit | 5151238c98492fe332a2603c05752f3319ae8035 (patch) | |
| tree | fd4310fa51ccc59983d9d2d9adb9ed491ab0642c /src/expr | |
| parent | 901cea314c4dc3be411c345e42c858063fe5aa1b (diff) | |
(proof-new) Proofs for expand definitions (#5562)
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.cpp | 1 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 3 |
2 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 4ba483101..885c36131 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -40,6 +40,7 @@ const char* toString(PfRule id) case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; + case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; case PfRule::TRUST_SUBS: return "TRUST_SUBS"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 58dfd973c..f00ef8367 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -231,6 +231,9 @@ enum class PfRule : uint32_t THEORY_PREPROCESS, // where F was added as a new assertion by theory preprocessing. THEORY_PREPROCESS_LEMMA, + // where F is an equality of the form t = t' where t was replaced by t' + // based on theory expand definitions. + THEORY_EXPAND_DEF, // where F is an existential (exists ((x T)) (P x)) used for introducing // a witness term (witness ((x T)) (P x)). WITNESS_AXIOM, |