diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-16 00:05:10 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 00:05:10 -0300 |
| commit | f58e7e32d99b9fda841ebfd0c29016c41a109bfe (patch) | |
| tree | 7279fc3cc22fcbebaa0356df81e2880cefdaee2d /src/expr/proof_rule.cpp | |
| parent | 8a126d59141d2889e3b10b07ece4b10f48511a71 (diff) | |
[proof-new] Resolution rules and checkers (#5070)
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 1d46b183f..57dd3e0bd 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -42,6 +42,10 @@ const char* toString(PfRule id) case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; //================================================= Boolean rules + case PfRule::RESOLUTION: return "RESOLUTION"; + case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; + case PfRule::FACTORING: return "FACTORING"; + case PfRule::REORDERING: return "REORDERING"; case PfRule::SPLIT: return "SPLIT"; case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; case PfRule::AND_ELIM: return "AND_ELIM"; |