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