# HG changeset patch
# User desharna
# Date 1642524920 -3600
# Node ID fc664e4fbf6da5ad7aa7596826233338ab3e4111
# Parent  ac3901e4e0a941383607d6a0a8d2f1c7f5fc977a
added Mirabelle option -r to randomize the goals before selection

diff -r ac3901e4e0a9 -r fc664e4fbf6d src/HOL/Mirabelle.thy
--- 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>
diff -r ac3901e4e0a9 -r fc664e4fbf6d src/HOL/Tools/Mirabelle/mirabelle.ML
--- 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
diff -r ac3901e4e0a9 -r fc664e4fbf6d src/HOL/Tools/Mirabelle/mirabelle.scala
--- 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),
diff -r ac3901e4e0a9 -r fc664e4fbf6d src/HOL/Tools/Mirabelle/mirabelle_util.ML
--- /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)
diff -r ac3901e4e0a9 -r fc664e4fbf6d src/HOL/Tools/etc/options
--- 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"