diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 11:41:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-12 09:41:26 -0700 |
| commit | 9d1ce085de6df543d9d9a2fa9b8fa9001feb4b6b (patch) | |
| tree | 023474f131ee9f21e829fc623e31de808b9235d5 /src/expr/proof_rule.cpp | |
| parent | 3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed (diff) | |
(proof-new) Witness form proof generator (#4782)
This class is responsible for the connection between terms and their witness form in the final proof.
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 7844dfccb..9713adbec 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::WITNESS_AXIOM: return "WITNESS_AXIOM"; case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; |