Adds S_with_fresh

formalsec · Jun 6, 2024 · 723f7f7 · 723f7f7
1 parent 4bb20f0
commit 723f7f7
Show file tree

Hide file tree

Showing 8 changed files with 22 additions and 11 deletions.
diff --git a/bin/main.ml b/bin/main.ml
@@ -34,7 +34,9 @@ let prove_mode_conv =
 
 let parse_cmdline =
   let aux files solver prover_mode debug print_statistics =
-    let module Mappings = (val mappings_of_solver solver : Mappings_intf.S) in
+    let module Mappings =
+      (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
+    in
     Mappings.set_debug debug;
     let module Solver =
       ( val match prover_mode with

diff --git a/lib/bitwuzla_mappings.mli b/lib/bitwuzla_mappings.mli
@@ -17,4 +17,4 @@
 (***************************************************************************)
 
 (** @inline *)
-include Mappings_intf.S
+include Mappings_intf.S_with_fresh
diff --git a/lib/colibri2_mappings.mli b/lib/colibri2_mappings.mli
@@ -17,4 +17,4 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
-include Mappings_intf.S
+include Mappings_intf.S_with_fresh
diff --git a/lib/cvc5_mappings.mli b/lib/cvc5_mappings.mli
@@ -17,4 +17,4 @@
 (***************************************************************************)
 
 (** @inline *)
-include Mappings_intf.S
+include Mappings_intf.S_with_fresh
diff --git a/lib/mappings.nop.ml b/lib/mappings.nop.ml
@@ -369,4 +369,8 @@ end
 
 module Impl' : M = Impl
 
-include Mappings.Make (Impl)
+module Fresh = struct
+  module Make () = Mappings.Make (Impl)
+end
+
+include Fresh.Make ()
diff --git a/lib/mappings_intf.ml b/lib/mappings_intf.ml
@@ -447,3 +447,11 @@ module type S = sig
     val pp_statistics : Format.formatter -> optimize -> unit
   end
 end
+
+module type S_with_fresh = sig
+  module Fresh : sig
+    module Make () : S
+  end
+
+  include S
+end
diff --git a/lib/solver_dispatcher.ml b/lib/solver_dispatcher.ml
@@ -5,7 +5,8 @@ type solver_type =
   | Colibri2_solver
   | Bitwuzla_solver
 
-let mappings_of_solver : solver_type -> (module Mappings_intf.S) = function
+let mappings_of_solver : solver_type -> (module Mappings_intf.S_with_fresh) =
+  function
   | Z3_solver -> (module Z3_mappings)
   | Cvc5_solver -> (module Cvc5_mappings)
   | Colibri2_solver -> (module Colibri2_mappings)

diff --git a/lib/z3_mappings.mli b/lib/z3_mappings.mli
@@ -16,9 +16,5 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
-module Fresh : sig
-  module Make () : Mappings_intf.S
-end
-
 (** @inline *)
-include Mappings_intf.S
+include Mappings_intf.S_with_fresh