src/HOL/Library/Old_SMT/old_smt_config.ML
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 58059 4e477dcd050a
child 58893 9e0ecb66d6a7
permissions -rw-r--r--
simpler proof
     1 (*  Title:      HOL/Library/Old_SMT/old_smt_config.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Configuration options and diagnostic tools for SMT.
     5 *)
     6 
     7 signature OLD_SMT_CONFIG =
     8 sig
     9   (*solver*)
    10   type solver_info = {
    11     name: string,
    12     class: Proof.context -> Old_SMT_Utils.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 -> Old_SMT_Utils.class
    22   val solver_options_of: Proof.context -> string list
    23 
    24   (*options*)
    25   val oracle: bool Config.T
    26   val datatypes: bool Config.T
    27   val 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 trace_used_facts: bool Config.T
    33   val monomorph_limit: int Config.T
    34   val monomorph_instances: int Config.T
    35   val infer_triggers: bool Config.T
    36   val filter_only_facts: bool Config.T
    37   val debug_files: string Config.T
    38 
    39   (*tools*)
    40   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
    41 
    42   (*diagnostics*)
    43   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
    44   val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
    45 
    46   (*certificates*)
    47   val select_certificates: string -> Context.generic -> Context.generic
    48   val certificates_of: Proof.context -> Cache_IO.cache option
    49 
    50   (*setup*)
    51   val setup: theory -> theory
    52   val print_setup: Proof.context -> unit
    53 end
    54 
    55 structure Old_SMT_Config: OLD_SMT_CONFIG =
    56 struct
    57 
    58 (* solver *)
    59 
    60 type solver_info = {
    61   name: string,
    62   class: Proof.context -> Old_SMT_Utils.class,
    63   avail: unit -> bool,
    64   options: Proof.context -> string list }
    65 
    66 (* FIXME just one data slot (record) per program unit *)
    67 structure Solvers = Generic_Data
    68 (
    69   type T = (solver_info * string list) Symtab.table * string option
    70   val empty = (Symtab.empty, NONE)
    71   val extend = I
    72   fun merge ((ss1, s1), (ss2, s2)) =
    73     (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
    74 )
    75 
    76 fun set_solver_options (name, options) =
    77   let val opts = String.tokens (Symbol.is_ascii_blank o str) options
    78   in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
    79 
    80 fun add_solver (info as {name, ...} : solver_info) context =
    81   if Symtab.defined (fst (Solvers.get context)) name then
    82     error ("Solver already registered: " ^ quote name)
    83   else
    84     context
    85     |> Solvers.map (apfst (Symtab.update (name, (info, []))))
    86     |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options"))
    87         (Scan.lift (@{keyword "="} |-- Args.name) >>
    88           (Thm.declaration_attribute o K o set_solver_options o pair name))
    89         ("Additional command line options for SMT solver " ^ quote name))
    90 
    91 fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
    92 
    93 fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
    94 
    95 fun is_available ctxt name =
    96   (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
    97     SOME ({avail, ...}, _) => avail ()
    98   | NONE => false)
    99 
   100 fun available_solvers_of ctxt =
   101   filter (is_available ctxt) (all_solvers_of ctxt)
   102 
   103 fun warn_solver (Context.Proof ctxt) name =
   104       if Context_Position.is_visible ctxt then
   105         warning ("The SMT solver " ^ quote name ^ " is not installed.")
   106       else ()
   107   | warn_solver _ _ = ();
   108 
   109 fun select_solver name context =
   110   let
   111     val ctxt = Context.proof_of context
   112     val upd = Solvers.map (apsnd (K (SOME name)))
   113   in
   114     if not (member (op =) (all_solvers_of ctxt) name) then
   115       error ("Trying to select unknown solver: " ^ quote name)
   116     else if not (is_available ctxt name) then
   117       (warn_solver context name; upd context)
   118     else upd context
   119   end
   120 
   121 fun no_solver_err () = error "No SMT solver selected"
   122 
   123 fun solver_of ctxt =
   124   (case solver_name_of ctxt of
   125     SOME name => name
   126   | NONE => no_solver_err ())
   127 
   128 fun solver_info_of default select ctxt =
   129   (case Solvers.get (Context.Proof ctxt) of
   130     (solvers, SOME name) => select (Symtab.lookup solvers name)
   131   | (_, NONE) => default ())
   132 
   133 fun solver_class_of ctxt =
   134   let fun class_of ({class, ...}: solver_info, _) = class ctxt
   135   in solver_info_of no_solver_err (class_of o the) ctxt end
   136 
   137 fun solver_options_of ctxt =
   138   let
   139     fun all_options NONE = []
   140       | all_options (SOME ({options, ...} : solver_info, opts)) =
   141           opts @ options ctxt
   142   in solver_info_of (K []) all_options ctxt end
   143 
   144 val setup_solver =
   145   Attrib.setup @{binding old_smt_solver}
   146     (Scan.lift (@{keyword "="} |-- Args.name) >>
   147       (Thm.declaration_attribute o K o select_solver))
   148     "SMT solver configuration"
   149 
   150 
   151 (* options *)
   152 
   153 val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true)
   154 val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false)
   155 val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0)
   156 val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1)
   157 val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false)
   158 val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true)
   159 val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false)
   160 val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false)
   161 val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10)
   162 val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500)
   163 val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false)
   164 val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false)
   165 val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "")
   166 
   167 
   168 (* diagnostics *)
   169 
   170 fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
   171 
   172 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
   173 
   174 fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
   175 
   176 
   177 (* tools *)
   178 
   179 fun with_timeout ctxt f x =
   180   TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
   181   handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
   182 
   183 
   184 (* certificates *)
   185 
   186 (* FIXME just one data slot (record) per program unit *)
   187 structure Certificates = Generic_Data
   188 (
   189   type T = Cache_IO.cache option
   190   val empty = NONE
   191   val extend = I
   192   fun merge (s, _) = s  (* FIXME merge options!? *)
   193 )
   194 
   195 val get_certificates_path =
   196   Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
   197 
   198 fun select_certificates name context = context |> Certificates.put (
   199   if name = "" then NONE
   200   else
   201     Path.explode name
   202     |> Path.append (Resources.master_directory (Context.theory_of context))
   203     |> SOME o Cache_IO.unsynchronized_init)
   204 
   205 val certificates_of = Certificates.get o Context.Proof
   206 
   207 val setup_certificates =
   208   Attrib.setup @{binding old_smt_certificates}
   209     (Scan.lift (@{keyword "="} |-- Args.name) >>
   210       (Thm.declaration_attribute o K o select_certificates))
   211     "SMT certificates configuration"
   212 
   213 
   214 (* setup *)
   215 
   216 val setup =
   217   setup_solver #>
   218   setup_certificates
   219 
   220 fun print_setup ctxt =
   221   let
   222     fun string_of_bool b = if b then "true" else "false"
   223 
   224     val names = available_solvers_of ctxt
   225     val ns = if null names then ["(none)"] else sort_strings names
   226     val n = the_default "(none)" (solver_name_of ctxt)
   227     val opts = solver_options_of ctxt
   228     
   229     val t = string_of_real (Config.get ctxt timeout)
   230 
   231     val certs_filename =
   232       (case get_certificates_path ctxt of
   233         SOME path => Path.print path
   234       | NONE => "(disabled)")
   235   in
   236     Pretty.writeln (Pretty.big_list "SMT setup:" [
   237       Pretty.str ("Current SMT solver: " ^ n),
   238       Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
   239       Pretty.str_list "Available SMT solvers: "  "" ns,
   240       Pretty.str ("Current timeout: " ^ t ^ " seconds"),
   241       Pretty.str ("With proofs: " ^
   242         string_of_bool (not (Config.get ctxt oracle))),
   243       Pretty.str ("Certificates cache: " ^ certs_filename),
   244       Pretty.str ("Fixed certificates: " ^
   245         string_of_bool (Config.get ctxt read_only_certificates))])
   246   end
   247 
   248 val _ =
   249   Outer_Syntax.improper_command @{command_spec "old_smt_status"}
   250     "show the available SMT solvers, the currently selected SMT solver, \
   251     \and the values of SMT configuration options"
   252     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
   253 
   254 end