From 71222b06521a881769d0b089ce8599afd43c07a5 Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 19:01:03 +0000 Subject: [PATCH 1/6] feat: random_seed --- src/smtml/altergo_mappings.default.ml | 1 + src/smtml/colibri2_mappings.default.ml | 1 + src/smtml/cvc5_mappings.default.ml | 2 +- src/smtml/params.ml | 8 +++++++- src/smtml/params.mli | 1 + src/smtml/z3_mappings.default.ml | 5 +++++ test/integration/test_solver.ml | 6 +++--- 7 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/smtml/altergo_mappings.default.ml b/src/smtml/altergo_mappings.default.ml index c45da5fc..00b40634 100644 --- a/src/smtml/altergo_mappings.default.ml +++ b/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 diff --git a/src/smtml/colibri2_mappings.default.ml b/src/smtml/colibri2_mappings.default.ml index 5c3dd119..24ab4293 100644 --- a/src/smtml/colibri2_mappings.default.ml +++ b/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 diff --git a/src/smtml/cvc5_mappings.default.ml b/src/smtml/cvc5_mappings.default.ml index 6700cf8f..c57c22c8 100644 --- a/src/smtml/cvc5_mappings.default.ml +++ b/src/smtml/cvc5_mappings.default.ml @@ -519,7 +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) - | Parallel | Num_threads | Debug -> () + | Parallel | Num_threads | Debug | Random_seed -> () let set_params slv params = List.iter diff --git a/src/smtml/params.ml b/src/smtml/params.ml index 96841ee3..c4542d63 100644 --- a/src/smtml/params.ml +++ b/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,8 @@ 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 diff --git a/src/smtml/params.mli b/src/smtml/params.mli index 5fc0cb91..2d892c40 100644 --- a/src/smtml/params.mli +++ b/src/smtml/params.mli @@ -24,6 +24,7 @@ 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' diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml index 51b8018a..6307f7b3 100644 --- a/src/smtml/z3_mappings.default.ml +++ b/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 -> if Option.is_none v then () else + Z3.set_global_param "sat.random_seed" (string_of_int (Option.get v)); + Z3.set_global_param "sls.random_seed" (string_of_int (Option.get v)); + Z3.set_global_param "smt.random_seed" (string_of_int (Option.get v)); + Z3.set_global_param "fp.spacer.random_seed" (string_of_int (Option.get v)) let set_params (params : Params.t) = List.iter (fun (Params.P (p, v)) -> set_param p v) (Params.to_list params) diff --git a/test/integration/test_solver.ml b/test/integration/test_solver.ml index f74eae9a..3f2f54be 100644 --- a/test/integration/test_solver.ml +++ b/test/integration/test_solver.ml @@ -19,8 +19,8 @@ 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 @@ -28,7 +28,7 @@ module Make (M : Mappings_intf.S_with_fresh) = struct 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 From 86ea17192ec1f2b1fbd1747196b7d649d91fd17a Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 19:39:11 +0000 Subject: [PATCH 2/6] fix: version template --- src/bin/main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bin/main.ml b/src/bin/main.ml index d90577d9..5df3271d 100644 --- a/src/bin/main.ml +++ b/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 = From 3418966e37d848dec0874b8d8ea696eb024e1022 Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 19:41:18 +0000 Subject: [PATCH 3/6] fix: oops tests --- src/smtml/z3_mappings.default.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml index 6307f7b3..df976f4e 100644 --- a/src/smtml/z3_mappings.default.ml +++ b/src/smtml/z3_mappings.default.ml @@ -552,10 +552,10 @@ module M = struct Z3.set_global_param "parallel.threads.max" (string_of_int v) | Debug -> () | Random_seed -> if Option.is_none v then () else - Z3.set_global_param "sat.random_seed" (string_of_int (Option.get v)); - Z3.set_global_param "sls.random_seed" (string_of_int (Option.get v)); - Z3.set_global_param "smt.random_seed" (string_of_int (Option.get v)); - Z3.set_global_param "fp.spacer.random_seed" (string_of_int (Option.get v)) + 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) From ad2712eae1fa84cff84f4c14930d01a549806c7a Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 19:43:22 +0000 Subject: [PATCH 4/6] fix: oops tests --- src/smtml/z3_mappings.default.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml index df976f4e..beb1bca9 100644 --- a/src/smtml/z3_mappings.default.ml +++ b/src/smtml/z3_mappings.default.ml @@ -551,7 +551,7 @@ module M = struct | Num_threads -> Z3.set_global_param "parallel.threads.max" (string_of_int v) | Debug -> () - | Random_seed -> if Option.is_none v then () else + | 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); From db1237c2bd4310613635e07d964033ee850ea1f5 Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 21:54:29 +0000 Subject: [PATCH 5/6] fix: formatting --- src/smtml/params.ml | 3 ++- src/smtml/params.mli | 3 ++- src/smtml/z3_mappings.default.ml | 8 ++++---- test/integration/test_solver.ml | 2 +- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smtml/params.ml b/src/smtml/params.ml index c4542d63..b2651416 100644 --- a/src/smtml/params.ml +++ b/src/smtml/params.ml @@ -92,7 +92,8 @@ let get (type a) (params : t) (param : a param) : a = | Num_threads, Some (P (Num_threads, v)) -> v | Debug, Some (P (Debug, v)) -> v | Random_seed, Some (P (Random_seed, v)) -> v - | ( (Timeout | Model | Unsat_core | Ematching | Parallel | Num_threads | Debug | Random_seed) + | ( ( Timeout | Model | Unsat_core | Ematching | Parallel | Num_threads + | Debug | Random_seed ) , _ ) -> assert false diff --git a/src/smtml/params.mli b/src/smtml/params.mli index 2d892c40..857b6665 100644 --- a/src/smtml/params.mli +++ b/src/smtml/params.mli @@ -24,7 +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. *) + | 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' diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml index beb1bca9..8d1f5e03 100644 --- a/src/smtml/z3_mappings.default.ml +++ b/src/smtml/z3_mappings.default.ml @@ -552,10 +552,10 @@ module M = struct 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) + 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) diff --git a/test/integration/test_solver.ml b/test/integration/test_solver.ml index 3f2f54be..a4cc5cc9 100644 --- a/test/integration/test_solver.ml +++ b/test/integration/test_solver.ml @@ -28,7 +28,7 @@ module Make (M : Mappings_intf.S_with_fresh) = struct Params.( default () $ (Timeout, 900) $ (Model, false) $ (Unsat_core, true) $ (Ematching, false) $ (Parallel, true) $ (Num_threads, 1) - $ (Debug, false) $ (Random_seed, 1227)) + $ (Debug, false) $ (Random_seed, 1227) ) in assert (Params.get params Unsat_core); let _ : Solver.t = Solver.create ~params () in From a7ad3f73a6b132d3c2ff9efa8242a9ff62e6135f Mon Sep 17 00:00:00 2001 From: Tiago Ferreira Date: Wed, 19 Nov 2025 22:10:08 +0000 Subject: [PATCH 6/6] feat: random_seed for cvc5 --- src/smtml/cvc5_mappings.default.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smtml/cvc5_mappings.default.ml b/src/smtml/cvc5_mappings.default.ml index c57c22c8..1094638c 100644 --- a/src/smtml/cvc5_mappings.default.ml +++ b/src/smtml/cvc5_mappings.default.ml @@ -519,7 +519,8 @@ 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) - | Parallel | Num_threads | Debug | Random_seed -> () + | Random_seed -> Solver.set_option slv "seed" (string_of_int v) + | Parallel | Num_threads | Debug -> () let set_params slv params = List.iter