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