author | wenzelm |
Mon, 06 Apr 2015 17:06:48 +0200 | |
changeset 59936 | b8ffc3dc9e24 |
parent 58893 | 9e0ecb66d6a7 |
child 60312 | ee6f9a97205d |
permissions | -rw-r--r-- |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
1 |
(* Title: HOL/Library/Old_SMT/old_smt_config.ML |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
3 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
4 |
Configuration options and diagnostic tools for SMT. |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
5 |
*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
6 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
7 |
signature OLD_SMT_CONFIG = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
8 |
sig |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
9 |
(*solver*) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
10 |
type solver_info = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
11 |
name: string, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
12 |
class: Proof.context -> Old_SMT_Utils.class, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
13 |
avail: unit -> bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
14 |
options: Proof.context -> string list } |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
15 |
val add_solver: solver_info -> Context.generic -> Context.generic |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
16 |
val set_solver_options: string * string -> Context.generic -> Context.generic |
46736
4dc7ddb47350
SMT fails if the chosen SMT solver is not installed
boehmes
parents:
46042
diff
changeset
|
17 |
val is_available: Proof.context -> string -> bool |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
18 |
val available_solvers_of: Proof.context -> string list |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
19 |
val select_solver: string -> Context.generic -> Context.generic |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
20 |
val solver_of: Proof.context -> string |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
21 |
val solver_class_of: Proof.context -> Old_SMT_Utils.class |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
22 |
val solver_options_of: Proof.context -> string list |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
23 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
24 |
(*options*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
25 |
val oracle: bool Config.T |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
26 |
val datatypes: bool Config.T |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
27 |
val timeout: real Config.T |
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset
|
28 |
val random_seed: int Config.T |
47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46961
diff
changeset
|
29 |
val read_only_certificates: bool Config.T |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
30 |
val verbose: bool Config.T |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
31 |
val trace: bool Config.T |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
32 |
val trace_used_facts: bool Config.T |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
33 |
val monomorph_limit: int Config.T |
41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41761
diff
changeset
|
34 |
val monomorph_instances: int Config.T |
41125 | 35 |
val infer_triggers: bool Config.T |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
36 |
val filter_only_facts: bool Config.T |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40513
diff
changeset
|
37 |
val debug_files: string Config.T |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
38 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
39 |
(*tools*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
40 |
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
41 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
42 |
(*diagnostics*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
43 |
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
44 |
val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
45 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
46 |
(*certificates*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
47 |
val select_certificates: string -> Context.generic -> Context.generic |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
48 |
val certificates_of: Proof.context -> Cache_IO.cache option |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
49 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
50 |
(*setup*) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
51 |
val setup: theory -> theory |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
52 |
val print_setup: Proof.context -> unit |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
53 |
end |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
54 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
55 |
structure Old_SMT_Config: OLD_SMT_CONFIG = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
56 |
struct |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
57 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
58 |
(* solver *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
59 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
60 |
type solver_info = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
61 |
name: string, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
62 |
class: Proof.context -> Old_SMT_Utils.class, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
63 |
avail: unit -> bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
64 |
options: Proof.context -> string list } |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
65 |
|
46042 | 66 |
(* FIXME just one data slot (record) per program unit *) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
67 |
structure Solvers = Generic_Data |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
68 |
( |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
69 |
type T = (solver_info * string list) Symtab.table * string option |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
70 |
val empty = (Symtab.empty, NONE) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
71 |
val extend = I |
41499 | 72 |
fun merge ((ss1, s1), (ss2, s2)) = |
73 |
(Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2)) |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
74 |
) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
75 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
76 |
fun set_solver_options (name, options) = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
77 |
let val opts = String.tokens (Symbol.is_ascii_blank o str) options |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40578
diff
changeset
|
78 |
in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
79 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
80 |
fun add_solver (info as {name, ...} : solver_info) context = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
81 |
if Symtab.defined (fst (Solvers.get context)) name then |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
82 |
error ("Solver already registered: " ^ quote name) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
83 |
else |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
84 |
context |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
85 |
|> Solvers.map (apfst (Symtab.update (name, (info, [])))) |
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
86 |
|> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options")) |
46949 | 87 |
(Scan.lift (@{keyword "="} |-- Args.name) >> |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
88 |
(Thm.declaration_attribute o K o set_solver_options o pair name)) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
89 |
("Additional command line options for SMT solver " ^ quote name)) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
90 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
91 |
fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt))) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
92 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
93 |
fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt)) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
94 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
95 |
fun is_available ctxt name = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
96 |
(case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
97 |
SOME ({avail, ...}, _) => avail () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
98 |
| NONE => false) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
99 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
100 |
fun available_solvers_of ctxt = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
101 |
filter (is_available ctxt) (all_solvers_of ctxt) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
102 |
|
52699 | 103 |
fun warn_solver (Context.Proof ctxt) name = |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56208
diff
changeset
|
104 |
if Context_Position.is_visible ctxt then |
52699 | 105 |
warning ("The SMT solver " ^ quote name ^ " is not installed.") |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56208
diff
changeset
|
106 |
else () |
52699 | 107 |
| warn_solver _ _ = (); |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
108 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
109 |
fun select_solver name context = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
110 |
let |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
111 |
val ctxt = Context.proof_of context |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
112 |
val upd = Solvers.map (apsnd (K (SOME name))) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
113 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
114 |
if not (member (op =) (all_solvers_of ctxt) name) then |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
115 |
error ("Trying to select unknown solver: " ^ quote name) |
41498
a45cfc6dfd10
only print warning in a visible context (previously, the warning was printed more than once)
boehmes
parents:
41472
diff
changeset
|
116 |
else if not (is_available ctxt name) then |
a45cfc6dfd10
only print warning in a visible context (previously, the warning was printed more than once)
boehmes
parents:
41472
diff
changeset
|
117 |
(warn_solver context name; upd context) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
118 |
else upd context |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
119 |
end |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
120 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40578
diff
changeset
|
121 |
fun no_solver_err () = error "No SMT solver selected" |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
122 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
123 |
fun solver_of ctxt = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
124 |
(case solver_name_of ctxt of |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
125 |
SOME name => name |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
126 |
| NONE => no_solver_err ()) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
127 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
128 |
fun solver_info_of default select ctxt = |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40578
diff
changeset
|
129 |
(case Solvers.get (Context.Proof ctxt) of |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
130 |
(solvers, SOME name) => select (Symtab.lookup solvers name) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
131 |
| (_, NONE) => default ()) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40578
diff
changeset
|
132 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40578
diff
changeset
|
133 |
fun solver_class_of ctxt = |
48043
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47152
diff
changeset
|
134 |
let fun class_of ({class, ...}: solver_info, _) = class ctxt |
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47152
diff
changeset
|
135 |
in solver_info_of no_solver_err (class_of o the) ctxt end |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
136 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
137 |
fun solver_options_of ctxt = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
138 |
let |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
139 |
fun all_options NONE = [] |
41438 | 140 |
| all_options (SOME ({options, ...} : solver_info, opts)) = |
141 |
opts @ options ctxt |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
142 |
in solver_info_of (K []) all_options ctxt end |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
143 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
144 |
val setup_solver = |
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
145 |
Attrib.setup @{binding old_smt_solver} |
46949 | 146 |
(Scan.lift (@{keyword "="} |-- Args.name) >> |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
147 |
(Thm.declaration_attribute o K o select_solver)) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
148 |
"SMT solver configuration" |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
149 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
150 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
151 |
(* options *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
152 |
|
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
153 |
val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
154 |
val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
155 |
val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
156 |
val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
157 |
val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
158 |
val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
159 |
val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
160 |
val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
161 |
val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
162 |
val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
163 |
val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
164 |
val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false) |
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
165 |
val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "") |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
166 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
167 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
168 |
(* diagnostics *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
169 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
170 |
fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else () |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
171 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
172 |
fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
173 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
174 |
fun trace_msg ctxt = cond_trace (Config.get ctxt trace) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
175 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
176 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
177 |
(* tools *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
178 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
179 |
fun with_timeout ctxt f x = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
180 |
TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
181 |
handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
182 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
183 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
184 |
(* certificates *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
185 |
|
46042 | 186 |
(* FIXME just one data slot (record) per program unit *) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
187 |
structure Certificates = Generic_Data |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
188 |
( |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
189 |
type T = Cache_IO.cache option |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
190 |
val empty = NONE |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
191 |
val extend = I |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41441
diff
changeset
|
192 |
fun merge (s, _) = s (* FIXME merge options!? *) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
193 |
) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
194 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
195 |
val get_certificates_path = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
196 |
Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
197 |
|
40513 | 198 |
fun select_certificates name context = context |> Certificates.put ( |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
199 |
if name = "" then NONE |
40513 | 200 |
else |
201 |
Path.explode name |
|
56208 | 202 |
|> Path.append (Resources.master_directory (Context.theory_of context)) |
50317
4d1590544b91
synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents:
48043
diff
changeset
|
203 |
|> SOME o Cache_IO.unsynchronized_init) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
204 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
205 |
val certificates_of = Certificates.get o Context.Proof |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
206 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
207 |
val setup_certificates = |
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset
|
208 |
Attrib.setup @{binding old_smt_certificates} |
46949 | 209 |
(Scan.lift (@{keyword "="} |-- Args.name) >> |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
210 |
(Thm.declaration_attribute o K o select_certificates)) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
211 |
"SMT certificates configuration" |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
212 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
213 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
214 |
(* setup *) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
215 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
216 |
val setup = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
217 |
setup_solver #> |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
218 |
setup_certificates |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
219 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
220 |
fun print_setup ctxt = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
221 |
let |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
222 |
fun string_of_bool b = if b then "true" else "false" |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
223 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
224 |
val names = available_solvers_of ctxt |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
225 |
val ns = if null names then ["(none)"] else sort_strings names |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41125
diff
changeset
|
226 |
val n = the_default "(none)" (solver_name_of ctxt) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
227 |
val opts = solver_options_of ctxt |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
228 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
229 |
val t = string_of_real (Config.get ctxt timeout) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
230 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
231 |
val certs_filename = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
232 |
(case get_certificates_path ctxt of |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41762
diff
changeset
|
233 |
SOME path => Path.print path |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
234 |
| NONE => "(disabled)") |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
235 |
in |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
236 |
Pretty.writeln (Pretty.big_list "SMT setup:" [ |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
237 |
Pretty.str ("Current SMT solver: " ^ n), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
238 |
Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
239 |
Pretty.str_list "Available SMT solvers: " "" ns, |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
240 |
Pretty.str ("Current timeout: " ^ t ^ " seconds"), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
241 |
Pretty.str ("With proofs: " ^ |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
242 |
string_of_bool (not (Config.get ctxt oracle))), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
243 |
Pretty.str ("Certificates cache: " ^ certs_filename), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
244 |
Pretty.str ("Fixed certificates: " ^ |
47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46961
diff
changeset
|
245 |
string_of_bool (Config.get ctxt read_only_certificates))]) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
246 |
end |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
247 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
248 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
58893
diff
changeset
|
249 |
Outer_Syntax.command @{command_keyword old_smt_status} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
250 |
"show the available SMT solvers, the currently selected SMT solver, \ |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
251 |
\and the values of SMT configuration options" |
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51575
diff
changeset
|
252 |
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
253 |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
254 |
end |