author | blanchet |
Wed, 15 Dec 2010 11:26:28 +0100 | |
changeset 41134 | de9e0adc21da |
parent 41126 | e0bd443c0fdd |
child 41136 | 30bedf58b177 |
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 |
40068 | 15 |
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
16 |
|
35969 | 17 |
type params = |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
18 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
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, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
22 |
provers: string list, |
35969 | 23 |
full_types: bool, |
41134 | 24 |
type_sys: string, |
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 |
|
41089 | 53 |
val das_Tool : string |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
54 |
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
|
55 |
val is_prover_available : Proof.context -> string -> bool |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
val atp_relevance_fudge : relevance_fudge |
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
61 |
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
|
62 |
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge |
38023 | 63 |
val dest_dir : string Config.T |
64 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
val available_provers : Proof.context -> unit |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
68 |
val kill_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
69 |
val running_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
70 |
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
|
71 |
val get_prover : Proof.context -> bool -> string -> prover |
38023 | 72 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
73 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
74 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
75 |
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
76 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
77 |
|
38028 | 78 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset
|
79 |
open ATP_Proof |
38028 | 80 |
open ATP_Systems |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset
|
81 |
open Metis_Translate |
38023 | 82 |
open Sledgehammer_Util |
38988 | 83 |
open Sledgehammer_Filter |
40068 | 84 |
open Sledgehammer_ATP_Translate |
85 |
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
|
86 |
|
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
|
87 |
(** 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
|
88 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
89 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
90 |
"Async_Manager". *) |
37585 | 91 |
val das_Tool = "Sledgehammer" |
92 |
||
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
| 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
|
99 |
end |
40062 | 100 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
end |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
105 |
|
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
106 |
fun is_prover_installed ctxt name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
107 |
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
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
else |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
112 |
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
|
113 |
end |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
114 |
|
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
115 |
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
|
116 |
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
|
117 |
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
|
118 |
(filter (SMT_Solver.is_remotely_available ctxt) smts) |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
119 |
end |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
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 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
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
(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
|
126 |
else |
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset
|
127 |
#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
|
128 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
129 |
|
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
|
130 |
(* These are typically simplified away by "Meson.presimplify". Equality is |
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
|
131 |
handled specially via "fequal". *) |
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
|
132 |
val atp_irrelevant_consts = |
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
|
133 |
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, |
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
|
134 |
@{const_name HOL.eq}] |
40206 | 135 |
|
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
41059
diff
changeset
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
140 |
(* FUDGE *) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
141 |
val atp_relevance_fudge = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
142 |
{worse_irrel_freq = 100.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
143 |
higher_order_irrel_weight = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
144 |
abs_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
145 |
abs_irrel_weight = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
146 |
skolem_irrel_weight = 0.75, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
147 |
theory_const_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
148 |
theory_const_irrel_weight = 0.25, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
149 |
intro_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
150 |
elim_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
151 |
simp_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
152 |
local_bonus = 0.55, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
153 |
assum_bonus = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
154 |
chained_bonus = 1.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
155 |
max_imperfect = 11.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
156 |
max_imperfect_exp = 1.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
157 |
threshold_divisor = 2.0, |
41093 | 158 |
ridiculous_threshold = 0.01} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
159 |
|
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
|
160 |
(* FUDGE (FIXME) *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
161 |
val smt_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
|
162 |
{worse_irrel_freq = #worse_irrel_freq 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
|
163 |
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
|
164 |
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
|
165 |
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
|
166 |
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
|
167 |
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
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
179 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
180 |
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
|
181 |
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
|
182 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
183 |
fun available_provers ctxt = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
184 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
185 |
val thy = ProofContext.theory_of ctxt |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
186 |
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
|
187 |
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
|
188 |
sort_strings (available_smt_solvers ctxt) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
189 |
|> List.partition (String.isPrefix remote_prefix) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
190 |
in |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
191 |
Output.urgent_message ("Available provers: " ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
192 |
commas (local_provers @ remote_provers) ^ ".") |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
193 |
end |
35969 | 194 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
199 |
(** problems, results, ATPs, etc. **) |
35969 | 200 |
|
201 |
type params = |
|
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
202 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
203 |
debug: bool, |
35969 | 204 |
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
|
205 |
overlord: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
206 |
provers: string list, |
35969 | 207 |
full_types: bool, |
41134 | 208 |
type_sys: string, |
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
|
209 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
210 |
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
|
211 |
max_relevant: int option, |
35969 | 212 |
isar_proof: bool, |
36924 | 213 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
214 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
215 |
expect: string} |
35867 | 216 |
|
41090 | 217 |
datatype prover_fact = |
218 |
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
|
219 |
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
|
220 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
221 |
type prover_problem = |
39318 | 222 |
{state: Proof.state, |
38998 | 223 |
goal: thm, |
224 |
subgoal: int, |
|
40065 | 225 |
subgoal_count: int, |
41090 | 226 |
facts: prover_fact list} |
35867 | 227 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
228 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
229 |
{outcome: failure option, |
35969 | 230 |
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
|
231 |
used_facts: (string * locality) list, |
40062 | 232 |
run_time_in_msecs: int option} |
35867 | 233 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
234 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 235 |
|
38023 | 236 |
(* configuration attributes *) |
237 |
||
38991 | 238 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
239 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 240 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 241 |
|
242 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
243 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 244 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
245 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
246 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 247 |
|
38023 | 248 |
fun with_path cleanup after f path = |
249 |
Exn.capture f path |
|
250 |
|> tap (fn _ => cleanup path) |
|
251 |
|> Exn.release |
|
252 |
|> tap (after path) |
|
253 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
254 |
fun proof_banner auto = |
40224 | 255 |
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
|
256 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
257 |
(* generic TPTP-based ATPs *) |
38023 | 258 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
259 |
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
|
260 |
| untranslated_fact (ATP_Translated_Fact (_, p)) = p |
41090 | 261 |
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
|
262 |
| 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
|
263 |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
264 |
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
|
265 |
| int_opt_add _ _ = NONE |
40062 | 266 |
|
39492 | 267 |
(* Important messages are important but not so important that users want to see |
268 |
them each time. *) |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
269 |
val important_message_keep_factor = 0.1 |
39492 | 270 |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
271 |
fun run_atp auto atp_name |
41103 | 272 |
({exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
273 |
known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) |
|
41134 | 274 |
({debug, verbose, overlord, full_types, type_sys, explicit_apply, |
275 |
isar_proof, isar_shrink_factor, timeout, ...} : params) |
|
40983 | 276 |
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = |
38023 | 277 |
let |
39318 | 278 |
val ctxt = Proof.context_of state |
41134 | 279 |
val type_sys = |
280 |
case (type_sys, full_types) of |
|
281 |
("tags", _) => Tags full_types |
|
282 |
| ("preds", _) => Preds full_types |
|
283 |
| ("const_args", _) => Const_Args |
|
284 |
| ("overload_args", _) => Overload_Args |
|
285 |
| ("none", _) => No_Types |
|
286 |
| _ => (if type_sys = "smart" then () |
|
287 |
else warning ("Unknown type system: " ^ quote type_sys ^ "."); |
|
288 |
if full_types then Tags true else Const_Args) |
|
38998 | 289 |
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
|
290 |
val facts = facts |> map (atp_translated_fact ctxt) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
291 |
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
292 |
else Config.get ctxt dest_dir |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
293 |
val problem_prefix = 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
|
294 |
val problem_file_name = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
295 |
Path.basic ((if overlord then "prob_" ^ atp_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
296 |
else problem_prefix ^ serial_string ()) |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
297 |
^ "_" ^ 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
|
298 |
val problem_path_name = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
299 |
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
|
300 |
File.tmp_path problem_file_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
301 |
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
|
302 |
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
|
303 |
else |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
304 |
error ("No such directory: " ^ quote dest_dir ^ ".") |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
305 |
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
|
306 |
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
|
307 |
(* write out problem file and call ATP *) |
38645 | 308 |
fun command_line complete timeout probfile = |
38023 | 309 |
let |
310 |
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
|
311 |
" " ^ File.shell_path probfile |
|
312 |
in |
|
39010 | 313 |
(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
|
314 |
else "exec " ^ core) ^ " 2>&1" |
38023 | 315 |
end |
316 |
fun split_time s = |
|
317 |
let |
|
318 |
val split = String.tokens (fn c => str c = "\n"); |
|
319 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
320 |
fun as_num f = f >> (fst o read_int); |
|
321 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
322 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
323 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
324 |
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
|
325 |
val as_time = Scan.read Symbol.stopper time o raw_explode |
38023 | 326 |
in (output, as_time t) end; |
327 |
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
|
328 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 329 |
(home_var, _) :: _ => |
38023 | 330 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 331 |
| [] => |
332 |
if File.exists command then |
|
333 |
let |
|
39318 | 334 |
fun run complete timeout = |
38032 | 335 |
let |
38645 | 336 |
val command = command_line complete timeout probfile |
38032 | 337 |
val ((output, msecs), res_code) = |
338 |
bash_output command |
|
339 |
|>> (if overlord then |
|
340 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
341 |
else |
|
342 |
I) |
|
40062 | 343 |
|>> (if measure_run_time then split_time else rpair NONE) |
39452 | 344 |
val (tstplike_proof, outcome) = |
345 |
extract_tstplike_proof_and_outcome complete res_code |
|
346 |
proof_delims known_failures output |
|
347 |
in (output, msecs, tstplike_proof, outcome) end |
|
38032 | 348 |
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
|
349 |
val (atp_problem, pool, conjecture_offset, fact_names) = |
41134 | 350 |
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
|
351 |
explicit_apply hyp_ts concl_t facts |
39452 | 352 |
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
|
353 |
atp_problem |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
354 |
val _ = File.write_list probfile ss |
38032 | 355 |
val conjecture_shape = |
356 |
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
|
357 |
|> map single |
39318 | 358 |
val run_twice = has_incomplete_mode andalso not auto |
38645 | 359 |
val timer = Timer.startRealTimer () |
38032 | 360 |
val result = |
39318 | 361 |
run false (if run_twice then |
362 |
Time.fromMilliseconds |
|
38645 | 363 |
(2 * Time.toMilliseconds timeout div 3) |
39318 | 364 |
else |
365 |
timeout) |
|
366 |
|> run_twice |
|
38645 | 367 |
? (fn (_, msecs0, _, SOME _) => |
39318 | 368 |
run true (Time.- (timeout, Timer.checkRealTimer timer)) |
39452 | 369 |
|> (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
|
370 |
(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
|
371 |
outcome)) |
38645 | 372 |
| 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
|
373 |
in ((pool, conjecture_shape, fact_names), result) end |
38032 | 374 |
else |
375 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 376 |
|
377 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
378 |
the proof file too. *) |
|
379 |
fun cleanup probfile = |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
380 |
if dest_dir = "" then try File.rm probfile else NONE |
38023 | 381 |
fun export probfile (_, (output, _, _, _)) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
382 |
if dest_dir = "" then |
38023 | 383 |
() |
384 |
else |
|
385 |
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
|
386 |
val ((pool, conjecture_shape, fact_names), |
39452 | 387 |
(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
|
388 |
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
|
389 |
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
|
390 |
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names |
39492 | 391 |
val important_message = |
40224 | 392 |
if not auto andalso random () <= important_message_keep_factor then |
39492 | 393 |
extract_important_message output |
394 |
else |
|
395 |
"" |
|
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 (message, used_facts) = |
38023 | 397 |
case outcome of |
398 |
NONE => |
|
399 |
proof_text isar_proof |
|
400 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
401 |
(proof_banner auto, full_types, 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
|
402 |
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
|
403 |
|>> (fn message => |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
404 |
message ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
405 |
(if verbose then |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
406 |
"\nATP real CPU time: " ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
407 |
string_from_time (Time.fromMilliseconds (the msecs)) ^ "." |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
408 |
else |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
409 |
"") ^ |
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
|
410 |
(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
|
411 |
"\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
|
412 |
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
|
413 |
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
|
414 |
"")) |
40669 | 415 |
| SOME failure => (string_for_failure "ATP" failure, []) |
38023 | 416 |
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
|
417 |
{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
|
418 |
run_time_in_msecs = msecs} |
38023 | 419 |
end |
420 |
||
40669 | 421 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until |
422 |
these are sorted out properly in the SMT module, we have to interpret these |
|
423 |
ourselves. *) |
|
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
424 |
val remote_smt_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
425 |
[(22, CantConnect), |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
426 |
(127, NoPerl), |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
427 |
(2, NoLibwwwPerl)] |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
428 |
val z3_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
429 |
[(103, MalformedInput), |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
430 |
(110, MalformedInput)] |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
431 |
val unix_failures = |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
432 |
[(139, Crashed)] |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
433 |
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures |
40555 | 434 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset
|
435 |
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset
|
436 |
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut |
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40558
diff
changeset
|
437 |
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = |
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
438 |
(case AList.lookup (op =) smt_failures code of |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
439 |
SOME failure => failure |
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset
|
440 |
| NONE => UnknownError) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset
|
441 |
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset
|
442 |
| failure_from_smt_failure _ = UnknownError |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
443 |
|
40698 | 444 |
(* FUDGE *) |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
445 |
val smt_max_iter = 8 |
40419
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents:
40417
diff
changeset
|
446 |
val smt_iter_fact_divisor = 2 |
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents:
40417
diff
changeset
|
447 |
val smt_iter_min_msecs = 5000 |
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents:
40417
diff
changeset
|
448 |
val smt_iter_timeout_divisor = 2 |
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
|
449 |
val smt_monomorph_limit = 4 |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
450 |
|
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
|
451 |
fun smt_filter_loop ({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
|
452 |
let |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
453 |
val ctxt = Proof.context_of state |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
454 |
fun iter timeout iter_num outcome0 msecs_so_far facts = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
455 |
let |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
456 |
val timer = Timer.startRealTimer () |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
457 |
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
|
458 |
val iter_timeout = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
459 |
if iter_num < smt_max_iter then |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
460 |
Int.min (ms, Int.max (smt_iter_min_msecs, |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
461 |
ms div smt_iter_timeout_divisor)) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
462 |
|> Time.fromMilliseconds |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
463 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
464 |
timeout |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
465 |
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
|
466 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
467 |
if verbose then |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
468 |
"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
|
469 |
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
|
470 |
|> Output.urgent_message |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
471 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
472 |
() |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
473 |
val {outcome, used_facts, run_time_in_msecs} = |
40979
e3ee5bbeb06e
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
blanchet
parents:
40978
diff
changeset
|
474 |
SMT_Solver.smt_filter remote iter_timeout state facts i |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
475 |
val _ = |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
476 |
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
|
477 |
"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
|
478 |
|> Output.urgent_message |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
479 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
480 |
() |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
481 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
482 |
val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
483 |
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
|
484 |
case outcome of |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
485 |
NONE => false |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
486 |
| 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
|
487 |
| 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
|
488 |
| 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
|
489 |
(if verbose then |
40555 | 490 |
"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
|
491 |
" fact" ^ plural_s num_facts ^ " terminated abnormally with \ |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
492 |
\exit code " ^ string_of_int code ^ "." |
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset
|
493 |
|> warning |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
494 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
495 |
(); |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
496 |
true (* kind of *)) |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
497 |
| SOME SMT_Failure.Out_Of_Memory => true |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
498 |
| SOME _ => true |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
499 |
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
|
500 |
in |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
501 |
if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
502 |
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
503 |
let val facts = take (num_facts div smt_iter_fact_divisor) facts in |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
504 |
iter timeout (iter_num + 1) outcome0 msecs_so_far facts |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
505 |
end |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
506 |
else |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
507 |
{outcome = if is_none outcome then NONE else the outcome0, |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
508 |
used_facts = used_facts, run_time_in_msecs = msecs_so_far} |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
509 |
end |
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset
|
510 |
in iter timeout 1 NONE (SOME 0) end |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
511 |
|
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
|
512 |
(* 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
|
513 |
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
|
514 |
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
|
515 |
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
|
516 |
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
|
517 |
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
|
518 |
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
|
519 |
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
|
520 |
| _ => 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
|
521 |
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
|
522 |
|
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
|
523 |
val smt_metis_timeout = seconds 0.5 |
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
|
524 |
|
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
525 |
fun can_apply_metis debug state i ths = |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
526 |
can_apply smt_metis_timeout |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
527 |
(Config.put Metis_Tactics.verbose debug |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
528 |
#> (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
|
529 |
|
40983 | 530 |
fun run_smt_solver auto name (params as {debug, ...}) minimize_command |
531 |
({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
|
532 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
533 |
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
|
534 |
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
|
535 |
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
|
536 |
| 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
|
537 |
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
|
538 |
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
|
539 |
#> Config.put SMT_Config.verbose debug |
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
|
540 |
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit |
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
|
541 |
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
|
542 |
val thy = Proof.theory_of state |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41103
diff
changeset
|
543 |
val facts = facts |> map (apsnd (pair NONE o Thm.transfer thy) o untranslated_fact) |
40181 | 544 |
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
|
545 |
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
|
546 |
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) |
40669 | 547 |
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
|
548 |
val message = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
549 |
case outcome of |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
550 |
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
|
551 |
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
|
552 |
val method = |
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
553 |
if can_apply_metis debug state subgoal (map snd used_facts) then |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
554 |
"metis" |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
555 |
else |
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset
|
556 |
"smt" |
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
|
557 |
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
|
558 |
try_command_line (proof_banner auto) |
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 |
(apply_on_subgoal subgoal subgoal_count ^ |
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
|
560 |
command_call method (map fst other_lemmas)) ^ |
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
|
561 |
minimize_line minimize_command |
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
|
562 |
(map fst (other_lemmas @ chained_lemmas)) |
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
|
563 |
end |
40669 | 564 |
| 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
|
565 |
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
|
566 |
{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
|
567 |
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
|
568 |
end |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
569 |
|
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
570 |
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
|
571 |
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
|
572 |
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
|
573 |
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
|
574 |
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
|
575 |
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
|
576 |
else |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
577 |
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
|
578 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
579 |
|
38023 | 580 |
val setup = |
581 |
dest_dir_setup |
|
582 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
583 |
#> measure_run_time_setup |
38023 | 584 |
|
28582 | 585 |
end; |