author | boehmes |
Wed, 30 May 2012 23:10:42 +0200 | |
changeset 48043 | 3ff2c76c9f64 |
parent 47701 | 157e6108a342 |
child 48532 | c0f44941e674 |
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, |
48043
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47701
diff
changeset
|
13 |
class: Proof.context -> SMT_Utils.class, |
41432
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*) |
46464 | 42 |
val smt_tac: Proof.context -> thm list -> int -> tactic |
43 |
val smt_tac': Proof.context -> thm list -> int -> tactic |
|
36898 | 44 |
end |
45 |
||
46 |
structure SMT_Solver: SMT_SOLVER = |
|
47 |
struct |
|
48 |
||
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
|
49 |
|
36898 | 50 |
(* interface to external solvers *) |
51 |
||
52 |
local |
|
53 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
54 |
fun make_cmd command options problem_path proof_path = space_implode " " ( |
41601 | 55 |
map File.shell_quote (command () @ options) @ |
36898 | 56 |
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
57 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
in f x end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
61 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
62 |
fun run ctxt name mk_cmd input = |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
63 |
(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
|
64 |
NONE => |
46743
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
65 |
if not (SMT_Config.is_available ctxt name) then |
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
66 |
error ("The SMT solver " ^ quote name ^ " is not installed.") |
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
67 |
else 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
|
68 |
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
|
69 |
(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
|
70 |
else |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
71 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
in Cache_IO.raw_run mk_cmd input in_path out_path end |
36898 | 76 |
| SOME certs => |
77 |
(case Cache_IO.lookup certs input of |
|
78 |
(NONE, key) => |
|
47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46743
diff
changeset
|
79 |
if Config.get ctxt SMT_Config.read_only_certificates then |
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46743
diff
changeset
|
80 |
error ("Bad certificate cache: missing certificate") |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
81 |
else |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
82 |
Cache_IO.run_and_cache certs key mk_cmd input |
36898 | 83 |
| (SOME output, _) => |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
I output)) |
36898 | 87 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
88 |
fun run_solver ctxt name mk_cmd input = |
36898 | 89 |
let |
90 |
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
91 |
(map Pretty.str ls)) |
|
92 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
93 |
val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input |
36898 | 94 |
|
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
|
95 |
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
|
96 |
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
|
97 |
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
36898 | 98 |
|
39811 | 99 |
val ls = rev (snd (chop_while (equal "") (rev res))) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
100 |
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
|
101 |
|
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 |
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
|
103 |
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
36898 | 104 |
in ls end |
105 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
106 |
fun trace_assms ctxt = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
107 |
SMT_Config.trace_msg ctxt (Pretty.string_of o |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
108 |
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
|
109 |
|
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
|
110 |
fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) = |
36898 | 111 |
let |
112 |
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
|
113 |
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
|
114 |
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
36898 | 115 |
in |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
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
|
119 |
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () |
36898 | 120 |
end |
121 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
122 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
123 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
124 |
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
|
125 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
126 |
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
|
127 |
val comments = ("solver: " ^ name) :: |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
128 |
("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) :: |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
129 |
("random seed: " ^ |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
130 |
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
|
131 |
"arguments:" :: options |
36898 | 132 |
|
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
|
133 |
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
|
134 |
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
|
135 |
|> 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
|
136 |
|> 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
|
137 |
||> tap trace_recon_data |
41601 | 138 |
in (run_solver ctxt' name (make_cmd command options) str, recon) end |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
139 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
140 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
141 |
|
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 |
(* configuration *) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
144 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
145 |
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
|
146 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
147 |
type solver_config = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
148 |
name: string, |
48043
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47701
diff
changeset
|
149 |
class: Proof.context -> SMT_Utils.class, |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
150 |
avail: unit -> bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
151 |
command: unit -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
152 |
options: Proof.context -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
153 |
default_max_relevant: int, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
154 |
supports_filter: bool, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
term list * term list) option, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
158 |
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
|
159 |
int list * thm) option } |
41041 | 160 |
|
161 |
||
162 |
(* registry *) |
|
163 |
||
164 |
type solver_info = { |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
165 |
command: unit -> string list, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
166 |
default_max_relevant: int, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
167 |
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
|
168 |
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
|
169 |
int list * thm } |
36898 | 170 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
171 |
structure Solvers = Generic_Data |
36898 | 172 |
( |
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
|
173 |
type T = solver_info Symtab.table |
36898 | 174 |
val empty = Symtab.empty |
175 |
val extend = I |
|
176 |
fun merge data = Symtab.merge (K true) data |
|
177 |
) |
|
178 |
||
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
|
179 |
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
|
180 |
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
|
181 |
(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
|
182 |
(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
|
183 |
(Unsat, ls) => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
184 |
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
|
185 |
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
|
186 |
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
|
187 |
| (result, ls) => |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
188 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
189 |
val (ts, us) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
190 |
(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
|
191 |
in |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
192 |
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
|
193 |
is_real_cex = (result = Sat), |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
194 |
free_constraints = ts, |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
|
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 |
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
|
199 |
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
|
200 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
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
|
202 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
203 |
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
|
204 |
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
|
205 |
|
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
|
206 |
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
|
207 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
208 |
fun solver ocl = { |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
209 |
command = command, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
210 |
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
|
211 |
supports_filter = supports_filter, |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
212 |
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
|
213 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
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
|
217 |
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
|
218 |
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
|
219 |
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
|
220 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
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
|
222 |
|
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
|
223 |
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
|
224 |
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
|
225 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
226 |
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
|
227 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
228 |
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
|
229 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
230 |
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
|
231 |
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
|
232 |
in (name, get_info ctxt name) end |
36898 | 233 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
234 |
fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt |
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
235 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
236 |
fun gen_apply (ithms, ctxt) = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
237 |
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
|
238 |
in |
46743
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
239 |
(ithms, ctxt) |
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
240 |
|-> invoke name command |
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
241 |
|> reconstruct ctxt |
8e365bc843e9
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset
|
242 |
|>> distinct (op =) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
243 |
end |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
244 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
245 |
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
|
246 |
|
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 |
val default_max_relevant = #default_max_relevant oo get_info |
36898 | 248 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
249 |
val supports_filter = #supports_filter o snd o name_and_info_of |
36898 | 250 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
251 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
252 |
(* 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
|
253 |
|
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 |
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
|
255 |
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
|
256 |
| 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
|
257 |
| _ => 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
|
258 |
|
41239 | 259 |
(* without this test, we would run into problems when atomizing the rules: *) |
260 |
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
|
261 |
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
|
262 |
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
|
263 |
"contains the universal sort {}")) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
264 |
else () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
265 |
|
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 |
(* 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
|
268 |
|
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
|
269 |
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
|
270 |
|
41239 | 271 |
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
|
272 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
273 |
type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
41239 | 274 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
275 |
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
|
276 |
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
|
277 |
val ctxt = |
40199 | 278 |
Proof.context_of st |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
279 |
|> Config.put SMT_Config.oracle false |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
280 |
|> Config.put SMT_Config.drop_bad_facts true |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
281 |
|> 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
|
282 |
|
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 |
val {facts, goal, ...} = Proof.goal st |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
284 |
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46464
diff
changeset
|
285 |
fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply |
42320
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
286 |
val cprop = |
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
287 |
(case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) of |
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
288 |
SOME ct => ct |
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
289 |
| NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure ( |
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
290 |
"goal is not a HOL term"))) |
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
|
291 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
292 |
map snd xwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
293 |
|> map_index I |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
294 |
|> 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
|
295 |
|> tap check_topsort |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
296 |
|> gen_preprocess ctxt' |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
297 |
|> pair (map (apsnd snd) xwthms) |
41239 | 298 |
end |
299 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
300 |
fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = |
41241 | 301 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
302 |
val ctxt' = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
303 |
ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
304 |
|> 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
|
305 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
306 |
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
|
307 |
| filter_thms true = map_filter (try (nth xthms)) o fst |
41241 | 308 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
309 |
(ithms, ctxt') |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
310 |
|> gen_apply |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
311 |
|> 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
|
312 |
|> 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
|
313 |
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
|
314 |
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
|
315 |
|
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
|
316 |
|
36898 | 317 |
(* SMT tactic *) |
318 |
||
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
319 |
local |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
320 |
fun trace_assumptions ctxt iwthms idxs = |
40165 | 321 |
let |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
322 |
val wthms = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
323 |
idxs |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
324 |
|> filter (fn i => i >= 0) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
325 |
|> map_filter (AList.lookup (op =) iwthms) |
40165 | 326 |
in |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
327 |
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
|
328 |
then |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
329 |
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
|
330 |
(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
|
331 |
else () |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
332 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
333 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
334 |
fun solve ctxt iwthms = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
335 |
iwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
336 |
|> tap check_topsort |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
337 |
|> apply_solver ctxt |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
338 |
|>> trace_assumptions ctxt iwthms |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
339 |
|> snd |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
340 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
341 |
fun str_of ctxt fail = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
342 |
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
|
343 |
|> prefix ("Solver " ^ SMT_Config.solver_of ctxt ^ ": ") |
36898 | 344 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
345 |
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
|
346 |
handle |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
347 |
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
|
348 |
(SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) |
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset
|
349 |
| SMT_Failure.SMT (fail as SMT_Failure.Time_Out) => |
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset
|
350 |
error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^ |
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset
|
351 |
SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^ |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42320
diff
changeset
|
352 |
"configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)") |
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset
|
353 |
| SMT_Failure.SMT fail => error (str_of ctxt fail) |
41432
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 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
|
356 |
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
|
357 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
358 |
fun resolve (SOME thm) = Tactic.rtac thm 1 |
46464 | 359 |
| resolve NONE = no_tac |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
360 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
361 |
fun tac prove ctxt rules = |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
362 |
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
|
363 |
THEN' Tactic.rtac @{thm ccontr} |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
364 |
THEN' SUBPROOF (fn {context, prems, ...} => |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
365 |
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
|
366 |
in |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
367 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
368 |
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
|
369 |
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
|
370 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
371 |
end |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
372 |
|
36898 | 373 |
end |