# HG changeset patch
# User wenzelm
# Date 1389640844 -3600
# Node ID 0c07990363a3d1c703ffcb667ae69dec347bc899
# Parent  ea9fc64327cbc88a251641185925559deb18904f
activation of Z3 via "z3_non_commercial" system option (without requiring restart);

diff -r ea9fc64327cb -r 0c07990363a3 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Jan 13 18:47:48 2014 +0100
+++ b/Admin/components/components.sha1	Mon Jan 13 20:20:44 2014 +0100
@@ -77,4 +77,5 @@
 2ae13aa17d0dc95ce254a52f1dba10929763a10d  xz-java-1.2.tar.gz
 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f  yices-1.0.28.tar.gz
 12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
+3a8f77822278fe9250890e357248bc678d8fac95  z3-3.2-1.tar.gz
 d94a716502c8503d63952bcb4d4176fac8b28704  z3-4.0.tar.gz
diff -r ea9fc64327cb -r 0c07990363a3 Admin/components/main
--- a/Admin/components/main	Mon Jan 13 18:47:48 2014 +0100
+++ b/Admin/components/main	Mon Jan 13 20:20:44 2014 +0100
@@ -10,5 +10,5 @@
 polyml-5.5.1-1
 scala-2.10.3
 spass-3.8ds
-z3-3.2
+z3-3.2-1
 xz-java-1.2-1
diff -r ea9fc64327cb -r 0c07990363a3 NEWS
--- a/NEWS	Mon Jan 13 18:47:48 2014 +0100
+++ b/NEWS	Mon Jan 13 20:20:44 2014 +0100
@@ -42,6 +42,11 @@
 
 *** HOL ***
 
+* Activation of Z3 now works via "z3_non_commercial" system option
+(without requiring restart), instead of former settings variable
+"Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
+Plugin Options / Isabelle / General.
+
 * "declare [[code abort: ...]]" replaces "code_abort ...".
 INCOMPATIBILITY.
 
diff -r ea9fc64327cb -r 0c07990363a3 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Jan 13 18:47:48 2014 +0100
+++ b/src/HOL/SMT.thy	Mon Jan 13 20:20:44 2014 +0100
@@ -169,8 +169,7 @@
 
 Due to licensing restrictions, Yices and Z3 are not installed/enabled
 by default.  Z3 is free for non-commercial applications and can be enabled
-by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
-@{text yes}.
+by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
 *}
 
 declare [[ smt_solver = z3 ]]
diff -r ea9fc64327cb -r 0c07990363a3 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 13 18:47:48 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 13 20:20:44 2014 +0100
@@ -111,29 +111,28 @@
 
 
 local
-  val flagN = "Z3_NON_COMMERCIAL"
+  val flagN = @{option z3_non_commercial}
 
   val accepted = member (op =) ["yes", "Yes", "YES"]
   val declined = member (op =) ["no", "No", "NO"]
 in
 
 fun z3_non_commercial () =
-  if accepted (getenv flagN) then Z3_Non_Commercial_Accepted
-  else if declined (getenv flagN) then Z3_Non_Commercial_Declined
+  if accepted (Options.default_string flagN) then Z3_Non_Commercial_Accepted
+  else if declined (Options.default_string flagN) then Z3_Non_Commercial_Declined
   else Z3_Non_Commercial_Unknown
 
 fun if_z3_non_commercial f =
   (case z3_non_commercial () of
     Z3_Non_Commercial_Accepted => f ()
   | Z3_Non_Commercial_Declined =>
-      error ("The SMT solver Z3 may only be used for non-commercial " ^
-        "applications.")
+      error (Pretty.string_of (Pretty.para
+        "The SMT solver Z3 may only be used for non-commercial applications."))
   | Z3_Non_Commercial_Unknown =>
-      error ("The SMT solver Z3 is not activated. To activate it, set\n" ^
-        "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ ",\n" ^
-        "and restart the Isabelle system." ^
-        (if getenv "Z3_COMPONENT" = "" then ""
-         else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings")))))
+      error (Pretty.string_of (Pretty.para
+        ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
+         \system option " ^ quote flagN ^ " to \"yes\" (e.g. via \
+         \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
 
 end
 
diff -r ea9fc64327cb -r 0c07990363a3 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Mon Jan 13 18:47:48 2014 +0100
+++ b/src/HOL/Tools/etc/options	Mon Jan 13 20:20:44 2014 +0100
@@ -29,3 +29,6 @@
 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)"
+