src/HOL/Tools/SMT/smt_solver.ML
changeset 41065 13424972ade4
parent 41062 304cfdbc6475
parent 41041 ec2734f34d0f
child 41121 5c5d05963f93
equal deleted inserted replaced
41064:0c447a17770a 41065:13424972ade4
   213       tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   213       tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   214         (map (Display.pretty_thm ctxt) thms)))
   214         (map (Display.pretty_thm ctxt) thms)))
   215     else ()
   215     else ()
   216   end
   216   end
   217 
   217 
   218 fun gen_solver name info rm ctxt irules =
   218 
       
   219 
       
   220 (* registry *)
       
   221 
       
   222 type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
       
   223 
       
   224 type solver_info = {
       
   225   env_var: string,
       
   226   is_remote: bool,
       
   227   options: Proof.context -> string list,
       
   228   interface: interface,
       
   229   reconstruct: string list * SMT_Translate.recon -> Proof.context ->
       
   230     (int list * thm) * Proof.context,
       
   231   default_max_relevant: int }
       
   232 
       
   233 fun gen_solver name (info : solver_info) rm ctxt irules =
   219   let
   234   let
   220     val {env_var, is_remote, options, interface, reconstruct, ...} = info
   235     val {env_var, is_remote, options, interface, reconstruct, ...} = info
   221     val {extra_norm, translate, ...} = interface
   236     val {extra_norm, translate, ...} = interface
   222     val (with_datatypes, translate') =
   237     val (with_datatypes, translate') =
   223       set_has_datatypes (Config.get ctxt C.datatypes) translate
   238       set_has_datatypes (Config.get ctxt C.datatypes) translate
   231     |> singleton (ProofContext.export ctxt' ctxt)
   246     |> singleton (ProofContext.export ctxt' ctxt)
   232     |> discharge_definitions
   247     |> discharge_definitions
   233     |> tap (fn _ => trace_assumptions ctxt irules idxs)
   248     |> tap (fn _ => trace_assumptions ctxt irules idxs)
   234     |> pair idxs)
   249     |> pair idxs)
   235   end
   250   end
   236 
       
   237 
       
   238 
       
   239 (* registry *)
       
   240 
       
   241 type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
       
   242 
       
   243 type solver_info = {
       
   244   env_var: string,
       
   245   is_remote: bool,
       
   246   options: Proof.context -> string list,
       
   247   interface: interface,
       
   248   reconstruct: string list * SMT_Translate.recon -> Proof.context ->
       
   249     (int list * thm) * Proof.context,
       
   250   default_max_relevant: int }
       
   251 
   251 
   252 structure Solvers = Generic_Data
   252 structure Solvers = Generic_Data
   253 (
   253 (
   254   type T = solver_info Symtab.table
   254   type T = solver_info Symtab.table
   255   val empty = Symtab.empty
   255   val empty = Symtab.empty