|
1 (* Title: HOL/Library/Old_SMT/old_smt_setup_solvers.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Setup SMT solvers. |
|
5 *) |
|
6 |
|
7 signature OLD_SMT_SETUP_SOLVERS = |
|
8 sig |
|
9 datatype z3_non_commercial = |
|
10 Z3_Non_Commercial_Unknown | |
|
11 Z3_Non_Commercial_Accepted | |
|
12 Z3_Non_Commercial_Declined |
|
13 val z3_non_commercial: unit -> z3_non_commercial |
|
14 val z3_with_extensions: bool Config.T |
|
15 val setup: theory -> theory |
|
16 end |
|
17 |
|
18 structure Old_SMT_Setup_Solvers: OLD_SMT_SETUP_SOLVERS = |
|
19 struct |
|
20 |
|
21 (* helper functions *) |
|
22 |
|
23 fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
|
24 |
|
25 fun make_command name () = [getenv (name ^ "_SOLVER")] |
|
26 |
|
27 fun outcome_of unsat sat unknown solver_name line = |
|
28 if String.isPrefix unsat line then Old_SMT_Solver.Unsat |
|
29 else if String.isPrefix sat line then Old_SMT_Solver.Sat |
|
30 else if String.isPrefix unknown line then Old_SMT_Solver.Unknown |
|
31 else raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ("Solver " ^ |
|
32 quote solver_name ^ " failed. Enable SMT tracing by setting the " ^ |
|
33 "configuration option " ^ quote (Config.name_of Old_SMT_Config.trace) ^ " and " ^ |
|
34 "see the trace for details.")) |
|
35 |
|
36 fun on_first_line test_outcome solver_name lines = |
|
37 let |
|
38 val empty_line = (fn "" => true | _ => false) |
|
39 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
|
40 val (l, ls) = split_first (snd (take_prefix empty_line lines)) |
|
41 in (test_outcome solver_name l, ls) end |
|
42 |
|
43 |
|
44 (* CVC3 *) |
|
45 |
|
46 local |
|
47 fun cvc3_options ctxt = [ |
|
48 "-seed", string_of_int (Config.get ctxt Old_SMT_Config.random_seed), |
|
49 "-lang", "smtlib", "-output-lang", "presentation", |
|
50 "-timeout", string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout))] |
|
51 in |
|
52 |
|
53 val cvc3: Old_SMT_Solver.solver_config = { |
|
54 name = "cvc3", |
|
55 class = K Old_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 } |
|
65 |
|
66 end |
|
67 |
|
68 |
|
69 (* Yices *) |
|
70 |
|
71 val yices: Old_SMT_Solver.solver_config = { |
|
72 name = "yices", |
|
73 class = K Old_SMTLIB_Interface.smtlibC, |
|
74 avail = make_avail "YICES", |
|
75 command = make_command "YICES", |
|
76 options = (fn ctxt => [ |
|
77 "--rand-seed=" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed), |
|
78 "--timeout=" ^ |
|
79 string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout)), |
|
80 "--smtlib"]), |
|
81 default_max_relevant = 350 (* FUDGE *), |
|
82 supports_filter = false, |
|
83 outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
84 cex_parser = NONE, |
|
85 reconstruct = NONE } |
|
86 |
|
87 |
|
88 (* Z3 *) |
|
89 |
|
90 datatype z3_non_commercial = |
|
91 Z3_Non_Commercial_Unknown | |
|
92 Z3_Non_Commercial_Accepted | |
|
93 Z3_Non_Commercial_Declined |
|
94 |
|
95 |
|
96 local |
|
97 val accepted = member (op =) ["yes", "Yes", "YES"] |
|
98 val declined = member (op =) ["no", "No", "NO"] |
|
99 in |
|
100 |
|
101 fun z3_non_commercial () = |
|
102 let |
|
103 val flag1 = Options.default_string @{system_option z3_non_commercial} |
|
104 val flag2 = getenv "Z3_NON_COMMERCIAL" |
|
105 in |
|
106 if accepted flag1 then Z3_Non_Commercial_Accepted |
|
107 else if declined flag1 then Z3_Non_Commercial_Declined |
|
108 else if accepted flag2 then Z3_Non_Commercial_Accepted |
|
109 else if declined flag2 then Z3_Non_Commercial_Declined |
|
110 else Z3_Non_Commercial_Unknown |
|
111 end |
|
112 |
|
113 fun if_z3_non_commercial f = |
|
114 (case z3_non_commercial () of |
|
115 Z3_Non_Commercial_Accepted => f () |
|
116 | Z3_Non_Commercial_Declined => |
|
117 error (Pretty.string_of (Pretty.para |
|
118 "The SMT solver Z3 may only be used for non-commercial applications.")) |
|
119 | Z3_Non_Commercial_Unknown => |
|
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"))) |
|
127 |
|
128 end |
|
129 |
|
130 |
|
131 val z3_with_extensions = |
|
132 Attrib.setup_config_bool @{binding z3_with_extensions} (K false) |
|
133 |
|
134 local |
|
135 fun z3_make_command name () = if_z3_non_commercial (make_command name) |
|
136 |
|
137 fun z3_options ctxt = |
|
138 ["-rs:" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed), |
|
139 "MODEL=true", |
|
140 "SOFT_TIMEOUT=" ^ |
|
141 string_of_int (Real.ceil (1000.0 * Config.get ctxt Old_SMT_Config.timeout)), |
|
142 "-smt"] |
|
143 |> not (Config.get ctxt Old_SMT_Config.oracle) ? |
|
144 append ["DISPLAY_PROOF=true", "PROOF_MODE=2"] |
|
145 |
|
146 fun z3_on_first_or_last_line solver_name lines = |
|
147 let |
|
148 fun junk l = |
|
149 if String.isPrefix "WARNING: Out of allocated virtual memory" l |
|
150 then raise Old_SMT_Failure.SMT Old_SMT_Failure.Out_Of_Memory |
|
151 else |
|
152 String.isPrefix "WARNING" l orelse |
|
153 String.isPrefix "ERROR" l orelse |
|
154 forall Symbol.is_ascii_blank (Symbol.explode l) |
|
155 val lines = filter_out junk lines |
|
156 fun outcome split = |
|
157 the_default ("", []) (try split lines) |
|
158 |>> outcome_of "unsat" "sat" "unknown" solver_name |
|
159 in |
|
160 (* Starting with version 4.0, Z3 puts the outcome on the first line of the |
|
161 output rather than on the last line. *) |
|
162 outcome (fn lines => (hd lines, tl lines)) |
|
163 handle Old_SMT_Failure.SMT _ => outcome (swap o split_last) |
|
164 end |
|
165 |
|
166 fun select_class ctxt = |
|
167 if Config.get ctxt z3_with_extensions then Old_Z3_Interface.smtlib_z3C |
|
168 else Old_SMTLIB_Interface.smtlibC |
|
169 in |
|
170 |
|
171 val z3: Old_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 Old_Z3_Model.parse_counterex, |
|
181 reconstruct = SOME Old_Z3_Proof_Reconstruction.reconstruct } |
|
182 |
|
183 end |
|
184 |
|
185 |
|
186 (* overall setup *) |
|
187 |
|
188 val setup = |
|
189 Old_SMT_Solver.add_solver cvc3 #> |
|
190 Old_SMT_Solver.add_solver yices #> |
|
191 Old_SMT_Solver.add_solver z3 |
|
192 |
|
193 end |