Allow using Z3 in parallel mode (Closes #205)

src/dune

@@ -57,9 +57,9 @@
   hc
   menhirLib
   ocaml_intrinsics
-  smtml.prelude
-  rusage
   patricia-tree
+  rusage
+  smtml.prelude
   yojson
   zarith
   (select

src/solvers/params.ml

@@ -21,12 +21,16 @@ type _ param =
   | Model : bool param
   | Unsat_core : bool param
   | Ematching : bool param
+  | Parallel : bool param
+  | Num_threads : int param
 
 type t =
   { timeout : int
   ; model : bool
   ; unsat_core : bool
   ; ematching : bool
+  ; parallel : bool
+  ; num_threads : int
   }
 
 let default_timeout = 2147483647
@@ -37,18 +41,27 @@ let default_unsat_core = false
 
 let default_ematching = true
 
+let default_parallel = false
+
+(* FIXME: Will this be problematic if only (Parallel, true) is specified? *)
+let default_num_threads = 1
+
 let default_value (type a) (param : a param) : a =
   match param with
   | Timeout -> default_timeout
   | Model -> default_model
   | Unsat_core -> default_unsat_core
   | Ematching -> default_ematching
+  | Parallel -> default_parallel
+  | Num_threads -> default_num_threads
 
 let default () =
   { timeout = default_timeout
   ; model = default_model
   ; unsat_core = default_unsat_core
   ; ematching = default_ematching
+  ; parallel = default_parallel
+  ; num_threads = default_num_threads
   }
 
 let set (type a) (params : t) (param : a param) (value : a) : t =
@@ -57,6 +70,11 @@ let set (type a) (params : t) (param : a param) (value : a) : t =
   | Model -> { params with model = value }
   | Unsat_core -> { params with unsat_core = value }
   | Ematching -> { params with ematching = value }
+  | Parallel -> { params with parallel = value }
+  | Num_threads -> { params with num_threads = value }
+
+let opt (type a) (params : t) (param : a param) (opt_value : a option) : t =
+  Option.fold ~none:params ~some:(set params param) opt_value
 
 let ( $ ) (type a) (params : t) ((param, value) : a param * a) : t =
   set params param value
@@ -67,3 +85,5 @@ let get (type a) (params : t) (param : a param) : a =
   | Model -> params.model
   | Unsat_core -> params.unsat_core
   | Ematching -> params.ematching
+  | Parallel -> params.parallel
+  | Num_threads -> params.num_threads

src/solvers/params.mli

@@ -18,9 +18,13 @@
 
 type _ param =
   | Timeout : int param
-  | Model : bool param
-  | Unsat_core : bool param
-  | Ematching : bool param
+    (** Specifies a timeout in miliseconds for each [check] call *)
+  | Model : bool param  (** Turn model production on/off *)
+  | Unsat_core : bool param  (** Turn unsatisfiable core on/off *)
+  | Ematching : bool param  (** Turn ematching on/off *)
+  | Parallel : bool param  (** Turn parallel mode on/off *)
+  | Num_threads : int param
+    (** Speficied the maximum number of threads to use in parallel mode *)
 
 type t
 
@@ -30,6 +34,12 @@ val default : unit -> t
 
 val ( $ ) : t -> 'a param * 'a -> t
 
+(** [set params p v] updates parameter [p] with value [v] *)
 val set : t -> 'a param -> 'a -> t
 
+(** [opt params p v_opt] updates parameter [p] with value [v] if [opt_v] is
+    [Some v] *)
+val opt : t -> 'a param -> 'a option -> t
+
+(** [get params p] fetches the current value for parameter [p] *)
 val get : t -> 'a param -> 'a

src/z3_mappings.default.ml

@@ -441,6 +441,10 @@ module M = struct
     let set_params (params : Params.t) =
       Z3.set_global_param "smt.ematching"
         (string_of_bool @@ Params.get params Ematching);
+      Z3.set_global_param "parallel.enable"
+        (string_of_bool @@ Params.get params Parallel);
+      Z3.set_global_param "parallel.threads.max"
+        (string_of_int @@ Params.get params Num_threads);
       Z3.Params.update_param_value ctx "timeout"
         (string_of_int @@ Params.get params Timeout);
       Z3.Params.update_param_value ctx "model"