From fb2202cd13881e214433d185cb02bb5f925fd65e Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Thu, 10 Aug 2023 13:56:40 +0200
Subject: [PATCH] Check ground models with Dolmen

---
 Makefile          |  2 +-
 alt-ergo-lib.opam |  1 +
 dune-project      |  1 +
 tools/gentest.ml  | 37 ++++++++++++++++++++++++++++++-------
 4 files changed, 33 insertions(+), 8 deletions(-)

diff --git a/Makefile b/Makefile
index 93f61b42a2..0125c62c9c 100644
--- a/Makefile
+++ b/Makefile
@@ -126,7 +126,7 @@ runtest: gentest bin
 
 # Run non-regression tests for the CI.
 runtest-ci: gentest bin
-	dune build @runtest @runtest-quick @runtest-ci
+	dune build @runtest @runtest-quick @runtest-ci @check-models
 
 # Promote new outputs of the tests.
 promote:
diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam
index 1c1da38843..fe75fe8c7f 100644
--- a/alt-ergo-lib.opam
+++ b/alt-ergo-lib.opam
@@ -20,6 +20,7 @@ depends: [
   "dolmen" {>= "0.9"}
   "dolmen_type" {>= "0.9"}
   "dolmen_loop" {>= "0.9"}
+  "dolmen_bin" {with-test}
   "ocplib-simplex" {>= "0.5"}
   "zarith" {>= "1.4"}
   "seq"
diff --git a/dune-project b/dune-project
index ad75c36052..e640f74876 100644
--- a/dune-project
+++ b/dune-project
@@ -80,6 +80,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (dolmen (>= 0.9))
   (dolmen_type (>= 0.9))
   (dolmen_loop (>= 0.9))
+  (dolmen_bin :with-test)
   (ocplib-simplex (>= 0.5))
   (zarith (>= 1.4))
   seq
diff --git a/tools/gentest.ml b/tools/gentest.ml
index 6faa45fed6..99aabb1453 100644
--- a/tools/gentest.ml
+++ b/tools/gentest.ml
@@ -109,11 +109,12 @@ end
 module Test : sig
   type t = private {
     cmd: Cmd.t;
-    pb_file: string
+    pb_file: string;
+    check_model: bool;
   }
   (** Type of a test. *)
 
-  val make: cmd: Cmd.t -> pb_file: string -> t
+  val make: cmd: Cmd.t -> pb_file: string -> check_model: bool -> t
   (** Set up the test. *)
 
   val pp_expected_output: t printer
@@ -124,10 +125,11 @@ module Test : sig
 end = struct
   type t = {
     cmd: Cmd.t;
-    pb_file: string
+    pb_file: string;
+    check_model: bool;
   }
 
-  let make ~cmd ~pb_file = {cmd; pb_file}
+  let make ~cmd ~pb_file ~check_model = {cmd; pb_file; check_model}
 
   let pp_output fmt tst =
     let filename = Filename.chop_extension tst.pb_file in
@@ -152,7 +154,8 @@ end = struct
 @[<v 1>(ignore-stderr@,\
 @[<v 1>(with-accepted-exit-codes 0@,\
 @[<v 1>(run %a))))))))@]@]@]@]@]@]@\n\
-@[<v 1>(rule@,\
+@[<v 1>\
+(rule@,\
 @[<v 1>(alias %s)@,\
 @[<v 1>(package alt-ergo)@,\
 @[<v 1>(action (diff %a @, %a)))@]@]@]@]@]@."
@@ -161,7 +164,23 @@ end = struct
       Cmd.pp tst.cmd
       (Cmd.group tst.cmd)
       pp_expected_output tst
-      pp_output tst
+      pp_output tst;
+    let () =
+      if tst.check_model then
+        Format.fprintf fmt "\
+@[<v 1>\
+(rule@,\
+(alias check-models)@,\
+(deps (:input %a) (:test %s))@,\
+(package alt-ergo)@,\
+@[<v 1>(action@,\
+@[<v 1>(with-accepted-exit-codes 0@,\
+@[<v 1>(bash \"sed 's/^unknown/sat/' %%{input} | \
+opam exec -- dolmen --check-model true %%{test}\"))))@]@]@]@]\n@."
+          pp_output tst
+          tst.pb_file
+    in
+    ()
 end
 
 module Batch : sig
@@ -208,7 +227,11 @@ end = struct
         in
         List.fold_left (fun acc2 cmd ->
             if filter ~exclude filters cmd then
-              Test.make ~cmd ~pb_file :: acc2
+              let check_model =
+                List.exists (String.equal "models")
+                  (String.split_on_char '.' pb_file)
+              in
+              Test.make ~cmd ~pb_file ~check_model :: acc2
             else
               acc2
           ) acc1 cmds) [] pb_files