# HG changeset patch
# User boehmes
# Date 1300886969 -3600
# Node ID 621321627d0f186c15f58dad84289a0939e665c3
# Parent  217a1b61d42d34fc9b898e7ec2cfa751d2582a89
export status function to query whether Z3 has been activated for usage within Isabelle

diff -r 217a1b61d42d -r 621321627d0f src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Mar 23 10:38:50 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Mar 23 14:29:29 2011 +0100
@@ -6,6 +6,7 @@
 
 signature SMT_SETUP_SOLVERS =
 sig
+  val z3_non_commercial: unit -> bool
   val setup: theory -> theory
 end
 
@@ -97,13 +98,23 @@
 
 local
   val flagN = "Z3_NON_COMMERCIAL"
+in
 
+fun z3_non_commercial () = (getenv flagN = "yes")
+
+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") ^
+      ".")
+
+end
+
+
+local
   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") ^
-        ".")
+    if_z3_non_commercial (make_command is_remote name)
 
   fun z3_options ctxt =
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),