src/HOL/Tools/SMT/smt_solver.ML
changeset 41059 d2b1fc1b8e19
parent 40981 67f436af0638
child 41062 304cfdbc6475
equal deleted inserted replaced
41058:42e0a0bfef73 41059:d2b1fc1b8e19
     6 
     6 
     7 signature SMT_SOLVER =
     7 signature SMT_SOLVER =
     8 sig
     8 sig
     9   (*configuration*)
     9   (*configuration*)
    10   type interface = {
    10   type interface = {
       
    11     class: SMT_Config.class,
    11     extra_norm: SMT_Normalize.extra_norm,
    12     extra_norm: SMT_Normalize.extra_norm,
    12     translate: SMT_Translate.config }
    13     translate: SMT_Translate.config }
    13   datatype outcome = Unsat | Sat | Unknown
    14   datatype outcome = Unsat | Sat | Unknown
    14   type solver_config = {
    15   type solver_config = {
    15     name: string,
    16     name: string,
    55 
    56 
    56 
    57 
    57 (* configuration *)
    58 (* configuration *)
    58 
    59 
    59 type interface = {
    60 type interface = {
       
    61   class: SMT_Config.class,
    60   extra_norm: SMT_Normalize.extra_norm,
    62   extra_norm: SMT_Normalize.extra_norm,
    61   translate: SMT_Translate.config }
    63   translate: SMT_Translate.config }
    62 
    64 
    63 datatype outcome = Unsat | Sat | Unknown
    65 datatype outcome = Unsat | Sat | Unknown
    64 
    66 
   193   if Thm.nprems_of thm = 0 then thm
   195   if Thm.nprems_of thm = 0 then thm
   194   else discharge_definitions (@{thm reflexive} RS thm)
   196   else discharge_definitions (@{thm reflexive} RS thm)
   195 
   197 
   196 fun set_has_datatypes with_datatypes translate =
   198 fun set_has_datatypes with_datatypes translate =
   197   let
   199   let
   198     val {prefixes, header, strict, builtins, serialize} = translate
   200     val {prefixes, header, is_fol, has_datatypes, serialize} = translate
   199     val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
       
   200     val with_datatypes' = has_datatypes andalso with_datatypes
   201     val with_datatypes' = has_datatypes andalso with_datatypes
   201     val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
   202     val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
   202       builtin_fun=builtin_fun, has_datatypes=with_datatypes}
   203       has_datatypes=with_datatypes', serialize=serialize}
   203     val translate' = {prefixes=prefixes, header=header, strict=strict,
       
   204       builtins=builtins', serialize=serialize}
       
   205   in (with_datatypes', translate') end
   204   in (with_datatypes', translate') end
   206 
   205 
   207 fun trace_assumptions ctxt irules idxs =
   206 fun trace_assumptions ctxt irules idxs =
   208   let
   207   let
   209     val thms = filter (fn i => i >= 0) idxs
   208     val thms = filter (fn i => i >= 0) idxs
   217   end
   216   end
   218 
   217 
   219 fun gen_solver name info rm ctxt irules =
   218 fun gen_solver name info rm ctxt irules =
   220   let
   219   let
   221     val {env_var, is_remote, options, interface, reconstruct, ...} = info
   220     val {env_var, is_remote, options, interface, reconstruct, ...} = info
   222     val {extra_norm, translate} = interface
   221     val {extra_norm, translate, ...} = interface
   223     val (with_datatypes, translate') =
   222     val (with_datatypes, translate') =
   224       set_has_datatypes (Config.get ctxt C.datatypes) translate
   223       set_has_datatypes (Config.get ctxt C.datatypes) translate
   225     val cmd = (rm, env_var, is_remote, name)
   224     val cmd = (rm, env_var, is_remote, name)
   226   in
   225   in
   227     (irules, ctxt)
   226     (irules, ctxt)
   282 
   281 
   283 fun add_solver cfg =
   282 fun add_solver cfg =
   284   let
   283   let
   285     val {name, env_var, is_remote, options, interface, outcome, cex_parser,
   284     val {name, env_var, is_remote, options, interface, outcome, cex_parser,
   286       reconstruct, default_max_relevant} = cfg
   285       reconstruct, default_max_relevant} = cfg
       
   286     val {class, ...} = interface
   287 
   287 
   288     fun core_oracle () = cfalse
   288     fun core_oracle () = cfalse
   289 
   289 
   290     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
   290     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
   291       interface=interface,
   291       interface=interface,
   292       reconstruct=finish (outcome name) cex_parser reconstruct ocl,
   292       reconstruct=finish (outcome name) cex_parser reconstruct ocl,
   293       default_max_relevant=default_max_relevant }
   293       default_max_relevant=default_max_relevant }
   294   in
   294   in
   295     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
   295     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
   296     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
   296     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
   297     Context.theory_map (C.add_solver name)
   297     Context.theory_map (C.add_solver (name, class))
   298   end
   298   end
   299 
   299 
   300 end
   300 end
   301 
   301 
   302 fun get_info ctxt name =
   302 fun get_info ctxt name =