src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 59966 c01cea2ba71e
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_setup_solvers.ML
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     3
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     4
Setup SMT solvers.
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     5
*)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_SETUP_SOLVERS =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
     8
sig
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
     9
  datatype z3_non_commercial =
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    10
    Z3_Non_Commercial_Unknown |
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    11
    Z3_Non_Commercial_Accepted |
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    12
    Z3_Non_Commercial_Declined
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    13
  val z3_non_commercial: unit -> z3_non_commercial
48069
e9b2782c4f99 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents: 48043
diff changeset
    14
  val z3_with_extensions: bool Config.T
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    15
  val setup: theory -> theory
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    16
end
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    17
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    18
structure Old_SMT_Setup_Solvers: OLD_SMT_SETUP_SOLVERS =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    19
struct
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    20
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    21
(* helper functions *)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    22
58063
663ae2463f32 added 'OLD_' prefix in front of old solvers
blanchet
parents: 58059
diff changeset
    23
fun make_avail name () = getenv ("OLD_" ^ name ^ "_SOLVER") <> ""
663ae2463f32 added 'OLD_' prefix in front of old solvers
blanchet
parents: 58059
diff changeset
    24
fun make_command name () = [getenv ("OLD_" ^ name ^ "_SOLVER")]
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    25
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    26
fun outcome_of unsat sat unknown solver_name line =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    27
  if String.isPrefix unsat line then Old_SMT_Solver.Unsat
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    28
  else if String.isPrefix sat line then Old_SMT_Solver.Sat
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    29
  else if String.isPrefix unknown line then Old_SMT_Solver.Unknown
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    30
  else raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ("Solver " ^
40276
6efa052b9213 clarified error message
boehmes
parents: 40208
diff changeset
    31
    quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    32
    "configuration option " ^ quote (Config.name_of Old_SMT_Config.trace) ^ " and " ^
40981
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40424
diff changeset
    33
    "see the trace for details."))
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    34
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    35
fun on_first_line test_outcome solver_name lines =
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    36
  let
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    37
    val empty_line = (fn "" => true | _ => false)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    38
    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
48902
44a6967240b7 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents: 48391
diff changeset
    39
    val (l, ls) = split_first (snd (take_prefix empty_line lines))
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    40
  in (test_outcome solver_name l, ls) end
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    41
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    42
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    43
(* CVC3 *)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    44
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    45
local
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    46
  fun cvc3_options ctxt = [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    47
    "-seed", string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
49980
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
    48
    "-lang", "smtlib", "-output-lang", "presentation",
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    49
    "-timeout", string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout))]
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    50
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    51
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    52
val cvc3: Old_SMT_Solver.solver_config = {
55049
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    53
  name = "cvc3",
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    54
  class = K Old_SMTLIB_Interface.smtlibC,
55049
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    55
  avail = make_avail "CVC3",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    56
  command = make_command "CVC3",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    57
  options = cvc3_options,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    58
  default_max_relevant = 400 (* FUDGE *),
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    59
  supports_filter = false,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    60
  outcome =
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    61
    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    62
  cex_parser = NONE,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    63
  reconstruct = NONE }
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    64
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    65
end
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    66
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    67
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    68
(* Yices *)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    69
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    70
val yices: Old_SMT_Solver.solver_config = {
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    71
  name = "yices",
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    72
  class = K Old_SMTLIB_Interface.smtlibC,
55049
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    73
  avail = make_avail "YICES",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
    74
  command = make_command "YICES",
41121
5c5d05963f93 added option to modify the random seed of SMT solvers
boehmes
parents: 40981
diff changeset
    75
  options = (fn ctxt => [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    76
    "--rand-seed=" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
49980
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
    77
    "--timeout=" ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    78
      string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout)),
41121
5c5d05963f93 added option to modify the random seed of SMT solvers
boehmes
parents: 40981
diff changeset
    79
    "--smtlib"]),
47645
8ca67d2b21c2 tuned "max_relevant" defaults for SMT solvers based on Judgment Day
blanchet
parents: 45025
diff changeset
    80
  default_max_relevant = 350 (* FUDGE *),
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    81
  supports_filter = false,
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    82
  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    83
  cex_parser = NONE,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    84
  reconstruct = NONE }
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    85
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    86
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    87
(* Z3 *)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
    88
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    89
datatype z3_non_commercial =
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    90
  Z3_Non_Commercial_Unknown |
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    91
  Z3_Non_Commercial_Accepted |
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    92
  Z3_Non_Commercial_Declined
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    93
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    94
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
    95
local
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    96
  val accepted = member (op =) ["yes", "Yes", "YES"]
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
    97
  val declined = member (op =) ["no", "No", "NO"]
42074
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
    98
in
41601
fda8511006f9 made Z3 the default SMT solver again
boehmes
parents: 41432
diff changeset
    99
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
   100
fun z3_non_commercial () =
55012
e6cfa56a8bcd fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents: 55007
diff changeset
   101
  let
59966
c01cea2ba71e updated 'old_smt' to loss of 'z3_non_commercial' option
blanchet
parents: 58063
diff changeset
   102
    val flag2 = getenv "OLD_Z3_NON_COMMERCIAL"
55012
e6cfa56a8bcd fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents: 55007
diff changeset
   103
  in
59966
c01cea2ba71e updated 'old_smt' to loss of 'z3_non_commercial' option
blanchet
parents: 58063
diff changeset
   104
    if accepted flag2 then Z3_Non_Commercial_Accepted
55012
e6cfa56a8bcd fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents: 55007
diff changeset
   105
    else if declined flag2 then Z3_Non_Commercial_Declined
e6cfa56a8bcd fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents: 55007
diff changeset
   106
    else Z3_Non_Commercial_Unknown
e6cfa56a8bcd fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents: 55007
diff changeset
   107
  end
42074
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   108
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   109
fun if_z3_non_commercial f =
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
   110
  (case z3_non_commercial () of
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
   111
    Z3_Non_Commercial_Accepted => f ()
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
   112
  | Z3_Non_Commercial_Declined =>
55007
0c07990363a3 activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents: 50856
diff changeset
   113
      error (Pretty.string_of (Pretty.para
0c07990363a3 activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents: 50856
diff changeset
   114
        "The SMT solver Z3 may only be used for non-commercial applications."))
42075
c8be98f12b1c Z3 non-commercial usage may explicitly be declined
boehmes
parents: 42074
diff changeset
   115
  | Z3_Non_Commercial_Unknown =>
55806
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   116
      error
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   117
        (Pretty.string_of
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   118
          (Pretty.para
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   119
            ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   120
             \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   121
             \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^
519625ec22a0 explicit link to Z3 license;
wenzelm
parents: 55049
diff changeset
   122
        "\n\nSee also " ^ Url.print (Url.explode "http://z3.codeplex.com/license")))
42074
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   123
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   124
end
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   125
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   126
48069
e9b2782c4f99 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents: 48043
diff changeset
   127
val z3_with_extensions =
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   128
  Attrib.setup_config_bool @{binding old_z3_with_extensions} (K false)
48069
e9b2782c4f99 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents: 48043
diff changeset
   129
42074
621321627d0f export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents: 41800
diff changeset
   130
local
55049
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   131
  fun z3_make_command name () = if_z3_non_commercial (make_command name)
41601
fda8511006f9 made Z3 the default SMT solver again
boehmes
parents: 41432
diff changeset
   132
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   133
  fun z3_options ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   134
    ["-rs:" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
49980
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
   135
      "MODEL=true",
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
   136
      "SOFT_TIMEOUT=" ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   137
        string_of_int (Real.ceil (1000.0 * Config.get ctxt Old_SMT_Config.timeout)),
49980
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
   138
      "-smt"]
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   139
    |> not (Config.get ctxt Old_SMT_Config.oracle) ?
49980
34b0464d7eef soft SMT timeout
blanchet
parents: 48902
diff changeset
   140
         append ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   141
47940
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   142
  fun z3_on_first_or_last_line solver_name lines =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   143
    let
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   144
      fun junk l =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   145
        if String.isPrefix "WARNING: Out of allocated virtual memory" l
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   146
        then raise Old_SMT_Failure.SMT Old_SMT_Failure.Out_Of_Memory
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   147
        else
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   148
          String.isPrefix "WARNING" l orelse
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   149
          String.isPrefix "ERROR" l orelse
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   150
          forall Symbol.is_ascii_blank (Symbol.explode l)
47940
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   151
      val lines = filter_out junk lines
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   152
      fun outcome split =
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   153
        the_default ("", []) (try split lines)
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   154
        |>> outcome_of "unsat" "sat" "unknown" solver_name
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   155
    in
47940
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   156
      (* Starting with version 4.0, Z3 puts the outcome on the first line of the
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   157
         output rather than on the last line. *)
4ef90b51641e robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents: 47645
diff changeset
   158
      outcome (fn lines => (hd lines, tl lines))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   159
      handle Old_SMT_Failure.SMT _ => outcome (swap o split_last)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   160
    end
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   161
48043
3ff2c76c9f64 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents: 47940
diff changeset
   162
  fun select_class ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   163
    if Config.get ctxt z3_with_extensions then Old_Z3_Interface.smtlib_z3C
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   164
    else Old_SMTLIB_Interface.smtlibC
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   165
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   166
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   167
val z3: Old_SMT_Solver.solver_config = {
55049
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   168
  name = "z3",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   169
  class = select_class,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   170
  avail = make_avail "Z3",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   171
  command = z3_make_command "Z3",
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   172
  options = z3_options,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   173
  default_max_relevant = 350 (* FUDGE *),
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   174
  supports_filter = true,
327eafb594ba removed obsolete remote_cvc3 and remote_z3
boehmes
parents: 55012
diff changeset
   175
  outcome = z3_on_first_or_last_line,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   176
  cex_parser = SOME Old_Z3_Model.parse_counterex,
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   177
  reconstruct = SOME Old_Z3_Proof_Reconstruction.reconstruct }
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   178
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41235
diff changeset
   179
end
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   180
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   181
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   182
(* overall setup *)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   183
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   184
val setup =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   185
  Old_SMT_Solver.add_solver cvc3 #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   186
  Old_SMT_Solver.add_solver yices #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   187
  Old_SMT_Solver.add_solver z3
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   188
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
diff changeset
   189
end