From a05f07c298692ced47c73918876b173bc0fc431d Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Tue, 26 Oct 2021 07:14:01 -0700 Subject: [PATCH] [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 --- src/proof/alethe/alethe_post_processor.cpp | 176 +++++++++++++++++++++ 1 file changed, 176 insertions(+) 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, -- 2.30.2