diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-15 19:04:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-15 19:04:29 -0500 |
| commit | df98bc96168869e1615bc0756bde3b2c5dba160e (patch) | |
| tree | d6f1d3bfcae647b3ed3c6d9a657db847f010ebf6 /src/expr/proof_rule.cpp | |
| parent | e5f51e82aceda35642acd92b417bfeb74edfdcdd (diff) | |
(proof-new) Add quantifiers proof checker (#4593)
Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.
This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 595e1d5f7..339b4f582 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,15 +31,6 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; - //================================================= Equality rules - case PfRule::REFL: return "REFL"; - case PfRule::SYMM: return "SYMM"; - case PfRule::TRANS: return "TRANS"; - case PfRule::CONG: return "CONG"; - case PfRule::TRUE_INTRO: return "TRUE_INTRO"; - case PfRule::TRUE_ELIM: return "TRUE_ELIM"; - case PfRule::FALSE_INTRO: return "FALSE_INTRO"; - case PfRule::FALSE_ELIM: return "FALSE_ELIM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; case PfRule::AND_ELIM: return "AND_ELIM"; @@ -85,6 +76,20 @@ const char* toString(PfRule id) case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; + //================================================= Equality rules + case PfRule::REFL: return "REFL"; + case PfRule::SYMM: return "SYMM"; + case PfRule::TRANS: return "TRANS"; + case PfRule::CONG: return "CONG"; + case PfRule::TRUE_INTRO: return "TRUE_INTRO"; + case PfRule::TRUE_ELIM: return "TRUE_ELIM"; + case PfRule::FALSE_INTRO: return "FALSE_INTRO"; + case PfRule::FALSE_ELIM: return "FALSE_ELIM"; + //================================================= Quantifiers rules + case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; + case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; + case PfRule::SKOLEMIZE: return "SKOLEMIZE"; + case PfRule::INSTANTIATE: return "INSTANTIATE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; |