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