author | blanchet |
Fri, 17 Dec 2010 12:10:08 +0100 | |
changeset 41241 | 7d07736aaaf6 |
parent 41239 | d6e804ff29c3 |
child 41242 | 8edeb1dbbc76 |
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, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
24 |
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
|
25 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
26 |
relevance_thresholds: real * real, |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
27 |
max_relevant: int option, |
35969 | 28 |
isar_proof: bool, |
36924 | 29 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
30 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
31 |
expect: string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
32 |
|
41090 | 33 |
datatype prover_fact = |
34 |
Untranslated_Fact of (string * locality) * thm | |
|
35 |
ATP_Translated_Fact of |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
36 |
translated_formula option * ((string * locality) * thm) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
37 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
38 |
type prover_problem = |
39318 | 39 |
{state: Proof.state, |
38998 | 40 |
goal: thm, |
41 |
subgoal: int, |
|
40065 | 42 |
subgoal_count: int, |
41090 | 43 |
facts: prover_fact list} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
44 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
45 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
46 |
{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
|
47 |
used_facts: (string * locality) list, |
40062 | 48 |
run_time_in_msecs: int option, |
49 |
message: string} |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
50 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
51 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 52 |
|
41168 | 53 |
(* for experimentation purposes -- do not use in production code *) |
41222 | 54 |
val smt_max_iters : int Unsynchronized.ref |
41169 | 55 |
val smt_iter_fact_frac : real Unsynchronized.ref |
56 |
val smt_iter_time_frac : real Unsynchronized.ref |
|
41168 | 57 |
val smt_iter_min_msecs : int Unsynchronized.ref |
58 |
val smt_monomorph_limit : int Unsynchronized.ref |
|
59 |
val smt_weights : bool Unsynchronized.ref |
|
60 |
val smt_min_weight : int Unsynchronized.ref |
|
61 |
val smt_max_weight : int Unsynchronized.ref |
|
62 |
val smt_max_index : int Unsynchronized.ref |
|
63 |
val smt_weight_curve : (int -> int) Unsynchronized.ref |
|
64 |
||
41089 | 65 |
val das_Tool : string |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
66 |
val is_smt_prover : Proof.context -> string -> bool |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
67 |
val is_prover_available : Proof.context -> string -> bool |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
68 |
val is_prover_installed : Proof.context -> string -> bool |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
69 |
val default_max_relevant_for_prover : Proof.context -> string -> int |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
70 |
val is_built_in_const_for_prover : |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
41059
diff
changeset
|
71 |
Proof.context -> string -> string * typ -> term list -> bool |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
72 |
val atp_relevance_fudge : relevance_fudge |
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
73 |
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
|
74 |
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge |
38023 | 75 |
val dest_dir : string Config.T |
76 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
77 |
val measure_run_time : bool Config.T |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
78 |
val untranslated_fact : prover_fact -> (string * locality) * thm |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
79 |
val available_provers : Proof.context -> unit |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
80 |
val kill_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
81 |
val running_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
82 |
val messages : int option -> unit |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
83 |
val get_prover : Proof.context -> bool -> string -> prover |
38023 | 84 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
85 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
86 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
87 |
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
88 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
89 |
|
38028 | 90 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset
|
91 |
open ATP_Proof |
38028 | 92 |
open ATP_Systems |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset
|
93 |
open Metis_Translate |
38023 | 94 |
open Sledgehammer_Util |
38988 | 95 |
open Sledgehammer_Filter |
40068 | 96 |
open Sledgehammer_ATP_Translate |
97 |
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
|
98 |
|
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
|
99 |
(** 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
|
100 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
101 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
102 |
"Async_Manager". *) |
37585 | 103 |
val das_Tool = "Sledgehammer" |
104 |
||
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
105 |
fun is_smt_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
|
106 |
let val smts = SMT_Solver.available_solvers_of ctxt in |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
107 |
case try (unprefix remote_prefix) name of |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
108 |
SOME suffix => member (op =) smts suffix andalso |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
109 |
SMT_Solver.is_remotely_available ctxt suffix |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
110 |
| NONE => member (op =) smts name |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
111 |
end |
40062 | 112 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
113 |
fun is_prover_available ctxt name = |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
114 |
let val thy = ProofContext.theory_of ctxt in |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
115 |
is_smt_prover ctxt name orelse member (op =) (available_atps thy) name |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
116 |
end |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
117 |
|
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
118 |
fun is_prover_installed ctxt name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
119 |
let val thy = ProofContext.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
|
120 |
if is_smt_prover ctxt name then |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
121 |
String.isPrefix remote_prefix name orelse |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
122 |
SMT_Solver.is_locally_installed ctxt name |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
123 |
else |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
124 |
is_atp_installed thy name |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
125 |
end |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
126 |
|
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
127 |
fun available_smt_solvers ctxt = |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
128 |
let val smts = SMT_Solver.available_solvers_of ctxt in |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
129 |
smts @ map (prefix remote_prefix) |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
130 |
(filter (SMT_Solver.is_remotely_available ctxt) smts) |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
131 |
end |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
132 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
133 |
fun default_max_relevant_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
|
134 |
let val thy = ProofContext.theory_of ctxt in |
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
135 |
if is_smt_prover ctxt name then |
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
136 |
SMT_Solver.default_max_relevant ctxt |
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
137 |
(perhaps (try (unprefix remote_prefix)) name) |
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
138 |
else |
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
139 |
#default_max_relevant (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
|
140 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
141 |
|
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
142 |
(* 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
|
143 |
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
|
144 |
val atp_irrelevant_consts = |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
145 |
[@{const_name False}, @{const_name True}, @{const_name Not}, |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
146 |
@{const_name conj}, @{const_name disj}, @{const_name implies}, |
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41138
diff
changeset
|
147 |
@{const_name HOL.eq}, @{const_name If}, @{const_name Let}] |
40206 | 148 |
|
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
41059
diff
changeset
|
149 |
fun is_built_in_const_for_prover ctxt name (s, T) args = |
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
41059
diff
changeset
|
150 |
if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
151 |
else member (op =) atp_irrelevant_consts s |
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
|
152 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
153 |
(* FUDGE *) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
154 |
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
|
155 |
{allow_ext = true, |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
156 |
worse_irrel_freq = 100.0, |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
157 |
higher_order_irrel_weight = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
158 |
abs_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
159 |
abs_irrel_weight = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
160 |
skolem_irrel_weight = 0.75, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
161 |
theory_const_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
162 |
theory_const_irrel_weight = 0.25, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
163 |
intro_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
164 |
elim_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
165 |
simp_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
166 |
local_bonus = 0.55, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
167 |
assum_bonus = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
168 |
chained_bonus = 1.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
169 |
max_imperfect = 11.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
170 |
max_imperfect_exp = 1.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
171 |
threshold_divisor = 2.0, |
41093 | 172 |
ridiculous_threshold = 0.01} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
173 |
|
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
|
174 |
(* FUDGE (FIXME) *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
175 |
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
|
176 |
{allow_ext = false, |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
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
|
185 |
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
|
186 |
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
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
194 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
198 |
fun available_provers ctxt = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
199 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
200 |
val thy = ProofContext.theory_of ctxt |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
201 |
val (remote_provers, local_provers) = |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
202 |
sort_strings (available_atps thy) @ |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
203 |
sort_strings (available_smt_solvers ctxt) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
204 |
|> List.partition (String.isPrefix remote_prefix) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
205 |
in |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
206 |
Output.urgent_message ("Available provers: " ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
207 |
commas (local_provers @ remote_provers) ^ ".") |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
208 |
end |
35969 | 209 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
210 |
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
|
211 |
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
|
212 |
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
|
213 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
214 |
(** problems, results, ATPs, etc. **) |
35969 | 215 |
|
216 |
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
|
217 |
{debug: bool, |
35969 | 218 |
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
|
219 |
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
|
220 |
blocking: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
221 |
provers: string list, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
222 |
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
|
223 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
224 |
relevance_thresholds: real * real, |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
225 |
max_relevant: int option, |
35969 | 226 |
isar_proof: bool, |
36924 | 227 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
228 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
229 |
expect: string} |
35867 | 230 |
|
41090 | 231 |
datatype prover_fact = |
232 |
Untranslated_Fact of (string * locality) * thm | |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
233 |
ATP_Translated_Fact of translated_formula option * ((string * locality) * thm) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
234 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
235 |
type prover_problem = |
39318 | 236 |
{state: Proof.state, |
38998 | 237 |
goal: thm, |
238 |
subgoal: int, |
|
40065 | 239 |
subgoal_count: int, |
41090 | 240 |
facts: prover_fact list} |
35867 | 241 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
242 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
243 |
{outcome: failure option, |
35969 | 244 |
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
|
245 |
used_facts: (string * locality) list, |
40062 | 246 |
run_time_in_msecs: int option} |
35867 | 247 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
248 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 249 |
|
38023 | 250 |
(* configuration attributes *) |
251 |
||
38991 | 252 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
253 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 254 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 255 |
|
256 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
257 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 258 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
259 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
260 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 261 |
|
38023 | 262 |
fun with_path cleanup after f path = |
263 |
Exn.capture f path |
|
264 |
|> tap (fn _ => cleanup path) |
|
265 |
|> Exn.release |
|
266 |
|> tap (after path) |
|
267 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
268 |
fun proof_banner auto = |
40224 | 269 |
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
|
270 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
271 |
(* generic TPTP-based ATPs *) |
38023 | 272 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
273 |
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
|
274 |
| untranslated_fact (ATP_Translated_Fact (_, p)) = p |
41090 | 275 |
fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
276 |
| atp_translated_fact _ (ATP_Translated_Fact q) = q |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
277 |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
278 |
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
|
279 |
| int_opt_add _ _ = NONE |
40062 | 280 |
|
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
281 |
fun overlord_file_location_for_prover prover = |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
282 |
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover) |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
283 |
|
41169 | 284 |
val atp_first_iter_time_frac = 0.67 |
41168 | 285 |
|
39492 | 286 |
(* Important messages are important but not so important that users want to see |
287 |
them each time. *) |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
288 |
val important_message_keep_factor = 0.1 |
39492 | 289 |
|
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
290 |
fun run_atp auto name |
41103 | 291 |
({exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
292 |
known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
293 |
: atp_config) |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
294 |
({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41136
diff
changeset
|
295 |
isar_shrink_factor, timeout, ...} : params) |
40983 | 296 |
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = |
38023 | 297 |
let |
39318 | 298 |
val ctxt = Proof.context_of state |
38998 | 299 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
300 |
val facts = facts |> 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
|
301 |
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
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
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
|
306 |
"_" ^ 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
|
307 |
val problem_path_name = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
308 |
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
|
309 |
File.tmp_path problem_file_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
310 |
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
|
311 |
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
|
312 |
else |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
313 |
error ("No such directory: " ^ quote dest_dir ^ ".") |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
314 |
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
|
315 |
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
316 |
(* write out problem file and call ATP *) |
38645 | 317 |
fun command_line complete timeout probfile = |
38023 | 318 |
let |
319 |
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
|
320 |
" " ^ File.shell_path probfile |
|
321 |
in |
|
39010 | 322 |
(if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
323 |
else "exec " ^ core) ^ " 2>&1" |
38023 | 324 |
end |
325 |
fun split_time s = |
|
326 |
let |
|
327 |
val split = String.tokens (fn c => str c = "\n"); |
|
328 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
329 |
fun as_num f = f >> (fst o read_int); |
|
330 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
331 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
332 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
333 |
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
|
334 |
val as_time = Scan.read Symbol.stopper time o raw_explode |
38023 | 335 |
in (output, as_time t) end; |
336 |
fun run_on probfile = |
|
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
|
337 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 338 |
(home_var, _) :: _ => |
38023 | 339 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 340 |
| [] => |
341 |
if File.exists command then |
|
342 |
let |
|
39318 | 343 |
fun run complete timeout = |
38032 | 344 |
let |
38645 | 345 |
val command = command_line complete timeout probfile |
38032 | 346 |
val ((output, msecs), res_code) = |
347 |
bash_output command |
|
348 |
|>> (if overlord then |
|
349 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
350 |
else |
|
351 |
I) |
|
40062 | 352 |
|>> (if measure_run_time then split_time else rpair NONE) |
39452 | 353 |
val (tstplike_proof, outcome) = |
354 |
extract_tstplike_proof_and_outcome complete res_code |
|
355 |
proof_delims known_failures output |
|
356 |
in (output, msecs, tstplike_proof, outcome) end |
|
38032 | 357 |
val readable_names = debug andalso overlord |
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
|
358 |
val (atp_problem, pool, conjecture_offset, fact_names) = |
41134 | 359 |
prepare_atp_problem ctxt readable_names explicit_forall type_sys |
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
|
360 |
explicit_apply hyp_ts concl_t facts |
39452 | 361 |
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
362 |
atp_problem |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
363 |
val _ = File.write_list probfile ss |
38032 | 364 |
val conjecture_shape = |
365 |
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |
|
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset
|
366 |
|> map single |
39318 | 367 |
val run_twice = has_incomplete_mode andalso not auto |
38645 | 368 |
val timer = Timer.startRealTimer () |
38032 | 369 |
val result = |
41168 | 370 |
run false |
371 |
(if run_twice then |
|
41169 | 372 |
seconds (0.001 * atp_first_iter_time_frac |
41168 | 373 |
* Real.fromInt (Time.toMilliseconds timeout)) |
374 |
else |
|
375 |
timeout) |
|
39318 | 376 |
|> run_twice |
38645 | 377 |
? (fn (_, msecs0, _, SOME _) => |
39318 | 378 |
run true (Time.- (timeout, Timer.checkRealTimer timer)) |
39452 | 379 |
|> (fn (output, msecs, tstplike_proof, outcome) => |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
380 |
(output, int_opt_add msecs0 msecs, tstplike_proof, |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
381 |
outcome)) |
38645 | 382 |
| result => result) |
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
|
383 |
in ((pool, conjecture_shape, fact_names), result) end |
38032 | 384 |
else |
385 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 386 |
|
387 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
388 |
the proof file too. *) |
|
389 |
fun cleanup probfile = |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
390 |
if dest_dir = "" then try File.rm probfile else NONE |
38023 | 391 |
fun export probfile (_, (output, _, _, _)) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
392 |
if dest_dir = "" then |
38023 | 393 |
() |
394 |
else |
|
395 |
File.write (Path.explode (Path.implode probfile ^ "_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
|
396 |
val ((pool, conjecture_shape, fact_names), |
39452 | 397 |
(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
|
398 |
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
|
399 |
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
|
400 |
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names |
39492 | 401 |
val important_message = |
40224 | 402 |
if not auto andalso random () <= important_message_keep_factor then |
39492 | 403 |
extract_important_message output |
404 |
else |
|
405 |
"" |
|
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
|
406 |
val (message, used_facts) = |
38023 | 407 |
case outcome of |
408 |
NONE => |
|
409 |
proof_text isar_proof |
|
410 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset
|
411 |
(proof_banner auto, type_sys, minimize_command, tstplike_proof, |
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
|
412 |
fact_names, goal, subgoal) |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
413 |
|>> (fn message => |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
414 |
message ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
415 |
(if verbose then |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
416 |
"\nATP real CPU time: " ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
417 |
string_from_time (Time.fromMilliseconds (the msecs)) ^ "." |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
418 |
else |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
419 |
"") ^ |
39107
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset
|
420 |
(if important_message <> "" then |
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset
|
421 |
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ |
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset
|
422 |
important_message |
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset
|
423 |
else |
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset
|
424 |
"")) |
40669 | 425 |
| SOME failure => (string_for_failure "ATP" failure, []) |
38023 | 426 |
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
|
427 |
{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
|
428 |
run_time_in_msecs = msecs} |
38023 | 429 |
end |
430 |
||
40669 | 431 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until |
432 |
these are sorted out properly in the SMT module, we have to interpret these |
|
433 |
ourselves. *) |
|
41222 | 434 |
val perl_failures = |
435 |
[(127, NoPerl)] |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
436 |
val remote_smt_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
437 |
[(22, CantConnect), |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
438 |
(2, NoLibwwwPerl)] |
41222 | 439 |
val z3_wrapper_failures = |
440 |
[(10, NoRealZ3), |
|
441 |
(11, InternalError), |
|
442 |
(12, InternalError), |
|
443 |
(13, InternalError)] |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
444 |
val z3_failures = |
41236 | 445 |
[(101, OutOfResources), |
446 |
(103, MalformedInput), |
|
41222 | 447 |
(110, MalformedInput)] |
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
448 |
val unix_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
449 |
[(139, Crashed)] |
41222 | 450 |
val smt_failures = |
451 |
perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @ |
|
452 |
unix_failures |
|
40555 | 453 |
|
41209 | 454 |
val internal_error_prefix = "Internal error: " |
455 |
||
41222 | 456 |
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable |
457 |
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut |
|
458 |
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = |
|
459 |
(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
|
460 |
SOME failure => failure |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
461 |
| NONE => UnknownError) |
41222 | 462 |
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
463 |
| failure_from_smt_failure (SMT_Failure.Other_Failure msg) = |
|
41209 | 464 |
if String.isPrefix internal_error_prefix msg then InternalError |
465 |
else UnknownError |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
466 |
|
40698 | 467 |
(* FUDGE *) |
41222 | 468 |
val smt_max_iters = Unsynchronized.ref 8 |
41169 | 469 |
val smt_iter_fact_frac = Unsynchronized.ref 0.5 |
470 |
val smt_iter_time_frac = Unsynchronized.ref 0.5 |
|
41168 | 471 |
val smt_iter_min_msecs = Unsynchronized.ref 5000 |
472 |
val smt_monomorph_limit = Unsynchronized.ref 4 |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
473 |
|
41171 | 474 |
fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
475 |
let |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
476 |
val ctxt = Proof.context_of state |
41168 | 477 |
fun iter timeout iter_num 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
|
478 |
let |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
479 |
val timer = Timer.startRealTimer () |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
480 |
val ms = timeout |> Time.toMilliseconds |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
481 |
val iter_timeout = |
41222 | 482 |
if iter_num < !smt_max_iters then |
41169 | 483 |
Int.min (ms, |
484 |
Int.max (!smt_iter_min_msecs, |
|
485 |
Real.ceil (!smt_iter_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
|
486 |
|> Time.fromMilliseconds |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
487 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
488 |
timeout |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
489 |
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
|
490 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
491 |
if verbose then |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
492 |
"SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ |
40668
661e334d31f0
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
blanchet
parents:
40666
diff
changeset
|
493 |
plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..." |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
494 |
|> Output.urgent_message |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
495 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
496 |
() |
41168 | 497 |
val birth = Timer.checkRealTimer timer |
41171 | 498 |
val _ = |
41211
1e2e16bc0077
no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset
|
499 |
if debug then Output.urgent_message "Invoking SMT solver..." else () |
41209 | 500 |
val (outcome, used_facts) = |
41241 | 501 |
SMT_Solver.smt_filter_head state facts i |
502 |
|> SMT_Solver.smt_filter_tail iter_timeout remote |
|
41239 | 503 |
|> (fn {outcome, used_facts} => (outcome, used_facts)) |
41209 | 504 |
handle exn => if Exn.is_interrupt exn then |
505 |
reraise exn |
|
506 |
else |
|
507 |
(internal_error_prefix ^ ML_Compiler.exn_message exn |
|
508 |
|> SMT_Failure.Other_Failure |> SOME, []) |
|
41168 | 509 |
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
|
510 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
511 |
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
|
512 |
"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
|
513 |
|> Output.urgent_message |
41171 | 514 |
else if debug then |
515 |
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
|
516 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
517 |
() |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
518 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
41168 | 519 |
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
|
520 |
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
|
521 |
case outcome of |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
522 |
NONE => false |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
523 |
| SOME (SMT_Failure.Counterexample _) => false |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
524 |
| SOME SMT_Failure.Time_Out => iter_timeout <> timeout |
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40558
diff
changeset
|
525 |
| 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
|
526 |
(if verbose then |
40555 | 527 |
"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
|
528 |
" fact" ^ plural_s num_facts ^ " terminated abnormally with \ |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
529 |
\exit code " ^ string_of_int code ^ "." |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
530 |
|> warning |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
531 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
532 |
(); |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
533 |
true (* kind of *)) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
534 |
| 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
|
535 |
| 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
|
536 |
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
|
537 |
in |
41222 | 538 |
if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
539 |
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then |
41169 | 540 |
let |
541 |
val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts) |
|
542 |
in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end |
|
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
543 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
544 |
{outcome = if is_none outcome then NONE else the outcome0, |
41168 | 545 |
used_facts = used_facts, |
546 |
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
|
547 |
end |
41168 | 548 |
in iter 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
|
549 |
|
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
|
550 |
(* 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
|
551 |
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
|
552 |
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
|
553 |
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
|
554 |
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
|
555 |
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
|
556 |
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
|
557 |
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
|
558 |
| _ => 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
|
559 |
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
|
560 |
|
41152
4a7410be4dfc
crank up Metis's timeout for SMT solvers, since users love Metis
blanchet
parents:
41151
diff
changeset
|
561 |
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
|
562 |
|
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
563 |
fun can_apply_metis debug state i ths = |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
564 |
can_apply smt_metis_timeout |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
565 |
(Config.put Metis_Tactics.verbose debug |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
566 |
#> (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
|
567 |
|
41168 | 568 |
val smt_weights = Unsynchronized.ref true |
569 |
val smt_weight_min_facts = 20 |
|
570 |
||
571 |
(* FUDGE *) |
|
572 |
val smt_min_weight = Unsynchronized.ref 0 |
|
573 |
val smt_max_weight = Unsynchronized.ref 10 |
|
574 |
val smt_max_index = Unsynchronized.ref 200 |
|
575 |
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) |
|
576 |
||
577 |
fun smt_fact_weight j num_facts = |
|
578 |
if !smt_weights andalso num_facts >= smt_weight_min_facts then |
|
579 |
SOME (!smt_max_weight |
|
41169 | 580 |
- (!smt_max_weight - !smt_min_weight + 1) |
581 |
* !smt_weight_curve (Int.max (0, !smt_max_index - j - 1)) |
|
41168 | 582 |
div !smt_weight_curve (!smt_max_index)) |
583 |
else |
|
584 |
NONE |
|
585 |
||
586 |
fun run_smt_solver auto name (params as {debug, verbose, overlord, ...}) |
|
587 |
minimize_command |
|
40983 | 588 |
({state, subgoal, subgoal_count, facts, ...} : 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
|
589 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
590 |
val (remote, suffix) = |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
591 |
case try (unprefix remote_prefix) name of |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
592 |
SOME suffix => (true, suffix) |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
593 |
| NONE => (false, name) |
40439
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset
|
594 |
val repair_context = |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
595 |
Context.proof_map (SMT_Config.select_solver suffix) |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
596 |
#> Config.put SMT_Config.verbose debug |
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
597 |
#> (if overlord then |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
598 |
Config.put SMT_Config.debug_files |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
599 |
(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
|
600 |
|> (fn (path, base) => path ^ "/" ^ base)) |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
601 |
else |
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset
|
602 |
I) |
41168 | 603 |
#> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit) |
40439
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset
|
604 |
val state = state |> Proof.map_context repair_context |
40668
661e334d31f0
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
blanchet
parents:
40666
diff
changeset
|
605 |
val thy = Proof.theory_of state |
41168 | 606 |
val num_facts = length facts |
607 |
val facts = |
|
608 |
facts ~~ (0 upto num_facts - 1) |
|
609 |
|> map (fn (fact, j) => |
|
610 |
fact |> untranslated_fact |
|
611 |
|> apsnd (pair (smt_fact_weight j num_facts) |
|
612 |
o Thm.transfer thy)) |
|
40181 | 613 |
val {outcome, used_facts, run_time_in_msecs} = |
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
614 |
smt_filter_loop params remote state subgoal 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
|
615 |
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) |
41222 | 616 |
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
|
617 |
val message = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
618 |
case outcome of |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
619 |
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
|
620 |
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
|
621 |
val (method, settings) = |
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
622 |
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
|
623 |
("metis", "") |
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
624 |
else |
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
|
625 |
("smt", if suffix = SMT_Config.solver_of @{context} then "" |
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
|
626 |
else "smt_solver = " ^ maybe_quote suffix) |
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
|
627 |
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
|
628 |
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
|
629 |
(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
|
630 |
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
|
631 |
minimize_line minimize_command |
41168 | 632 |
(map fst (other_lemmas @ chained_lemmas)) ^ |
633 |
(if verbose then |
|
634 |
"\nSMT solver real CPU time: " ^ |
|
635 |
string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^ |
|
636 |
"." |
|
637 |
else |
|
638 |
"") |
|
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
|
639 |
end |
40669 | 640 |
| SOME failure => string_for_failure "SMT solver" failure |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
641 |
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
|
642 |
{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
|
643 |
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
|
644 |
end |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
645 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
646 |
fun get_prover ctxt auto name = |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
647 |
let val thy = ProofContext.theory_of ctxt in |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
648 |
if is_smt_prover ctxt name then |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
649 |
run_smt_solver auto name |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
650 |
else if member (op =) (available_atps thy) name then |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
651 |
run_atp auto name (get_atp thy name) |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
652 |
else |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
653 |
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
|
654 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
655 |
|
38023 | 656 |
val setup = |
657 |
dest_dir_setup |
|
658 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
659 |
#> measure_run_time_setup |
38023 | 660 |
|
28582 | 661 |
end; |