[Tests] Add unfolding tests

TDacik · Feb 19, 2025 · 6bca7a6 · 6bca7a6
1 parent 2d6f69e
commit 6bca7a6
Show file tree

Hide file tree

Showing 2 changed files with 81 additions and 3 deletions.
diff --git a/tests/InductiveDefinition_tests.ml b/tests/InductiveDefinition_tests.ml
@@ -11,12 +11,14 @@ let ls_def x y =
     SL.mk_exists' [SL_builtins.loc_ls] (fun [n] ->
       SL.mk_star [
         SL.mk_distinct [x; y];
-        SL.mk_pto x y;
-        SL.mk_predicate "ls" [n; x]
+        SL.mk_pto x n;
+        SL.mk_predicate "ls" [n; y]
   ])]
 
 let ls = InductiveDefinition.mk "ls" [Var.x; Var.y] @@ ls_def x y
 
+let sid_ls = InductiveDefinition.ID_map.of_list [("ls", ls)]
+
 let instantiate_test1 () =
   let actual = InductiveDefinition.instantiate ~refresh:false ls [u; v] in
   let expected = ls_def u v in
@@ -27,11 +29,87 @@ let instantiate_test2 () =
   let expected = ls_def u v in
   SL.check_equal actual expected
 
+
+(** Unfolding tests *)
+
+(* TODO: we could test more properties of unfolded formulas *)
+
+let unfold_test1 () =
+  let actual = InductiveDefinition.unfold sid_ls ls [x; y] 0 in
+  let expected = SL.mk_eq [x; y] in
+  SL.check_equal actual expected
+
+let unfold_test2 () =
+  let actual = InductiveDefinition.unfold sid_ls ls [x; y] 1 in
+  let expected =
+    SL.mk_or [
+      SL.mk_eq [x; y];
+      SL.mk_exists' [SL_builtins.loc_ls] (fun [n] ->
+        SL.mk_star [
+          SL.mk_distinct [x; y];
+          SL.mk_pto x n;
+          SL.mk_eq [n; y]
+  ])]
+  in
+  SL.check_equal actual expected
+
+let unfold_test3 () =
+  let actual = InductiveDefinition.unfold sid_ls ls [x; y] 2 in
+  let expected =
+    SL.mk_or [
+      SL.mk_eq [x; y];
+      SL.mk_exists' [SL_builtins.loc_ls] (fun [n] ->
+        SL.mk_star [
+          SL.mk_distinct [x; y];
+          SL.mk_pto x n;
+
+            SL.mk_or [
+              SL.mk_eq [n; y];
+              SL.mk_exists' [SL_builtins.loc_ls] (fun [n2] ->
+                SL.mk_star [
+                  SL.mk_distinct [n; y];
+                  SL.mk_pto n n2;
+                  SL.mk_eq [n2; y];
+            ])]
+  ])]
+  in
+  SL.check_equal actual expected
+
+let unfold_test4 () =
+  let id = InductiveDefinition.map IntroduceIfThenElse.apply ls in
+  let sid = InductiveDefinition.ID_map.of_list [("ls", id)] in
+  let actual = Simplifier.simplify @@ InductiveDefinition.unfold sid id [x; y] 0 in
+  let expected = SL.mk_eq [x; y] in
+  SL.check_equal actual expected
+
+let unfold_test5 () =
+  let id = InductiveDefinition.map IntroduceIfThenElse.apply ls in
+  let sid = InductiveDefinition.ID_map.of_list [("ls", id)] in
+  let actual = Simplifier.simplify @@ InductiveDefinition.unfold sid id [x; y] 1 in
+  let expected =
+    SL.mk_ite
+      (SL.mk_eq [x; y])
+      (SL.emp)
+      (SL.mk_exists' [SL_builtins.loc_ls] (fun [n] ->
+        SL.mk_star [
+          SL.mk_pto x n;
+          SL.mk_eq [n; y]
+        ]))
+  in
+  SL.check_equal actual expected
+
 let () =
   run "Inductive definitions" [
     "instantiate", [
       test_case "no refresh" `Quick instantiate_test1;
       test_case "refresh"    `Quick instantiate_test2;
     ];
+    "unfold", [
+      test_case "unfold ls, depth: 0"     `Quick unfold_test1;
+      test_case "unfold ls, depth: 1"     `Quick unfold_test2;
+      test_case "unfold ls, depth: 2"     `Quick unfold_test3;
+      test_case "unfold ls-ite, depth: 0" `Quick unfold_test4;
+      test_case "unfold ls-ite, depth: 1" `Quick unfold_test5;
+    ];
   ]
 
diff --git a/tests/testables/Builder.ml b/tests/testables/Builder.ml
@@ -20,7 +20,7 @@ module Make (T : TESTABLE_BASE) = struct
     Alcotest.check' (module T' : TESTABLE with type t = t) ~msg ~actual ~expected
 
   let check_distinct lhs rhs =
-    let msg = Format.asprintf "Objects %s and %s are equal (expected to be distinct)" (T.show lhs) (T.show rhs) in
+    let msg = Format.asprintf "Objects\n%s\n\nand\n\n%s\n are equal (expected to be distinct)" (T.show lhs) (T.show rhs) in
     Alcotest.check' Alcotest.bool ~msg ~actual:(T.equal lhs rhs) ~expected:false
 
   let check_apply ~input ~expected fn =