# HG changeset patch
# User blanchet
# Date 1428511658 -7200
# Node ID 372ddff012442750c1fc7adbd61dd8555d1884f1
# Parent  1e3383a5204bd0191d25ada730bba785ddf5eb87
updated SMT module and Sledgehammer to fully open source Z3

diff -r 1e3383a5204b -r 372ddff01244 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Apr 08 18:43:43 2015 +0200
+++ b/src/HOL/SMT.thy	Wed Apr 08 18:47:38 2015 +0200
@@ -192,10 +192,6 @@
 The option @{text smt_solver} can be used to change the target SMT
 solver. The possible values can be obtained from the @{text smt_status}
 command.
-
-Due to licensing restrictions, Z3 is not enabled by default. Z3 is free
-for non-commercial applications and can be enabled by setting Isabelle
-system option @{text z3_non_commercial} to @{text yes}.
 *}
 
 declare [[smt_solver = z3]]
diff -r 1e3383a5204b -r 372ddff01244 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Apr 08 18:43:43 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Apr 08 18:47:38 2015 +0200
@@ -6,11 +6,7 @@
 
 signature SMT_SYSTEMS =
 sig
-  datatype z3_non_commercial =
-    Z3_Non_Commercial_Unknown |
-    Z3_Non_Commercial_Accepted |
-    Z3_Non_Commercial_Declined
-  val z3_non_commercial: unit -> z3_non_commercial
+  val cvc4_extensions: bool Config.T
   val z3_extensions: bool Config.T
 end;
 
@@ -117,47 +113,9 @@
 
 (* Z3 *)
 
-datatype z3_non_commercial =
-  Z3_Non_Commercial_Unknown |
-  Z3_Non_Commercial_Accepted |
-  Z3_Non_Commercial_Declined
-
-local
-  val accepted = member (op =) ["yes", "Yes", "YES"]
-  val declined = member (op =) ["no", "No", "NO"]
-in
-
-fun z3_non_commercial () =
-  let
-    val flag1 = Options.default_string @{system_option z3_non_commercial}
-    val flag2 = getenv "Z3_NON_COMMERCIAL"
-  in
-    if accepted flag1 then Z3_Non_Commercial_Accepted
-    else if declined flag1 then Z3_Non_Commercial_Declined
-    else if accepted flag2 then Z3_Non_Commercial_Accepted
-    else if declined flag2 then Z3_Non_Commercial_Declined
-    else Z3_Non_Commercial_Unknown
-  end
-
-fun if_z3_non_commercial f =
-  (case z3_non_commercial () of
-    Z3_Non_Commercial_Accepted => f ()
-  | Z3_Non_Commercial_Declined =>
-      error (Pretty.string_of (Pretty.para
-        "The SMT solver Z3 may be used only for non-commercial applications."))
-  | Z3_Non_Commercial_Unknown =>
-      error (Pretty.string_of (Pretty.para
-        ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
-         \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
-         \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
-
-end
-
 val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
 
 local
-  fun z3_make_command name () = if_z3_non_commercial (make_command name)
-
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
      "smt.refine_inj_axioms=false",
@@ -171,8 +129,8 @@
 val z3: SMT_Solver.solver_config = {
   name = "z3",
   class = select_class,
-  avail = make_avail "Z3_NEW",
-  command = z3_make_command "Z3_NEW",
+  avail = make_avail "Z3",
+  command = make_command "Z3",
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
diff -r 1e3383a5204b -r 372ddff01244 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Wed Apr 08 18:43:43 2015 +0200
+++ b/src/HOL/Tools/etc/options	Wed Apr 08 18:47:38 2015 +0200
@@ -32,8 +32,5 @@
 public option sledgehammer_timeout : int = 30
   -- "ATPs will be interrupted after this time (in seconds)"
 
-public option z3_non_commercial : string = "unknown"
-  -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
-
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"