1 (* Title: HOL/Tools/SMT2/smt2_systems.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Setup SMT solvers. |
|
5 *) |
|
6 |
|
7 signature SMT2_SYSTEMS = |
|
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_extensions: bool Config.T |
|
15 end; |
|
16 |
|
17 structure SMT2_Systems: SMT2_SYSTEMS = |
|
18 struct |
|
19 |
|
20 (* helper functions *) |
|
21 |
|
22 fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
|
23 |
|
24 fun make_command name () = [getenv (name ^ "_SOLVER")] |
|
25 |
|
26 fun outcome_of unsat sat unknown solver_name line = |
|
27 if String.isPrefix unsat line then SMT2_Solver.Unsat |
|
28 else if String.isPrefix sat line then SMT2_Solver.Sat |
|
29 else if String.isPrefix unknown line then SMT2_Solver.Unknown |
|
30 else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^ quote solver_name ^ |
|
31 " failed -- enable tracing using the " ^ quote (Config.name_of SMT2_Config.trace) ^ |
|
32 " option for details")) |
|
33 |
|
34 fun on_first_line test_outcome solver_name lines = |
|
35 let |
|
36 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
|
37 val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines)) |
|
38 in (test_outcome solver_name l, ls) end |
|
39 |
|
40 fun on_first_non_unsupported_line test_outcome solver_name lines = |
|
41 on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) |
|
42 |
|
43 (* CVC3 *) |
|
44 |
|
45 local |
|
46 fun cvc3_options ctxt = [ |
|
47 "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed), |
|
48 "-lang", "smt2", |
|
49 "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))] |
|
50 in |
|
51 |
|
52 val cvc3: SMT2_Solver.solver_config = { |
|
53 name = "cvc3", |
|
54 class = K SMTLIB2_Interface.smtlib2C, |
|
55 avail = make_avail "CVC3", |
|
56 command = make_command "CVC3", |
|
57 options = cvc3_options, |
|
58 smt_options = [], |
|
59 default_max_relevant = 400 (* FUDGE *), |
|
60 outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
61 parse_proof = NONE, |
|
62 replay = NONE } |
|
63 |
|
64 end |
|
65 |
|
66 |
|
67 (* CVC4 *) |
|
68 |
|
69 local |
|
70 fun cvc4_options ctxt = [ |
|
71 "--random-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
|
72 "--lang=smt2", |
|
73 "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT2_Config.timeout))] |
|
74 in |
|
75 |
|
76 val cvc4: SMT2_Solver.solver_config = { |
|
77 name = "cvc4", |
|
78 class = K SMTLIB2_Interface.smtlib2C, |
|
79 avail = make_avail "CVC4", |
|
80 command = make_command "CVC4", |
|
81 options = cvc4_options, |
|
82 smt_options = [], |
|
83 default_max_relevant = 400 (* FUDGE *), |
|
84 outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
85 parse_proof = NONE, |
|
86 replay = NONE } |
|
87 |
|
88 end |
|
89 |
|
90 (* veriT *) |
|
91 |
|
92 val veriT: SMT2_Solver.solver_config = { |
|
93 name = "veriT", |
|
94 class = K SMTLIB2_Interface.smtlib2C, |
|
95 avail = make_avail "VERIT", |
|
96 command = make_command "VERIT", |
|
97 options = (fn ctxt => [ |
|
98 "--proof-version=1", |
|
99 "--proof=-", |
|
100 "--proof-prune", |
|
101 "--proof-merge", |
|
102 "--disable-print-success", |
|
103 "--disable-banner", |
|
104 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]), |
|
105 smt_options = [], |
|
106 default_max_relevant = 120 (* FUDGE *), |
|
107 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" |
|
108 "warning : proof_done: status is still open"), |
|
109 parse_proof = SOME VeriT_Proof_Parse.parse_proof, |
|
110 replay = NONE } |
|
111 |
|
112 (* Z3 *) |
|
113 |
|
114 datatype z3_non_commercial = |
|
115 Z3_Non_Commercial_Unknown | |
|
116 Z3_Non_Commercial_Accepted | |
|
117 Z3_Non_Commercial_Declined |
|
118 |
|
119 local |
|
120 val accepted = member (op =) ["yes", "Yes", "YES"] |
|
121 val declined = member (op =) ["no", "No", "NO"] |
|
122 in |
|
123 |
|
124 fun z3_non_commercial () = |
|
125 let |
|
126 val flag1 = Options.default_string @{system_option z3_non_commercial} |
|
127 val flag2 = getenv "Z3_NON_COMMERCIAL" |
|
128 in |
|
129 if accepted flag1 then Z3_Non_Commercial_Accepted |
|
130 else if declined flag1 then Z3_Non_Commercial_Declined |
|
131 else if accepted flag2 then Z3_Non_Commercial_Accepted |
|
132 else if declined flag2 then Z3_Non_Commercial_Declined |
|
133 else Z3_Non_Commercial_Unknown |
|
134 end |
|
135 |
|
136 fun if_z3_non_commercial f = |
|
137 (case z3_non_commercial () of |
|
138 Z3_Non_Commercial_Accepted => f () |
|
139 | Z3_Non_Commercial_Declined => |
|
140 error (Pretty.string_of (Pretty.para |
|
141 "The SMT solver Z3 may be used only for non-commercial applications.")) |
|
142 | Z3_Non_Commercial_Unknown => |
|
143 error (Pretty.string_of (Pretty.para |
|
144 ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ |
|
145 \system option \"z3_non_commercial\" to \"yes\" (e.g. via \ |
|
146 \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")))) |
|
147 |
|
148 end |
|
149 |
|
150 val z3_extensions = Attrib.setup_config_bool @{binding z3_new_extensions} (K false) |
|
151 |
|
152 local |
|
153 fun z3_make_command name () = if_z3_non_commercial (make_command name) |
|
154 |
|
155 fun z3_options ctxt = |
|
156 ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
|
157 "smt.refine_inj_axioms=false", |
|
158 "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), |
|
159 "-smt2"] |
|
160 |
|
161 fun select_class ctxt = |
|
162 if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C |
|
163 else SMTLIB2_Interface.smtlib2C |
|
164 in |
|
165 |
|
166 val z3: SMT2_Solver.solver_config = { |
|
167 name = "z3", |
|
168 class = select_class, |
|
169 avail = make_avail "Z3_NEW", |
|
170 command = z3_make_command "Z3_NEW", |
|
171 options = z3_options, |
|
172 smt_options = [(":produce-proofs", "true")], |
|
173 default_max_relevant = 350 (* FUDGE *), |
|
174 outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
175 parse_proof = SOME Z3_New_Replay.parse_proof, |
|
176 replay = SOME Z3_New_Replay.replay } |
|
177 |
|
178 end |
|
179 |
|
180 |
|
181 (* overall setup *) |
|
182 |
|
183 val _ = Theory.setup ( |
|
184 SMT2_Solver.add_solver cvc3 #> |
|
185 SMT2_Solver.add_solver cvc4 #> |
|
186 SMT2_Solver.add_solver veriT #> |
|
187 SMT2_Solver.add_solver z3) |
|
188 |
|
189 end; |
|