activation of Z3 via "z3_non_commercial" system option (without requiring restart);
--- 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
--- 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
--- 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.
--- 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 ]]
--- 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
--- 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)"
+