1(*  Title:      HOL/Tools/SMT/smt_config.ML
2    Author:     Sascha Boehme, TU Muenchen
3
4Configuration options and diagnostic tools for SMT.
5*)
6
7signature SMT_CONFIG =
8sig
9  (*solver*)
10  type solver_info = {
11    name: string,
12    class: Proof.context -> SMT_Util.class,
13    avail: unit -> bool,
14    options: Proof.context -> string list }
15  val add_solver: solver_info -> Context.generic -> Context.generic
16  val set_solver_options: string * string -> Context.generic -> Context.generic
17  val is_available: Proof.context -> string -> bool
18  val available_solvers_of: Proof.context -> string list
19  val select_solver: string -> Context.generic -> Context.generic
20  val solver_of: Proof.context -> string
21  val solver_class_of: Proof.context -> SMT_Util.class
22  val solver_options_of: Proof.context -> string list
23
24  (*options*)
25  val oracle: bool Config.T
26  val timeout: real Config.T
27  val reconstruction_step_timeout: real Config.T
28  val random_seed: int Config.T
29  val read_only_certificates: bool Config.T
30  val verbose: bool Config.T
31  val trace: bool Config.T
32  val statistics: bool Config.T
33  val monomorph_limit: int Config.T
34  val monomorph_instances: int Config.T
35  val explicit_application: int Config.T
36  val higher_order: bool Config.T
37  val nat_as_int: bool Config.T
38  val infer_triggers: bool Config.T
39  val debug_files: string Config.T
40  val sat_solver: string Config.T
41
42  (*tools*)
43  val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
44  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
45
46  (*diagnostics*)
47  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
48  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
49  val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
50  val veriT_msg: Proof.context -> (unit -> 'a) -> unit
51
52  (*certificates*)
53  val select_certificates: string -> Context.generic -> Context.generic
54  val certificates_of: Proof.context -> Cache_IO.cache option
55
56  (*setup*)
57  val print_setup: Proof.context -> unit
58end;
59
60structure SMT_Config: SMT_CONFIG =
61struct
62
63(* solver *)
64
65type solver_info = {
66  name: string,
67  class: Proof.context -> SMT_Util.class,
68  avail: unit -> bool,
69  options: Proof.context -> string list}
70
71type data = {
72  solvers: (solver_info * string list) Symtab.table,
73  solver: string option,
74  certs: Cache_IO.cache option}
75
76fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs}
77
78val empty_data = mk_data Symtab.empty NONE NONE
79
80fun solvers_of ({solvers, ...}: data) = solvers
81fun solver_of ({solver, ...}: data) = solver
82fun certs_of ({certs, ...}: data) = certs
83
84fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs
85fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs
86fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c
87
88fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) =
89  mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2))
90
91structure Data = Generic_Data
92(
93  type T = data
94  val empty = empty_data
95  val extend = I
96  val merge = merge_data
97)
98
99fun set_solver_options (name, options) =
100  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
101  in Data.map (map_solvers (Symtab.map_entry name (apsnd (K opts)))) end
102
103fun add_solver (info as {name, ...} : solver_info) context =
104  if Symtab.defined (solvers_of (Data.get context)) name then
105    error ("Solver already registered: " ^ quote name)
106  else
107    context
108    |> Data.map (map_solvers (Symtab.update (name, (info, []))))
109    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
110        (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
111          (Thm.declaration_attribute o K o set_solver_options o pair name))
112        ("additional command line options for SMT solver " ^ quote name))
113
114fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
115
116fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt))
117
118fun is_available ctxt name =
119  (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of
120    SOME ({avail, ...}, _) => avail ()
121  | NONE => false)
122
123fun available_solvers_of ctxt =
124  filter (is_available ctxt) (all_solvers_of ctxt)
125
126fun warn_solver (Context.Proof ctxt) name =
127      if Context_Position.is_visible ctxt then
128        warning ("The SMT solver " ^ quote name ^ " is not installed")
129      else ()
130  | warn_solver _ _ = ()
131
132fun select_solver name context =
133  let
134    val ctxt = Context.proof_of context
135    val upd = Data.map (map_solver (K (SOME name)))
136  in
137    if not (member (op =) (all_solvers_of ctxt) name) then
138      error ("Trying to select unknown solver: " ^ quote name)
139    else if not (is_available ctxt name) then
140      (warn_solver context name; upd context)
141    else upd context
142  end
143
144fun no_solver_err () = error "No SMT solver selected"
145
146fun solver_of ctxt =
147  (case solver_name_of ctxt of
148    SOME name => name
149  | NONE => no_solver_err ())
150
151fun solver_info_of default select ctxt =
152  (case solver_name_of ctxt of
153    NONE => default ()
154  | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name))
155
156fun solver_class_of ctxt =
157  let fun class_of ({class, ...}: solver_info, _) = class ctxt
158  in solver_info_of no_solver_err (class_of o the) ctxt end
159
160fun solver_options_of ctxt =
161  let
162    fun all_options NONE = []
163      | all_options (SOME ({options, ...} : solver_info, opts)) =
164          opts @ options ctxt
165  in solver_info_of (K []) all_options ctxt end
166
167val setup_solver =
168  Attrib.setup \<^binding>\<open>smt_solver\<close>
169    (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
170      (Thm.declaration_attribute o K o select_solver))
171    "SMT solver configuration"
172
173
174(* options *)
175
176val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
177val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 30.0)
178val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
179val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
180val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
181val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
182val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
183val trace_veriT = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
184val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
185val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
186val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
187val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
188val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
189val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
190val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
191val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
192val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
193
194
195(* diagnostics *)
196
197fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
198
199fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
200fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
201fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
202
203fun veriT_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_veriT) then ignore(x ()) else ()
204
205
206(* tools *)
207
208fun with_time_limit ctxt timeout_config f x =
209  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
210    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
211
212fun with_timeout ctxt = with_time_limit ctxt timeout
213
214
215(* certificates *)
216
217val certificates_of = certs_of o Data.get o Context.Proof
218
219val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of
220
221fun select_certificates name context = context |> Data.map (put_certs (
222  if name = "" then NONE
223  else
224    Path.explode name
225    |> Path.append (Resources.master_directory (Context.theory_of context))
226    |> SOME o Cache_IO.unsynchronized_init))
227
228val setup_certificates =
229  Attrib.setup \<^binding>\<open>smt_certificates\<close>
230    (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
231      (Thm.declaration_attribute o K o select_certificates))
232    "SMT certificates configuration"
233
234
235(* setup *)
236
237val _ = Theory.setup (
238  setup_solver #>
239  setup_certificates)
240
241fun print_setup ctxt =
242  let
243    fun string_of_bool b = if b then "true" else "false"
244
245    val names = available_solvers_of ctxt
246    val ns = if null names then ["(none)"] else sort_strings names
247    val n = the_default "(none)" (solver_name_of ctxt)
248    val opts = solver_options_of ctxt
249
250    val t = string_of_real (Config.get ctxt timeout)
251
252    val certs_filename =
253      (case get_certificates_path ctxt of
254        SOME path => Path.print path
255      | NONE => "(disabled)")
256  in
257    Pretty.writeln (Pretty.big_list "SMT setup:" [
258      Pretty.str ("Current SMT solver: " ^ n),
259      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
260      Pretty.str_list "Available SMT solvers: "  "" ns,
261      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
262      Pretty.str ("With proofs: " ^
263        string_of_bool (not (Config.get ctxt oracle))),
264      Pretty.str ("Certificates cache: " ^ certs_filename),
265      Pretty.str ("Fixed certificates: " ^
266        string_of_bool (Config.get ctxt read_only_certificates))])
267  end
268
269val _ =
270  Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
271    "show the available SMT solvers, the currently selected SMT solver, \
272    \and the values of SMT configuration options"
273    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
274
275end;
276