# HG changeset patch
# User boehmes
# Date 1295282752 -3600
# Node ID fda8511006f9de5374475955059f2f0307f7f814
# Parent  ced4f78bb7289c1c001a1652fd4f8a88e16b1120
made Z3 the default SMT solver again

diff -r ced4f78bb728 -r fda8511006f9 NEWS
--- a/NEWS	Sun Jan 16 21:10:30 2011 +0100
+++ b/NEWS	Mon Jan 17 17:45:52 2011 +0100
@@ -279,9 +279,12 @@
 * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
 manually as command 'solve_direct'.
 
-* The default SMT solver is now CVC3.  Z3 must be enabled explicitly
-(due to licensing issues) via Z3_NON_COMMERCIAL in etc/settings of the
-component, for example.
+* The default SMT solver Z3 must be enabled explicitly (due to
+licensing issues) by setting the environment variable
+Z3_NON_COMMERCIAL in etc/settings of the component, for example.
+For commercial applications, the SMT solver CVC3 is provided as
+fall-back; changing the SMT solver is done via the configuration
+option "smt_solver".
 
 * Remote SMT solvers need to be referred to by the "remote_" prefix,
 i.e. "remote_cvc3" and "remote_z3".
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -84,7 +84,7 @@
 
 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_vc Dijkstra
   by boogie
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -41,7 +41,7 @@
 
 declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_vc max
   by boogie
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -49,7 +49,7 @@
 
 declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_status
 
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -12,7 +12,7 @@
 
 declare [[smt_certificates="Integration.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
 
@@ -5527,6 +5527,5 @@
 
 declare [[smt_certificates=""]]
 declare [[smt_fixed=false]]
-declare [[smt_solver=cvc3]]
 
 end
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/SMT.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -185,7 +185,7 @@
 @{text yes}.
 *}
 
-declare [[ smt_solver = cvc3 ]]
+declare [[ smt_solver = z3 ]]
 
 text {*
 Since SMT solvers are potentially non-terminating, there is a timeout
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 declare [[smt_certificates="SMT_Examples.certs"]]
 declare [[smt_fixed=true]]
 
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 declare [[smt_certificates="SMT_Tests.certs"]]
 declare [[smt_fixed=true]]
 
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Mon Jan 17 17:45:52 2011 +0100
@@ -8,7 +8,7 @@
 imports Word
 begin
 
-declare [[smt_solver=z3, smt_oracle=true]]
+declare [[smt_oracle=true]]
 declare [[smt_certificates="SMT_Word_Examples.certs"]]
 declare [[smt_fixed=true]]
 
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 17 17:45:52 2011 +0100
@@ -93,6 +93,15 @@
 (* Z3 *)
 
 local
+  val flagN = "Z3_NON_COMMERCIAL"
+
+  fun z3_make_command is_remote name () =
+    if getenv flagN = "yes" then make_command is_remote name ()
+    else
+      error ("The SMT solver Z3 is not enabled. To enable it, set " ^
+        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
+        ".")
+
   fun z3_options ctxt =
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
       "MODEL=true", "-smt"]
@@ -117,7 +126,7 @@
     name = make_name is_remote "z3",
     class = Z3_Interface.smtlib_z3C,
     avail = make_avail is_remote "Z3",
-    command = make_command is_remote "Z3",
+    command = z3_make_command is_remote "Z3",
     options = z3_options,
     default_max_relevant = 225,
     supports_filter = true,
diff -r ced4f78bb728 -r fda8511006f9 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Jan 17 17:45:52 2011 +0100
@@ -55,7 +55,7 @@
 local
 
 fun make_cmd command options problem_path proof_path = space_implode " " (
-  map File.shell_quote (command @ options) @
+  map File.shell_quote (command () @ options) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
 fun trace_and ctxt msg f x =
@@ -136,7 +136,7 @@
       |> tap (trace_assms ctxt)
       |> SMT_Translate.translate ctxt comments
       ||> tap trace_recon_data
-  in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end
+  in (run_solver ctxt' name (make_cmd command options) str, recon) end
 
 end