author | wenzelm |
Fri, 25 Sep 2015 20:37:59 +0200 | |
changeset 61268 | abe08fb15a12 |
parent 60752 | b48830b670a1 |
child 62549 | 9498623b27f0 |
permissions | -rw-r--r-- |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
1 |
(* Title: HOL/Library/Old_SMT/old_smt_solver.ML |
36898 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
||
4 |
SMT solvers registry and SMT tactic. |
|
5 |
*) |
|
6 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
7 |
signature OLD_SMT_SOLVER = |
36898 | 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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
13 |
class: Proof.context -> Old_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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
20 |
cex_parser: (Proof.context -> Old_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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
22 |
reconstruct: (Proof.context -> Old_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) |
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset
|
36 |
val smt_filter_preprocess: Proof.context -> thm list -> thm -> |
41432
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 -> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
39 |
{outcome: Old_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 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
46 |
structure Old_SMT_Solver: OLD_SMT_SOLVER = |
36898 | 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 " " ( |
48532
c0f44941e674
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents:
48043
diff
changeset
|
55 |
"(exec 2>&1;" :: map File.shell_quote (command () @ options) @ |
c0f44941e674
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents:
48043
diff
changeset
|
56 |
[File.shell_path problem_path, ")", ">", File.shell_path proof_path]) |
36898 | 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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
59 |
let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) () |
41432
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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
63 |
(case Old_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 => |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
65 |
if not (Old_SMT_Config.is_available ctxt name) then |
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
|
66 |
error ("The SMT solver " ^ quote name ^ " is not installed.") |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
67 |
else if Config.get ctxt Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
72 |
val base_path = Path.explode (Config.get ctxt Old_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) => |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
79 |
if Config.get ctxt Old_SMT_Config.read_only_certificates then |
47152
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 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
93 |
val _ = Old_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} = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
96 |
Old_SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
97 |
val _ = Old_SMT_Config.trace_msg ctxt (pretty "Solver:") err |
36898 | 98 |
|
48902
44a6967240b7
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents:
48534
diff
changeset
|
99 |
val ls = fst (take_suffix (equal "") res) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
100 |
val _ = Old_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 |
|
48534
2307efbfc554
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
blanchet
parents:
48532
diff
changeset
|
102 |
val _ = return_code <> 0 andalso |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
103 |
raise Old_SMT_Failure.SMT (Old_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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
107 |
Old_SMT_Config.trace_msg ctxt (Pretty.string_of o |
61268 | 108 |
Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
109 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
110 |
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
116 |
Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
126 |
val options = Old_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) :: |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
128 |
("timeout: " ^ string_of_real (Config.get ctxt Old_SMT_Config.timeout)) :: |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41300
diff
changeset
|
129 |
("random seed: " ^ |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
130 |
string_of_int (Config.get ctxt Old_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) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
136 |
|> Old_SMT_Translate.translate ctxt comments |
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
|
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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
149 |
class: Proof.context -> Old_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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
156 |
cex_parser: (Proof.context -> Old_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
|
157 |
term list * term list) option, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
158 |
reconstruct: (Proof.context -> Old_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
|
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, |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
168 |
reconstruct: Proof.context -> string list * Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
181 |
(output, (recon as {context=ctxt, ...} : Old_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) => |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
184 |
if not (Config.get ctxt Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
192 |
raise Old_SMT_Failure.SMT (Old_SMT_Failure.Counterexample { |
40828
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 |
|
59634 | 198 |
val cfalse = Thm.cterm_of @{context} (@{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)))) #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
218 |
Context.theory_map (Old_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 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
226 |
val solver_name_of = Old_SMT_Config.solver_of |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
227 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
228 |
val available_solvers_of = Old_SMT_Config.available_solvers_of |
41432
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 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
234 |
fun gen_preprocess ctxt iwthms = Old_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: *) |
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
260 |
fun check_topsort ctxt thm = |
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
261 |
if has_topsort (Thm.prop_of thm) then |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
262 |
(Old_SMT_Normalize.drop_fact_warning ctxt thm; TrueI) |
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
263 |
else |
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
264 |
thm |
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
265 |
|
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
266 |
fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms |
41432
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 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
269 |
(* 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
|
270 |
|
59634 | 271 |
val cnot = Thm.cterm_of @{context} @{const Not} |
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
|
272 |
|
41239 | 273 |
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
|
274 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset
|
275 |
type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
41239 | 276 |
|
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset
|
277 |
fun smt_filter_preprocess ctxt facts goal 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
|
278 |
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
|
279 |
val ctxt = |
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset
|
280 |
ctxt |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
281 |
|> Config.put Old_SMT_Config.oracle false |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
282 |
|> Config.put Old_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 |
|
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
59634
diff
changeset
|
284 |
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE 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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
287 |
(case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of |
42320
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset
|
288 |
SOME ct => ct |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
289 |
| NONE => raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ( |
42320
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)) |
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
295 |
|> check_topsorts ctxt' |
41432
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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
304 |
|> Config.put Old_SMT_Config.timeout (Time.toReal time_limit) |
41432
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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
314 |
handle Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
327 |
if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0 |
41432
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:" |
61268 | 330 |
(map (Thm.pretty_thm ctxt o snd) wthms))) |
41432
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 |
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset
|
336 |
|> check_topsorts ctxt |
41432
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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
342 |
Old_SMT_Failure.string_of_failure ctxt fail |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
343 |
|> prefix ("Solver " ^ Old_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 |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
347 |
Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Counterexample _) => |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
348 |
(Old_SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
349 |
| Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Time_Out) => |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
350 |
error ("SMT: Solver " ^ quote (Old_SMT_Config.solver_of ctxt) ^ ": " ^ |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
351 |
Old_SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^ |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
352 |
"configuration option " ^ quote (Config.name_of Old_SMT_Config.timeout) ^ " might help)") |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
353 |
| Old_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 |
|
60752 | 358 |
fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 |
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 = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
362 |
CONVERSION (Old_SMT_Normalize.atomize_conv ctxt) |
60752 | 363 |
THEN' resolve_tac ctxt @{thms ccontr} |
364 |
THEN' SUBPROOF (fn {context = ctxt', prems, ...} => |
|
365 |
resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt |
|
41432
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 |