From: Lachnitt Date: Thu, 18 Nov 2021 14:44:48 +0000 (-0800) Subject: [proofs] Alethe: Rename DUPLICATED_LITERALS (#7661) X-Git-Tag: cvc5-1.0.0~800 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2686f57262348908b88a7bd9abda214b8980d287;p=cvc5.git [proofs] Alethe: Rename DUPLICATED_LITERALS (#7661) In the Alethe specification the DUPLICATED_LITERALS rule was renamed to CONTRACTION. This PR renames the rule to be consistent with the standard. --- diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 994fe83d2..d5cb07f79 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -162,7 +162,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP2a // ------------------------------------ REORDERING // VP2b - // ------ DUPLICATED_LITERALS ------- IMPLIES_NEG1 + // ------ CONTRACTION ------- IMPLIES_NEG1 // VP3 VP4 // ------------------------------------ RESOLUTION ------- IMPLIES_NEG2 // VP5 VP6 @@ -188,7 +188,7 @@ bool AletheProofPostprocessCallback::update(Node res, // // --------- IMPLIES_SIMPLIFY // T1 VP9 - // --------- DUPLICATED_LITERALS --------- EQUIV_1 + // --------- CONTRACTION --------- EQUIV_1 // VP8 VP10 // -------------------------------------------- RESOLUTION // (cl (not (and F1 ... Fn)))* @@ -200,7 +200,7 @@ bool AletheProofPostprocessCallback::update(Node res, // // Otherwise, // T1 - // ------------------------------ DUPLICATED_LITERALS + // ------------------------------ CONTRACTION // (cl (=> (and F1 ... Fn) F))** // // @@ -260,8 +260,8 @@ bool AletheProofPostprocessCallback::update(Node res, addAletheStep(AletheRule::REORDERING, vp2b, vp2b, {vp2a}, {}, *cdp); vp3 = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]); - success &= addAletheStep( - AletheRule::DUPLICATED_LITERALS, vp3, vp3, {vp2b}, {}, *cdp); + success &= + addAletheStep(AletheRule::CONTRACTION, vp3, vp3, {vp2b}, {}, *cdp); } Node vp8 = nm->mkNode( @@ -285,13 +285,13 @@ bool AletheProofPostprocessCallback::update(Node res, if (children[0] != nm->mkConst(false)) { - success &= addAletheStep( - AletheRule::DUPLICATED_LITERALS, res, vp8, {vp7}, {}, *cdp); + success &= + addAletheStep(AletheRule::CONTRACTION, res, vp8, {vp7}, {}, *cdp); } else { - success &= addAletheStep( - AletheRule::DUPLICATED_LITERALS, vp8, vp8, {vp7}, {}, *cdp); + success &= + addAletheStep(AletheRule::CONTRACTION, vp8, vp8, {vp7}, {}, *cdp); Node vp9 = nm->mkNode(kind::SEXPR, @@ -646,7 +646,7 @@ bool AletheProofPostprocessCallback::update(Node res, // Fn) Otherwise, VC2 = (cl C2). // // P - // ------- DUPLICATED_LITERALS + // ------- CONTRACTION // VC2* // // * the corresponding proof node is C2 @@ -659,11 +659,11 @@ bool AletheProofPostprocessCallback::update(Node res, if (child != res) { return addAletheStepFromOr( - AletheRule::DUPLICATED_LITERALS, res, children, {}, *cdp); + AletheRule::CONTRACTION, res, children, {}, *cdp); } } } - return addAletheStep(AletheRule::DUPLICATED_LITERALS, + return addAletheStep(AletheRule::CONTRACTION, res, nm->mkNode(kind::SEXPR, d_cl, res), children, @@ -716,7 +716,7 @@ bool AletheProofPostprocessCallback::update(Node res, // P1 VP21 ... VP2n // ---------------------------- RESOLUTION // VP3 - // ---------------------------- DUPLICATED_LITERALS + // ---------------------------- CONTRACTION // VP4 // // for i=1 to n, VP2i: (cl (or G1 ... Gn) (not Gi)) @@ -785,8 +785,8 @@ bool AletheProofPostprocessCallback::update(Node res, AletheRule::RESOLUTION, vp3, vp3, vp2Nodes, {}, *cdp); Node vp4 = nm->mkNode(kind::SEXPR, d_cl, children[0]); - success &= addAletheStep( - AletheRule::DUPLICATED_LITERALS, vp4, vp4, {vp3}, {}, *cdp); + success &= + addAletheStep(AletheRule::CONTRACTION, vp4, vp4, {vp3}, {}, *cdp); child1 = vp4; } } @@ -1102,7 +1102,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP3 // ------------------------------- REORDERING // VP4 - // ------------------------------- DUPLICATED_LITERALS + // ------------------------------- CONTRACTION // (cl (not (ite C F1 F2)) F1 F2) // // VP1: (cl (not (ite C F1 F2)) C F2) @@ -1127,7 +1127,7 @@ bool AletheProofPostprocessCallback::update(Node res, AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp) && addAletheStepFromOr( - AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + AletheRule::CONTRACTION, res, {vp4}, {}, *cdp); } // ======== CNF ITE Neg version 3 // @@ -1137,7 +1137,7 @@ bool AletheProofPostprocessCallback::update(Node res, // VP3 // ------------------------------- REORDERING // VP4 - // ------------------------------- DUPLICATED_LITERALS + // ------------------------------- CONTRACTION // (cl (ite C F1 F2) C (not F2)) // // VP1: (cl (ite C F1 F2) C (not F2)) @@ -1162,7 +1162,7 @@ bool AletheProofPostprocessCallback::update(Node res, AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp) && addAletheStepFromOr( - AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + AletheRule::CONTRACTION, res, {vp4}, {}, *cdp); } //================================================= Equality rules // The following rules are all translated according to the singleton diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp index 5372ef100..52a47fe37 100644 --- a/src/proof/alethe/alethe_proof_rule.cpp +++ b/src/proof/alethe/alethe_proof_rule.cpp @@ -92,7 +92,7 @@ const char* aletheRuleToString(AletheRule id) case AletheRule::NOT_ITE1: return "not_ite1"; case AletheRule::NOT_ITE2: return "not_ite2"; case AletheRule::ITE_INTRO: return "ite_intro"; - case AletheRule::DUPLICATED_LITERALS: return "duplicate_literals"; + case AletheRule::CONTRACTION: return "contraction"; case AletheRule::CONNECTIVE_DEF: return "connective_def"; case AletheRule::ITE_SIMPLIFY: return "ite_simplify"; case AletheRule::EQ_SIMPLIFY: return "eq_simplify"; diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h index 258e645e8..331e38ac6 100644 --- a/src/proof/alethe/alethe_proof_rule.h +++ b/src/proof/alethe/alethe_proof_rule.h @@ -334,13 +334,13 @@ enum class AletheRule : uint32_t // ite, i.e. Gi := (ite Fi Hi Hi'), then Fi = (ite Fi (= Gi Hi) (= Gi Hi')) if // Hi is of sort Bool ITE_INTRO, - // ======== duplicated_literals + // ======== contraction // > i. (cl F1 ... Fn) // ... // > j. (cl Fk1 ... Fkm) // where m <= n and k1,...,km is a monotonic map to 1,...,n such that Fk1 ... // Fkm are pairwise distinct and {F1,...,Fn} = {Fk1 ... Fkm} - DUPLICATED_LITERALS, + CONTRACTION, // ======== connective_def // G > i. (= (xor F1 F2) (or (and (not F1) F2) (and F1 (not F2)))) // or