author | haftmann |
Tue, 08 Jul 2025 19:13:44 +0200 | |
changeset 82824 | 7ddae44464d4 |
parent 82094 | 5b662ccae0af |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_config.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Configuration options and diagnostic tools for SMT. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
58061 | 7 |
signature SMT_CONFIG = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
(*solver*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
type solver_info = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
name: string, |
58061 | 12 |
class: Proof.context -> SMT_Util.class, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
avail: unit -> bool, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
options: Proof.context -> string list } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
val add_solver: solver_info -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
val set_solver_options: string * string -> Context.generic -> Context.generic |
75036 | 17 |
val all_solvers_of: Proof.context -> string list |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
val is_available: Proof.context -> string -> bool |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
val available_solvers_of: Proof.context -> string list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
val select_solver: string -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
21 |
val solver_of: Proof.context -> string |
58061 | 22 |
val solver_class_of: Proof.context -> SMT_Util.class |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
val solver_options_of: Proof.context -> string list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
(*options*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
val oracle: bool Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
val timeout: real Config.T |
59213
ef5e68575bc4
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
boehmes
parents:
58893
diff
changeset
|
28 |
val reconstruction_step_timeout: real Config.T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
val random_seed: int Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
val read_only_certificates: bool Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
val verbose: bool Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
val trace: bool Config.T |
59215
35c13f4995b1
optionally display statistics for Z3 proof reconstruction
boehmes
parents:
59214
diff
changeset
|
33 |
val statistics: bool Config.T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
34 |
val monomorph_limit: int Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
val monomorph_instances: int Config.T |
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
36 |
val explicit_application: int Config.T |
66551 | 37 |
val higher_order: bool Config.T |
74817
1fd8705503b4
generate problems with correct logic for veriT
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
74561
diff
changeset
|
38 |
val native_bv: bool Config.T |
66298 | 39 |
val nat_as_int: bool Config.T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
val infer_triggers: bool Config.T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
41 |
val debug_files: string Config.T |
56816
2f3756ccba41
use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents:
56294
diff
changeset
|
42 |
val sat_solver: string Config.T |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
43 |
val compress_verit_proofs: Proof.context -> bool |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
(*tools*) |
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
72908
diff
changeset
|
46 |
val get_timeout: Proof.context -> Time.time option |
59213
ef5e68575bc4
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
boehmes
parents:
58893
diff
changeset
|
47 |
val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
(*diagnostics*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
51 |
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit |
59215
35c13f4995b1
optionally display statistics for Z3 proof reconstruction
boehmes
parents:
59214
diff
changeset
|
53 |
val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
54 |
val verit_msg: Proof.context -> (unit -> 'a) -> unit |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
55 |
val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
56 |
val spy_verit: Proof.context -> bool |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
57 |
val spy_Z3: Proof.context -> bool |
78177
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75063
diff
changeset
|
58 |
val use_lethe_proof_from_cvc: Proof.context -> bool |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
(*certificates*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
val select_certificates: string -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
val certificates_of: Proof.context -> Cache_IO.cache option |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
(*setup*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
val print_setup: Proof.context -> unit |
82083 | 66 |
end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
67 |
|
58061 | 68 |
structure SMT_Config: SMT_CONFIG = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
69 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
70 |
|
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
71 |
(* context data *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
type solver_info = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
74 |
name: string, |
58061 | 75 |
class: Proof.context -> SMT_Util.class, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
76 |
avail: unit -> bool, |
82083 | 77 |
options: Proof.context -> string list}; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
|
59214 | 79 |
structure Data = Generic_Data |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
80 |
( |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
81 |
type T = |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
82 |
(solver_info * string list) Symtab.table * (*all solvers*) |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
83 |
string option * (*selected solver*) |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
84 |
Cache_IO.cache option; (*certificates*) |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
85 |
val empty: T = (Symtab.empty, NONE, NONE); |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
86 |
fun merge ((ss1, s1, c1): T, (ss2, s2, c2): T) = |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
87 |
(Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2), merge_options (c1, c2)); |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
88 |
); |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
89 |
|
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
90 |
val get_solvers' = #1 o Data.get; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
91 |
val get_solvers = get_solvers' o Context.Proof; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
92 |
val get_solver = #2 o Data.get o Context.Proof; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
93 |
val certificates_of = #3 o Data.get o Context.Proof; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
94 |
|
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
95 |
val map_solvers = Data.map o @{apply 3(1)} |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
96 |
val put_solver = Data.map o @{apply 3(2)} o K o SOME; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
97 |
val put_certificates = Data.map o @{apply 3(3)} o K; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
98 |
|
82077 | 99 |
val defined_solvers = Symtab.defined o get_solvers'; |
100 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
fun set_solver_options (name, options) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
102 |
let val opts = String.tokens (Symbol.is_ascii_blank o str) options |
82083 | 103 |
in map_solvers (Symtab.map_entry name (apsnd (K opts))) end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
104 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
fun add_solver (info as {name, ...} : solver_info) context = |
82077 | 106 |
if defined_solvers context name then |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
error ("Solver already registered: " ^ quote name) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
else |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
context |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
110 |
|> map_solvers (Symtab.update (name, (info, []))) |
58061 | 111 |
|> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options")) |
67149 | 112 |
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
(Thm.declaration_attribute o K o set_solver_options o pair name)) |
82083 | 114 |
("additional command-line options for SMT solver " ^ quote name)); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
115 |
|
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
116 |
val all_solvers_of' = Symtab.keys o get_solvers'; |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
117 |
val all_solvers_of = all_solvers_of' o Context.Proof; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
|
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
119 |
fun is_available' context name = |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
120 |
(case Symtab.lookup (get_solvers' context) name of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
SOME ({avail, ...}, _) => avail () |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
122 |
| NONE => false); |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
123 |
|
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
124 |
val is_available = is_available' o Context.Proof; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
fun available_solvers_of ctxt = |
82077 | 127 |
filter (is_available ctxt) (all_solvers_of ctxt); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
fun warn_solver (Context.Proof ctxt) name = |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56208
diff
changeset
|
130 |
if Context_Position.is_visible ctxt then |
57199 | 131 |
warning ("The SMT solver " ^ quote name ^ " is not installed") |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56208
diff
changeset
|
132 |
else () |
82083 | 133 |
| warn_solver _ _ = (); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
fun select_solver name context = |
82078 | 136 |
if not (defined_solvers context name) then |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
137 |
error ("Trying to select unknown solver: " ^ quote name) |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
138 |
else if not (is_available' context name) then |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
139 |
(warn_solver context name; put_solver name context) |
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
140 |
else put_solver name context; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
|
82083 | 142 |
fun no_solver_err () = error "No SMT solver selected"; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
fun solver_of ctxt = |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
145 |
(case get_solver ctxt of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
SOME name => name |
82083 | 147 |
| NONE => no_solver_err ()); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
148 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
fun solver_info_of default select ctxt = |
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
150 |
(case get_solver ctxt of |
59214 | 151 |
NONE => default () |
82083 | 152 |
| SOME name => select (Symtab.lookup (get_solvers ctxt) name)); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
fun solver_class_of ctxt = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
let fun class_of ({class, ...}: solver_info, _) = class ctxt |
82083 | 156 |
in solver_info_of no_solver_err (class_of o the) ctxt end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
fun solver_options_of ctxt = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
fun all_options NONE = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
161 |
| all_options (SOME ({options, ...} : solver_info, opts)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
162 |
opts @ options ctxt |
82083 | 163 |
in solver_info_of (K []) all_options ctxt end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
164 |
|
82084 | 165 |
val _ = |
166 |
Theory.setup (Attrib.setup \<^binding>\<open>smt_solver\<close> |
|
67149 | 167 |
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
168 |
(Thm.declaration_attribute o K o select_solver)) |
82084 | 169 |
"SMT solver configuration"); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
170 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
171 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
172 |
(* options *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
|
82083 | 174 |
val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true); |
175 |
val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0); |
|
176 |
val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0); |
|
177 |
val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1); |
|
178 |
val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false); |
|
179 |
val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true); |
|
180 |
val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false); |
|
181 |
val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false); |
|
182 |
val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false); |
|
183 |
val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false); |
|
184 |
val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false); |
|
185 |
val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true); |
|
186 |
val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false); |
|
187 |
val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10); |
|
188 |
val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500); |
|
189 |
val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1); |
|
190 |
val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false); |
|
191 |
val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true); |
|
192 |
val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false); |
|
193 |
val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false); |
|
194 |
val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K ""); |
|
195 |
val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite"); |
|
196 |
val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false); |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
197 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
198 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
199 |
(* diagnostics *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
|
82083 | 201 |
fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else (); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
202 |
|
82083 | 203 |
fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose); |
204 |
fun trace_msg ctxt = cond_trace (Config.get ctxt trace); |
|
205 |
fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics); |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
206 |
|
82083 | 207 |
fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else (); |
208 |
fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else (); |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72343
diff
changeset
|
209 |
|
82083 | 210 |
fun spy_verit ctxt = Config.get ctxt spy_verit_attr; |
211 |
fun spy_Z3 ctxt = Config.get ctxt spy_z3; |
|
212 |
fun compress_verit_proofs ctxt = Config.get ctxt trace_verit_compression; |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67149
diff
changeset
|
213 |
|
82083 | 214 |
fun use_lethe_proof_from_cvc ctxt = Config.get ctxt cvc_experimental_lethe; |
78177
ea7a3cc64df5
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75063
diff
changeset
|
215 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
216 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
217 |
(* tools *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
218 |
|
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
72908
diff
changeset
|
219 |
fun get_timeout ctxt = |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
72908
diff
changeset
|
220 |
let val t = seconds (Config.get ctxt timeout); |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
72908
diff
changeset
|
221 |
in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end; |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
72908
diff
changeset
|
222 |
|
59213
ef5e68575bc4
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
boehmes
parents:
58893
diff
changeset
|
223 |
fun with_time_limit ctxt timeout_config f x = |
62519 | 224 |
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x |
82083 | 225 |
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
226 |
|
82083 | 227 |
fun with_timeout ctxt = with_time_limit ctxt timeout; |
59213
ef5e68575bc4
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
boehmes
parents:
58893
diff
changeset
|
228 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
229 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
(* certificates *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
231 |
|
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
232 |
val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
233 |
|
82075
090b0ed235d2
tuned signature: more concise access to context data;
wenzelm
parents:
80910
diff
changeset
|
234 |
fun select_certificates name context = context |> put_certificates ( |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
235 |
if name = "" then NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
236 |
else |
82079 | 237 |
let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name |
238 |
in SOME (Cache_IO.unsynchronized_init dir) end); |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
|
82084 | 240 |
val _ = |
241 |
Theory.setup (Attrib.setup \<^binding>\<open>smt_certificates\<close> |
|
67149 | 242 |
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
243 |
(Thm.declaration_attribute o K o select_certificates)) |
82084 | 244 |
"SMT certificates configuration"); |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
245 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
246 |
|
82084 | 247 |
(* print_setup *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
249 |
fun print_setup ctxt = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
250 |
let |
82083 | 251 |
val names = available_solvers_of ctxt; |
252 |
val ns = if null names then ["(none)"] else sort_strings names; |
|
253 |
val n = the_default "(none)" (get_solver ctxt); |
|
254 |
val opts = solver_options_of ctxt; |
|
82094 | 255 |
val t = seconds (Config.get ctxt timeout) |
57230 | 256 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
257 |
val certs_filename = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
258 |
(case get_certificates_path ctxt of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
259 |
SOME path => Path.print path |
82083 | 260 |
| NONE => "(disabled)"); |
82085 | 261 |
|
262 |
val items = |
|
263 |
[Pretty.str ("Current SMT solver: " ^ n), |
|
80910 | 264 |
Pretty.str ("Current SMT solver options: " ^ implode_space opts), |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
265 |
Pretty.str_list "Available SMT solvers: " "" ns, |
82094 | 266 |
Pretty.str ("Current timeout: " ^ (if Timeout.ignored t then "(none)" else Time.message t)), |
82084 | 267 |
Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))), |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
Pretty.str ("Certificates cache: " ^ certs_filename), |
82085 | 269 |
Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))]; |
270 |
in Pretty.writeln (Pretty.big_list "SMT setup:" (map (Pretty.item o single) items)) end; |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
271 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
272 |
val _ = |
67149 | 273 |
Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
274 |
"show the available SMT solvers, the currently selected SMT solver, \ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
275 |
\and the values of SMT configuration options" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
276 |
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
277 |
|
82083 | 278 |
end |