diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-02 08:48:56 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-02 08:48:56 -0500 |
| commit | e4aa0f1c1a025496a42b78488190eb78f6de4d5c (patch) | |
| tree | 832eaadaddbadc9d7eaab52a36f470f5f1c24ca2 | |
| parent | 3823bf3fbf981ee53990a21b49016fd00073b2bd (diff) | |
Add missing Boolean rules to LFSC printer
| -rw-r--r-- | src/proof/lfsc/lfsc_printer.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 69cc79399..d25543238 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -514,11 +514,12 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, case PfRule::FACTORING: pf << h << h << cs[0]; break; // Boolean case PfRule::SPLIT: pf << as[0]; break; + case PfRule::NOT_NOT_ELIM: pf << h << cs[0]; break; case PfRule::CONTRA: pf << h << cs[0] << cs[1]; break; case PfRule::MODUS_PONENS: case PfRule::EQ_RESOLVE: pf << h << h << cs[0] << cs[1]; break; case PfRule::NOT_AND: pf << h << h << cs[0]; break; - // case PfRule::NOT_OR_ELIM: pf << h << h << + case PfRule::NOT_OR_ELIM: case PfRule::AND_ELIM: pf << h << h << args[0] << cs[0]; break; case PfRule::IMPLIES_ELIM: case PfRule::NOT_IMPLIES_ELIM1: |