author | boehmes |
Mon, 10 Jan 2011 17:39:54 +0100 | |
changeset 41497 | 3fd79c771ed2 |
parent 41472 | f6ab14e61604 |
child 41601 | fda8511006f9 |
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*) |
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
|
10 |
datatype outcome = Unsat | Sat | Unknown |
36898 | 11 |
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
|
12 |
name: string, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
13 |
class: SMT_Utils.class, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
14 |
avail: unit -> bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
15 |
command: unit -> string list, |
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
|
16 |
options: Proof.context -> string list, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
17 |
default_max_relevant: int, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
18 |
supports_filter: bool, |
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
|
19 |
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
|
20 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
21 |
term list * term list) option, |
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 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
23 |
int list * thm) option } |
36898 | 24 |
|
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
|
25 |
(*registry*) |
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
|
26 |
val add_solver: solver_config -> theory -> theory |
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
27 |
val solver_name_of: Proof.context -> string |
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
28 |
val available_solvers_of: Proof.context -> string list |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
29 |
val apply_solver: Proof.context -> (int * (int option * thm)) list -> |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
30 |
int list * thm |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
31 |
val default_max_relevant: Proof.context -> string -> int |
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*) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
34 |
type 'a smt_filter_data = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
35 |
('a * thm) list * ((int * thm) list * Proof.context) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
36 |
val smt_filter_preprocess: Proof.state -> |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
37 |
('a * (int option * thm)) list -> int -> 'a smt_filter_data |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
38 |
val smt_filter_apply: Time.time -> 'a smt_filter_data -> |
41239 | 39 |
{outcome: SMT_Failure.failure option, used_facts: ('a * thm) list} |
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
|
40 |
|
36898 | 41 |
(*tactic*) |
42 |
val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
43 |
val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic |
36898 | 44 |
|
45 |
(*setup*) |
|
46 |
val setup: theory -> theory |
|
47 |
end |
|
48 |
||
49 |
structure SMT_Solver: SMT_SOLVER = |
|
50 |
struct |
|
51 |
||
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
|
52 |
|
36898 | 53 |
(* interface to external solvers *) |
54 |
||
55 |
local |
|
56 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
57 |
fun make_cmd command options problem_path proof_path = space_implode " " ( |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
58 |
map File.shell_quote (command @ options) @ |
36898 | 59 |
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
60 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
61 |
fun trace_and ctxt msg f x = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
62 |
let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
63 |
in f x end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
64 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
65 |
fun run ctxt name mk_cmd input = |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
66 |
(case SMT_Config.certificates_of ctxt of |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
67 |
NONE => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
68 |
if Config.get ctxt SMT_Config.debug_files = "" then |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
69 |
trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
70 |
(Cache_IO.run mk_cmd) input |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
71 |
else |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
72 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
73 |
val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
74 |
val in_path = Path.ext "smt_in" base_path |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
75 |
val out_path = Path.ext "smt_out" base_path |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
76 |
in Cache_IO.raw_run mk_cmd input in_path out_path end |
36898 | 77 |
| SOME certs => |
78 |
(case Cache_IO.lookup certs input of |
|
79 |
(NONE, key) => |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
80 |
if Config.get ctxt SMT_Config.fixed then |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
81 |
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
|
82 |
else |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
83 |
Cache_IO.run_and_cache certs key mk_cmd input |
36898 | 84 |
| (SOME output, _) => |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
85 |
trace_and ctxt ("Using cached certificate from " ^ |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
86 |
File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
87 |
I output)) |
36898 | 88 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
89 |
fun run_solver ctxt name mk_cmd input = |
36898 | 90 |
let |
91 |
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
92 |
(map Pretty.str ls)) |
|
93 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
94 |
val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input |
36898 | 95 |
|
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
|
96 |
val {redirected_output=res, output=err, return_code} = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
97 |
SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
98 |
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
36898 | 99 |
|
39811 | 100 |
val ls = rev (snd (chop_while (equal "") (rev res))) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
101 |
val _ = SMT_Config.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
|
102 |
|
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
|
103 |
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
|
104 |
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
36898 | 105 |
in ls end |
106 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
107 |
fun trace_assms ctxt = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
108 |
SMT_Config.trace_msg ctxt (Pretty.string_of o |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
109 |
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
|
110 |
|
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
111 |
fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) = |
36898 | 112 |
let |
113 |
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
|
114 |
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
|
115 |
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
36898 | 116 |
in |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
117 |
SMT_Config.trace_msg ctxt (fn () => |
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
|
118 |
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
|
119 |
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
|
120 |
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () |
36898 | 121 |
end |
122 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
123 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
124 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
125 |
fun invoke name command ithms 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
|
126 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
127 |
val options = SMT_Config.solver_options_of 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
|
128 |
val comments = ("solver: " ^ name) :: |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
129 |
("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) :: |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
130 |
("random seed: " ^ |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
131 |
string_of_int (Config.get ctxt SMT_Config.random_seed)) :: |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
132 |
"arguments:" :: options |
36898 | 133 |
|
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
134 |
val (str, recon as {context=ctxt', ...}) = |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
135 |
ithms |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
136 |
|> tap (trace_assms ctxt) |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
137 |
|> SMT_Translate.translate ctxt comments |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
138 |
||> tap trace_recon_data |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
139 |
in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
140 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
141 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
142 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
143 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
144 |
(* configuration *) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
145 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
146 |
datatype outcome = Unsat | Sat | Unknown |
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
|
147 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
148 |
type solver_config = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
149 |
name: string, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
150 |
class: SMT_Utils.class, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
151 |
avail: unit -> bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
152 |
command: unit -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
153 |
options: Proof.context -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
154 |
default_max_relevant: int, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
155 |
supports_filter: bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
156 |
outcome: string -> string list -> outcome * string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
157 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
158 |
term list * term list) option, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
159 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
160 |
int list * thm) option } |
41041 | 161 |
|
162 |
||
163 |
(* registry *) |
|
164 |
||
165 |
type solver_info = { |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
166 |
command: unit -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
167 |
default_max_relevant: int, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
168 |
supports_filter: bool, |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
169 |
reconstruct: Proof.context -> string list * SMT_Translate.recon -> |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
170 |
int list * thm } |
36898 | 171 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
172 |
structure Solvers = Generic_Data |
36898 | 173 |
( |
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
|
174 |
type T = solver_info Symtab.table |
36898 | 175 |
val empty = Symtab.empty |
176 |
val extend = I |
|
177 |
fun merge data = Symtab.merge (K true) data |
|
178 |
) |
|
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 |
local |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
181 |
fun finish outcome cex_parser reconstruct ocl outer_ctxt |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
182 |
(output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) = |
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
|
183 |
(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
|
184 |
(Unsat, ls) => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
185 |
if not (Config.get ctxt SMT_Config.oracle) andalso is_some reconstruct |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
186 |
then the reconstruct outer_ctxt recon ls |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
187 |
else ([], ocl ()) |
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
|
188 |
| (result, ls) => |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
189 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
190 |
val (ts, us) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
191 |
(case cex_parser of SOME f => f ctxt recon ls | _ => ([], [])) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
192 |
in |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
193 |
raise SMT_Failure.SMT (SMT_Failure.Counterexample { |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
194 |
is_real_cex = (result = Sat), |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
195 |
free_constraints = ts, |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
196 |
const_defs = us}) |
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
|
197 |
end) |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
198 |
|
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
199 |
val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const 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
|
200 |
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
|
201 |
|
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
|
202 |
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
|
203 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
204 |
val {name, class, avail, command, options, default_max_relevant, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
205 |
supports_filter, outcome, cex_parser, reconstruct} = cfg |
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
|
206 |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
207 |
fun core_oracle () = cfalse |
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
|
208 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
209 |
fun solver ocl = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
210 |
command = command, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
211 |
default_max_relevant = default_max_relevant, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
212 |
supports_filter = supports_filter, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
213 |
reconstruct = finish (outcome name) cex_parser reconstruct ocl } |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
214 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
215 |
val info = {name=name, class=class, avail=avail, options=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
|
216 |
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
|
217 |
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
|
218 |
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
219 |
Context.theory_map (SMT_Config.add_solver info) |
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
|
220 |
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
|
221 |
|
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
|
222 |
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
|
223 |
|
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
224 |
fun get_info ctxt name = |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
225 |
the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
226 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
227 |
val solver_name_of = SMT_Config.solver_of |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
228 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
229 |
val available_solvers_of = SMT_Config.available_solvers_of |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
230 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
231 |
fun name_and_info_of ctxt = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
232 |
let val name = solver_name_of ctxt |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
233 |
in (name, get_info ctxt name) end |
36898 | 234 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
235 |
fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt |
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
236 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
237 |
fun gen_apply (ithms, ctxt) = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
238 |
let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
239 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
240 |
(ithms, ctxt) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
241 |
|-> invoke name command |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
242 |
|> reconstruct ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
243 |
|>> distinct (op =) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
244 |
end |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
245 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
246 |
fun apply_solver ctxt = gen_apply o gen_preprocess ctxt |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
247 |
|
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
248 |
val default_max_relevant = #default_max_relevant oo get_info |
36898 | 249 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
250 |
val supports_filter = #supports_filter o snd o name_and_info_of |
36898 | 251 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
252 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
253 |
(* check well-sortedness *) |
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
|
254 |
|
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
|
255 |
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
|
256 |
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
|
257 |
| 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
|
258 |
| _ => 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
|
259 |
|
41239 | 260 |
(* without this test, we would run into problems when atomizing the rules: *) |
261 |
fun check_topsort iwthms = |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
262 |
if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then |
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
|
263 |
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
|
264 |
"contains the universal sort {}")) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
265 |
else () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
266 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
267 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
268 |
(* filter *) |
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
|
269 |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
270 |
val cnot = Thm.cterm_of @{theory} @{const Not} |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
271 |
|
41239 | 272 |
fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
273 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
274 |
type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
41239 | 275 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
276 |
fun smt_filter_preprocess st xwthms 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
|
277 |
let |
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
|
278 |
val ctxt = |
40199 | 279 |
Proof.context_of st |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
280 |
|> Config.put SMT_Config.oracle false |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
281 |
|> Config.put SMT_Config.drop_bad_facts true |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
282 |
|> Config.put SMT_Config.filter_only_facts true |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
283 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
284 |
val {facts, goal, ...} = Proof.goal st |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
285 |
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
286 |
fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
287 |
val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) |
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 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
289 |
map snd xwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
290 |
|> map_index I |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
291 |
|> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
292 |
|> tap check_topsort |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
293 |
|> gen_preprocess ctxt' |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
294 |
|> pair (map (apsnd snd) xwthms) |
41239 | 295 |
end |
296 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
297 |
fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = |
41241 | 298 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
299 |
val ctxt' = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
300 |
ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
301 |
|> Config.put SMT_Config.timeout (Time.toReal time_limit) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
302 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
303 |
fun filter_thms false = K xthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
304 |
| filter_thms true = map_filter (try (nth xthms)) o fst |
41241 | 305 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
306 |
(ithms, ctxt') |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
307 |
|> gen_apply |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
308 |
|> filter_thms (supports_filter ctxt') |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
309 |
|> mk_result 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
|
310 |
end |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
311 |
handle SMT_Failure.SMT fail => mk_result (SOME fail) [] |
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
|
312 |
|
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
|
313 |
|
36898 | 314 |
(* SMT tactic *) |
315 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
316 |
local |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
317 |
fun trace_assumptions ctxt iwthms idxs = |
40165 | 318 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
319 |
val wthms = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
320 |
idxs |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
321 |
|> filter (fn i => i >= 0) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
322 |
|> map_filter (AList.lookup (op =) iwthms) |
40165 | 323 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
324 |
if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0 |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
325 |
then |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
326 |
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
327 |
(map (Display.pretty_thm ctxt o snd) wthms))) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
328 |
else () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
329 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
330 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
331 |
fun solve ctxt iwthms = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
332 |
iwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
333 |
|> tap check_topsort |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
334 |
|> apply_solver ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
335 |
|>> trace_assumptions ctxt iwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
336 |
|> snd |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
337 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
338 |
fun str_of ctxt fail = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
339 |
SMT_Failure.string_of_failure ctxt fail |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
340 |
|> prefix ("Solver " ^ SMT_Config.solver_of ctxt ^ ": ") |
36898 | 341 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
342 |
fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
343 |
handle |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
344 |
SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
345 |
(SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
346 |
| SMT_Failure.SMT fail => |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
347 |
(SMT_Config.trace_msg ctxt (str_of ctxt) fail; NONE) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
348 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
349 |
fun tag_rules thms = map_index (apsnd (pair NONE)) thms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
350 |
fun tag_prems thms = map (pair ~1 o pair NONE) thms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
351 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
352 |
fun resolve (SOME thm) = Tactic.rtac thm 1 |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
353 |
| resolve NONE = Tactical.no_tac |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
354 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
355 |
fun tac prove ctxt rules = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
356 |
CONVERSION (SMT_Normalize.atomize_conv ctxt) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
357 |
THEN' Tactic.rtac @{thm ccontr} |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
358 |
THEN' SUBPROOF (fn {context, prems, ...} => |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
359 |
resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
360 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
361 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
362 |
val smt_tac = tac safe_solve |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
363 |
val smt_tac' = tac (SOME oo solve) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
364 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
365 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
366 |
|
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
|
367 |
|
36898 | 368 |
val smt_method = |
369 |
Scan.optional Attrib.thms [] >> |
|
370 |
(fn thms => fn ctxt => METHOD (fn facts => |
|
371 |
HEADGOAL (smt_tac ctxt (thms @ facts)))) |
|
372 |
||
373 |
||
374 |
(* setup *) |
|
375 |
||
376 |
val setup = |
|
38808 | 377 |
Method.setup @{binding smt} smt_method |
36898 | 378 |
"Applies an SMT solver to the current goal." |
379 |
||
380 |
end |