diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-26 07:14:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-26 14:14:01 +0000 |
commit | a05f07c298692ced47c73918876b173bc0fc431d (patch) | |
tree | 30a00ad61e8d914457ebe8d82172e9e5f4df8d6e | |
parent | 8995119775293b5b3e618701d2e4e318f18e5fed (diff) |
[proofs] Alethe: Translate Block of clause pattern rule (#7406)
Implementation of the translation of a number of rules that follow the clause pattern into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 8060eb697..119972863 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -993,6 +993,182 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + // ======== Not Or elimination + // This rule is translated according to the singleton pattern. + case PfRule::NOT_OR_ELIM: + { + return addAletheStep(AletheRule::NOT_OR, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + {}, + *cdp); + } + // ======== Implication elimination + // This rule is translated according to the clause pattern. + case PfRule::IMPLIES_ELIM: + { + return addAletheStepFromOr(AletheRule::IMPLIES, res, children, {}, *cdp); + } + // ======== Not Implication elimination version 1 + // This rule is translated according to the singleton pattern. + case PfRule::NOT_IMPLIES_ELIM1: + { + return addAletheStep(AletheRule::NOT_IMPLIES1, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + {}, + *cdp); + } + // ======== Not Implication elimination version 2 + // This rule is translated according to the singleton pattern. + case PfRule::NOT_IMPLIES_ELIM2: + { + return addAletheStep(AletheRule::NOT_IMPLIES2, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + {}, + *cdp); + } + // ======== Various elimination rules + // The following rules are all translated according to the clause pattern. + case PfRule::EQUIV_ELIM1: + { + return addAletheStepFromOr(AletheRule::EQUIV1, res, children, {}, *cdp); + } + case PfRule::EQUIV_ELIM2: + { + return addAletheStepFromOr(AletheRule::EQUIV2, res, children, {}, *cdp); + } + case PfRule::NOT_EQUIV_ELIM1: + { + return addAletheStepFromOr( + AletheRule::NOT_EQUIV1, res, children, {}, *cdp); + } + case PfRule::NOT_EQUIV_ELIM2: + { + return addAletheStepFromOr( + AletheRule::NOT_EQUIV2, res, children, {}, *cdp); + } + case PfRule::XOR_ELIM1: + { + return addAletheStepFromOr(AletheRule::XOR1, res, children, {}, *cdp); + } + case PfRule::XOR_ELIM2: + { + return addAletheStepFromOr(AletheRule::XOR2, res, children, {}, *cdp); + } + case PfRule::NOT_XOR_ELIM1: + { + return addAletheStepFromOr(AletheRule::NOT_XOR1, res, children, {}, *cdp); + } + case PfRule::NOT_XOR_ELIM2: + { + return addAletheStepFromOr(AletheRule::NOT_XOR2, res, children, {}, *cdp); + } + case PfRule::ITE_ELIM1: + { + return addAletheStepFromOr(AletheRule::ITE2, res, children, {}, *cdp); + } + case PfRule::ITE_ELIM2: + { + return addAletheStepFromOr(AletheRule::ITE1, res, children, {}, *cdp); + } + case PfRule::NOT_ITE_ELIM1: + { + return addAletheStepFromOr(AletheRule::NOT_ITE2, res, children, {}, *cdp); + } + case PfRule::NOT_ITE_ELIM2: + { + return addAletheStepFromOr(AletheRule::NOT_ITE1, res, children, {}, *cdp); + } + //================================================= De Morgan rules + // ======== Not And + // This rule is translated according to the clause pattern. + case PfRule::NOT_AND: + { + return addAletheStepFromOr(AletheRule::NOT_AND, res, children, {}, *cdp); + } + + //================================================= CNF rules + // The following rules are all translated according to the clause pattern. + case PfRule::CNF_AND_POS: + { + return addAletheStepFromOr(AletheRule::AND_POS, res, children, {}, *cdp); + } + case PfRule::CNF_AND_NEG: + { + return addAletheStepFromOr(AletheRule::AND_NEG, res, children, {}, *cdp); + } + case PfRule::CNF_OR_POS: + { + return addAletheStepFromOr(AletheRule::OR_POS, res, children, {}, *cdp); + } + case PfRule::CNF_OR_NEG: + { + return addAletheStepFromOr(AletheRule::OR_NEG, res, children, {}, *cdp); + } + case PfRule::CNF_IMPLIES_POS: + { + return addAletheStepFromOr( + AletheRule::IMPLIES_POS, res, children, {}, *cdp); + } + case PfRule::CNF_IMPLIES_NEG1: + { + return addAletheStepFromOr( + AletheRule::IMPLIES_NEG1, res, children, {}, *cdp); + } + case PfRule::CNF_IMPLIES_NEG2: + { + return addAletheStepFromOr( + AletheRule::IMPLIES_NEG2, res, children, {}, *cdp); + } + case PfRule::CNF_EQUIV_POS1: + { + return addAletheStepFromOr( + AletheRule::EQUIV_POS2, res, children, {}, *cdp); + } + case PfRule::CNF_EQUIV_POS2: + { + return addAletheStepFromOr( + AletheRule::EQUIV_POS1, res, children, {}, *cdp); + } + case PfRule::CNF_EQUIV_NEG1: + { + return addAletheStepFromOr( + AletheRule::EQUIV_NEG2, res, children, {}, *cdp); + } + case PfRule::CNF_EQUIV_NEG2: + { + return addAletheStepFromOr( + AletheRule::EQUIV_NEG1, res, children, {}, *cdp); + } + case PfRule::CNF_XOR_POS1: + { + return addAletheStepFromOr(AletheRule::XOR_POS1, res, children, {}, *cdp); + } + case PfRule::CNF_XOR_POS2: + { + return addAletheStepFromOr(AletheRule::XOR_POS2, res, children, {}, *cdp); + } + case PfRule::CNF_XOR_NEG1: + { + return addAletheStepFromOr(AletheRule::XOR_NEG2, res, children, {}, *cdp); + } + case PfRule::CNF_XOR_NEG2: + { + return addAletheStepFromOr(AletheRule::XOR_NEG1, res, children, {}, *cdp); + } + case PfRule::CNF_ITE_POS1: + { + return addAletheStepFromOr(AletheRule::ITE_POS2, res, children, {}, *cdp); + } + case PfRule::CNF_ITE_POS2: + { + return addAletheStepFromOr(AletheRule::ITE_POS1, res, children, {}, *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |