updated SMT module and Sledgehammer to fully open source Z3
authorblanchet
Wed Apr 08 18:47:38 2015 +0200 (2015-04-08)
changeset 59960372ddff01244
parent 59959 1e3383a5204b
child 59961 a965060dcbb8
updated SMT module and Sledgehammer to fully open source Z3
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/etc/options
     1.1 --- a/src/HOL/SMT.thy	Wed Apr 08 18:43:43 2015 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Apr 08 18:47:38 2015 +0200
     1.3 @@ -192,10 +192,6 @@
     1.4  The option @{text smt_solver} can be used to change the target SMT
     1.5  solver. The possible values can be obtained from the @{text smt_status}
     1.6  command.
     1.7 -
     1.8 -Due to licensing restrictions, Z3 is not enabled by default. Z3 is free
     1.9 -for non-commercial applications and can be enabled by setting Isabelle
    1.10 -system option @{text z3_non_commercial} to @{text yes}.
    1.11  *}
    1.12  
    1.13  declare [[smt_solver = z3]]
     2.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Apr 08 18:43:43 2015 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Apr 08 18:47:38 2015 +0200
     2.3 @@ -6,11 +6,7 @@
     2.4  
     2.5  signature SMT_SYSTEMS =
     2.6  sig
     2.7 -  datatype z3_non_commercial =
     2.8 -    Z3_Non_Commercial_Unknown |
     2.9 -    Z3_Non_Commercial_Accepted |
    2.10 -    Z3_Non_Commercial_Declined
    2.11 -  val z3_non_commercial: unit -> z3_non_commercial
    2.12 +  val cvc4_extensions: bool Config.T
    2.13    val z3_extensions: bool Config.T
    2.14  end;
    2.15  
    2.16 @@ -117,47 +113,9 @@
    2.17  
    2.18  (* Z3 *)
    2.19  
    2.20 -datatype z3_non_commercial =
    2.21 -  Z3_Non_Commercial_Unknown |
    2.22 -  Z3_Non_Commercial_Accepted |
    2.23 -  Z3_Non_Commercial_Declined
    2.24 -
    2.25 -local
    2.26 -  val accepted = member (op =) ["yes", "Yes", "YES"]
    2.27 -  val declined = member (op =) ["no", "No", "NO"]
    2.28 -in
    2.29 -
    2.30 -fun z3_non_commercial () =
    2.31 -  let
    2.32 -    val flag1 = Options.default_string @{system_option z3_non_commercial}
    2.33 -    val flag2 = getenv "Z3_NON_COMMERCIAL"
    2.34 -  in
    2.35 -    if accepted flag1 then Z3_Non_Commercial_Accepted
    2.36 -    else if declined flag1 then Z3_Non_Commercial_Declined
    2.37 -    else if accepted flag2 then Z3_Non_Commercial_Accepted
    2.38 -    else if declined flag2 then Z3_Non_Commercial_Declined
    2.39 -    else Z3_Non_Commercial_Unknown
    2.40 -  end
    2.41 -
    2.42 -fun if_z3_non_commercial f =
    2.43 -  (case z3_non_commercial () of
    2.44 -    Z3_Non_Commercial_Accepted => f ()
    2.45 -  | Z3_Non_Commercial_Declined =>
    2.46 -      error (Pretty.string_of (Pretty.para
    2.47 -        "The SMT solver Z3 may be used only for non-commercial applications."))
    2.48 -  | Z3_Non_Commercial_Unknown =>
    2.49 -      error (Pretty.string_of (Pretty.para
    2.50 -        ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
    2.51 -         \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
    2.52 -         \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
    2.53 -
    2.54 -end
    2.55 -
    2.56  val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
    2.57  
    2.58  local
    2.59 -  fun z3_make_command name () = if_z3_non_commercial (make_command name)
    2.60 -
    2.61    fun z3_options ctxt =
    2.62      ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    2.63       "smt.refine_inj_axioms=false",
    2.64 @@ -171,8 +129,8 @@
    2.65  val z3: SMT_Solver.solver_config = {
    2.66    name = "z3",
    2.67    class = select_class,
    2.68 -  avail = make_avail "Z3_NEW",
    2.69 -  command = z3_make_command "Z3_NEW",
    2.70 +  avail = make_avail "Z3",
    2.71 +  command = make_command "Z3",
    2.72    options = z3_options,
    2.73    smt_options = [(":produce-proofs", "true")],
    2.74    default_max_relevant = 350 (* FUDGE *),
     3.1 --- a/src/HOL/Tools/etc/options	Wed Apr 08 18:43:43 2015 +0200
     3.2 +++ b/src/HOL/Tools/etc/options	Wed Apr 08 18:47:38 2015 +0200
     3.3 @@ -32,8 +32,5 @@
     3.4  public option sledgehammer_timeout : int = 30
     3.5    -- "ATPs will be interrupted after this time (in seconds)"
     3.6  
     3.7 -public option z3_non_commercial : string = "unknown"
     3.8 -  -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     3.9 -
    3.10  public option MaSh : string = "sml"
    3.11    -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"