--- 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
--- 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 #>
--- 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"]
--- 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