Fix simplification test.

proof-ninja · May 13, 2024 · da39f02 · da39f02
1 parent ed49e9e
commit da39f02
Showing 1 changed file with 28 additions and 28 deletions.
diff --git a/test/simplification_test.ml b/test/simplification_test.ml
@@ -248,17 +248,17 @@ let main () =
         (Pred ("f", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]);
       ];
       expected = [
-        (Pred ("f", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]);
-        (Pred ("g", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]);
-        (Deltainsert ("f", [NamedVar "X"]), [Rel (Pred ("f", [NamedVar "X"]))]);
-        (Deltadelete ("g", [NamedVar "X"]), [Rel (Pred ("g", [NamedVar "X"]))]);
-        (Deltainsert ("a", [NamedVar "X"]), [
-          Rel (Pred ("n", [NamedVar "X"])); Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 42))))
-        ]);
+        (Deltadelete ("d", [NamedVar "X"]), [ Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 42)))) ]);
         (Deltadelete ("b", [NamedVar "X"]), [
           Not (Pred ("n", [NamedVar "X"])); Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 42))))
         ]);
-        (Deltadelete ("d", [NamedVar "X"]), [ Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 42)))) ]);
+        (Deltainsert ("a", [NamedVar "X"]), [
+          Rel (Pred ("n", [NamedVar "X"])); Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 42))))
+        ]);
+        (Deltadelete ("g", [NamedVar "X"]), [Rel (Pred ("g", [NamedVar "X"]))]);
+        (Deltainsert ("f", [NamedVar "X"]), [Rel (Pred ("f", [NamedVar "X"]))]);
+        (Pred ("g", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]);
+        (Pred ("f", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]);
       ];
     };
     {
@@ -299,30 +299,30 @@ let main () =
           (Pred ("v", [NamedVar "A"]), [Rel (Pred ("s", [NamedVar "A"; NamedVar "B"]))]);
       ];
       expected = [
-        (Pred ("v", [NamedVar "A"]), [Rel (Pred ("s", [NamedVar "A"; AnonVar]))]);
+        (Deltainsert ("s", [NamedVar "A"; NamedVar "B"]), [
+          Rel (Deltainsert ("v", [NamedVar "A"]));
+          Not (Deltadelete ("s", [AnonVar; NamedVar "B"]));
+          Not (Pred ("s", [NamedVar "A"; AnonVar]));
+        ]);
+        (Deltainsert ("s", [NamedVar "A"; NamedVar "B"]), [
+          Rel (Deltainsert ("v", [NamedVar "A"]));
+          Not (Deltadelete ("s", [AnonVar; AnonVar]));
+          Not (Pred ("s", [NamedVar "A"; AnonVar]));
+          Equat (Equation ("=", (Var (NamedVar "B")), (Const (Int (-1)))))
+        ]);
+        (Deltadelete ("s", [NamedVar "A"; NamedVar "B"]), [
+         Rel (Deltadelete ("v", [NamedVar "A"]));
+          Rel (Pred ("s", [NamedVar "A"; NamedVar "B"]));
+        ]);
+        (Deltainsert ("v", [NamedVar "GV1"]), [
+          Rel (Deltadelete ("v", [AnonVar]));
+          Equat (Equation ("=", (Var (NamedVar "GV1")), (Const (Int 4))));
+        ]);
         (Deltadelete ("v", [NamedVar "GV1"]), [
           Rel (Pred ("v", [NamedVar "GV1"]));
           Equat (Equation ("=", (Var (NamedVar "GV1")), (Const (Int 1))));
         ]);
-         (Deltainsert ("v", [NamedVar "GV1"]), [
-           Rel (Deltadelete ("v", [AnonVar]));
-           Equat (Equation ("=", (Var (NamedVar "GV1")), (Const (Int 4))));
-         ]);
-         (Deltadelete ("s", [NamedVar "A"; NamedVar "B"]), [
-          Rel (Deltadelete ("v", [NamedVar "A"]));
-           Rel (Pred ("s", [NamedVar "A"; NamedVar "B"]));
-         ]);
-         (Deltainsert ("s", [NamedVar "A"; NamedVar "B"]), [
-           Rel (Deltainsert ("v", [NamedVar "A"]));
-           Not (Deltadelete ("s", [AnonVar; AnonVar]));
-           Not (Pred ("s", [NamedVar "A"; AnonVar]));
-           Equat (Equation ("=", (Var (NamedVar "B")), (Const (Int (-1)))))
-         ]);
-         (Deltainsert ("s", [NamedVar "A"; NamedVar "B"]), [
-           Rel (Deltainsert ("v", [NamedVar "A"]));
-           Not (Deltadelete ("s", [AnonVar; NamedVar "B"]));
-           Not (Pred ("s", [NamedVar "A"; AnonVar]));
-         ]);
+        (Pred ("v", [NamedVar "A"]), [Rel (Pred ("s", [NamedVar "A"; AnonVar]))]);
       ]
     }
   ]