author | blanchet |
Thu, 28 Aug 2014 00:40:37 +0200 | |
changeset 58055 | 625bdd5c70b2 |
parent 56467 | src/HOL/Tools/SMT/smt_setup_solvers.ML@8d7d6f17c6a7 |
permissions | -rw-r--r-- |
58055 | 1 |
(* Title: HOL/Library/SMT/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 |
|
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
|
7 |
signature SMT_SETUP_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
|
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 |
|
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
|
18 |
structure SMT_Setup_Solvers: SMT_SETUP_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
|
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 |
|
55049 | 23 |
fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
24 |
|
55049 | 25 |
fun make_command name () = [getenv (name ^ "_SOLVER")] |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
26 |
|
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
|
27 |
fun outcome_of unsat sat unknown solver_name line = |
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
|
28 |
if String.isPrefix unsat line then SMT_Solver.Unsat |
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
|
29 |
else if String.isPrefix sat line then SMT_Solver.Sat |
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
|
30 |
else if String.isPrefix unknown line then SMT_Solver.Unknown |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40276
diff
changeset
|
31 |
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ |
40276 | 32 |
quote solver_name ^ " failed. Enable SMT tracing by setting the " ^ |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42075
diff
changeset
|
33 |
"configuration option " ^ quote (Config.name_of 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
|
34 |
"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
|
35 |
|
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 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
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
|
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 |
|
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 |
(* 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
|
45 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
46 |
local |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
47 |
fun cvc3_options ctxt = [ |
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
40981
diff
changeset
|
48 |
"-seed", string_of_int (Config.get ctxt SMT_Config.random_seed), |
49980 | 49 |
"-lang", "smtlib", "-output-lang", "presentation", |
50 |
"-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))] |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
51 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
52 |
|
55049 | 53 |
val cvc3: SMT_Solver.solver_config = { |
54 |
name = "cvc3", |
|
55 |
class = K SMTLIB_Interface.smtlibC, |
|
56 |
avail = make_avail "CVC3", |
|
57 |
command = make_command "CVC3", |
|
58 |
options = cvc3_options, |
|
59 |
default_max_relevant = 400 (* FUDGE *), |
|
60 |
supports_filter = false, |
|
61 |
outcome = |
|
62 |
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), |
|
63 |
cex_parser = NONE, |
|
64 |
reconstruct = NONE } |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
65 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
66 |
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
|
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 |
|
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 |
(* 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
|
70 |
|
55049 | 71 |
val yices: 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
|
72 |
name = "yices", |
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
|
73 |
class = K SMTLIB_Interface.smtlibC, |
55049 | 74 |
avail = make_avail "YICES", |
75 |
command = make_command "YICES", |
|
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
40981
diff
changeset
|
76 |
options = (fn ctxt => [ |
41235
975db7bd23e3
fixed the command-line syntax for setting Yices' random seed
boehmes
parents:
41130
diff
changeset
|
77 |
"--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
49980 | 78 |
"--timeout=" ^ |
79 |
string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)), |
|
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
40981
diff
changeset
|
80 |
"--smtlib"]), |
47645
8ca67d2b21c2
tuned "max_relevant" defaults for SMT solvers based on Judgment Day
blanchet
parents:
45025
diff
changeset
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
cex_parser = NONE, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
85 |
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
|
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 |
|
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 |
(* 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
|
89 |
|
42075
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
90 |
datatype z3_non_commercial = |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
91 |
Z3_Non_Commercial_Unknown | |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
92 |
Z3_Non_Commercial_Accepted | |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
93 |
Z3_Non_Commercial_Declined |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
94 |
|
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
95 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
96 |
local |
42075
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
97 |
val accepted = member (op =) ["yes", "Yes", "YES"] |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
98 |
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
|
99 |
in |
41601 | 100 |
|
42075
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
101 |
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
|
102 |
let |
56467 | 103 |
val flag1 = Options.default_string @{system_option 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
|
104 |
val flag2 = getenv "Z3_NON_COMMERCIAL" |
e6cfa56a8bcd
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents:
55007
diff
changeset
|
105 |
in |
e6cfa56a8bcd
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents:
55007
diff
changeset
|
106 |
if accepted flag1 then Z3_Non_Commercial_Accepted |
e6cfa56a8bcd
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents:
55007
diff
changeset
|
107 |
else if declined flag1 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
|
108 |
else if accepted flag2 then Z3_Non_Commercial_Accepted |
e6cfa56a8bcd
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
wenzelm
parents:
55007
diff
changeset
|
109 |
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
|
110 |
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
|
111 |
end |
42074
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
112 |
|
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
113 |
fun if_z3_non_commercial f = |
42075
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
114 |
(case z3_non_commercial () of |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
115 |
Z3_Non_Commercial_Accepted => f () |
c8be98f12b1c
Z3 non-commercial usage may explicitly be declined
boehmes
parents:
42074
diff
changeset
|
116 |
| Z3_Non_Commercial_Declined => |
55007
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
50856
diff
changeset
|
117 |
error (Pretty.string_of (Pretty.para |
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
50856
diff
changeset
|
118 |
"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
|
119 |
| Z3_Non_Commercial_Unknown => |
55806 | 120 |
error |
121 |
(Pretty.string_of |
|
122 |
(Pretty.para |
|
123 |
("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ |
|
124 |
\system option \"z3_non_commercial\" to \"yes\" (e.g. via \ |
|
125 |
\the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^ |
|
126 |
"\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
|
127 |
|
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
128 |
end |
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
129 |
|
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
130 |
|
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
|
131 |
val z3_with_extensions = |
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
|
132 |
Attrib.setup_config_bool @{binding z3_with_extensions} (K false) |
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
|
133 |
|
42074
621321627d0f
export status function to query whether Z3 has been activated for usage within Isabelle
boehmes
parents:
41800
diff
changeset
|
134 |
local |
55049 | 135 |
fun z3_make_command name () = if_z3_non_commercial (make_command name) |
41601 | 136 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
137 |
fun z3_options ctxt = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
138 |
["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
49980 | 139 |
"MODEL=true", |
140 |
"SOFT_TIMEOUT=" ^ |
|
50661
acea12b85315
Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently
blanchet
parents:
49980
diff
changeset
|
141 |
string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout)), |
49980 | 142 |
"-smt"] |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
143 |
|> not (Config.get ctxt SMT_Config.oracle) ? |
49980 | 144 |
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
|
145 |
|
47940
4ef90b51641e
robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents:
47645
diff
changeset
|
146 |
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
|
147 |
let |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
148 |
fun junk l = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
149 |
if String.isPrefix "WARNING: Out of allocated virtual memory" l |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
150 |
then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
151 |
else |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
152 |
String.isPrefix "WARNING" l orelse |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
153 |
String.isPrefix "ERROR" l orelse |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
|>> 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
|
159 |
in |
47940
4ef90b51641e
robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents:
47645
diff
changeset
|
160 |
(* 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
|
161 |
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
|
162 |
outcome (fn lines => (hd lines, tl lines)) |
4ef90b51641e
robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
blanchet
parents:
47645
diff
changeset
|
163 |
handle 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
|
164 |
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
|
165 |
|
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
|
166 |
fun select_class ctxt = |
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
|
167 |
if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C |
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
|
168 |
else SMTLIB_Interface.smtlibC |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
169 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
170 |
|
55049 | 171 |
val z3: SMT_Solver.solver_config = { |
172 |
name = "z3", |
|
173 |
class = select_class, |
|
174 |
avail = make_avail "Z3", |
|
175 |
command = z3_make_command "Z3", |
|
176 |
options = z3_options, |
|
177 |
default_max_relevant = 350 (* FUDGE *), |
|
178 |
supports_filter = true, |
|
179 |
outcome = z3_on_first_or_last_line, |
|
180 |
cex_parser = SOME Z3_Model.parse_counterex, |
|
181 |
reconstruct = SOME Z3_Proof_Reconstruction.reconstruct } |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
182 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41235
diff
changeset
|
183 |
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
|
184 |
|
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
|
185 |
|
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
|
186 |
(* 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
|
187 |
|
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 |
val setup = |
55049 | 189 |
SMT_Solver.add_solver cvc3 #> |
190 |
SMT_Solver.add_solver yices #> |
|
191 |
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
|
192 |
|
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
|
193 |
end |