[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (#7753)

Translation of the ARITH_TRICHOTOMY rule 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 7ef9cc9dbb611738ac0a8b012f7fb07863cdd841..9bfb34cf713030535fa613a434ff70859f83f927 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1384,6 +1384,232 @@ bool AletheProofPostprocessCallback::update(Node res,
                               {},
                               *cdp);
     }
+    // ======== Trichotomy of the reals
+    // See proof_rule.h for documentation on the ARITH_TRICHOTOMY rule. This
+    // comment uses variable names as introduced there.
+    //
+    // If C = (= x c) or C = (> x c) pre-processing has to transform (>= x c)
+    // into (<= c x)
+    //
+    // ------------------------------------------------------ LA_DISEQUALITY
+    //  (VP1: (cl (or (= x c) (not (<= x c)) (not (<= c x)))))
+    // -------------------------------------------------------- OR
+    //  (VP2: (cl (= x c) (not (<= x c)) (not (<= c x))))
+    //
+    // If C = (> x c) or C = (< x c) post-processing has to be added. In these
+    // cases resolution on VP2 A B yields (not (<=x c)) or (not (<= c x)) and
+    // comp_simplify is used to transform it into C. Otherwise,
+    //
+    //  VP2   A   B
+    // ---------------- RESOLUTION
+    //  (cl C)*
+    //
+    // * the corresponding proof node is C
+    case PfRule::ARITH_TRICHOTOMY:
+    {
+      bool success = true;
+      Node equal, lesser, greater;
+
+      Kind k = res.getKind();
+      if (k == kind::EQUAL)
+      {
+        equal = res;
+        if (children[0].getKind() == kind::LEQ)
+        {
+          greater = children[0];
+          lesser = children[1];
+        }
+        else
+        {
+          greater = children[1];
+          lesser = children[0];
+        }
+      }
+      // Add case where res is not =
+      else if (res.getKind() == kind::GT)
+      {
+        greater = res;
+        if (children[0].getKind() == kind::NOT)
+        {
+          equal = children[0];
+          lesser = children[1];
+        }
+        else
+        {
+          equal = children[1];
+          lesser = children[0];
+        }
+      }
+      else
+      {
+        lesser = res;
+        if (children[0].getKind() == kind::NOT)
+        {
+          equal = children[0];
+          greater = children[1];
+        }
+        else
+        {
+          equal = children[1];
+          greater = children[0];
+        }
+      }
+
+      Node x, c;
+      if (equal.getKind() == kind::NOT)
+      {
+        x = equal[0][0];
+        c = equal[0][1];
+      }
+      else
+      {
+        x = equal[0];
+        c = equal[1];
+      }
+      Node vp_child1 = children[0], vp_child2 = children[1];
+
+      // Preprocessing
+      if (res == equal || res == greater)
+      {  // C = (= x c) or C = (> x c)
+        // lesser = (>= x c)
+        Node vpc2 = nm->mkNode(
+            kind::SEXPR,
+            d_cl,
+            nm->mkNode(kind::GEQ, x, c).eqNode(nm->mkNode(kind::LEQ, c, x)));
+        // (cl (= (>= x c) (<= c x)))
+        Node vpc1 = nm->mkNode(kind::SEXPR,
+                               {d_cl,
+                                vpc2[1].notNode(),
+                                nm->mkNode(kind::GEQ, x, c).notNode(),
+                                nm->mkNode(kind::LEQ, c, x)});
+        // (cl (not(= (>= x c) (<= c x))) (not (>= x c)) (<= c x))
+        vp_child1 = nm->mkNode(
+            kind::SEXPR, d_cl, nm->mkNode(kind::LEQ, c, x));  // (cl (<= c x))
+
+        success &=
+            addAletheStep(AletheRule::EQUIV_POS2, vpc1, vpc1, {}, {}, *cdp)
+            && addAletheStep(
+                AletheRule::COMP_SIMPLIFY, vpc2, vpc2, {}, {}, *cdp)
+            && addAletheStep(AletheRule::RESOLUTION,
+                             vp_child1,
+                             vp_child1,
+                             {vpc1, vpc2, lesser},
+                             {},
+                             *cdp);
+        // greater = (<= x c) or greater = (not (= x c)) -> no preprocessing
+        // necessary
+        vp_child2 = res == equal ? greater : equal;
+      }
+
+      // Process
+      Node vp1 = nm->mkNode(kind::SEXPR,
+                            d_cl,
+                            nm->mkNode(kind::OR,
+                                       nm->mkNode(kind::EQUAL, x, c),
+                                       nm->mkNode(kind::LEQ, x, c).notNode(),
+                                       nm->mkNode(kind::LEQ, c, x).notNode()));
+      // (cl (or (= x c) (not (<= x c)) (not (<= c x))))
+      Node vp2 = nm->mkNode(kind::SEXPR,
+                            {d_cl,
+                             nm->mkNode(kind::EQUAL, x, c),
+                             nm->mkNode(kind::LEQ, x, c).notNode(),
+                             nm->mkNode(kind::LEQ, c, x).notNode()});
+      // (cl (= x c) (not (<= x c)) (not (<= c x)))
+      success &=
+          addAletheStep(AletheRule::LA_DISEQUALITY, vp1, vp1, {}, {}, *cdp)
+          && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp);
+
+      // Postprocessing
+      if (res == equal)
+      {  // no postprocessing necessary
+        return success
+               && addAletheStep(AletheRule::RESOLUTION,
+                                res,
+                                nm->mkNode(kind::SEXPR, d_cl, res),
+                                {vp2, vp_child1, vp_child2},
+                                {},
+                                *cdp);
+      }
+      if (res == greater)
+      {  // have (not (<= x c)) but result should be (> x c)
+        Node vp3 = nm->mkNode(
+            kind::SEXPR,
+            d_cl,
+            nm->mkNode(kind::LEQ, x, c).notNode());  // (cl (not (<= x c)))
+        Node vp4 = nm->mkNode(
+            kind::SEXPR,
+            {d_cl,
+             nm->mkNode(kind::EQUAL,
+                        nm->mkNode(kind::GT, x, c),
+                        nm->mkNode(kind::LEQ, x, c).notNode())
+                 .notNode(),
+             nm->mkNode(kind::GT, x, c),
+             nm->mkNode(kind::LEQ, x, c)
+                 .notNode()
+                 .notNode()});  // (cl (not(= (> x c) (not (<= x c)))) (> x c)
+                                // (not (not (<= x c))))
+        Node vp5 =
+            nm->mkNode(kind::SEXPR,
+                       d_cl,
+                       nm->mkNode(kind::GT, x, c)
+                           .eqNode(nm->mkNode(kind::LEQ, x, c).notNode()));
+        // (cl (= (> x c) (not (<= x c))))
+
+        return success
+               && addAletheStep(AletheRule::RESOLUTION,
+                                vp3,
+                                vp3,
+                                {vp2, vp_child1, vp_child2},
+                                {},
+                                *cdp)
+               && addAletheStep(AletheRule::EQUIV_POS1, vp4, vp4, {}, {}, *cdp)
+               && addAletheStep(
+                   AletheRule::COMP_SIMPLIFY, vp5, vp5, {}, {}, *cdp)
+               && addAletheStep(AletheRule::RESOLUTION,
+                                res,
+                                nm->mkNode(kind::SEXPR, d_cl, res),
+                                {vp3, vp4, vp5},
+                                {},
+                                *cdp);
+      }
+      // have (not (<= c x)) but result should be (< x c)
+      Node vp3 = nm->mkNode(
+          kind::SEXPR,
+          d_cl,
+          nm->mkNode(kind::LEQ, c, x).notNode());  // (cl (not (<= c x)))
+      Node vp4 =
+          nm->mkNode(kind::SEXPR,
+                     {d_cl,
+                      nm->mkNode(kind::LT, x, c)
+                          .eqNode(nm->mkNode(kind::LEQ, c, x).notNode())
+                          .notNode(),
+                      nm->mkNode(kind::LT, x, c),
+                      nm->mkNode(kind::LEQ, c, x)
+                          .notNode()
+                          .notNode()});  // (cl (not(= (< x c) (not (<= c x))))
+                                         // (< x c) (not (not (<= c x))))
+      Node vp5 = nm->mkNode(
+          kind::SEXPR,
+          d_cl,
+          nm->mkNode(kind::LT, x, c)
+              .eqNode(nm->mkNode(kind::LEQ, c, x)
+                          .notNode()));  // (cl (= (< x c) (not (<= c x))))
+      return success
+             && addAletheStep(AletheRule::RESOLUTION,
+                              vp3,
+                              vp3,
+                              {vp2, vp_child1, vp_child2},
+                              {},
+                              *cdp)
+             && addAletheStep(AletheRule::EQUIV_POS1, vp4, vp4, {}, {}, *cdp)
+             && addAletheStep(AletheRule::COMP_SIMPLIFY, vp5, vp5, {}, {}, *cdp)
+             && addAletheStep(AletheRule::RESOLUTION,
+                              res,
+                              nm->mkNode(kind::SEXPR, d_cl, res),
+                              {vp3, vp4, vp5},
+                              {},
+                              *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,