author | boehmes |
Tue, 26 Oct 2010 17:35:52 +0200 | |
changeset 40198 | 8d470bbaafd7 |
parent 40197 | d99f74ed95be |
child 40199 | 2963511e121c |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smt_solver.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
SMT solvers registry and SMT tactic. |
|
5 |
*) |
|
6 |
||
7 |
signature SMT_SOLVER = |
|
8 |
sig |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
9 |
datatype failure = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
10 |
Counterexample of bool * term list | |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
11 |
Time_Out | |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
12 |
Out_Of_Memory | |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
13 |
Other_Failure of string |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
14 |
val string_of_failure: Proof.context -> string -> failure -> string |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
15 |
exception SMT of failure |
36898 | 16 |
|
17 |
type interface = { |
|
18 |
extra_norm: SMT_Normalize.extra_norm, |
|
19 |
translate: SMT_Translate.config } |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
20 |
datatype outcome = Unsat | Sat | Unknown |
36898 | 21 |
type solver_config = { |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
22 |
name: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
23 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
24 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
25 |
options: Proof.context -> string list, |
36898 | 26 |
interface: interface, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
27 |
outcome: string -> string list -> outcome * string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
28 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
29 |
term list) option, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
30 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
31 |
(int list * thm) * Proof.context) option } |
36898 | 32 |
|
33 |
(*options*) |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
34 |
val oracle: bool Config.T |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
35 |
val filter_only: bool Config.T |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
36 |
val datatypes: bool Config.T |
36898 | 37 |
val timeout: int Config.T |
38 |
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
|
39 |
val trace: bool Config.T |
|
40 |
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
41 |
val trace_used_facts: bool Config.T |
36898 | 42 |
|
43 |
(*certificates*) |
|
44 |
val fixed_certificates: bool Config.T |
|
45 |
val select_certificates: string -> Context.generic -> Context.generic |
|
46 |
||
47 |
(*solvers*) |
|
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
48 |
type solver = bool option -> Proof.context -> (int * thm) list -> |
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
49 |
int list * thm |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
50 |
val add_solver: solver_config -> theory -> theory |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
51 |
val set_solver_options: string -> string -> Context.generic -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
52 |
Context.generic |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
53 |
val all_solver_names_of: Context.generic -> string list |
36898 | 54 |
val solver_name_of: Context.generic -> string |
55 |
val select_solver: string -> Context.generic -> Context.generic |
|
56 |
val solver_of: Context.generic -> solver |
|
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
57 |
val is_locally_installed: Proof.context -> bool |
36898 | 58 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
59 |
(*filter*) |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
60 |
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int -> |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
61 |
{outcome: failure option, used_facts: 'a list, |
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
62 |
run_time_in_msecs: int option} |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
63 |
|
36898 | 64 |
(*tactic*) |
65 |
val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic |
|
66 |
val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic |
|
67 |
||
68 |
(*setup*) |
|
69 |
val setup: theory -> theory |
|
70 |
val print_setup: Context.generic -> unit |
|
71 |
end |
|
72 |
||
73 |
structure SMT_Solver: SMT_SOLVER = |
|
74 |
struct |
|
75 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
76 |
datatype failure = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
77 |
Counterexample of bool * term list | |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
78 |
Time_Out | |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
79 |
Out_Of_Memory | |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
80 |
Other_Failure of string |
36898 | 81 |
|
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
82 |
fun string_of_failure ctxt _ (Counterexample (real, ex)) = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
83 |
let |
40165 | 84 |
val msg = (if real then "C" else "Potential c") ^ "ounterexample found" |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
85 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
86 |
if null ex then msg ^ "." |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
87 |
else Pretty.string_of (Pretty.big_list (msg ^ ":") |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
88 |
(map (Syntax.pretty_term ctxt) ex)) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
89 |
end |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
90 |
| string_of_failure _ name Time_Out = name ^ " timed out." |
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
91 |
| string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory." |
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
92 |
| string_of_failure _ _ (Other_Failure msg) = msg |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
93 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
94 |
exception SMT of failure |
36898 | 95 |
|
96 |
type interface = { |
|
97 |
extra_norm: SMT_Normalize.extra_norm, |
|
98 |
translate: SMT_Translate.config } |
|
99 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
100 |
datatype outcome = Unsat | Sat | Unknown |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
101 |
|
36898 | 102 |
type solver_config = { |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
103 |
name: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
104 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
105 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
106 |
options: Proof.context -> string list, |
36898 | 107 |
interface: interface, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
108 |
outcome: string -> string list -> outcome * string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
109 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
110 |
term list) option, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
111 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
112 |
(int list * thm) * Proof.context) option } |
36898 | 113 |
|
114 |
||
115 |
||
116 |
(* SMT options *) |
|
117 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
118 |
val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
119 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
120 |
val (filter_only, setup_filter_only) = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
121 |
Attrib.config_bool "smt_filter_only" (K false) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
122 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
123 |
val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
124 |
|
36898 | 125 |
val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30) |
126 |
||
127 |
fun with_timeout ctxt f x = |
|
128 |
TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
129 |
handle TimeLimit.TimeOut => raise SMT Time_Out |
36898 | 130 |
|
131 |
val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false) |
|
132 |
||
133 |
fun trace_msg ctxt f x = |
|
134 |
if Config.get ctxt trace then tracing (f x) else () |
|
135 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
136 |
val (trace_used_facts, setup_trace_used_facts) = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
137 |
Attrib.config_bool "smt_trace_used_facts" (K false) |
36898 | 138 |
|
139 |
||
140 |
(* SMT certificates *) |
|
141 |
||
142 |
val (fixed_certificates, setup_fixed_certificates) = |
|
143 |
Attrib.config_bool "smt_fixed" (K false) |
|
144 |
||
145 |
structure Certificates = Generic_Data |
|
146 |
( |
|
147 |
type T = Cache_IO.cache option |
|
148 |
val empty = NONE |
|
149 |
val extend = I |
|
150 |
fun merge (s, _) = s |
|
151 |
) |
|
152 |
||
153 |
val get_certificates_path = |
|
154 |
Option.map (Cache_IO.cache_path_of) o Certificates.get |
|
155 |
||
156 |
fun select_certificates name = Certificates.put ( |
|
157 |
if name = "" then NONE |
|
158 |
else SOME (Cache_IO.make (Path.explode name))) |
|
159 |
||
160 |
||
161 |
||
162 |
(* interface to external solvers *) |
|
163 |
||
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
164 |
fun get_local_solver env_var = |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
165 |
let val local_solver = getenv env_var |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
166 |
in if local_solver <> "" then SOME local_solver else NONE end |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
167 |
|
36898 | 168 |
local |
169 |
||
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
170 |
fun choose (rm, env_var, is_remote, name) = |
36898 | 171 |
let |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
172 |
val force_local = (case rm of SOME false => true | _ => false) |
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
173 |
val force_remote = (case rm of SOME true => true | _ => false) |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
174 |
val lsolver = get_local_solver env_var |
36898 | 175 |
val remote_url = getenv "REMOTE_SMT_URL" |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
176 |
val trace = if is_some rm then K () else tracing |
36898 | 177 |
in |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
178 |
if not force_remote andalso is_some lsolver |
36898 | 179 |
then |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
180 |
(trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ..."); |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
181 |
[the lsolver]) |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
182 |
else if not force_local andalso is_remote |
36898 | 183 |
then |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
184 |
(trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ |
36898 | 185 |
quote remote_url ^ " ..."); |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
186 |
[getenv "REMOTE_SMT", name]) |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
187 |
else if force_remote |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
188 |
then error ("The SMT solver " ^ quote name ^ " is not remotely available.") |
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
189 |
else error ("The SMT solver " ^ quote name ^ " has not been found " ^ |
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
190 |
"on this computer. Please set the Isabelle environment variable " ^ |
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
191 |
quote env_var ^ ".") |
36898 | 192 |
end |
193 |
||
194 |
fun make_cmd solver args problem_path proof_path = space_implode " " ( |
|
195 |
map File.shell_quote (solver @ args) @ |
|
196 |
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
|
197 |
||
198 |
fun run ctxt cmd args input = |
|
199 |
(case Certificates.get (Context.Proof ctxt) of |
|
200 |
NONE => Cache_IO.run (make_cmd (choose cmd) args) input |
|
201 |
| SOME certs => |
|
202 |
(case Cache_IO.lookup certs input of |
|
203 |
(NONE, key) => |
|
204 |
if Config.get ctxt fixed_certificates |
|
205 |
then error ("Bad certificates cache: missing certificate") |
|
206 |
else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) |
|
207 |
input |
|
208 |
| (SOME output, _) => |
|
209 |
(tracing ("Using cached certificate from " ^ |
|
210 |
File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); |
|
211 |
output))) |
|
212 |
||
213 |
in |
|
214 |
||
215 |
fun run_solver ctxt cmd args input = |
|
216 |
let |
|
217 |
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
218 |
(map Pretty.str ls)) |
|
219 |
||
220 |
val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input |
|
221 |
||
222 |
val (res, err) = with_timeout ctxt (run ctxt cmd args) input |
|
223 |
val _ = trace_msg ctxt (pretty "SMT solver:") err |
|
224 |
||
39811 | 225 |
val ls = rev (snd (chop_while (equal "") (rev res))) |
36898 | 226 |
val _ = trace_msg ctxt (pretty "SMT result:") ls |
227 |
in ls end |
|
228 |
||
229 |
end |
|
230 |
||
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
231 |
fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o |
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
232 |
Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd)) |
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
233 |
|
36940 | 234 |
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) = |
36898 | 235 |
let |
236 |
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] |
|
237 |
fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) |
|
238 |
fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
|
239 |
in |
|
240 |
trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [ |
|
241 |
Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)), |
|
242 |
Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () |
|
243 |
end |
|
244 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
245 |
fun invoke translate_config name cmd more_opts options irules ctxt = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
246 |
let |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
247 |
val args = more_opts @ options ctxt |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
248 |
val comments = ("solver: " ^ name) :: |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
249 |
("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
250 |
"arguments:" :: args |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
251 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
252 |
irules |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
253 |
|> tap (trace_assms ctxt) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
254 |
|> SMT_Translate.translate translate_config ctxt comments |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
255 |
||> tap (trace_recon_data ctxt) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
256 |
|>> run_solver ctxt cmd args |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
257 |
|> rpair ctxt |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
258 |
end |
36898 | 259 |
|
260 |
fun discharge_definitions thm = |
|
261 |
if Thm.nprems_of thm = 0 then thm |
|
262 |
else discharge_definitions (@{thm reflexive} RS thm) |
|
263 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
264 |
fun set_has_datatypes with_datatypes translate = |
36898 | 265 |
let |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
266 |
val {prefixes, header, strict, builtins, serialize} = translate |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
267 |
val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
268 |
val with_datatypes' = has_datatypes andalso with_datatypes |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
269 |
val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
270 |
builtin_fun=builtin_fun, has_datatypes=with_datatypes} |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
271 |
val translate' = {prefixes=prefixes, header=header, strict=strict, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
272 |
builtins=builtins', serialize=serialize} |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
273 |
in (with_datatypes', translate') end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
274 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
275 |
fun trace_assumptions ctxt irules idxs = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
276 |
let |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
277 |
val thms = filter (fn i => i >= 0) idxs |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
278 |
|> map_filter (AList.lookup (op =) irules) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
279 |
in |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
280 |
if Config.get ctxt trace_used_facts andalso length thms > 0 |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
281 |
then |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
282 |
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
283 |
(map (Display.pretty_thm ctxt) thms))) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
284 |
else () |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
285 |
end |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
286 |
|
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
287 |
fun gen_solver name info rm ctxt irules = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
288 |
let |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
289 |
val {env_var, is_remote, options, more_options, interface, reconstruct} = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
290 |
info |
36898 | 291 |
val {extra_norm, translate} = interface |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
292 |
val (with_datatypes, translate') = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
293 |
set_has_datatypes (Config.get ctxt datatypes) translate |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
294 |
val cmd = (rm, env_var, is_remote, name) |
36898 | 295 |
in |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
296 |
(irules, ctxt) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
297 |
|-> SMT_Normalize.normalize extra_norm with_datatypes |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
298 |
|-> invoke translate' name cmd more_options options |
36898 | 299 |
|-> reconstruct |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
300 |
|-> (fn (idxs, thm) => fn ctxt' => thm |
36898 | 301 |
|> singleton (ProofContext.export ctxt' ctxt) |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
302 |
|> discharge_definitions |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
303 |
|> tap (fn _ => trace_assumptions ctxt irules idxs) |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
304 |
|> pair idxs) |
36898 | 305 |
end |
306 |
||
307 |
||
308 |
||
309 |
(* solver store *) |
|
310 |
||
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
311 |
type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
312 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
313 |
type solver_info = { |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
314 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
315 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
316 |
options: Proof.context -> string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
317 |
more_options: string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
318 |
interface: interface, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
319 |
reconstruct: string list * SMT_Translate.recon -> Proof.context -> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
320 |
(int list * thm) * Proof.context } |
36898 | 321 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
322 |
structure Solvers = Generic_Data |
36898 | 323 |
( |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
324 |
type T = solver_info Symtab.table |
36898 | 325 |
val empty = Symtab.empty |
326 |
val extend = I |
|
327 |
fun merge data = Symtab.merge (K true) data |
|
328 |
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) |
|
329 |
) |
|
330 |
||
331 |
val no_solver = "(none)" |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
332 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
333 |
fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
334 |
{env_var, is_remote, options, interface, reconstruct, ...} => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
335 |
{env_var=env_var, is_remote=is_remote, options=options, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
336 |
more_options=String.tokens (Symbol.is_ascii_blank o str) opts, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
337 |
interface=interface, reconstruct=reconstruct})) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
338 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
339 |
local |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
340 |
fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
341 |
(case outcome output of |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
342 |
(Unsat, ls) => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
343 |
if not (Config.get ctxt oracle) andalso is_some reconstruct |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
344 |
then the reconstruct ctxt recon ls |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
345 |
else (([], ocl ()), ctxt) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
346 |
| (result, ls) => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
347 |
let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => []) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
348 |
in raise SMT (Counterexample (result = Sat, ts)) end) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
349 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
350 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
351 |
fun add_solver cfg = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
352 |
let |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
353 |
val {name, env_var, is_remote, options, interface, outcome, cex_parser, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
354 |
reconstruct} = cfg |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
355 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
356 |
fun core_oracle () = @{cprop False} |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
357 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
358 |
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
359 |
more_options=[], interface=interface, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
360 |
reconstruct=finish (outcome name) cex_parser reconstruct ocl } |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
361 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
362 |
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
363 |
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
364 |
Attrib.setup (Binding.name (name ^ "_options")) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
365 |
(Scan.lift (Parse.$$$ "=" |-- Args.name) >> |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
366 |
(Thm.declaration_attribute o K o set_solver_options name)) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
367 |
("Additional command line options for SMT solver " ^ quote name) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
368 |
end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
369 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
370 |
end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
371 |
|
36898 | 372 |
val all_solver_names_of = Symtab.keys o Solvers.get |
373 |
val lookup_solver = Symtab.lookup o Solvers.get |
|
374 |
||
375 |
||
376 |
||
377 |
(* selected solver *) |
|
378 |
||
379 |
structure Selected_Solver = Generic_Data |
|
380 |
( |
|
381 |
type T = string |
|
382 |
val empty = no_solver |
|
383 |
val extend = I |
|
384 |
fun merge (s, _) = s |
|
385 |
) |
|
386 |
||
387 |
val solver_name_of = Selected_Solver.get |
|
388 |
||
389 |
fun select_solver name context = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
390 |
if is_none (lookup_solver context name) |
36898 | 391 |
then error ("SMT solver not registered: " ^ quote name) |
392 |
else Selected_Solver.map (K name) context |
|
393 |
||
394 |
fun raw_solver_of context name = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
395 |
(case lookup_solver context name of |
36898 | 396 |
NONE => error "No SMT solver selected" |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
397 |
| SOME s => s) |
36898 | 398 |
|
399 |
fun solver_of context = |
|
400 |
let val name = solver_name_of context |
|
401 |
in gen_solver name (raw_solver_of context name) end |
|
402 |
||
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
403 |
fun is_locally_installed ctxt = |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
404 |
let |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
405 |
val name = solver_name_of (Context.Proof ctxt) |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
406 |
val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
407 |
in is_some (get_local_solver env_var) end |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
408 |
|
36898 | 409 |
|
410 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
411 |
(* SMT filter *) |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
412 |
|
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
413 |
val has_topsort = Term.exists_type (Term.exists_subtype (fn |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
414 |
TFree (_, []) => true |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
415 |
| TVar (_, []) => true |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
416 |
| _ => false)) |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
417 |
|
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
418 |
fun smt_solver rm ctxt irules = |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
419 |
(* without this test, we would run into problems when atomizing the rules: *) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
420 |
if exists (has_topsort o Thm.prop_of o snd) irules |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
421 |
then raise SMT (Other_Failure "proof state contains the universal sort {}") |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
422 |
else solver_of (Context.Proof ctxt) rm ctxt irules |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
423 |
|
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
424 |
fun smt_filter run_remote time_limit st xrules i = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
425 |
let |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
426 |
val {context, facts, goal} = Proof.goal st |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
427 |
val ctxt = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
428 |
context |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
429 |
|> Config.put timeout (Time.toSeconds time_limit) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
430 |
|> Config.put oracle false |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
431 |
|> Config.put filter_only true |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
432 |
val cprop = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
433 |
Thm.cprem_of goal i |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
434 |
|> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
435 |
|> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
436 |
val irs = map (pair ~1) (Thm.assume cprop :: facts) |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
437 |
val rm = SOME run_remote |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
438 |
in |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
439 |
split_list xrules |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
440 |
||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
441 |
|-> map_filter o try o nth |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
442 |
|> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE}) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
443 |
end |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
444 |
handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE} |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
445 |
(* FIXME: measure runtime *) |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
446 |
|
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
447 |
|
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
448 |
|
36898 | 449 |
(* SMT tactic *) |
450 |
||
451 |
fun smt_tac' pass_exns ctxt rules = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
452 |
CONVERSION (SMT_Normalize.atomize_conv ctxt) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
453 |
THEN' Tactic.rtac @{thm ccontr} |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
454 |
THEN' SUBPROOF (fn {context=cx, prems, ...} => |
40165 | 455 |
let |
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset
|
456 |
fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems))) |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
457 |
val name = solver_name_of (Context.Proof cx) |
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
458 |
val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name) |
40165 | 459 |
in |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
460 |
(if pass_exns then SOME (solve ()) |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
461 |
else (SOME (solve ()) handle SMT fail => (trace fail; NONE))) |
40165 | 462 |
|> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
463 |
end) ctxt |
36898 | 464 |
|
465 |
val smt_tac = smt_tac' false |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
466 |
|
36898 | 467 |
val smt_method = |
468 |
Scan.optional Attrib.thms [] >> |
|
469 |
(fn thms => fn ctxt => METHOD (fn facts => |
|
470 |
HEADGOAL (smt_tac ctxt (thms @ facts)))) |
|
471 |
||
472 |
||
473 |
||
474 |
(* setup *) |
|
475 |
||
476 |
val setup = |
|
38808 | 477 |
Attrib.setup @{binding smt_solver} |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset
|
478 |
(Scan.lift (Parse.$$$ "=" |-- Args.name) >> |
36898 | 479 |
(Thm.declaration_attribute o K o select_solver)) |
480 |
"SMT solver configuration" #> |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
481 |
setup_oracle #> |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
482 |
setup_filter_only #> |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
483 |
setup_datatypes #> |
36898 | 484 |
setup_timeout #> |
485 |
setup_trace #> |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
486 |
setup_trace_used_facts #> |
36898 | 487 |
setup_fixed_certificates #> |
38808 | 488 |
Attrib.setup @{binding smt_certificates} |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset
|
489 |
(Scan.lift (Parse.$$$ "=" |-- Args.name) >> |
36898 | 490 |
(Thm.declaration_attribute o K o select_certificates)) |
491 |
"SMT certificates" #> |
|
38808 | 492 |
Method.setup @{binding smt} smt_method |
36898 | 493 |
"Applies an SMT solver to the current goal." |
494 |
||
495 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
496 |
fun print_setup context = |
36898 | 497 |
let |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
498 |
val t = string_of_int (Config.get_generic context timeout) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
499 |
val names = sort_strings (all_solver_names_of context) |
36898 | 500 |
val ns = if null names then [no_solver] else names |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
501 |
val n = solver_name_of context |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
502 |
val opts = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
503 |
(case Symtab.lookup (Solvers.get context) n of |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
504 |
NONE => [] |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
505 |
| SOME {more_options, options, ...} => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
506 |
more_options @ options (Context.proof_of context)) |
36898 | 507 |
val certs_filename = |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
508 |
(case get_certificates_path context of |
36898 | 509 |
SOME path => Path.implode path |
510 |
| NONE => "(disabled)") |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
511 |
val fixed = if Config.get_generic context fixed_certificates then "true" |
36898 | 512 |
else "false" |
513 |
in |
|
514 |
Pretty.writeln (Pretty.big_list "SMT setup:" [ |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
515 |
Pretty.str ("Current SMT solver: " ^ n), |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
516 |
Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), |
36898 | 517 |
Pretty.str_list "Available SMT solvers: " "" ns, |
518 |
Pretty.str ("Current timeout: " ^ t ^ " seconds"), |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
519 |
Pretty.str ("With proofs: " ^ |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
520 |
(if Config.get_generic context oracle then "false" else "true")), |
36898 | 521 |
Pretty.str ("Certificates cache: " ^ certs_filename), |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
522 |
Pretty.str ("Fixed certificates: " ^ fixed)]) |
36898 | 523 |
end |
524 |
||
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset
|
525 |
val _ = |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset
|
526 |
Outer_Syntax.improper_command "smt_status" |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
527 |
"show the available SMT solvers and the currently selected solver" |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset
|
528 |
Keyword.diag |
36898 | 529 |
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => |
530 |
print_setup (Context.Proof (Toplevel.context_of state))))) |
|
531 |
||
532 |
end |