equal
deleted
inserted
replaced
24 (*options*) |
24 (*options*) |
25 val oracle: bool Config.T |
25 val oracle: bool Config.T |
26 val datatypes: bool Config.T |
26 val datatypes: bool Config.T |
27 val timeout: real Config.T |
27 val timeout: real Config.T |
28 val random_seed: int Config.T |
28 val random_seed: int Config.T |
29 val fixed: bool Config.T |
29 val read_only_certificates: bool Config.T |
30 val verbose: bool Config.T |
30 val verbose: bool Config.T |
31 val trace: bool Config.T |
31 val trace: bool Config.T |
32 val trace_used_facts: bool Config.T |
32 val trace_used_facts: bool Config.T |
33 val monomorph_limit: int Config.T |
33 val monomorph_limit: int Config.T |
34 val monomorph_instances: int Config.T |
34 val monomorph_instances: int Config.T |
151 |
151 |
152 val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true) |
152 val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true) |
153 val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false) |
153 val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false) |
154 val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0) |
154 val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0) |
155 val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1) |
155 val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1) |
156 val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false) |
156 val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false) |
157 val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true) |
157 val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true) |
158 val trace = Attrib.setup_config_bool @{binding smt_trace} (K false) |
158 val trace = Attrib.setup_config_bool @{binding smt_trace} (K false) |
159 val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false) |
159 val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false) |
160 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) |
160 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) |
161 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) |
161 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) |
241 Pretty.str ("Current timeout: " ^ t ^ " seconds"), |
241 Pretty.str ("Current timeout: " ^ t ^ " seconds"), |
242 Pretty.str ("With proofs: " ^ |
242 Pretty.str ("With proofs: " ^ |
243 string_of_bool (not (Config.get ctxt oracle))), |
243 string_of_bool (not (Config.get ctxt oracle))), |
244 Pretty.str ("Certificates cache: " ^ certs_filename), |
244 Pretty.str ("Certificates cache: " ^ certs_filename), |
245 Pretty.str ("Fixed certificates: " ^ |
245 Pretty.str ("Fixed certificates: " ^ |
246 string_of_bool (Config.get ctxt fixed))]) |
246 string_of_bool (Config.get ctxt read_only_certificates))]) |
247 end |
247 end |
248 |
248 |
249 val _ = |
249 val _ = |
250 Outer_Syntax.improper_command @{command_spec "smt_status"} |
250 Outer_Syntax.improper_command @{command_spec "smt_status"} |
251 "show the available SMT solvers, the currently selected SMT solver, \ |
251 "show the available SMT solvers, the currently selected SMT solver, \ |