7 signature SMT2_CONFIG = |
7 signature SMT2_CONFIG = |
8 sig |
8 sig |
9 (*solver*) |
9 (*solver*) |
10 type solver_info = { |
10 type solver_info = { |
11 name: string, |
11 name: string, |
12 class: Proof.context -> SMT2_Utils.class, |
12 class: Proof.context -> SMT2_Util.class, |
13 avail: unit -> bool, |
13 avail: unit -> bool, |
14 options: Proof.context -> string list } |
14 options: Proof.context -> string list } |
15 val add_solver: solver_info -> Context.generic -> Context.generic |
15 val add_solver: solver_info -> Context.generic -> Context.generic |
16 val set_solver_options: string * string -> Context.generic -> Context.generic |
16 val set_solver_options: string * string -> Context.generic -> Context.generic |
17 val is_available: Proof.context -> string -> bool |
17 val is_available: Proof.context -> string -> bool |
18 val available_solvers_of: Proof.context -> string list |
18 val available_solvers_of: Proof.context -> string list |
19 val select_solver: string -> Context.generic -> Context.generic |
19 val select_solver: string -> Context.generic -> Context.generic |
20 val solver_of: Proof.context -> string |
20 val solver_of: Proof.context -> string |
21 val solver_class_of: Proof.context -> SMT2_Utils.class |
21 val solver_class_of: Proof.context -> SMT2_Util.class |
22 val solver_options_of: Proof.context -> string list |
22 val solver_options_of: Proof.context -> string list |
23 |
23 |
24 (*options*) |
24 (*options*) |
25 val oracle: bool Config.T |
25 val oracle: bool Config.T |
26 val timeout: real Config.T |
26 val timeout: real Config.T |
55 |
55 |
56 (* solver *) |
56 (* solver *) |
57 |
57 |
58 type solver_info = { |
58 type solver_info = { |
59 name: string, |
59 name: string, |
60 class: Proof.context -> SMT2_Utils.class, |
60 class: Proof.context -> SMT2_Util.class, |
61 avail: unit -> bool, |
61 avail: unit -> bool, |
62 options: Proof.context -> string list } |
62 options: Proof.context -> string list} |
63 |
63 |
64 (* FIXME just one data slot (record) per program unit *) |
64 (* FIXME just one data slot (record) per program unit *) |
65 structure Solvers = Generic_Data |
65 structure Solvers = Generic_Data |
66 ( |
66 ( |
67 type T = (solver_info * string list) Symtab.table * string option |
67 type T = (solver_info * string list) Symtab.table * string option |