[proofs] Alethe: Translate REORDERING rule (#7533)

Implementation of the translation of REORDERING rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index b02f1cbdd96bc399f6dd010235de49b19db56a99..ff17941e9561436b4d40f180a264f3c8d8b297c9 100644 (file)
--- 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 aa3858969b09a0e58356b30ee3eb35b8f22aba37..5372ef100281c30df50e3ee17bb59003b73f705c 100644 (file)
--- 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 026f69bd4e55d0447bd293cc4a0537e2c58b0f26..258e645e85a5eee462fd75a7ced98c35c7d00b69 100644 (file)
--- 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