36 val higher_order: bool Config.T |
36 val higher_order: bool Config.T |
37 val nat_as_int: bool Config.T |
37 val nat_as_int: bool Config.T |
38 val infer_triggers: bool Config.T |
38 val infer_triggers: bool Config.T |
39 val debug_files: string Config.T |
39 val debug_files: string Config.T |
40 val sat_solver: string Config.T |
40 val sat_solver: string Config.T |
|
41 val compress_verit_proofs: Proof.context -> bool |
41 |
42 |
42 (*tools*) |
43 (*tools*) |
43 val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b |
44 val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b |
44 val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
45 val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
45 |
46 |
46 (*diagnostics*) |
47 (*diagnostics*) |
47 val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
48 val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
48 val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit |
49 val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit |
49 val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit |
50 val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit |
50 val veriT_msg: Proof.context -> (unit -> 'a) -> unit |
51 val verit_msg: Proof.context -> (unit -> 'a) -> unit |
|
52 val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit |
|
53 val spy_verit: Proof.context -> bool |
|
54 val spy_Z3: Proof.context -> bool |
51 |
55 |
52 (*certificates*) |
56 (*certificates*) |
53 val select_certificates: string -> Context.generic -> Context.generic |
57 val select_certificates: string -> Context.generic -> Context.generic |
54 val certificates_of: Proof.context -> Cache_IO.cache option |
58 val certificates_of: Proof.context -> Cache_IO.cache option |
55 |
59 |
178 val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0) |
182 val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0) |
179 val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1) |
183 val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1) |
180 val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false) |
184 val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false) |
181 val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true) |
185 val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true) |
182 val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false) |
186 val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false) |
183 val trace_veriT = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false) |
187 val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false) |
|
188 val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false) |
|
189 val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false) |
|
190 val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false) |
|
191 val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K false) |
184 val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false) |
192 val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false) |
185 val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10) |
193 val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10) |
186 val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500) |
194 val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500) |
187 val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1) |
195 val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1) |
188 val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false) |
196 val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false) |
198 |
206 |
199 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) |
207 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) |
200 fun trace_msg ctxt = cond_trace (Config.get ctxt trace) |
208 fun trace_msg ctxt = cond_trace (Config.get ctxt trace) |
201 fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics) |
209 fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics) |
202 |
210 |
203 fun veriT_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_veriT) then ignore(x ()) else () |
211 fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else () |
|
212 fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else () |
|
213 |
|
214 fun spy_verit ctxt = Config.get ctxt spy_verit_attr |
|
215 fun spy_Z3 ctxt = Config.get ctxt spy_z3 |
|
216 fun compress_verit_proofs ctxt = Config.get ctxt trace_verit_compression |
204 |
217 |
205 |
218 |
206 (* tools *) |
219 (* tools *) |
207 |
220 |
208 fun with_time_limit ctxt timeout_config f x = |
221 fun with_time_limit ctxt timeout_config f x = |