# HG changeset patch
# User boehmes
# Date 1300890797 -3600
# Node ID c8be98f12b1c786f21cccb030d3405bd8a029c37
# Parent  621321627d0f186c15f58dad84289a0939e665c3
Z3 non-commercial usage may explicitly be declined

diff -r 621321627d0f -r c8be98f12b1c src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Mar 23 14:29:29 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Mar 23 15:33:17 2011 +0100
@@ -6,7 +6,11 @@
 
 signature SMT_SETUP_SOLVERS =
 sig
-  val z3_non_commercial: unit -> bool
+  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 setup: theory -> theory
 end
 
@@ -96,18 +100,34 @@
 
 (* Z3 *)
 
+datatype z3_non_commercial =
+  Z3_Non_Commercial_Unknown |
+  Z3_Non_Commercial_Accepted |
+  Z3_Non_Commercial_Declined
+
+
 local
   val flagN = "Z3_NON_COMMERCIAL"
+
+  val accepted = member (op =) ["yes", "Yes", "YES"]
+  val declined = member (op =) ["no", "No", "NO"]
 in
 
-fun z3_non_commercial () = (getenv flagN = "yes")
+fun z3_non_commercial () =
+  if accepted (getenv flagN) then Z3_Non_Commercial_Accepted
+  else if declined (getenv flagN) then Z3_Non_Commercial_Declined
+  else Z3_Non_Commercial_Unknown
 
 fun if_z3_non_commercial f =
-  if z3_non_commercial () then f ()
-  else
-    error ("The SMT solver Z3 is not enabled. To enable it, set " ^
-      "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
-      ".")
+  (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.")
+  | Z3_Non_Commercial_Unknown =>
+      error ("The SMT solver Z3 is not activated. To activate it, set " ^
+        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
+        "."))
 
 end