author | blanchet |
Wed, 10 Nov 2010 09:03:07 +0100 | |
changeset 40471 | 2269544b6457 |
parent 40439 | fb6ee11e776a |
child 40553 | 1264c9172338 |
permissions | -rw-r--r-- |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer.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 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
6 |
Sledgehammer's heart. |
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 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
9 |
signature SLEDGEHAMMER = |
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 |
38988 | 14 |
type relevance_override = Sledgehammer_Filter.relevance_override |
40114 | 15 |
type translated_formula = Sledgehammer_ATP_Translate.translated_formula |
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 = |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
19 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
20 |
debug: bool, |
35969 | 21 |
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
|
22 |
overlord: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
23 |
provers: string list, |
35969 | 24 |
full_types: bool, |
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 |
|
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
|
33 |
datatype fact = |
40114 | 34 |
Untranslated of (string * locality) * thm | |
35 |
Translated of term * ((string * locality) * translated_formula) option |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
36 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
37 |
type prover_problem = |
39318 | 38 |
{state: Proof.state, |
38998 | 39 |
goal: thm, |
40 |
subgoal: int, |
|
40065 | 41 |
subgoal_count: int, |
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
|
42 |
facts: fact list, |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
43 |
only: bool} |
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 |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
53 |
val smtN : string |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
54 |
val is_prover_available : theory -> string -> bool |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
55 |
val is_prover_installed : Proof.context -> string -> bool |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
56 |
val default_max_relevant_for_prover : theory -> string -> int |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
57 |
val is_built_in_const_for_prover : |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
58 |
Proof.context -> string -> string * typ -> bool |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
59 |
val relevance_fudge_for_prover : string -> relevance_fudge |
38023 | 60 |
val dest_dir : string Config.T |
61 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
62 |
val measure_run_time : bool Config.T |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
63 |
val available_provers : theory -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
64 |
val kill_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
65 |
val running_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
66 |
val messages : int option -> unit |
40200 | 67 |
val get_prover : theory -> bool -> string -> prover |
38044 | 68 |
val run_sledgehammer : |
39318 | 69 |
params -> bool -> int -> relevance_override -> (string -> minimize_command) |
70 |
-> Proof.state -> bool * Proof.state |
|
38023 | 71 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
72 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
73 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
74 |
structure Sledgehammer : SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
75 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
76 |
|
38028 | 77 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset
|
78 |
open ATP_Proof |
38028 | 79 |
open ATP_Systems |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset
|
80 |
open Metis_Translate |
38023 | 81 |
open Sledgehammer_Util |
38988 | 82 |
open Sledgehammer_Filter |
40068 | 83 |
open Sledgehammer_ATP_Translate |
84 |
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
|
85 |
|
38023 | 86 |
|
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
|
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 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
93 |
val smtN = "smt" |
40062 | 94 |
val smt_prover_names = [smtN, remote_prefix ^ smtN] |
95 |
||
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
96 |
val is_smt_prover = member (op =) smt_prover_names |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
97 |
|
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
98 |
fun is_prover_available thy name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
99 |
is_smt_prover name orelse member (op =) (available_atps thy) name |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
100 |
|
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
101 |
fun is_prover_installed ctxt name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
102 |
let val thy = ProofContext.theory_of ctxt in |
40181 | 103 |
if is_smt_prover name then SMT_Solver.is_locally_installed ctxt |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
104 |
else is_atp_installed thy name |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
105 |
end |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
106 |
|
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
|
107 |
val smt_default_max_relevant = 200 (* FUDGE *) |
40062 | 108 |
val auto_max_relevant_divisor = 2 (* FUDGE *) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
109 |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
110 |
fun default_max_relevant_for_prover thy name = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
111 |
if is_smt_prover name then smt_default_max_relevant |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
112 |
else #default_max_relevant (get_atp thy name) |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
113 |
|
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
|
114 |
(* 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
|
115 |
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
|
116 |
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
|
117 |
[@{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
|
118 |
@{const_name HOL.eq}] |
40206 | 119 |
|
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
120 |
fun is_built_in_const_for_prover ctxt name (s, T) = |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
121 |
if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T) |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
122 |
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
|
123 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
124 |
(* FUDGE *) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
125 |
val atp_relevance_fudge = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
126 |
{worse_irrel_freq = 100.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
127 |
higher_order_irrel_weight = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
128 |
abs_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
129 |
abs_irrel_weight = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
130 |
skolem_irrel_weight = 0.75, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
131 |
theory_const_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
132 |
theory_const_irrel_weight = 0.25, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
133 |
intro_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
134 |
elim_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
135 |
simp_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
136 |
local_bonus = 0.55, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
137 |
assum_bonus = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
138 |
chained_bonus = 1.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
139 |
max_imperfect = 11.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
140 |
max_imperfect_exp = 1.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
141 |
threshold_divisor = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
142 |
ridiculous_threshold = 0.1} |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
143 |
|
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 |
(* FUDGE (FIXME) *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
145 |
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
|
146 |
{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
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
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
|
162 |
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
163 |
|
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
164 |
fun relevance_fudge_for_prover name = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
165 |
if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
166 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
167 |
fun available_provers thy = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
168 |
let |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
169 |
val (remote_provers, local_provers) = |
40062 | 170 |
sort_strings (available_atps thy) @ smt_prover_names |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
171 |
|> List.partition (String.isPrefix remote_prefix) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
172 |
in |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
173 |
Output.urgent_message ("Available provers: " ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
174 |
commas (local_provers @ remote_provers) ^ ".") |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
175 |
end |
35969 | 176 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
181 |
(** problems, results, ATPs, etc. **) |
35969 | 182 |
|
183 |
type params = |
|
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
184 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
185 |
debug: bool, |
35969 | 186 |
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
|
187 |
overlord: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
188 |
provers: string list, |
35969 | 189 |
full_types: bool, |
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
|
190 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
191 |
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
|
192 |
max_relevant: int option, |
35969 | 193 |
isar_proof: bool, |
36924 | 194 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
195 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
196 |
expect: string} |
35867 | 197 |
|
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
|
198 |
datatype fact = |
40114 | 199 |
Untranslated of (string * locality) * thm | |
200 |
Translated of term * ((string * locality) * translated_formula) option |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
201 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
202 |
type prover_problem = |
39318 | 203 |
{state: Proof.state, |
38998 | 204 |
goal: thm, |
205 |
subgoal: int, |
|
40065 | 206 |
subgoal_count: int, |
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
|
207 |
facts: fact list, |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
208 |
only: bool} |
35867 | 209 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
210 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
211 |
{outcome: failure option, |
35969 | 212 |
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
|
213 |
used_facts: (string * locality) list, |
40062 | 214 |
run_time_in_msecs: int option} |
35867 | 215 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
216 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 217 |
|
38023 | 218 |
(* configuration attributes *) |
219 |
||
38991 | 220 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
221 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 222 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 223 |
|
224 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
225 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 226 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
227 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
228 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 229 |
|
38023 | 230 |
fun with_path cleanup after f path = |
231 |
Exn.capture f path |
|
232 |
|> tap (fn _ => cleanup path) |
|
233 |
|> Exn.release |
|
234 |
|> tap (after path) |
|
235 |
||
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
|
236 |
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i |
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
|
237 |
n goal = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
238 |
quote name ^ |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
239 |
(if verbose then |
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
|
240 |
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
241 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
242 |
"") ^ |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
243 |
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
244 |
(if blocking then |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
245 |
"" |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
246 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
247 |
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
248 |
|
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
249 |
fun proof_banner auto = |
40224 | 250 |
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
|
251 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
252 |
(* generic TPTP-based ATPs *) |
38023 | 253 |
|
40114 | 254 |
fun dest_Untranslated (Untranslated p) = p |
255 |
| dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" |
|
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
|
256 |
fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p |
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
|
257 |
| translated_fact _ (Translated p) = p |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
258 |
fun fact_name (Untranslated ((name, _), _)) = SOME name |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
259 |
| fact_name (Translated (_, p)) = Option.map (fst o fst) p |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
260 |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
261 |
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
|
262 |
| int_opt_add _ _ = NONE |
40062 | 263 |
|
39492 | 264 |
(* Important messages are important but not so important that users want to see |
265 |
them each time. *) |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
266 |
val important_message_keep_factor = 0.1 |
39492 | 267 |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
268 |
fun run_atp auto atp_name |
38645 | 269 |
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
38997 | 270 |
known_failures, default_max_relevant, explicit_forall, |
271 |
use_conjecture_for_hypotheses} |
|
38455 | 272 |
({debug, verbose, overlord, full_types, explicit_apply, |
38998 | 273 |
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
274 |
minimize_command |
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
|
275 |
({state, goal, subgoal, facts, only, ...} : prover_problem) = |
38023 | 276 |
let |
39318 | 277 |
val ctxt = Proof.context_of state |
38998 | 278 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
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
|
279 |
val facts = |
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
|
280 |
facts |> not only ? take (the_default default_max_relevant max_relevant) |
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
|
281 |
|> map (translated_fact ctxt) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
282 |
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
|
283 |
else Config.get ctxt dest_dir |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
284 |
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
|
285 |
val problem_file_name = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
286 |
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
|
287 |
else problem_prefix ^ serial_string ()) |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
288 |
^ "_" ^ 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
|
289 |
val problem_path_name = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
290 |
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
|
291 |
File.tmp_path problem_file_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
292 |
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
|
293 |
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
|
294 |
else |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
295 |
error ("No such directory: " ^ quote dest_dir ^ ".") |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
296 |
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
|
297 |
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
|
298 |
(* write out problem file and call ATP *) |
38645 | 299 |
fun command_line complete timeout probfile = |
38023 | 300 |
let |
301 |
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
|
302 |
" " ^ File.shell_path probfile |
|
303 |
in |
|
39010 | 304 |
(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
|
305 |
else "exec " ^ core) ^ " 2>&1" |
38023 | 306 |
end |
307 |
fun split_time s = |
|
308 |
let |
|
309 |
val split = String.tokens (fn c => str c = "\n"); |
|
310 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
311 |
fun as_num f = f >> (fst o read_int); |
|
312 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
313 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
314 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
315 |
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
|
40062 | 316 |
val as_time = Scan.read Symbol.stopper time o explode |
38023 | 317 |
in (output, as_time t) end; |
318 |
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
|
319 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 320 |
(home_var, _) :: _ => |
38023 | 321 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 322 |
| [] => |
323 |
if File.exists command then |
|
324 |
let |
|
39318 | 325 |
fun run complete timeout = |
38032 | 326 |
let |
38645 | 327 |
val command = command_line complete timeout probfile |
38032 | 328 |
val ((output, msecs), res_code) = |
329 |
bash_output command |
|
330 |
|>> (if overlord then |
|
331 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
332 |
else |
|
333 |
I) |
|
40062 | 334 |
|>> (if measure_run_time then split_time else rpair NONE) |
39452 | 335 |
val (tstplike_proof, outcome) = |
336 |
extract_tstplike_proof_and_outcome complete res_code |
|
337 |
proof_delims known_failures output |
|
338 |
in (output, msecs, tstplike_proof, outcome) end |
|
38032 | 339 |
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
|
340 |
val (atp_problem, pool, conjecture_offset, fact_names) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
341 |
prepare_atp_problem ctxt readable_names explicit_forall full_types |
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
|
342 |
explicit_apply hyp_ts concl_t facts |
39452 | 343 |
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
|
344 |
atp_problem |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
345 |
val _ = File.write_list probfile ss |
38032 | 346 |
val conjecture_shape = |
347 |
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
|
348 |
|> map single |
39318 | 349 |
val run_twice = has_incomplete_mode andalso not auto |
38645 | 350 |
val timer = Timer.startRealTimer () |
38032 | 351 |
val result = |
39318 | 352 |
run false (if run_twice then |
353 |
Time.fromMilliseconds |
|
38645 | 354 |
(2 * Time.toMilliseconds timeout div 3) |
39318 | 355 |
else |
356 |
timeout) |
|
357 |
|> run_twice |
|
38645 | 358 |
? (fn (_, msecs0, _, SOME _) => |
39318 | 359 |
run true (Time.- (timeout, Timer.checkRealTimer timer)) |
39452 | 360 |
|> (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
|
361 |
(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
|
362 |
outcome)) |
38645 | 363 |
| 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
|
364 |
in ((pool, conjecture_shape, fact_names), result) end |
38032 | 365 |
else |
366 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 367 |
|
368 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
369 |
the proof file too. *) |
|
370 |
fun cleanup probfile = |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
371 |
if dest_dir = "" then try File.rm probfile else NONE |
38023 | 372 |
fun export probfile (_, (output, _, _, _)) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
373 |
if dest_dir = "" then |
38023 | 374 |
() |
375 |
else |
|
376 |
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
|
377 |
val ((pool, conjecture_shape, fact_names), |
39452 | 378 |
(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
|
379 |
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
|
380 |
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
|
381 |
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names |
39492 | 382 |
val important_message = |
40224 | 383 |
if not auto andalso random () <= important_message_keep_factor then |
39492 | 384 |
extract_important_message output |
385 |
else |
|
386 |
"" |
|
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
|
387 |
val (message, used_facts) = |
38023 | 388 |
case outcome of |
389 |
NONE => |
|
390 |
proof_text isar_proof |
|
391 |
(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
|
392 |
(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
|
393 |
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
|
394 |
|>> (fn message => |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
395 |
message ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
396 |
(if verbose then |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
397 |
"\nATP real CPU time: " ^ |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
398 |
string_from_time (Time.fromMilliseconds (the msecs)) ^ "." |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
399 |
else |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset
|
400 |
"") ^ |
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
|
401 |
(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
|
402 |
"\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
|
403 |
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
|
404 |
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
|
405 |
"")) |
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset
|
406 |
| SOME failure => (string_for_failure failure, []) |
38023 | 407 |
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
|
408 |
{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
|
409 |
run_time_in_msecs = msecs} |
38023 | 410 |
end |
411 |
||
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
|
412 |
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
|
413 |
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut |
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
|
414 |
| 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
|
415 |
| failure_from_smt_failure _ = UnknownError |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
416 |
|
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
|
417 |
val smt_max_iter = 5 |
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
|
418 |
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
|
419 |
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
|
420 |
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
|
421 |
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
|
422 |
|
40412
f2fbea1e5f9e
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet
parents:
40409
diff
changeset
|
423 |
fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i = |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
424 |
let |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
425 |
val timer = Timer.startRealTimer () |
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
|
426 |
val ms = timeout |> Time.toMilliseconds |
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
|
427 |
val iter_timeout = |
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
|
428 |
if iter < smt_max_iter then |
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
|
429 |
Int.min (ms, Int.max (smt_iter_min_msecs, |
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
|
430 |
ms div smt_iter_timeout_divisor)) |
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
|
431 |
|> Time.fromMilliseconds |
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
|
432 |
else |
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
|
433 |
timeout |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
434 |
val {outcome, used_facts, run_time_in_msecs} = |
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
|
435 |
TimeLimit.timeLimit iter_timeout |
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
|
436 |
(SMT_Solver.smt_filter remote iter_timeout state facts) i |
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
|
437 |
handle TimeLimit.TimeOut => |
40428 | 438 |
{outcome = SOME SMT_Failure.Time_Out, used_facts = [], |
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
|
439 |
run_time_in_msecs = NONE} |
40412
f2fbea1e5f9e
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet
parents:
40409
diff
changeset
|
440 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
441 |
val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
442 |
val too_many_facts_perhaps = |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
443 |
case outcome of |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
444 |
NONE => false |
40428 | 445 |
| SOME (SMT_Failure.Counterexample _) => false |
446 |
| SOME SMT_Failure.Time_Out => iter_timeout <> timeout |
|
447 |
| SOME SMT_Failure.Out_Of_Memory => true |
|
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
448 |
| SOME _ => true |
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
|
449 |
val timeout = Time.- (timeout, Timer.checkRealTimer timer) |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
450 |
in |
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
|
451 |
if too_many_facts_perhaps andalso iter < smt_max_iter andalso |
40471 | 452 |
not (null facts) andalso Time.> (timeout, Time.zeroTime) then |
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
|
453 |
let val facts = take (length facts div smt_iter_fact_divisor) facts in |
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
|
454 |
smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
455 |
facts i |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
456 |
end |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
457 |
else |
40412
f2fbea1e5f9e
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet
parents:
40409
diff
changeset
|
458 |
{outcome = if is_none outcome then NONE else the outcome0, |
f2fbea1e5f9e
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet
parents:
40409
diff
changeset
|
459 |
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
|
460 |
end |
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
461 |
|
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
|
462 |
fun run_smt_solver auto remote ({debug, timeout, ...} : params) minimize_command |
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
|
463 |
({state, subgoal, subgoal_count, facts, ...} |
40065 | 464 |
: 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
|
465 |
let |
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
|
466 |
val repair_context = |
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
|
467 |
Config.put SMT_Config.verbose debug |
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
|
468 |
#> 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
|
469 |
val state = state |> Proof.map_context repair_context |
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset
|
470 |
val ctxt = Proof.context_of state |
40181 | 471 |
val {outcome, used_facts, run_time_in_msecs} = |
40412
f2fbea1e5f9e
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet
parents:
40409
diff
changeset
|
472 |
smt_filter_loop 1 NONE (SOME 0) remote timeout state |
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset
|
473 |
(map_filter (try dest_Untranslated) facts) subgoal |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
474 |
val message = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
475 |
case outcome of |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
476 |
NONE => |
40224 | 477 |
try_command_line (proof_banner auto) |
40065 | 478 |
(apply_on_subgoal subgoal subgoal_count ^ |
40181 | 479 |
command_call smtN (map fst used_facts)) ^ |
480 |
minimize_line minimize_command (map fst used_facts) |
|
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
|
481 |
| SOME SMT_Failure.Time_Out => "Timed out." |
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
|
482 |
| SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable." |
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset
|
483 |
| SOME failure => |
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
|
484 |
SMT_Failure.string_of_failure ctxt failure |
40200 | 485 |
val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *) |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
486 |
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
|
487 |
{outcome = outcome, used_facts = used_facts, |
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
|
488 |
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
|
489 |
end |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
490 |
|
40200 | 491 |
fun get_prover thy auto name = |
40224 | 492 |
if is_smt_prover name then |
493 |
run_smt_solver auto (String.isPrefix remote_prefix name) |
|
494 |
else |
|
495 |
run_atp auto name (get_atp thy name) |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
496 |
|
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
497 |
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) |
40065 | 498 |
auto minimize_command |
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
|
499 |
(problem as {state, goal, subgoal, subgoal_count, facts, ...}) |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
500 |
name = |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
501 |
let |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
502 |
val thy = Proof.theory_of state |
39318 | 503 |
val ctxt = Proof.context_of state |
37584 | 504 |
val birth_time = Time.now () |
505 |
val death_time = Time.+ (birth_time, timeout) |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
506 |
val max_relevant = |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
507 |
the_default (default_max_relevant_for_prover thy name) max_relevant |
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
|
508 |
val num_facts = Int.min (length facts, max_relevant) |
40065 | 509 |
val desc = |
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
|
510 |
prover_description ctxt params name num_facts subgoal subgoal_count goal |
39318 | 511 |
fun go () = |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
512 |
let |
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
513 |
fun really_go () = |
40200 | 514 |
get_prover thy auto name params (minimize_command name) problem |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
515 |
|> (fn {outcome, message, ...} => |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
516 |
(if is_some outcome then "none" else "some", message)) |
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
517 |
val (outcome_code, message) = |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
518 |
if debug then |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
519 |
really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
520 |
else |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
521 |
(really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
522 |
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
523 |
| exn => ("unknown", "Internal error:\n" ^ |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
524 |
ML_Compiler.exn_message exn ^ "\n")) |
39318 | 525 |
val _ = |
526 |
if expect = "" orelse outcome_code = expect then |
|
527 |
() |
|
528 |
else if blocking then |
|
529 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
530 |
else |
|
531 |
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
532 |
in (outcome_code = "some", message) end |
|
533 |
in |
|
534 |
if auto then |
|
535 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
536 |
(success, state |> success ? Proof.goal_message (fn () => |
|
537 |
Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite |
|
39327 | 538 |
(Pretty.str message)])) |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
539 |
end |
39318 | 540 |
else if blocking then |
541 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
542 |
List.app Output.urgent_message |
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset
|
543 |
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); |
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset
|
544 |
(success, state) |
39318 | 545 |
end |
546 |
else |
|
547 |
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); |
|
548 |
(false, state)) |
|
37584 | 549 |
end |
28582 | 550 |
|
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
551 |
fun run_sledgehammer (params as {blocking, debug, provers, full_types, |
40069 | 552 |
relevance_thresholds, max_relevant, ...}) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
553 |
auto i (relevance_override as {only, ...}) minimize_command |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
554 |
state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
555 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
556 |
error "No prover is set." |
39318 | 557 |
else case subgoal_count state of |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
558 |
0 => (Output.urgent_message "No subgoal!"; (false, state)) |
39318 | 559 |
| n => |
560 |
let |
|
39364 | 561 |
val _ = Proof.assert_backward state |
39318 | 562 |
val thy = Proof.theory_of state |
40200 | 563 |
val ctxt = Proof.context_of state |
564 |
val {facts = chained_ths, goal, ...} = Proof.goal state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
565 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
566 |
val _ = () |> not blocking ? kill_provers |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
567 |
val _ = if auto then () else Output.urgent_message "Sledgehammering..." |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
568 |
val (smts, atps) = provers |> List.partition is_smt_prover |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
569 |
fun run_provers label full_types relevance_fudge maybe_translate provers |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
570 |
(res as (success, state)) = |
40065 | 571 |
if success orelse null provers then |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
572 |
res |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
573 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
574 |
let |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
575 |
val max_max_relevant = |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
576 |
case max_relevant of |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
577 |
SOME n => n |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
578 |
| NONE => |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
579 |
0 |> fold (Integer.max o default_max_relevant_for_prover thy) |
40065 | 580 |
provers |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
581 |
|> auto ? (fn n => n div auto_max_relevant_divisor) |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
582 |
val is_built_in_const = |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
583 |
is_built_in_const_for_prover ctxt (hd provers) |
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
|
584 |
val facts = |
40065 | 585 |
relevant_facts ctxt full_types relevance_thresholds |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
586 |
max_max_relevant is_built_in_const 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
|
587 |
relevance_override chained_ths hyp_ts concl_t |
40114 | 588 |
|> map maybe_translate |
40062 | 589 |
val problem = |
40065 | 590 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
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
|
591 |
facts = facts, only = only} |
40065 | 592 |
val run_prover = run_prover params auto minimize_command |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
593 |
in |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
594 |
if debug then |
40370 | 595 |
Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
596 |
(if null facts then |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
597 |
"Found no relevant facts." |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
598 |
else |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
599 |
"Including (up to) " ^ string_of_int (length facts) ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
600 |
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
601 |
(facts |> map_filter fact_name |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
602 |
|> space_implode " ") ^ ".")) |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
603 |
else |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
604 |
(); |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
605 |
if auto then |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
606 |
fold (fn prover => fn (true, state) => (true, state) |
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset
|
607 |
| (false, _) => run_prover problem prover) |
40065 | 608 |
provers (false, state) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
609 |
else |
40065 | 610 |
provers |> (if blocking then Par_List.map else map) |
611 |
(run_prover problem) |
|
612 |
|> exists fst |> rpair state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
613 |
end |
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
|
614 |
val run_atps = |
40370 | 615 |
run_provers "ATP" full_types atp_relevance_fudge |
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
|
616 |
(Translated o translate_fact ctxt) atps |
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
|
617 |
val run_smts = |
40370 | 618 |
run_provers "SMT solver" true smt_relevance_fudge Untranslated smts |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
619 |
fun run_atps_and_smt_solvers () = |
40065 | 620 |
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
621 |
in |
40065 | 622 |
(false, state) |
623 |
|> (if blocking then run_atps #> not auto ? run_smts |
|
624 |
else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
625 |
end |
38044 | 626 |
|
38023 | 627 |
val setup = |
628 |
dest_dir_setup |
|
629 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
630 |
#> measure_run_time_setup |
38023 | 631 |
|
28582 | 632 |
end; |