added option to modify the random seed of SMT solvers
authorboehmes
Wed Dec 15 08:39:24 2010 +0100 (2010-12-15)
changeset 411215c5d05963f93
parent 41119 573f557ed716
child 41122 72176ec5e031
added option to modify the random seed of SMT solvers
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/SMT.thy	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -205,6 +205,13 @@
     1.4  declare [[ smt_timeout = 20 ]]
     1.5  
     1.6  text {*
     1.7 +SMT solvers apply randomized heuristics.  In case a problem is not
     1.8 +solvable by an SMT solver, changing the following option might help.
     1.9 +*}
    1.10 +
    1.11 +declare [[ smt_random_seed = 1 ]]
    1.12 +
    1.13 +text {*
    1.14  In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
    1.15  solvers are fully trusted without additional checks.  The following
    1.16  option can cause the SMT solver to run in proof-producing mode, giving
     2.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Dec 14 00:16:30 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
     2.3 @@ -22,6 +22,7 @@
     2.4    val oracle: bool Config.T
     2.5    val datatypes: bool Config.T
     2.6    val timeout: real Config.T
     2.7 +  val random_seed: int Config.T
     2.8    val fixed: bool Config.T
     2.9    val verbose: bool Config.T
    2.10    val traceN: string
    2.11 @@ -124,6 +125,9 @@
    2.12  val timeoutN = "smt_timeout"
    2.13  val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
    2.14  
    2.15 +val random_seedN = "smt_random_seed"
    2.16 +val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
    2.17 +
    2.18  val fixedN = "smt_fixed"
    2.19  val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
    2.20  
    2.21 @@ -157,6 +161,7 @@
    2.22    setup_oracle #>
    2.23    setup_datatypes #>
    2.24    setup_timeout #>
    2.25 +  setup_random_seed #>
    2.26    setup_fixed #>
    2.27    setup_trace #>
    2.28    setup_verbose #>
     3.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Dec 14 00:16:30 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 08:39:24 2010 +0100
     3.3 @@ -35,7 +35,9 @@
     3.4    name = "cvc3",
     3.5    env_var = "CVC3_SOLVER",
     3.6    is_remote = true,
     3.7 -  options = K ["-lang", "smtlib", "-output-lang", "presentation"],
     3.8 +  options = (fn ctxt => [
     3.9 +    "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
    3.10 +    "-lang", "smtlib", "-output-lang", "presentation"]),
    3.11    interface = SMTLIB_Interface.interface,
    3.12    outcome =
    3.13      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    3.14 @@ -50,7 +52,9 @@
    3.15    name = "yices",
    3.16    env_var = "YICES_SOLVER",
    3.17    is_remote = false,
    3.18 -  options = K ["--smtlib"],
    3.19 +  options = (fn ctxt => [
    3.20 +    "--rand-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
    3.21 +    "--smtlib"]),
    3.22    interface = SMTLIB_Interface.interface,
    3.23    outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    3.24    cex_parser = NONE,
    3.25 @@ -61,7 +65,8 @@
    3.26  (* Z3 *)
    3.27  
    3.28  fun z3_options ctxt =
    3.29 -  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
    3.30 +  ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    3.31 +    "MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
    3.32    |> not (Config.get ctxt SMT_Config.oracle) ?
    3.33         append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
    3.34  
     4.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 14 00:16:30 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 08:39:24 2010 +0100
     4.3 @@ -181,6 +181,7 @@
     4.4      val args = C.solver_options_of ctxt @ options ctxt
     4.5      val comments = ("solver: " ^ name) ::
     4.6        ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
     4.7 +      ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
     4.8        "arguments:" :: args
     4.9    in
    4.10      irules