Expose parametric optimizer

CHANGES.md

@@ -8,6 +8,7 @@ availability of installed solvers
 
 ### Changed
 
+- Exposes `Optimizer.Make` to allow for parametric optimizers
 - Makes Z3 optional
 
 ### Fixed

lib/dune

@@ -28,6 +28,7 @@
   num
   op_intf
   optimizer
+  optimizer_intf
   parser
   params
   parse

lib/optimizer.ml

@@ -16,6 +16,8 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
+include Optimizer_intf
+
 let solver_time = ref 0.0
 
 let ( let+ ) o f = Option.map f o
@@ -33,6 +35,12 @@ module Make (M : Mappings_intf.S) = struct
 
   let add (opt : t) (es : Expr.t list) : unit = O.add opt es
 
+  let protect (opt : t) (f : unit -> 'a) : 'a =
+    push opt;
+    let result = f () in
+    pop opt;
+    result
+
   let check (opt : t) =
     Utils.run_and_time_call
       ~use:(fun time -> solver_time := !solver_time +. time)

lib/optimizer.mli

@@ -16,22 +16,4 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
-module Z3 : sig
-  type t
-
-  val create : unit -> t
-
-  val push : t -> unit
-
-  val pop : t -> unit
-
-  val add : t -> Expr.t list -> unit
-
-  val check : t -> Mappings_intf.satisfiability
-
-  val model : t -> Model.t option
-
-  val maximize : t -> Expr.t -> Value.t option
-
-  val minimize : t -> Expr.t -> Value.t option
-end
+include Optimizer_intf.Intf (** @inline *)

lib/optimizer_intf.ml

@@ -0,0 +1,33 @@
+include Mappings_intf
+
+module type S = sig
+  type t
+
+  val create : unit -> t
+
+  val push : t -> unit
+
+  val pop : t -> unit
+
+  val add : t -> Expr.t list -> unit
+
+  val protect : t -> (unit -> 'a) -> 'a
+
+  val check : t -> Mappings_intf.satisfiability
+
+  val model : t -> Model.t option
+
+  val maximize : t -> Expr.t -> Value.t option
+
+  val minimize : t -> Expr.t -> Value.t option
+end
+
+module type Intf = sig
+  type nonrec satisfiability = satisfiability
+
+  module type S = S
+
+  module Make (_ : Mappings_intf.S) : S
+
+  module Z3 : S
+end