activation of Z3 via "z3_non_commercial" system option (without requiring restart);
authorwenzelm
Mon Jan 13 20:20:44 2014 +0100 (2014-01-13)
changeset 550070c07990363a3
parent 55006 ea9fc64327cb
child 55008 b5b2e193ca33
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
Admin/components/components.sha1
Admin/components/main
NEWS
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/etc/options
     1.1 --- a/Admin/components/components.sha1	Mon Jan 13 18:47:48 2014 +0100
     1.2 +++ b/Admin/components/components.sha1	Mon Jan 13 20:20:44 2014 +0100
     1.3 @@ -77,4 +77,5 @@
     1.4  2ae13aa17d0dc95ce254a52f1dba10929763a10d  xz-java-1.2.tar.gz
     1.5  4530a1aa6f4498ee3d78d6000fa71a3f63bd077f  yices-1.0.28.tar.gz
     1.6  12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
     1.7 +3a8f77822278fe9250890e357248bc678d8fac95  z3-3.2-1.tar.gz
     1.8  d94a716502c8503d63952bcb4d4176fac8b28704  z3-4.0.tar.gz
     2.1 --- a/Admin/components/main	Mon Jan 13 18:47:48 2014 +0100
     2.2 +++ b/Admin/components/main	Mon Jan 13 20:20:44 2014 +0100
     2.3 @@ -10,5 +10,5 @@
     2.4  polyml-5.5.1-1
     2.5  scala-2.10.3
     2.6  spass-3.8ds
     2.7 -z3-3.2
     2.8 +z3-3.2-1
     2.9  xz-java-1.2-1
     3.1 --- a/NEWS	Mon Jan 13 18:47:48 2014 +0100
     3.2 +++ b/NEWS	Mon Jan 13 20:20:44 2014 +0100
     3.3 @@ -42,6 +42,11 @@
     3.4  
     3.5  *** HOL ***
     3.6  
     3.7 +* Activation of Z3 now works via "z3_non_commercial" system option
     3.8 +(without requiring restart), instead of former settings variable
     3.9 +"Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
    3.10 +Plugin Options / Isabelle / General.
    3.11 +
    3.12  * "declare [[code abort: ...]]" replaces "code_abort ...".
    3.13  INCOMPATIBILITY.
    3.14  
     4.1 --- a/src/HOL/SMT.thy	Mon Jan 13 18:47:48 2014 +0100
     4.2 +++ b/src/HOL/SMT.thy	Mon Jan 13 20:20:44 2014 +0100
     4.3 @@ -169,8 +169,7 @@
     4.4  
     4.5  Due to licensing restrictions, Yices and Z3 are not installed/enabled
     4.6  by default.  Z3 is free for non-commercial applications and can be enabled
     4.7 -by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
     4.8 -@{text yes}.
     4.9 +by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
    4.10  *}
    4.11  
    4.12  declare [[ smt_solver = z3 ]]
     5.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 13 18:47:48 2014 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jan 13 20:20:44 2014 +0100
     5.3 @@ -111,29 +111,28 @@
     5.4  
     5.5  
     5.6  local
     5.7 -  val flagN = "Z3_NON_COMMERCIAL"
     5.8 +  val flagN = @{option z3_non_commercial}
     5.9  
    5.10    val accepted = member (op =) ["yes", "Yes", "YES"]
    5.11    val declined = member (op =) ["no", "No", "NO"]
    5.12  in
    5.13  
    5.14  fun z3_non_commercial () =
    5.15 -  if accepted (getenv flagN) then Z3_Non_Commercial_Accepted
    5.16 -  else if declined (getenv flagN) then Z3_Non_Commercial_Declined
    5.17 +  if accepted (Options.default_string flagN) then Z3_Non_Commercial_Accepted
    5.18 +  else if declined (Options.default_string flagN) then Z3_Non_Commercial_Declined
    5.19    else Z3_Non_Commercial_Unknown
    5.20  
    5.21  fun if_z3_non_commercial f =
    5.22    (case z3_non_commercial () of
    5.23      Z3_Non_Commercial_Accepted => f ()
    5.24    | Z3_Non_Commercial_Declined =>
    5.25 -      error ("The SMT solver Z3 may only be used for non-commercial " ^
    5.26 -        "applications.")
    5.27 +      error (Pretty.string_of (Pretty.para
    5.28 +        "The SMT solver Z3 may only be used for non-commercial applications."))
    5.29    | Z3_Non_Commercial_Unknown =>
    5.30 -      error ("The SMT solver Z3 is not activated. To activate it, set\n" ^
    5.31 -        "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ ",\n" ^
    5.32 -        "and restart the Isabelle system." ^
    5.33 -        (if getenv "Z3_COMPONENT" = "" then ""
    5.34 -         else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings")))))
    5.35 +      error (Pretty.string_of (Pretty.para
    5.36 +        ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
    5.37 +         \system option " ^ quote flagN ^ " to \"yes\" (e.g. via \
    5.38 +         \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
    5.39  
    5.40  end
    5.41  
     6.1 --- a/src/HOL/Tools/etc/options	Mon Jan 13 18:47:48 2014 +0100
     6.2 +++ b/src/HOL/Tools/etc/options	Mon Jan 13 20:20:44 2014 +0100
     6.3 @@ -29,3 +29,6 @@
     6.4  public option sledgehammer_timeout : int = 30
     6.5    -- "ATPs will be interrupted after this time (in seconds)"
     6.6  
     6.7 +public option z3_non_commercial : string = "unknown"
     6.8 +  -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     6.9 +