comp_simp -> comp_simplify

HanielB · Aug 9, 2024 · 48c1a58 · 48c1a58
1 parent df2652e
commit 48c1a58
Showing 1 changed file with 12 additions and 12 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -1630,8 +1630,8 @@ bool AletheProofPostprocessCallback::update(Node res,
           //   with @p1: (=> x c)
           //   with @p2: (<= c x)
           //
-          // ----- comp_simp  -------------------equiv_pos2   --- geq
-          //  @p0             (cl (not @p0) (not @p1) @p2)    @p1
+          // ----- comp_simplify  -------------------equiv_pos2   --- geq
+          //  @p0                 (cl (not @p0) (not @p1) @p2)    @p1
           // ---------------------------------------------------- resolution
           //                     @p2
           //
@@ -1725,8 +1725,8 @@ bool AletheProofPostprocessCallback::update(Node res,
             //
             // PI_a:
             //
-            // ----- comp_simp  --------------------- equiv_pos1     ---- notLT
-            //  @pa             (cl (not @pa) @pb (not (not @pc)))   (not @pb)
+            // --- comp_simplify --------------------- equiv_pos1    ----- notLT
+            // @pa               (cl (not @pa) @pb (not (not @pc)))  (not @pb)
             // ------------------------------------------------------ resolution
             //              (cl (not (not @pc)))
             //
@@ -1742,8 +1742,8 @@ bool AletheProofPostprocessCallback::update(Node res,
             //
             //  @pd: (= (>= x c) (<= c x))
             //
-            // ----- comp_simp  -------------------------- equiv_pos1  --- PI_b
-            //  @pd             (cl (not @pd) (>= x c) (not @pc))      @pc
+            // --- comp_simplify -------------------------- equiv_pos1  --- PI_b
+            // @pd               (cl (not @pd) (>= x c) (not @pc))      @pc
             // ------------------------------------------------------ resolution
             //              (cl (>= x c))
             success &= addAletheStep(AletheRule::HOLE,
@@ -1768,9 +1768,9 @@ bool AletheProofPostprocessCallback::update(Node res,
           //   with @p4: (> x c)
           //   with @p5: (<= x c)
           //
-          // ----- comp_simp  ----------------------------------- equiv_pos1
-          //  @p3             (cl (not @p3) @p4 (not (not @p5)))
-          // --------------------------------------------------- resolution
+          // ----- comp_simplify  ----------------------------------- equiv_pos1
+          //  @p3                 (cl (not @p3) @p4 (not (not @p5)))
+          // ------------------------------------------------------- resolution
           //              (cl @p4 (not (not @p5)))
           //
           // Then we combine the proofs PI_0, the premise for "notEq", and
@@ -1888,9 +1888,9 @@ bool AletheProofPostprocessCallback::update(Node res,
           //   with @p7: (< x c)
           //   with @p8: (<= c x)
           //
-          // ----- comp_simp  ----------------------------------- equiv_pos1
-          //  @p6             (cl (not @p6) @p7 (not (not @p8)))
-          // --------------------------------------------------- resolution
+          // ----- comp_simplify  ----------------------------------- equiv_pos1
+          //  @p6                  (cl (not @p6) @p7 (not (not @p8)))
+          // -------------------------------------------------------- resolution
           //              (cl @p7 (not (not @p8)))
           //
           // Then we combine the proofs PI_0, the premise for "notEq", the