From a78a1959ae41d2e6f7a93ae77109eec00b39dab6 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Tue, 9 Nov 2021 10:29:54 -0800 Subject: [PATCH] [proofs] Alethe: Translate REORDERING rule (#7533) Implementation of the translation of REORDERING rules into the Alethe calculus. Co-authored-by: Haniel Barbosa --- src/proof/alethe/alethe_post_processor.cpp | 19 +++++++++++++------ src/proof/alethe/alethe_proof_rule.cpp | 2 +- src/proof/alethe/alethe_proof_rule.h | 6 +++--- 3 files changed, 17 insertions(+), 10 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index b02f1cbdd..ff17941e9 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -158,7 +158,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP1 VP2_1 ... VP2_n // ------------------------------------ RESOLUTION // VP2a - // ------------------------------------ REORDER + // ------------------------------------ REORDERING // VP2b // ------ DUPLICATED_LITERALS ------- IMPLIES_NEG1 // VP3 VP4 @@ -255,7 +255,7 @@ bool AletheProofPostprocessCallback::update(Node res, notAnd.push_back(children[0]); //(cl (not (and F1 ... Fn))^n F) Node vp2b = nm->mkNode(kind::SEXPR, notAnd); success &= - addAletheStep(AletheRule::REORDER, vp2b, vp2b, {vp2a}, {}, *cdp); + addAletheStep(AletheRule::REORDERING, vp2b, vp2b, {vp2a}, {}, *cdp); vp3 = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]); success &= addAletheStep( @@ -668,6 +668,13 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + // ======== Reordering + // This rule is translated according to the clause pattern. + case PfRule::REORDERING: + { + return addAletheStepFromOr( + AletheRule::REORDERING, res, children, {}, *cdp); + } // ======== Split // See proof_rule.h for documentation on the SPLIT rule. This comment // uses variable names as introduced there. @@ -1091,7 +1098,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP1 VP2 // ------------------------------- RESOLUTION // VP3 - // ------------------------------- REORDER + // ------------------------------- REORDERING // VP4 // ------------------------------- DUPLICATED_LITERALS // (cl (not (ite C F1 F2)) F1 F2) @@ -1116,7 +1123,7 @@ bool AletheProofPostprocessCallback::update(Node res, && addAletheStep(AletheRule::ITE_POS2, vp2, vp2, {}, {}, *cdp) && addAletheStep( AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) - && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp) && addAletheStepFromOr( AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); } @@ -1126,7 +1133,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP1 VP2 // ------------------------------- RESOLUTION // VP3 - // ------------------------------- REORDER + // ------------------------------- REORDERING // VP4 // ------------------------------- DUPLICATED_LITERALS // (cl (ite C F1 F2) C (not F2)) @@ -1151,7 +1158,7 @@ bool AletheProofPostprocessCallback::update(Node res, && addAletheStep(AletheRule::ITE_NEG2, vp2, vp2, {}, {}, *cdp) && addAletheStep( AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) - && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp) && addAletheStepFromOr( AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); } diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp index aa3858969..5372ef100 100644 --- a/src/proof/alethe/alethe_proof_rule.cpp +++ b/src/proof/alethe/alethe_proof_rule.cpp @@ -116,7 +116,7 @@ const char* aletheRuleToString(AletheRule id) case AletheRule::SKO_FORALL: return "sko_forall"; case AletheRule::SYMM: return "symm"; case AletheRule::NOT_SYMM: return "not_symm"; - case AletheRule::REORDER: return "reorder"; + case AletheRule::REORDERING: return "reordering"; //================================================= Undefined rule case AletheRule::UNDEFINED: return "undefined"; default: return "?"; diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h index 026f69bd4..258e645e8 100644 --- a/src/proof/alethe/alethe_proof_rule.h +++ b/src/proof/alethe/alethe_proof_rule.h @@ -349,8 +349,8 @@ enum class AletheRule : uint32_t // G > i. (= (ite F1 F2 F3) (and (=> F1 F2) (=> (not F1) (not F3)))) CONNECTIVE_DEF, // ======== Simplify rules - // The following rules are simplifying rules introduced as tautologies that can be - // verified by a number of simple transformations + // The following rules are simplifying rules introduced as tautologies that + // can be verified by a number of simple transformations ITE_SIMPLIFY, EQ_SIMPLIFY, AND_SIMPLIFY, @@ -399,7 +399,7 @@ enum class AletheRule : uint32_t // > j. F2 // where set representation of F1 and F2 are the same and the number of // literals in C2 is the same of that of C1. - REORDER, + REORDERING, // ======== undefined // Used in case that a step in the proof rule could not be translated. UNDEFINED -- 2.30.2