made Z3 the default SMT solver again
authorboehmes
Mon Jan 17 17:45:52 2011 +0100 (2011-01-17)
changeset 41601fda8511006f9
parent 41597 ced4f78bb728
child 41602 2aef57d825ff
made Z3 the default SMT solver again
NEWS
src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
src/HOL/Boogie/Examples/Boogie_Max.thy
src/HOL/Boogie/Examples/VCC_Max.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/SMT_Examples/SMT_Word_Examples.thy
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/NEWS	Sun Jan 16 21:10:30 2011 +0100
     1.2 +++ b/NEWS	Mon Jan 17 17:45:52 2011 +0100
     1.3 @@ -279,9 +279,12 @@
     1.4  * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
     1.5  manually as command 'solve_direct'.
     1.6  
     1.7 -* The default SMT solver is now CVC3.  Z3 must be enabled explicitly
     1.8 -(due to licensing issues) via Z3_NON_COMMERCIAL in etc/settings of the
     1.9 -component, for example.
    1.10 +* The default SMT solver Z3 must be enabled explicitly (due to
    1.11 +licensing issues) by setting the environment variable
    1.12 +Z3_NON_COMMERCIAL in etc/settings of the component, for example.
    1.13 +For commercial applications, the SMT solver CVC3 is provided as
    1.14 +fall-back; changing the SMT solver is done via the configuration
    1.15 +option "smt_solver".
    1.16  
    1.17  * Remote SMT solvers need to be referred to by the "remote_" prefix,
    1.18  i.e. "remote_cvc3" and "remote_z3".
     2.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Sun Jan 16 21:10:30 2011 +0100
     2.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Mon Jan 17 17:45:52 2011 +0100
     2.3 @@ -84,7 +84,7 @@
     2.4  
     2.5  declare [[smt_certificates="Boogie_Dijkstra.certs"]]
     2.6  declare [[smt_fixed=true]]
     2.7 -declare [[smt_solver=z3, smt_oracle=false]]
     2.8 +declare [[smt_oracle=false]]
     2.9  
    2.10  boogie_vc Dijkstra
    2.11    by boogie
     3.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Sun Jan 16 21:10:30 2011 +0100
     3.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Mon Jan 17 17:45:52 2011 +0100
     3.3 @@ -41,7 +41,7 @@
     3.4  
     3.5  declare [[smt_certificates="Boogie_Max.certs"]]
     3.6  declare [[smt_fixed=true]]
     3.7 -declare [[smt_solver=z3, smt_oracle=false]]
     3.8 +declare [[smt_oracle=false]]
     3.9  
    3.10  boogie_vc max
    3.11    by boogie
     4.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Sun Jan 16 21:10:30 2011 +0100
     4.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Mon Jan 17 17:45:52 2011 +0100
     4.3 @@ -49,7 +49,7 @@
     4.4  
     4.5  declare [[smt_certificates="VCC_Max.certs"]]
     4.6  declare [[smt_fixed=true]]
     4.7 -declare [[smt_solver=z3, smt_oracle=false]]
     4.8 +declare [[smt_oracle=false]]
     4.9  
    4.10  boogie_status
    4.11  
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Jan 16 21:10:30 2011 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jan 17 17:45:52 2011 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  
     5.5  declare [[smt_certificates="Integration.certs"]]
     5.6  declare [[smt_fixed=true]]
     5.7 -declare [[smt_solver=z3, smt_oracle=false]]
     5.8 +declare [[smt_oracle=false]]
     5.9  
    5.10  setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
    5.11  
    5.12 @@ -5527,6 +5527,5 @@
    5.13  
    5.14  declare [[smt_certificates=""]]
    5.15  declare [[smt_fixed=false]]
    5.16 -declare [[smt_solver=cvc3]]
    5.17  
    5.18  end
     6.1 --- a/src/HOL/SMT.thy	Sun Jan 16 21:10:30 2011 +0100
     6.2 +++ b/src/HOL/SMT.thy	Mon Jan 17 17:45:52 2011 +0100
     6.3 @@ -185,7 +185,7 @@
     6.4  @{text yes}.
     6.5  *}
     6.6  
     6.7 -declare [[ smt_solver = cvc3 ]]
     6.8 +declare [[ smt_solver = z3 ]]
     6.9  
    6.10  text {*
    6.11  Since SMT solvers are potentially non-terminating, there is a timeout
     7.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 16 21:10:30 2011 +0100
     7.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jan 17 17:45:52 2011 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  imports Complex_Main
     7.5  begin
     7.6  
     7.7 -declare [[smt_solver=z3, smt_oracle=false]]
     7.8 +declare [[smt_oracle=false]]
     7.9  declare [[smt_certificates="SMT_Examples.certs"]]
    7.10  declare [[smt_fixed=true]]
    7.11  
     8.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Jan 16 21:10:30 2011 +0100
     8.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Jan 17 17:45:52 2011 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  imports Complex_Main
     8.5  begin
     8.6  
     8.7 -declare [[smt_solver=z3, smt_oracle=false]]
     8.8 +declare [[smt_oracle=false]]
     8.9  declare [[smt_certificates="SMT_Tests.certs"]]
    8.10  declare [[smt_fixed=true]]
    8.11  
     9.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Jan 16 21:10:30 2011 +0100
     9.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Mon Jan 17 17:45:52 2011 +0100
     9.3 @@ -8,7 +8,7 @@
     9.4  imports Word
     9.5  begin
     9.6  
     9.7 -declare [[smt_solver=z3, smt_oracle=true]]
     9.8 +declare [[smt_oracle=true]]
     9.9  declare [[smt_certificates="SMT_Word_Examples.certs"]]
    9.10  declare [[smt_fixed=true]]
    9.11  
    10.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 16 21:10:30 2011 +0100
    10.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 17 17:45:52 2011 +0100
    10.3 @@ -93,6 +93,15 @@
    10.4  (* Z3 *)
    10.5  
    10.6  local
    10.7 +  val flagN = "Z3_NON_COMMERCIAL"
    10.8 +
    10.9 +  fun z3_make_command is_remote name () =
   10.10 +    if getenv flagN = "yes" then make_command is_remote name ()
   10.11 +    else
   10.12 +      error ("The SMT solver Z3 is not enabled. To enable it, set " ^
   10.13 +        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
   10.14 +        ".")
   10.15 +
   10.16    fun z3_options ctxt =
   10.17      ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
   10.18        "MODEL=true", "-smt"]
   10.19 @@ -117,7 +126,7 @@
   10.20      name = make_name is_remote "z3",
   10.21      class = Z3_Interface.smtlib_z3C,
   10.22      avail = make_avail is_remote "Z3",
   10.23 -    command = make_command is_remote "Z3",
   10.24 +    command = z3_make_command is_remote "Z3",
   10.25      options = z3_options,
   10.26      default_max_relevant = 225,
   10.27      supports_filter = true,
    11.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 16 21:10:30 2011 +0100
    11.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Jan 17 17:45:52 2011 +0100
    11.3 @@ -55,7 +55,7 @@
    11.4  local
    11.5  
    11.6  fun make_cmd command options problem_path proof_path = space_implode " " (
    11.7 -  map File.shell_quote (command @ options) @
    11.8 +  map File.shell_quote (command () @ options) @
    11.9    [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
   11.10  
   11.11  fun trace_and ctxt msg f x =
   11.12 @@ -136,7 +136,7 @@
   11.13        |> tap (trace_assms ctxt)
   11.14        |> SMT_Translate.translate ctxt comments
   11.15        ||> tap trace_recon_data
   11.16 -  in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end
   11.17 +  in (run_solver ctxt' name (make_cmd command options) str, recon) end
   11.18  
   11.19  end
   11.20