author | blanchet |
Thu, 21 Apr 2011 18:39:22 +0200 | |
changeset 42444 | 8e5438dc70bb |
parent 42443 | 724e612ba248 |
child 42445 | c6ea64ebb8c5 |
permissions | -rw-r--r-- |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_provers.ML |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
2 |
Author: Fabian Immler, TU Muenchen |
32996
d2e48879e65a
removed disjunctive group cancellation -- provers run independently;
wenzelm
parents:
32995
diff
changeset
|
3 |
Author: Makarius |
35969 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
5 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
6 |
Generic prover abstraction for Sledgehammer. |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
7 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
8 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
9 |
signature SLEDGEHAMMER_PROVERS = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
sig |
40181 | 11 |
type failure = ATP_Proof.failure |
38988 | 12 |
type locality = Sledgehammer_Filter.locality |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
13 |
type relevance_fudge = Sledgehammer_Filter.relevance_fudge |
40114 | 14 |
type translated_formula = Sledgehammer_ATP_Translate.translated_formula |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
15 |
type type_system = Sledgehammer_ATP_Translate.type_system |
40068 | 16 |
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
17 |
|
35969 | 18 |
type params = |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset
|
19 |
{debug: bool, |
35969 | 20 |
verbose: bool, |
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset
|
21 |
overlord: bool, |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset
|
22 |
blocking: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
23 |
provers: string list, |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
24 |
relevance_thresholds: real * real, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
25 |
max_relevant: int option, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
26 |
monomorphize: bool, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
27 |
monomorphize_limit: int, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
28 |
type_sys: type_system, |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset
|
29 |
explicit_apply: bool, |
35969 | 30 |
isar_proof: bool, |
36924 | 31 |
isar_shrink_factor: int, |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
32 |
slicing: bool, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
33 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
34 |
expect: string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
35 |
|
41090 | 36 |
datatype prover_fact = |
37 |
Untranslated_Fact of (string * locality) * thm | |
|
38 |
ATP_Translated_Fact of |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
39 |
translated_formula option * ((string * locality) * thm) | |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
40 |
SMT_Weighted_Fact of (string * locality) * (int option * thm) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
41 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
42 |
type prover_problem = |
39318 | 43 |
{state: Proof.state, |
38998 | 44 |
goal: thm, |
45 |
subgoal: int, |
|
40065 | 46 |
subgoal_count: int, |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
47 |
facts: prover_fact list, |
41741 | 48 |
smt_filter: (string * locality) SMT_Solver.smt_filter_data option} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
49 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
50 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
51 |
{outcome: failure option, |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
52 |
used_facts: (string * locality) list, |
40062 | 53 |
run_time_in_msecs: int option, |
54 |
message: string} |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
55 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
56 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 57 |
|
41168 | 58 |
(* for experimentation purposes -- do not use in production code *) |
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset
|
59 |
val smt_triggers : bool Unsynchronized.ref |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
60 |
val smt_weights : bool Unsynchronized.ref |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
61 |
val smt_weight_min_facts : int Unsynchronized.ref |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
62 |
val smt_min_weight : int Unsynchronized.ref |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
63 |
val smt_max_weight : int Unsynchronized.ref |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
64 |
val smt_max_weight_index : int Unsynchronized.ref |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
65 |
val smt_weight_curve : (int -> int) Unsynchronized.ref |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
66 |
val smt_max_slices : int Unsynchronized.ref |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
67 |
val smt_slice_fact_frac : real Unsynchronized.ref |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
68 |
val smt_slice_time_frac : real Unsynchronized.ref |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
69 |
val smt_slice_min_secs : int Unsynchronized.ref |
41168 | 70 |
|
41089 | 71 |
val das_Tool : string |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
72 |
val select_smt_solver : string -> Proof.context -> Proof.context |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
73 |
val is_smt_prover : Proof.context -> string -> bool |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
74 |
val is_prover_supported : Proof.context -> string -> bool |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
75 |
val is_prover_installed : Proof.context -> string -> bool |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
76 |
val default_max_relevant_for_prover : Proof.context -> bool -> string -> int |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
77 |
val is_built_in_const_for_prover : |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
78 |
Proof.context -> string -> string * typ -> term list -> bool * term list |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
79 |
val atp_relevance_fudge : relevance_fudge |
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
80 |
val smt_relevance_fudge : relevance_fudge |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
81 |
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge |
38023 | 82 |
val dest_dir : string Config.T |
83 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
84 |
val measure_run_time : bool Config.T |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
85 |
val weight_smt_fact : |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
86 |
theory -> int -> ((string * locality) * thm) * int |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
87 |
-> (string * locality) * (int option * thm) |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
88 |
val untranslated_fact : prover_fact -> (string * locality) * thm |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
89 |
val smt_weighted_fact : |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
90 |
theory -> int -> prover_fact * int |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
91 |
-> (string * locality) * (int option * thm) |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
92 |
val supported_provers : Proof.context -> unit |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
93 |
val kill_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
94 |
val running_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
95 |
val messages : int option -> unit |
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
96 |
val get_prover : Proof.context -> bool -> string -> prover |
38023 | 97 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
98 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
99 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
100 |
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
101 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
102 |
|
38028 | 103 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset
|
104 |
open ATP_Proof |
38028 | 105 |
open ATP_Systems |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset
|
106 |
open Metis_Translate |
38023 | 107 |
open Sledgehammer_Util |
38988 | 108 |
open Sledgehammer_Filter |
40068 | 109 |
open Sledgehammer_ATP_Translate |
110 |
open Sledgehammer_ATP_Reconstruct |
|
37583
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
111 |
|
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
112 |
(** The Sledgehammer **) |
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
113 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
114 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
115 |
"Async_Manager". *) |
37585 | 116 |
val das_Tool = "Sledgehammer" |
117 |
||
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
118 |
val select_smt_solver = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
119 |
Context.proof_map o SMT_Config.select_solver |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
120 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
121 |
fun is_smt_prover ctxt name = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
122 |
member (op =) (SMT_Solver.available_solvers_of ctxt) name |
40062 | 123 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
124 |
fun is_prover_supported ctxt name = |
42361 | 125 |
let val thy = Proof_Context.theory_of ctxt in |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
126 |
is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
127 |
end |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
128 |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
129 |
fun is_prover_installed ctxt = |
42361 | 130 |
is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
131 |
|
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
132 |
fun get_slices slicing slices = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
133 |
(0 upto length slices - 1) ~~ slices |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
134 |
|> not slicing ? (List.last #> single) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
135 |
|
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
136 |
fun default_max_relevant_for_prover ctxt slicing name = |
42361 | 137 |
let val thy = Proof_Context.theory_of ctxt in |
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
138 |
if is_smt_prover ctxt name then |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
139 |
SMT_Solver.default_max_relevant ctxt name |
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
140 |
else |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
141 |
fold (Integer.max o snd o snd o snd) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
142 |
(get_slices slicing (#slices (get_atp thy name) ())) 0 |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
143 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
144 |
|
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
145 |
(* These are either simplified away by "Meson.presimplify" (most of the time) or |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
146 |
handled specially via "fFalse", "fTrue", ..., "fequal". *) |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
147 |
val atp_irrelevant_consts = |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
148 |
[@{const_name False}, @{const_name True}, @{const_name Not}, |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
149 |
@{const_name conj}, @{const_name disj}, @{const_name implies}, |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
150 |
@{const_name HOL.eq}, @{const_name If}, @{const_name Let}] |
40206 | 151 |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
152 |
fun is_built_in_const_for_prover ctxt name = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
153 |
if is_smt_prover ctxt name then |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
154 |
let val ctxt = ctxt |> select_smt_solver name in |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
155 |
fn x => fn ts => |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
156 |
if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
157 |
(true, []) |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
158 |
else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
159 |
(true, ts) |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
160 |
else |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
161 |
(false, ts) |
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
162 |
end |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
163 |
else |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset
|
164 |
fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts) |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
165 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
166 |
(* FUDGE *) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
167 |
val atp_relevance_fudge = |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
168 |
{allow_ext = true, |
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41744
diff
changeset
|
169 |
local_const_multiplier = 1.5, |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
170 |
worse_irrel_freq = 100.0, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
171 |
higher_order_irrel_weight = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
172 |
abs_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
173 |
abs_irrel_weight = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
174 |
skolem_irrel_weight = 0.75, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
175 |
theory_const_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
176 |
theory_const_irrel_weight = 0.25, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
177 |
intro_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
178 |
elim_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
179 |
simp_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
180 |
local_bonus = 0.55, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
181 |
assum_bonus = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
182 |
chained_bonus = 1.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
183 |
max_imperfect = 11.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
184 |
max_imperfect_exp = 1.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
185 |
threshold_divisor = 2.0, |
41093 | 186 |
ridiculous_threshold = 0.01} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
187 |
|
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
188 |
(* FUDGE (FIXME) *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
189 |
val smt_relevance_fudge = |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
190 |
{allow_ext = false, |
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41744
diff
changeset
|
191 |
local_const_multiplier = #local_const_multiplier atp_relevance_fudge, |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
192 |
worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
193 |
higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
194 |
abs_rel_weight = #abs_rel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
195 |
abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
196 |
skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
197 |
theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
198 |
theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
199 |
intro_bonus = #intro_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
200 |
elim_bonus = #elim_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
201 |
simp_bonus = #simp_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
202 |
local_bonus = #local_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
203 |
assum_bonus = #assum_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
204 |
chained_bonus = #chained_bonus atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
205 |
max_imperfect = #max_imperfect atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
206 |
max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
207 |
threshold_divisor = #threshold_divisor atp_relevance_fudge, |
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
208 |
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
209 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
210 |
fun relevance_fudge_for_prover ctxt name = |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
211 |
if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
212 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
213 |
fun supported_provers ctxt = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
214 |
let |
42361 | 215 |
val thy = Proof_Context.theory_of ctxt |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
216 |
val (remote_provers, local_provers) = |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
217 |
sort_strings (supported_atps thy) @ |
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
218 |
sort_strings (SMT_Solver.available_solvers_of ctxt) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
219 |
|> List.partition (String.isPrefix remote_prefix) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
220 |
in |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
221 |
Output.urgent_message ("Supported provers: " ^ |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
222 |
commas (local_provers @ remote_provers) ^ ".") |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
223 |
end |
35969 | 224 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
225 |
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
226 |
fun running_provers () = Async_Manager.running_threads das_Tool "provers" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
227 |
val messages = Async_Manager.thread_messages das_Tool "prover" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
228 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
229 |
(** problems, results, ATPs, etc. **) |
35969 | 230 |
|
231 |
type params = |
|
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset
|
232 |
{debug: bool, |
35969 | 233 |
verbose: bool, |
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset
|
234 |
overlord: bool, |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset
|
235 |
blocking: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
236 |
provers: string list, |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
237 |
relevance_thresholds: real * real, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
238 |
max_relevant: int option, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
239 |
monomorphize: bool, |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
240 |
monomorphize_limit: int, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
241 |
type_sys: type_system, |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset
|
242 |
explicit_apply: bool, |
35969 | 243 |
isar_proof: bool, |
36924 | 244 |
isar_shrink_factor: int, |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
245 |
slicing: bool, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
246 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
247 |
expect: string} |
35867 | 248 |
|
41090 | 249 |
datatype prover_fact = |
250 |
Untranslated_Fact of (string * locality) * thm | |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
251 |
ATP_Translated_Fact of |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
252 |
translated_formula option * ((string * locality) * thm) | |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
253 |
SMT_Weighted_Fact of (string * locality) * (int option * thm) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
254 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
255 |
type prover_problem = |
39318 | 256 |
{state: Proof.state, |
38998 | 257 |
goal: thm, |
258 |
subgoal: int, |
|
40065 | 259 |
subgoal_count: int, |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
260 |
facts: prover_fact list, |
41741 | 261 |
smt_filter: (string * locality) SMT_Solver.smt_filter_data option} |
35867 | 262 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
263 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
264 |
{outcome: failure option, |
35969 | 265 |
message: string, |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
266 |
used_facts: (string * locality) list, |
40062 | 267 |
run_time_in_msecs: int option} |
35867 | 268 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
269 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 270 |
|
38023 | 271 |
(* configuration attributes *) |
272 |
||
38991 | 273 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
274 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 275 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 276 |
|
277 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
278 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 279 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
280 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
281 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 282 |
|
38023 | 283 |
fun with_path cleanup after f path = |
284 |
Exn.capture f path |
|
285 |
|> tap (fn _ => cleanup path) |
|
286 |
|> Exn.release |
|
287 |
|> tap (after path) |
|
288 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
289 |
fun proof_banner auto = |
40224 | 290 |
if auto then "Auto Sledgehammer found a proof" else "Try this command" |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
291 |
|
41723
bb366da22483
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
blanchet
parents:
41432
diff
changeset
|
292 |
val smt_triggers = Unsynchronized.ref true |
bb366da22483
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
blanchet
parents:
41432
diff
changeset
|
293 |
val smt_weights = Unsynchronized.ref true |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
294 |
val smt_weight_min_facts = Unsynchronized.ref 20 |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
295 |
|
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
296 |
(* FUDGE *) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
297 |
val smt_min_weight = Unsynchronized.ref 0 |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
298 |
val smt_max_weight = Unsynchronized.ref 10 |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
299 |
val smt_max_weight_index = Unsynchronized.ref 200 |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
300 |
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
301 |
|
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
302 |
fun smt_fact_weight j num_facts = |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
303 |
if !smt_weights andalso num_facts >= !smt_weight_min_facts then |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
304 |
SOME (!smt_max_weight |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
305 |
- (!smt_max_weight - !smt_min_weight + 1) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
306 |
* !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1)) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
307 |
div !smt_weight_curve (!smt_max_weight_index)) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
308 |
else |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
309 |
NONE |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
310 |
|
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
311 |
fun weight_smt_fact thy num_facts ((info, th), j) = |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
312 |
(info, (smt_fact_weight j num_facts, th |> Thm.transfer thy)) |
38023 | 313 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
314 |
fun untranslated_fact (Untranslated_Fact p) = p |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
315 |
| untranslated_fact (ATP_Translated_Fact (_, p)) = p |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
316 |
| untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
317 |
fun atp_translated_fact _ (ATP_Translated_Fact p) = p |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
318 |
| atp_translated_fact ctxt fact = |
41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41944
diff
changeset
|
319 |
translate_atp_fact ctxt false (untranslated_fact fact) |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
320 |
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
321 |
| smt_weighted_fact thy num_facts (fact, j) = |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
322 |
(untranslated_fact fact, j) |> weight_smt_fact thy num_facts |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
323 |
|
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
324 |
fun overlord_file_location_for_prover prover = |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
325 |
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover) |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
326 |
|
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
327 |
|
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
328 |
(* generic TPTP-based ATPs *) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
329 |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
330 |
fun int_opt_add (SOME m) (SOME n) = SOME (m + n) |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
331 |
| int_opt_add _ _ = NONE |
40062 | 332 |
|
39492 | 333 |
(* Important messages are important but not so important that users want to see |
334 |
them each time. *) |
|
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
335 |
val atp_important_message_keep_factor = 0.1 |
39492 | 336 |
|
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
337 |
fun run_atp auto name |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
338 |
({exec, required_execs, arguments, slices, proof_delims, known_failures, |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
339 |
explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
340 |
({debug, verbose, overlord, max_relevant, monomorphize, |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
341 |
monomorphize_limit, type_sys, explicit_apply, isar_proof, |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
342 |
isar_shrink_factor, slicing, timeout, ...} : params) |
40983 | 343 |
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = |
38023 | 344 |
let |
42182
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset
|
345 |
val thy = Proof.theory_of state |
39318 | 346 |
val ctxt = Proof.context_of state |
38998 | 347 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
348 |
fun monomorphize_facts facts = |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
349 |
let |
42193
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
350 |
val repair_context = |
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
351 |
Config.put SMT_Config.verbose debug |
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
352 |
#> Config.put SMT_Config.monomorph_full false |
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
353 |
#> Config.put SMT_Config.monomorph_limit monomorphize_limit |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
354 |
val facts = facts |> map untranslated_fact |
42182
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset
|
355 |
(* pseudo-theorem involving the same constants as the subgoal *) |
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset
|
356 |
val subgoal_th = |
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset
|
357 |
Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
358 |
val indexed_facts = |
42182
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset
|
359 |
(~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts) |
42193
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
360 |
val mono_facts = |
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
361 |
SMT_Monomorph.monomorph indexed_facts (repair_context ctxt) |> fst |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
362 |
in |
42181
8f25605e646c
temporary workaround: filter out spurious monomorphic instances
blanchet
parents:
42180
diff
changeset
|
363 |
mono_facts |
8f25605e646c
temporary workaround: filter out spurious monomorphic instances
blanchet
parents:
42180
diff
changeset
|
364 |
|> sort (int_ord o pairself fst) |
8f25605e646c
temporary workaround: filter out spurious monomorphic instances
blanchet
parents:
42180
diff
changeset
|
365 |
|> filter_out (curry (op =) ~1 o fst) |
8f25605e646c
temporary workaround: filter out spurious monomorphic instances
blanchet
parents:
42180
diff
changeset
|
366 |
|> map (Untranslated_Fact o apfst (fst o nth facts)) |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
367 |
end |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
368 |
val facts = facts |> monomorphize ? monomorphize_facts |
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
369 |
|> map (atp_translated_fact ctxt) |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
370 |
val (dest_dir, problem_prefix) = |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
371 |
if overlord then overlord_file_location_for_prover name |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
372 |
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
373 |
val problem_file_name = |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
374 |
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
375 |
"_" ^ string_of_int subgoal) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
376 |
val problem_path_name = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
377 |
if dest_dir = "" then |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
378 |
File.tmp_path problem_file_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
379 |
else if File.exists (Path.explode dest_dir) then |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
380 |
Path.append (Path.explode dest_dir) problem_file_name |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
381 |
else |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
382 |
error ("No such directory: " ^ quote dest_dir ^ ".") |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
383 |
val measure_run_time = verbose orelse Config.get ctxt measure_run_time |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset
|
384 |
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) |
38023 | 385 |
fun split_time s = |
386 |
let |
|
387 |
val split = String.tokens (fn c => str c = "\n"); |
|
388 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
389 |
fun as_num f = f >> (fst o read_int); |
|
390 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
391 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
392 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
393 |
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40562
diff
changeset
|
394 |
val as_time = Scan.read Symbol.stopper time o raw_explode |
38023 | 395 |
in (output, as_time t) end; |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
396 |
fun run_on prob_file = |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset
|
397 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 398 |
(home_var, _) :: _ => |
38023 | 399 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 400 |
| [] => |
401 |
if File.exists command then |
|
402 |
let |
|
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
403 |
val readable_names = debug andalso overlord |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
404 |
(* If slicing is disabled, we expand the last slice to fill the |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
405 |
entire time available. *) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
406 |
val actual_slices = get_slices slicing (slices ()) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
407 |
val num_actual_slices = length actual_slices |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
408 |
fun run_slice (slice, (time_frac, (complete, default_max_relevant))) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
409 |
time_left = |
38032 | 410 |
let |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
411 |
val num_facts = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
412 |
length facts |> is_none max_relevant |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
413 |
? Integer.min default_max_relevant |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
414 |
val real_ms = Real.fromInt o Time.toMilliseconds |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
415 |
val slice_timeout = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
416 |
((real_ms time_left |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
417 |
|> (if slice < num_actual_slices - 1 then |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
418 |
curry Real.min (time_frac * real_ms timeout) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
419 |
else |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
420 |
I)) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
421 |
* 0.001) |> seconds |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
422 |
val _ = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
423 |
if verbose then |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
424 |
"ATP slice " ^ string_of_int (slice + 1) ^ " with " ^ |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
425 |
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
426 |
" for " ^ string_from_time slice_timeout ^ "..." |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
427 |
|> Output.urgent_message |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
428 |
else |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
429 |
() |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
430 |
val (atp_problem, pool, conjecture_offset, fact_names) = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
431 |
prepare_atp_problem ctxt readable_names explicit_forall |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
432 |
type_sys explicit_apply hyp_ts concl_t |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
433 |
(facts |> take num_facts) |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
434 |
fun weights () = atp_problem_weights atp_problem |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
435 |
val core = |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
436 |
File.shell_path command ^ " " ^ |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
437 |
arguments slice slice_timeout weights ^ " " ^ |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
438 |
File.shell_path prob_file |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
439 |
val command = |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
440 |
(if measure_run_time then |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
441 |
"TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
442 |
else |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
443 |
"exec " ^ core) ^ " 2>&1" |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
444 |
val _ = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
445 |
atp_problem |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
446 |
|> tptp_strings_for_atp_problem use_conjecture_for_hypotheses |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
447 |
|> cons ("% " ^ command ^ "\n") |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
448 |
|> File.write_list prob_file |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
449 |
val conjecture_shape = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
450 |
conjecture_offset + 1 |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
451 |
upto conjecture_offset + length hyp_ts + 1 |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
452 |
|> map single |
38032 | 453 |
val ((output, msecs), res_code) = |
454 |
bash_output command |
|
455 |
|>> (if overlord then |
|
456 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
457 |
else |
|
458 |
I) |
|
40062 | 459 |
|>> (if measure_run_time then split_time else rpair NONE) |
39452 | 460 |
val (tstplike_proof, outcome) = |
42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41990
diff
changeset
|
461 |
extract_tstplike_proof_and_outcome debug verbose complete |
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41990
diff
changeset
|
462 |
res_code proof_delims known_failures output |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
463 |
in |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
464 |
((pool, conjecture_shape, fact_names), |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
465 |
(output, msecs, tstplike_proof, outcome)) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
466 |
end |
38645 | 467 |
val timer = Timer.startRealTimer () |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
468 |
fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
469 |
run_slice slice (Time.- (timeout, Timer.checkRealTimer timer)) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
470 |
|> (fn (stuff, (output, msecs, tstplike_proof, outcome)) => |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
471 |
(stuff, (output, int_opt_add msecs0 msecs, |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
472 |
tstplike_proof, outcome))) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
473 |
| maybe_run_slice _ result = result |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
474 |
in |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
475 |
((Symtab.empty, [], Vector.fromList []), |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
476 |
("", SOME 0, "", SOME InternalError)) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
477 |
|> fold maybe_run_slice actual_slices |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
478 |
end |
38032 | 479 |
else |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41799
diff
changeset
|
480 |
error ("Bad executable: " ^ Path.print command ^ ".") |
38023 | 481 |
|
482 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
483 |
the proof file too. *) |
|
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
484 |
fun cleanup prob_file = |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
485 |
if dest_dir = "" then try File.rm prob_file else NONE |
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
486 |
fun export prob_file (_, (output, _, _, _)) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
487 |
if dest_dir = "" then |
38023 | 488 |
() |
489 |
else |
|
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
490 |
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
491 |
val ((pool, conjecture_shape, fact_names), |
39452 | 492 |
(output, msecs, tstplike_proof, outcome)) = |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
493 |
with_path cleanup export run_on problem_path_name |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
494 |
val (conjecture_shape, fact_names) = |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
495 |
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names |
39492 | 496 |
val important_message = |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
497 |
if not auto andalso random () <= atp_important_message_keep_factor then |
39492 | 498 |
extract_important_message output |
499 |
else |
|
500 |
"" |
|
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
501 |
fun append_to_message message = |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
502 |
message ^ |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
503 |
(if verbose then |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
504 |
"\nATP real CPU time: " ^ |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
505 |
string_from_time (Time.fromMilliseconds (the msecs)) ^ "." |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
506 |
else |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
507 |
"") ^ |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
508 |
(if important_message <> "" then |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
509 |
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
510 |
else |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
511 |
"") |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
512 |
val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
513 |
val metis_params = |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
514 |
(proof_banner auto, type_sys, minimize_command, tstplike_proof, |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
515 |
fact_names, goal, subgoal) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
516 |
val (outcome, (message, used_facts)) = |
38023 | 517 |
case outcome of |
518 |
NONE => |
|
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
519 |
(NONE, proof_text isar_proof isar_params metis_params |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
520 |
|>> append_to_message) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
521 |
| SOME ProofMissing => |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
522 |
(NONE, metis_proof_text metis_params |>> append_to_message) |
41744 | 523 |
| SOME failure => (outcome, (string_for_failure failure, [])) |
38023 | 524 |
in |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
525 |
{outcome = outcome, message = message, used_facts = used_facts, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
526 |
run_time_in_msecs = msecs} |
38023 | 527 |
end |
528 |
||
40669 | 529 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until |
530 |
these are sorted out properly in the SMT module, we have to interpret these |
|
531 |
ourselves. *) |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
532 |
val remote_smt_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
533 |
[(22, CantConnect), |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
534 |
(2, NoLibwwwPerl)] |
41222 | 535 |
val z3_wrapper_failures = |
536 |
[(10, NoRealZ3), |
|
537 |
(11, InternalError), |
|
538 |
(12, InternalError), |
|
539 |
(13, InternalError)] |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
540 |
val z3_failures = |
41236 | 541 |
[(101, OutOfResources), |
542 |
(103, MalformedInput), |
|
41222 | 543 |
(110, MalformedInput)] |
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
544 |
val unix_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
545 |
[(139, Crashed)] |
41222 | 546 |
val smt_failures = |
41799
98b3d5ce0935
exit code 127 can mean many things -- not just (and probably not) Perl missing
blanchet
parents:
41790
diff
changeset
|
547 |
remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures |
40555 | 548 |
|
42100
062381c5f9f8
more precise failure reporting in Sledgehammer/SMT
blanchet
parents:
42061
diff
changeset
|
549 |
|
062381c5f9f8
more precise failure reporting in Sledgehammer/SMT
blanchet
parents:
42061
diff
changeset
|
550 |
fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) = |
062381c5f9f8
more precise failure reporting in Sledgehammer/SMT
blanchet
parents:
42061
diff
changeset
|
551 |
if is_real_cex then Unprovable else IncompleteUnprovable |
41222 | 552 |
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut |
553 |
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = |
|
554 |
(case AList.lookup (op =) smt_failures code of |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
555 |
SOME failure => failure |
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset
|
556 |
| NONE => UnknownError ("Abnormal termination with exit code " ^ |
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset
|
557 |
string_of_int code ^ ".")) |
41222 | 558 |
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
559 |
| failure_from_smt_failure (SMT_Failure.Other_Failure msg) = |
|
42061
71077681eaf6
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
blanchet
parents:
42060
diff
changeset
|
560 |
UnknownError msg |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
561 |
|
40698 | 562 |
(* FUDGE *) |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
563 |
val smt_max_slices = Unsynchronized.ref 8 |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
564 |
val smt_slice_fact_frac = Unsynchronized.ref 0.5 |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
565 |
val smt_slice_time_frac = Unsynchronized.ref 0.5 |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
566 |
val smt_slice_min_secs = Unsynchronized.ref 5 |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
567 |
|
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
568 |
fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, |
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
569 |
timeout, slicing, ...} : params) |
41741 | 570 |
state i smt_filter = |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
571 |
let |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
572 |
val ctxt = Proof.context_of state |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
573 |
val max_slices = if slicing then !smt_max_slices else 1 |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
574 |
val repair_context = |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
575 |
select_smt_solver name |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
576 |
#> Config.put SMT_Config.verbose debug |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
577 |
#> (if overlord then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
578 |
Config.put SMT_Config.debug_files |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
579 |
(overlord_file_location_for_prover name |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
580 |
|> (fn (path, name) => path ^ "/" ^ name)) |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
581 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
582 |
I) |
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset
|
583 |
#> Config.put SMT_Config.infer_triggers (!smt_triggers) |
42193
8eed749527b6
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
blanchet
parents:
42190
diff
changeset
|
584 |
#> Config.put SMT_Config.monomorph_full false |
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents:
42100
diff
changeset
|
585 |
#> Config.put SMT_Config.monomorph_limit monomorphize_limit |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
586 |
val state = state |> Proof.map_context repair_context |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
587 |
|
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
588 |
fun do_slice timeout slice outcome0 time_so_far facts = |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
589 |
let |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
590 |
val timer = Timer.startRealTimer () |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
591 |
val ms = timeout |> Time.toMilliseconds |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
592 |
val slice_timeout = |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
593 |
if slice < max_slices then |
41169 | 594 |
Int.min (ms, |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
595 |
Int.max (1000 * !smt_slice_min_secs, |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
596 |
Real.ceil (!smt_slice_time_frac * Real.fromInt ms))) |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
597 |
|> Time.fromMilliseconds |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
598 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
599 |
timeout |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
600 |
val num_facts = length facts |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
601 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
602 |
if verbose then |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
603 |
"SMT slice with " ^ string_of_int num_facts ^ " fact" ^ |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
604 |
plural_s num_facts ^ " for " ^ string_from_time slice_timeout ^ |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
605 |
"..." |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
606 |
|> Output.urgent_message |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
607 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
608 |
() |
41168 | 609 |
val birth = Timer.checkRealTimer timer |
41171 | 610 |
val _ = |
41211
1e2e16bc0077
no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset
|
611 |
if debug then Output.urgent_message "Invoking SMT solver..." else () |
41209 | 612 |
val (outcome, used_facts) = |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
613 |
(case (slice, smt_filter) of |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
614 |
(1, SOME head) => head |> apsnd (apsnd repair_context) |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
615 |
| _ => SMT_Solver.smt_filter_preprocess state facts i) |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
616 |
|> SMT_Solver.smt_filter_apply slice_timeout |
41239 | 617 |
|> (fn {outcome, used_facts} => (outcome, used_facts)) |
41209 | 618 |
handle exn => if Exn.is_interrupt exn then |
619 |
reraise exn |
|
620 |
else |
|
42061
71077681eaf6
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
blanchet
parents:
42060
diff
changeset
|
621 |
(ML_Compiler.exn_message exn |
41209 | 622 |
|> SMT_Failure.Other_Failure |> SOME, []) |
41168 | 623 |
val death = Timer.checkRealTimer timer |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
624 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
625 |
if verbose andalso is_some outcome then |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
626 |
"SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
627 |
|> Output.urgent_message |
41171 | 628 |
else if debug then |
629 |
Output.urgent_message "SMT solver returned." |
|
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
630 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
631 |
() |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
632 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
41168 | 633 |
val time_so_far = Time.+ (time_so_far, Time.- (death, birth)) |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
634 |
val too_many_facts_perhaps = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
635 |
case outcome of |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
636 |
NONE => false |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
637 |
| SOME (SMT_Failure.Counterexample _) => false |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
638 |
| SOME SMT_Failure.Time_Out => slice_timeout <> timeout |
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40558
diff
changeset
|
639 |
| SOME (SMT_Failure.Abnormal_Termination code) => |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
640 |
(if verbose then |
40555 | 641 |
"The SMT solver invoked with " ^ string_of_int num_facts ^ |
40692
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
642 |
" fact" ^ plural_s num_facts ^ " terminated abnormally with \ |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
643 |
\exit code " ^ string_of_int code ^ "." |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
644 |
|> warning |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
645 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
646 |
(); |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
647 |
true (* kind of *)) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
648 |
| SOME SMT_Failure.Out_Of_Memory => true |
41211
1e2e16bc0077
no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset
|
649 |
| SOME (SMT_Failure.Other_Failure _) => true |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
650 |
val timeout = Time.- (timeout, Timer.checkRealTimer timer) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
651 |
in |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
652 |
if too_many_facts_perhaps andalso slice < max_slices andalso |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
653 |
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then |
41169 | 654 |
let |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
655 |
val n = Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
656 |
in |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
657 |
do_slice timeout (slice + 1) outcome0 time_so_far (take n facts) |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
658 |
end |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
659 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
660 |
{outcome = if is_none outcome then NONE else the outcome0, |
41168 | 661 |
used_facts = used_facts, |
662 |
run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)} |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
663 |
end |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
664 |
in do_slice timeout 1 NONE Time.zeroTime end |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
665 |
|
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
666 |
(* taken from "Mirabelle" and generalized *) |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
667 |
fun can_apply timeout tac state i = |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
668 |
let |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
669 |
val {context = ctxt, facts, goal} = Proof.goal state |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
670 |
val full_tac = Method.insert_tac facts i THEN tac ctxt i |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
671 |
in |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
672 |
case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
673 |
SOME (SOME _) => true |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
674 |
| _ => false |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
675 |
end |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
676 |
|
41152
4a7410be4dfc
crank up Metis's timeout for SMT solvers, since users love Metis
blanchet
parents:
41151
diff
changeset
|
677 |
val smt_metis_timeout = seconds 1.0 |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
678 |
|
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
679 |
fun can_apply_metis debug state i ths = |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
680 |
can_apply smt_metis_timeout |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
681 |
(Config.put Metis_Tactics.verbose debug |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
682 |
#> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
683 |
|
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
684 |
fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
685 |
({state, subgoal, subgoal_count, facts, smt_filter, ...} |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
686 |
: prover_problem) = |
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset
|
687 |
let |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset
|
688 |
val ctxt = Proof.context_of state |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
689 |
val thy = Proof.theory_of state |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
690 |
val num_facts = length facts |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
691 |
val facts = facts ~~ (0 upto num_facts - 1) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset
|
692 |
|> map (smt_weighted_fact thy num_facts) |
40181 | 693 |
val {outcome, used_facts, run_time_in_msecs} = |
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
694 |
smt_filter_loop name params state subgoal smt_filter facts |
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40701
diff
changeset
|
695 |
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) |
41222 | 696 |
val outcome = outcome |> Option.map failure_from_smt_failure |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
697 |
val message = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
698 |
case outcome of |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
699 |
NONE => |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
700 |
let |
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset
|
701 |
val (method, settings) = |
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
702 |
if can_apply_metis debug state subgoal (map snd used_facts) then |
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset
|
703 |
("metis", "") |
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
704 |
else |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
705 |
("smt", if name = SMT_Solver.solver_name_of ctxt then "" |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset
|
706 |
else "smt_solver = " ^ maybe_quote name) |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
707 |
in |
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
708 |
try_command_line (proof_banner auto) |
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset
|
709 |
(apply_on_subgoal settings subgoal subgoal_count ^ |
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset
|
710 |
command_call method (map fst other_lemmas)) ^ |
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40701
diff
changeset
|
711 |
minimize_line minimize_command |
41168 | 712 |
(map fst (other_lemmas @ chained_lemmas)) ^ |
713 |
(if verbose then |
|
714 |
"\nSMT solver real CPU time: " ^ |
|
715 |
string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^ |
|
716 |
"." |
|
717 |
else |
|
718 |
"") |
|
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
719 |
end |
41744 | 720 |
| SOME failure => string_for_failure failure |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
721 |
in |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset
|
722 |
{outcome = outcome, used_facts = map fst used_facts, |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
723 |
run_time_in_msecs = run_time_in_msecs, message = message} |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
724 |
end |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
725 |
|
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
726 |
fun get_prover ctxt auto name = |
42361 | 727 |
let val thy = Proof_Context.theory_of ctxt in |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
728 |
if is_smt_prover ctxt name then |
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
729 |
run_smt_solver auto name |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset
|
730 |
else if member (op =) (supported_atps thy) name then |
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset
|
731 |
run_atp auto name (get_atp thy name) |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
732 |
else |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
733 |
error ("No such prover: " ^ name ^ ".") |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
734 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
735 |
|
38023 | 736 |
val setup = |
737 |
dest_dir_setup |
|
738 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
739 |
#> measure_run_time_setup |
38023 | 740 |
|
28582 | 741 |
end; |