# HG changeset patch
# User boehmes
# Date 1292398764 -3600
# Node ID 5c5d05963f93f709ab1550f9fcc168870dc5cf71
# Parent  573f557ed716accf87c47828a89772762d7c70e4
added option to modify the random seed of SMT solvers

diff -r 573f557ed716 -r 5c5d05963f93 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
@@ -205,6 +205,13 @@
 declare [[ smt_timeout = 20 ]]
 
 text {*
+SMT solvers apply randomized heuristics.  In case a problem is not
+solvable by an SMT solver, changing the following option might help.
+*}
+
+declare [[ smt_random_seed = 1 ]]
+
+text {*
 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
 solvers are fully trusted without additional checks.  The following
 option can cause the SMT solver to run in proof-producing mode, giving
diff -r 573f557ed716 -r 5c5d05963f93 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
@@ -22,6 +22,7 @@
   val oracle: bool Config.T
   val datatypes: bool Config.T
   val timeout: real Config.T
+  val random_seed: int Config.T
   val fixed: bool Config.T
   val verbose: bool Config.T
   val traceN: string
@@ -124,6 +125,9 @@
 val timeoutN = "smt_timeout"
 val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
 
+val random_seedN = "smt_random_seed"
+val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
+
 val fixedN = "smt_fixed"
 val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
 
@@ -157,6 +161,7 @@
   setup_oracle #>
   setup_datatypes #>
   setup_timeout #>
+  setup_random_seed #>
   setup_fixed #>
   setup_trace #>
   setup_verbose #>
diff -r 573f557ed716 -r 5c5d05963f93 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 08:39:24 2010 +0100
@@ -35,7 +35,9 @@
   name = "cvc3",
   env_var = "CVC3_SOLVER",
   is_remote = true,
-  options = K ["-lang", "smtlib", "-output-lang", "presentation"],
+  options = (fn ctxt => [
+    "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
+    "-lang", "smtlib", "-output-lang", "presentation"]),
   interface = SMTLIB_Interface.interface,
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -50,7 +52,9 @@
   name = "yices",
   env_var = "YICES_SOLVER",
   is_remote = false,
-  options = K ["--smtlib"],
+  options = (fn ctxt => [
+    "--rand-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
+    "--smtlib"]),
   interface = SMTLIB_Interface.interface,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
@@ -61,7 +65,8 @@
 (* Z3 *)
 
 fun z3_options ctxt =
-  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
+  ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+    "MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
   |> not (Config.get ctxt SMT_Config.oracle) ?
        append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
 
diff -r 573f557ed716 -r 5c5d05963f93 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 08:39:24 2010 +0100
@@ -181,6 +181,7 @@
     val args = C.solver_options_of ctxt @ options ctxt
     val comments = ("solver: " ^ name) ::
       ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
+      ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
       "arguments:" :: args
   in
     irules