From 1c334d32645c8f8930c50fee441f081051e2aada Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Fri, 5 Nov 2021 11:35:05 -0700 Subject: [PATCH] Alethe: Translate CNF rules (#7532) Implementation of the translation of various CNF rules into the Alethe calculus. Co-authored-by: Haniel Barbosa --- src/proof/alethe/alethe_post_processor.cpp | 78 ++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 2eb3d8d1d..4013a226c 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1077,6 +1077,84 @@ bool AletheProofPostprocessCallback::update(Node res, { return addAletheStepFromOr(AletheRule::ITE_POS1, res, children, {}, *cdp); } + case PfRule::CNF_ITE_NEG1: + { + return addAletheStepFromOr(AletheRule::ITE_NEG2, res, children, {}, *cdp); + } + case PfRule::CNF_ITE_NEG2: + { + return addAletheStepFromOr(AletheRule::ITE_NEG1, res, children, {}, *cdp); + } + // ======== CNF ITE Pos version 3 + // + // ----- ITE_POS1 ----- ITE_POS2 + // VP1 VP2 + // ------------------------------- RESOLUTION + // VP3 + // ------------------------------- REORDER + // VP4 + // ------------------------------- DUPLICATED_LITERALS + // (cl (not (ite C F1 F2)) F1 F2) + // + // VP1: (cl (not (ite C F1 F2)) C F2) + // VP2: (cl (not (ite C F1 F2)) (not C) F1) + // VP3: (cl (not (ite C F1 F2)) F2 (not (ite C F1 F2)) F1) + // VP4: (cl (not (ite C F1 F2)) (not (ite C F1 F2)) F1 F2) + // + // * the corresponding proof node is (or (not (ite C F1 F2)) F1 F2) + case PfRule::CNF_ITE_POS3: + { + Node vp1 = nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0], res[2]}); + Node vp2 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]}); + Node vp3 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]}); + Node vp4 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]}); + + return addAletheStep(AletheRule::ITE_POS1, vp1, vp1, {}, {}, *cdp) + && addAletheStep(AletheRule::ITE_POS2, vp2, vp2, {}, {}, *cdp) + && addAletheStep( + AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) + && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStepFromOr( + AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + } + // ======== CNF ITE Neg version 3 + // + // ----- ITE_NEG1 ----- ITE_NEG2 + // VP1 VP2 + // ------------------------------- RESOLUTION + // VP3 + // ------------------------------- REORDER + // VP4 + // ------------------------------- DUPLICATED_LITERALS + // (cl (ite C F1 F2) C (not F2)) + // + // VP1: (cl (ite C F1 F2) C (not F2)) + // VP2: (cl (ite C F1 F2) (not C) (not F1)) + // VP3: (cl (ite C F1 F2) (not F2) (ite C F1 F2) (not F1)) + // VP4: (cl (ite C F1 F2) (ite C F1 F2) (not F1) (not F2)) + // + // * the corresponding proof node is (or (ite C F1 F2) C (not F2)) + case PfRule::CNF_ITE_NEG3: + { + Node vp1 = nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0], res[2]}); + Node vp2 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]}); + Node vp3 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]}); + Node vp4 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]}); + + return addAletheStep(AletheRule::ITE_NEG1, vp1, vp1, {}, {}, *cdp) + && addAletheStep(AletheRule::ITE_NEG2, vp2, vp2, {}, {}, *cdp) + && addAletheStep( + AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) + && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStepFromOr( + AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, -- 2.30.2