author | boehmes |
Mon, 15 Nov 2010 22:23:28 +0100 | |
changeset 40561 | 0125cbb5d3c7 |
parent 40560 | b57f7fee72ee |
child 40578 | 2b098a549450 |
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 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
9 |
(*configuration*) |
36898 | 10 |
type interface = { |
11 |
extra_norm: SMT_Normalize.extra_norm, |
|
12 |
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
|
13 |
datatype outcome = Unsat | Sat | Unknown |
36898 | 14 |
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
|
15 |
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
|
16 |
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
|
17 |
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
|
18 |
options: Proof.context -> string list, |
36898 | 19 |
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
(int list * thm) * Proof.context) option } |
36898 | 25 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
26 |
(*registry*) |
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
|
27 |
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
|
28 |
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
|
29 |
val add_solver: solver_config -> theory -> theory |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
30 |
val solver_of: Proof.context -> solver |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
31 |
val is_locally_installed: Proof.context -> bool |
36898 | 32 |
|
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
|
33 |
(*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
|
34 |
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int -> |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
35 |
{outcome: SMT_Failure.failure option, used_facts: 'a list, |
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
|
36 |
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
|
37 |
|
36898 | 38 |
(*tactic*) |
39 |
val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic |
|
40 |
val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic |
|
41 |
||
42 |
(*setup*) |
|
43 |
val setup: theory -> theory |
|
44 |
end |
|
45 |
||
46 |
structure SMT_Solver: SMT_SOLVER = |
|
47 |
struct |
|
48 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
49 |
structure C = SMT_Config |
36898 | 50 |
|
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
|
51 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
52 |
(* configuration *) |
36898 | 53 |
|
54 |
type interface = { |
|
55 |
extra_norm: SMT_Normalize.extra_norm, |
|
56 |
translate: SMT_Translate.config } |
|
57 |
||
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
|
58 |
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
|
59 |
|
36898 | 60 |
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
|
61 |
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
|
62 |
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
|
63 |
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
|
64 |
options: Proof.context -> string list, |
36898 | 65 |
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
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
(int list * thm) * Proof.context) option } |
36898 | 71 |
|
72 |
||
73 |
(* interface to external solvers *) |
|
74 |
||
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
75 |
fun get_local_solver env_var = |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
|
36898 | 79 |
local |
80 |
||
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
|
81 |
fun choose (rm, env_var, is_remote, name) = |
36898 | 82 |
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
|
83 |
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
|
84 |
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
|
85 |
val lsolver = get_local_solver env_var |
36898 | 86 |
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
|
87 |
val trace = if is_some rm then K () else tracing |
36898 | 88 |
in |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
89 |
if not force_remote andalso is_some lsolver |
36898 | 90 |
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
|
91 |
(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
|
92 |
[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
|
93 |
else if not force_local andalso is_remote |
36898 | 94 |
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
|
95 |
(trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ |
36898 | 96 |
quote remote_url ^ " ..."); |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
97 |
[getenv "REMOTE_SMT", name]) |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
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
|
101 |
"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
|
102 |
quote env_var ^ ".") |
36898 | 103 |
end |
104 |
||
105 |
fun make_cmd solver args problem_path proof_path = space_implode " " ( |
|
106 |
map File.shell_quote (solver @ args) @ |
|
107 |
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
|
108 |
||
109 |
fun run ctxt cmd args input = |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
110 |
(case C.certificates_of ctxt of |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
111 |
NONE => Cache_IO.run (make_cmd (choose cmd) args) input |
36898 | 112 |
| SOME certs => |
113 |
(case Cache_IO.lookup certs input of |
|
114 |
(NONE, key) => |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
115 |
if Config.get ctxt C.fixed then |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
116 |
error ("Bad certificates cache: missing certificate") |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
117 |
else |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
118 |
Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input |
36898 | 119 |
| (SOME output, _) => |
120 |
(tracing ("Using cached certificate from " ^ |
|
121 |
File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); |
|
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
122 |
output))) |
36898 | 123 |
|
124 |
in |
|
125 |
||
126 |
fun run_solver ctxt cmd args input = |
|
127 |
let |
|
128 |
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
129 |
(map Pretty.str ls)) |
|
130 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
131 |
val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input |
36898 | 132 |
|
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
133 |
val {redirected_output=res, output=err, return_code} = |
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
134 |
C.with_timeout ctxt (run ctxt cmd args) input |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
135 |
val _ = C.trace_msg ctxt (pretty "Solver:") err |
36898 | 136 |
|
39811 | 137 |
val ls = rev (snd (chop_while (equal "") (rev res))) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
138 |
val _ = C.trace_msg ctxt (pretty "Result:") ls |
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
139 |
|
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
140 |
val _ = null ls andalso return_code <> 0 andalso |
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40560
diff
changeset
|
141 |
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
36898 | 142 |
in ls end |
143 |
||
144 |
end |
|
145 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
146 |
fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
147 |
Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
148 |
|
36940 | 149 |
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) = |
36898 | 150 |
let |
151 |
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
152 |
fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
153 |
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
36898 | 154 |
in |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
155 |
C.trace_msg ctxt (fn () => |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
156 |
Pretty.string_of (Pretty.big_list "Names:" [ |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
157 |
Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
158 |
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () |
36898 | 159 |
end |
160 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
161 |
fun invoke translate_config name cmd options irules 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
|
162 |
let |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
163 |
val args = C.solver_options_of ctxt @ options 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
|
164 |
val comments = ("solver: " ^ name) :: |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
165 |
("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) :: |
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
|
166 |
"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
|
167 |
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
|
168 |
irules |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
169 |
|> 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
|
170 |
|> 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
|
171 |
||> 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
|
172 |
|>> 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
|
173 |
|> 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
|
174 |
end |
36898 | 175 |
|
176 |
fun discharge_definitions thm = |
|
177 |
if Thm.nprems_of thm = 0 then thm |
|
178 |
else discharge_definitions (@{thm reflexive} RS thm) |
|
179 |
||
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
|
180 |
fun set_has_datatypes with_datatypes translate = |
36898 | 181 |
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
|
182 |
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
|
183 |
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
|
184 |
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
|
185 |
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
|
186 |
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
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
|
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
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
|> 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
|
195 |
in |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
196 |
if Config.get ctxt C.trace_used_facts andalso length thms > 0 |
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
|
197 |
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
|
198 |
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
|
199 |
(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
|
200 |
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
|
201 |
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
|
202 |
|
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
|
203 |
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
|
204 |
let |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
205 |
val {env_var, is_remote, options, interface, reconstruct} = info |
36898 | 206 |
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
|
207 |
val (with_datatypes, translate') = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
208 |
set_has_datatypes (Config.get ctxt C.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
|
209 |
val cmd = (rm, env_var, is_remote, name) |
36898 | 210 |
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
|
211 |
(irules, ctxt) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
212 |
|-> SMT_Normalize.normalize extra_norm with_datatypes |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
213 |
|-> invoke translate' name cmd options |
36898 | 214 |
|-> 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
|
215 |
|-> (fn (idxs, thm) => fn ctxt' => thm |
36898 | 216 |
|> 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
|
217 |
|> 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
|
218 |
|> 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
|
219 |
|> pair idxs) |
36898 | 220 |
end |
221 |
||
222 |
||
223 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
224 |
(* registry *) |
36898 | 225 |
|
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
|
226 |
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
|
227 |
|
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
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
(int list * thm) * Proof.context } |
36898 | 235 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
236 |
structure Solvers = Generic_Data |
36898 | 237 |
( |
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
|
238 |
type T = solver_info Symtab.table |
36898 | 239 |
val empty = Symtab.empty |
240 |
val extend = I |
|
241 |
fun merge data = Symtab.merge (K true) data |
|
242 |
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) |
|
243 |
) |
|
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 |
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
|
246 |
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
|
247 |
(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
|
248 |
(Unsat, ls) => |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
249 |
if not (Config.get ctxt C.oracle) andalso is_some reconstruct |
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
|
250 |
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
|
251 |
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
|
252 |
| (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
|
253 |
let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => []) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
254 |
in |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
255 |
raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts)) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
256 |
end) |
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
|
257 |
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
|
258 |
|
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
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
|
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 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
|
265 |
|
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 |
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
267 |
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
|
268 |
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
|
269 |
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
|
270 |
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
|
271 |
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
272 |
Context.theory_map (C.add_solver name) |
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
|
273 |
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 |
|
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
|
275 |
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
|
276 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
277 |
fun name_and_solver_of ctxt = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
278 |
let val name = C.solver_of ctxt |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
279 |
in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end |
36898 | 280 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
281 |
fun solver_of ctxt = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
282 |
let val (name, raw_solver) = name_and_solver_of ctxt |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
283 |
in gen_solver name raw_solver end |
36898 | 284 |
|
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
285 |
fun is_locally_installed ctxt = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
286 |
let val (_, {env_var, ...}) = name_and_solver_of ctxt |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
287 |
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
|
288 |
|
36898 | 289 |
|
290 |
||
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
291 |
(* 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
|
292 |
|
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
|
293 |
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
|
294 |
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
|
295 |
| 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
|
296 |
| _ => 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
|
297 |
|
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
|
298 |
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
|
299 |
(* without this test, we would run into problems when atomizing the rules: *) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
300 |
if exists (has_topsort o Thm.prop_of o snd) irules then |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
301 |
raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
302 |
"contains the universal sort {}")) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
303 |
else solver_of 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
|
304 |
|
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
|
305 |
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
|
306 |
let |
40199 | 307 |
val {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
|
308 |
val ctxt = |
40199 | 309 |
Proof.context_of st |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
310 |
|> Config.put C.oracle false |
40560
b57f7fee72ee
honour timeouts which are not rounded to full seconds
boehmes
parents:
40550
diff
changeset
|
311 |
|> Config.put C.timeout (Time.toReal time_limit) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
312 |
|> Config.put C.drop_bad_facts true |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
313 |
|> Config.put C.filter_only_facts true |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
314 |
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
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
|
315 |
val cprop = |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
316 |
concl |
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
317 |
|> 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
|
318 |
|> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
319 |
val irs = map (pair ~1) (Thm.assume cprop :: prems @ 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
|
320 |
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
|
321 |
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
|
322 |
split_list xrules |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
323 |
||> 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
|
324 |
|-> 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
|
325 |
|> (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
|
326 |
end |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
327 |
handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[], |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
328 |
run_time_in_msecs=NONE} |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
329 |
(* 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
|
330 |
|
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
|
331 |
|
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
|
332 |
|
36898 | 333 |
(* SMT tactic *) |
334 |
||
335 |
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
|
336 |
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
|
337 |
THEN' Tactic.rtac @{thm ccontr} |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
338 |
THEN' SUBPROOF (fn {context=ctxt', prems, ...} => |
40165 | 339 |
let |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
340 |
fun solve irules = snd (smt_solver NONE ctxt' irules) |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
341 |
val tag = "Solver " ^ C.solver_of ctxt' ^ ": " |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
342 |
val str_of = SMT_Failure.string_of_failure ctxt' |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
343 |
fun safe_solve irules = |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
344 |
if pass_exns then SOME (solve irules) |
40515
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
345 |
else (SOME (solve irules) |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
346 |
handle |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
347 |
SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
348 |
(C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE) |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
349 |
| SMT_Failure.SMT fail => |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
350 |
(C.trace_msg ctxt' (prefix tag o str_of) fail; NONE)) |
40165 | 351 |
in |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset
|
352 |
safe_solve (map (pair ~1) (rules @ prems)) |
40165 | 353 |
|> (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
|
354 |
end) ctxt |
36898 | 355 |
|
356 |
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
|
357 |
|
36898 | 358 |
val smt_method = |
359 |
Scan.optional Attrib.thms [] >> |
|
360 |
(fn thms => fn ctxt => METHOD (fn facts => |
|
361 |
HEADGOAL (smt_tac ctxt (thms @ facts)))) |
|
362 |
||
363 |
||
364 |
||
365 |
(* setup *) |
|
366 |
||
367 |
val setup = |
|
38808 | 368 |
Method.setup @{binding smt} smt_method |
36898 | 369 |
"Applies an SMT solver to the current goal." |
370 |
||
371 |
end |