author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 59966 | c01cea2ba71e |
permissions | -rw-r--r-- |
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 | 23 |
fun make_avail name () = getenv ("OLD_" ^ name ^ "_SOLVER") <> "" |
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 | 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 | 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 | 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 | 55 |
avail = make_avail "CVC3", |
56 |
command = make_command "CVC3", |
|
57 |
options = cvc3_options, |
|
58 |
default_max_relevant = 400 (* FUDGE *), |
|
59 |
supports_filter = false, |
|
60 |
outcome = |
|
61 |
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), |
|
62 |
cex_parser = NONE, |
|
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 | 73 |
avail = make_avail "YICES", |
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 | 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 | 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 | 116 |
error |
117 |
(Pretty.string_of |
|
118 |
(Pretty.para |
|
119 |
("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ |
|
120 |
\system option \"z3_non_commercial\" to \"yes\" (e.g. via \ |
|
121 |
\the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^ |
|
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 | 131 |
fun z3_make_command name () = if_z3_non_commercial (make_command name) |
41601 | 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 | 135 |
"MODEL=true", |
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 | 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 | 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 | 168 |
name = "z3", |
169 |
class = select_class, |
|
170 |
avail = make_avail "Z3", |
|
171 |
command = z3_make_command "Z3", |
|
172 |
options = z3_options, |
|
173 |
default_max_relevant = 350 (* FUDGE *), |
|
174 |
supports_filter = true, |
|
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 |