--- a/src/HOL/Mirabelle.thy Mon Jan 17 17:04:50 2022 +0000
+++ b/src/HOL/Mirabelle.thy Tue Jan 18 17:55:20 2022 +0100
@@ -9,6 +9,7 @@
imports Sledgehammer Predicate_Compile Presburger
begin
+ML_file \<open>Tools/Mirabelle/mirabelle_util.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
ML \<open>
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Jan 17 17:04:50 2022 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Jan 18 17:55:20 2022 +0100
@@ -206,6 +206,7 @@
val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>;
val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>;
+ val mirabelle_randomize = Options.default_int \<^system_option>\<open>mirabelle_randomize\<close>;
val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
val check_theory = check_theories (space_explode "," mirabelle_theories);
@@ -254,6 +255,10 @@
loaded_theories
|> map_index I
|> maps make_commands
+ |> (if mirabelle_randomize <= 0 then
+ I
+ else
+ fst o MLCG.shuffle (MLCG.initialize mirabelle_randomize))
|> (fn xs => fold_map (fn x => fn i => ((i, x), i + 1)) xs 0)
|> (fn (indexed_commands, commands_length) =>
let
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Mon Jan 17 17:04:50 2022 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Jan 18 17:55:20 2022 +0100
@@ -119,6 +119,7 @@
var options = Options.init(opts = build_options)
val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
+ val mirabelle_randomize = options.check_name("mirabelle_randomize")
val mirabelle_stride = options.check_name("mirabelle_stride")
val mirabelle_timeout = options.check_name("mirabelle_timeout")
val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
@@ -154,6 +155,7 @@
-j INT maximum number of parallel jobs (default 1)
-m INT """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -r INT """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """)
-s INT """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """)
-t SECONDS """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
-v verbose
@@ -185,6 +187,7 @@
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
"m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
"o:" -> (arg => options = options + arg),
+ "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
"s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
"t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
"v" -> (_ => verbose = true),
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_util.ML Tue Jan 18 17:55:20 2022 +0100
@@ -0,0 +1,54 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_util.ML
+ Author: Martin Desharnais, MPI-INF Saarbruecken
+*)
+
+(* Pseudorandom number generator *)
+signature PRNG = sig
+ type state
+ val initialize : int -> state
+ val next : state -> int * state
+end
+
+(* Pseudorandom algorithms *)
+signature PRNG_ALGORITHMS = sig
+ include PRNG
+ val shuffle : state -> 'a list -> 'a list * state
+end
+
+functor PRNG_Algorithms(PRNG : PRNG) : PRNG_ALGORITHMS = struct
+
+open PRNG
+
+fun shuffle prng_state xs =
+ fold_map (fn x => fn prng_state =>
+ let
+ val (n, prng_state') = next prng_state
+ in ((n, x), prng_state') end) xs prng_state
+ |> apfst (sort (int_ord o apply2 fst))
+ |> apfst (map snd)
+
+end
+
+(* multiplicative linear congruential generator *)
+structure MLCG_PRNG : PRNG = struct
+ (* The modulus is implicitly 2^64 through using Word64.
+ The multiplier and increment are the same as Newlib and Musl according to Wikipedia.
+ See: https://en.wikipedia.org/wiki/Linear_congruential_generator#Parameters_in_common_use
+ *)
+ val multiplier = Word64.fromInt 6364136223846793005
+ val increment = Word64.fromInt 1
+
+ type state = Word64.word
+
+ val initialize = Word64.fromInt
+
+ fun next s =
+ let
+ open Word64
+ val s' = multiplier * s + increment
+ in
+ (toInt s', s')
+ end
+end
+
+structure MLCG = PRNG_Algorithms(MLCG_PRNG)
--- a/src/HOL/Tools/etc/options Mon Jan 17 17:04:50 2022 +0000
+++ b/src/HOL/Tools/etc/options Tue Jan 18 17:55:20 2022 +0100
@@ -56,6 +56,9 @@
option mirabelle_max_calls : int = 0
-- "max. no. of calls to each action (0: unbounded)"
+option mirabelle_randomize : int = 0
+ -- "seed to randomize the goals before selection (0: no randomization)"
+
option mirabelle_output_dir : string = "mirabelle"
-- "output directory for log files and generated artefacts"