Feature: Random_seed parameter

src/bin/main.ml

@@ -21,7 +21,7 @@ let cli =
   let cmd_run = Cmd.v Cli.info_run Cli.cmd_run in
   let cmd_to_smt2 = Cmd.v Cli.info_to_smt2 Cli.cmd_to_smt2 in
   let cmd_to_smtml = Cmd.v Cli.info_to_smtml Cli.cmd_to_smtml in
-  let info = Cmd.info "smtml" ~version:"%%VERSION%%" in
+  let info = Cmd.info "smtml" in
   Cmd.group info [ cmd_run; cmd_to_smt2; cmd_to_smtml ]
 
 let returncode =

src/smtml/altergo_mappings.default.ml

@@ -72,6 +72,7 @@ module M = struct
         | Parallel -> ()
         | Num_threads -> ()
         | Debug -> ()
+        | Random_seed -> ()
 
       let set_params (params : Params.t) =
         List.iter

src/smtml/colibri2_mappings.default.ml

@@ -72,6 +72,7 @@ module M = struct
         | Parallel -> ()
         | Num_threads -> ()
         | Debug -> Colibri2_stdlib.Debug.set_info_flags v
+        | Random_seed -> ()
 
       let set_params (params : Params.t) =
         List.iter

src/smtml/cvc5_mappings.default.ml

@@ -519,6 +519,7 @@ module Fresh_cvc5 () = struct
       | Unsat_core ->
         Solver.set_option slv "produce-unsat-cores" (string_of_bool v)
       | Ematching -> Solver.set_option slv "e-matching" (string_of_bool v)
+      | Random_seed -> Solver.set_option slv "seed" (string_of_int v)
       | Parallel | Num_threads | Debug -> ()
 
     let set_params slv params =

src/smtml/params.ml

@@ -10,6 +10,7 @@ type _ param =
   | Parallel : bool param
   | Num_threads : int param
   | Debug : bool param
+  | Random_seed : int param
 
 let discr : type a. a param -> int = function
   | Timeout -> 0
@@ -19,6 +20,7 @@ let discr : type a. a param -> int = function
   | Parallel -> 4
   | Num_threads -> 5
   | Debug -> 6
+  | Random_seed -> 7
 
 module Key = struct
   type t = K : 'a param -> t
@@ -50,6 +52,8 @@ let default_num_threads = 1
 
 let default_debug = false
 
+let default_random_seed = 0
+
 let default_value (type a) (param : a param) : a =
   match param with
   | Timeout -> default_timeout
@@ -59,6 +63,7 @@ let default_value (type a) (param : a param) : a =
   | Parallel -> default_parallel
   | Num_threads -> default_num_threads
   | Debug -> default_debug
+  | Random_seed -> default_random_seed
 
 let default () =
   Pmap.empty
@@ -86,7 +91,9 @@ let get (type a) (params : t) (param : a param) : a =
   | Parallel, Some (P (Parallel, v)) -> v
   | Num_threads, Some (P (Num_threads, v)) -> v
   | Debug, Some (P (Debug, v)) -> v
-  | ( (Timeout | Model | Unsat_core | Ematching | Parallel | Num_threads | Debug)
+  | Random_seed, Some (P (Random_seed, v)) -> v
+  | ( ( Timeout | Model | Unsat_core | Ematching | Parallel | Num_threads
+      | Debug | Random_seed )
     , _ ) ->
     assert false
 

src/smtml/params.mli

@@ -24,6 +24,8 @@ type _ param =
   | Num_threads : int param
     (** Specifies the maximum number of threads to use in parallel mode. *)
   | Debug : bool param  (** Enable or disable solver debugging messages. *)
+  | Random_seed : int param
+    (** Specifies the random seed used by the solver. *)
 
 (** The type [param'] is a wrapper for storing parameter-value pairs. *)
 type param' = P : 'a param * 'a -> param'

src/smtml/z3_mappings.default.ml

@@ -551,6 +551,11 @@ module M = struct
       | Num_threads ->
         Z3.set_global_param "parallel.threads.max" (string_of_int v)
       | Debug -> ()
+      | Random_seed ->
+        Z3.set_global_param "sat.random_seed" (string_of_int v);
+        Z3.set_global_param "sls.random_seed" (string_of_int v);
+        Z3.set_global_param "smt.random_seed" (string_of_int v);
+        Z3.set_global_param "fp.spacer.random_seed" (string_of_int v)
 
     let set_params (params : Params.t) =
       List.iter (fun (Params.P (p, v)) -> set_param p v) (Params.to_list params)

test/integration/test_solver.ml

@@ -19,16 +19,16 @@ module Make (M : Mappings_intf.S_with_fresh) = struct
     assert_equal (Params.default_value Timeout) Int32.(to_int max_int);
     assert_equal (Params.default_value Model) true;
     assert_equal (Params.default_value Unsat_core) false;
-
-    assert_equal (Params.default_value Ematching) true
+    assert_equal (Params.default_value Ematching) true;
+    assert_equal (Params.default_value Random_seed) 0
 
   let test_solver_params solver_module =
     let module Solver = (val solver_module : Solver_intf.S) in
     let params =
       Params.(
         default () $ (Timeout, 900) $ (Model, false) $ (Unsat_core, true)
         $ (Ematching, false) $ (Parallel, true) $ (Num_threads, 1)
-        $ (Debug, false) )
+        $ (Debug, false) $ (Random_seed, 1227) )
     in
     assert (Params.get params Unsat_core);
     let _ : Solver.t = Solver.create ~params () in