author | blanchet |
Tue, 26 Oct 2010 13:50:57 +0200 | |
changeset 40184 | 91b4b73dbafb |
parent 40181 | 3788b7adab36 |
child 40190 | 9f82ed60e7ec |
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 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
33 |
datatype axiom = |
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, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
42 |
axioms: axiom 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, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
47 |
used_axioms: (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 |
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
|
57 |
val irrelevant_consts_for_prover : string -> string list |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
58 |
val relevance_fudge_for_prover : string -> relevance_fudge |
38023 | 59 |
val dest_dir : string Config.T |
60 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
61 |
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
|
62 |
val available_provers : theory -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
63 |
val kill_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
64 |
val running_provers : unit -> unit |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
65 |
val messages : int option -> unit |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
66 |
val get_prover : Proof.context -> bool -> string -> prover |
38044 | 67 |
val run_sledgehammer : |
39318 | 68 |
params -> bool -> int -> relevance_override -> (string -> minimize_command) |
69 |
-> Proof.state -> bool * Proof.state |
|
38023 | 70 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
71 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
72 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
73 |
structure Sledgehammer : SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
74 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
75 |
|
38028 | 76 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset
|
77 |
open ATP_Proof |
38028 | 78 |
open ATP_Systems |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset
|
79 |
open Metis_Translate |
38023 | 80 |
open Sledgehammer_Util |
38988 | 81 |
open Sledgehammer_Filter |
40068 | 82 |
open Sledgehammer_ATP_Translate |
83 |
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
|
84 |
|
38023 | 85 |
|
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 |
(** 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
|
87 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
88 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
89 |
"Async_Manager". *) |
37585 | 90 |
val das_Tool = "Sledgehammer" |
91 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
92 |
val smtN = "smt" |
40062 | 93 |
val smt_prover_names = [smtN, remote_prefix ^ smtN] |
94 |
||
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
95 |
val is_smt_prover = member (op =) smt_prover_names |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
96 |
|
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
97 |
fun is_prover_available thy name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
98 |
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
|
99 |
|
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
100 |
fun is_prover_installed ctxt name = |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
101 |
let val thy = ProofContext.theory_of ctxt in |
40181 | 102 |
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
|
103 |
else is_atp_installed thy name |
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
104 |
end |
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 |
val smt_default_max_relevant = 300 (* FUDGE (FIXME) *) |
40062 | 107 |
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
|
108 |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
109 |
fun default_max_relevant_for_prover thy name = |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
110 |
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
|
111 |
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
|
112 |
|
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
|
113 |
(* 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
|
114 |
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
|
115 |
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
|
116 |
[@{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
|
117 |
@{const_name HOL.eq}] |
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 |
val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *) |
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
|
119 |
|
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
|
120 |
fun irrelevant_consts_for_prover name = |
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
|
121 |
if is_smt_prover name then smt_irrelevant_consts else 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
|
122 |
|
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
123 |
(* FUDGE *) |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
124 |
val atp_relevance_fudge = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
125 |
{worse_irrel_freq = 100.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
126 |
higher_order_irrel_weight = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
127 |
abs_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
128 |
abs_irrel_weight = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
129 |
skolem_irrel_weight = 0.75, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
130 |
theory_const_rel_weight = 0.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
131 |
theory_const_irrel_weight = 0.25, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
132 |
intro_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
133 |
elim_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
134 |
simp_bonus = 0.15, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
135 |
local_bonus = 0.55, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
136 |
assum_bonus = 1.05, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
137 |
chained_bonus = 1.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
138 |
max_imperfect = 11.5, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
139 |
max_imperfect_exp = 1.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
140 |
threshold_divisor = 2.0, |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
141 |
ridiculous_threshold = 0.1} |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
142 |
|
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
|
143 |
(* FUDGE (FIXME) *) |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
144 |
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
|
145 |
{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
|
146 |
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
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} |
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
162 |
|
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
163 |
fun relevance_fudge_for_prover name = |
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset
|
164 |
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
|
165 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
166 |
fun available_provers thy = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
167 |
let |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
168 |
val (remote_provers, local_provers) = |
40062 | 169 |
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
|
170 |
|> List.partition (String.isPrefix remote_prefix) |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
171 |
in |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
172 |
Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^ |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
173 |
".") |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
174 |
end |
35969 | 175 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
176 |
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
|
177 |
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
|
178 |
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
|
179 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
180 |
(** problems, results, ATPs, etc. **) |
35969 | 181 |
|
182 |
type params = |
|
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
183 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
184 |
debug: bool, |
35969 | 185 |
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
|
186 |
overlord: bool, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
187 |
provers: string list, |
35969 | 188 |
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
|
189 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
190 |
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
|
191 |
max_relevant: int option, |
35969 | 192 |
isar_proof: bool, |
36924 | 193 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
194 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
195 |
expect: string} |
35867 | 196 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
197 |
datatype axiom = |
40114 | 198 |
Untranslated of (string * locality) * thm | |
199 |
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
|
200 |
|
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
201 |
type prover_problem = |
39318 | 202 |
{state: Proof.state, |
38998 | 203 |
goal: thm, |
204 |
subgoal: int, |
|
40065 | 205 |
subgoal_count: int, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
206 |
axioms: axiom list, |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
207 |
only: bool} |
35867 | 208 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
209 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
210 |
{outcome: failure option, |
35969 | 211 |
message: string, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
212 |
used_axioms: (string * locality) list, |
40062 | 213 |
run_time_in_msecs: int option} |
35867 | 214 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
215 |
type prover = params -> minimize_command -> prover_problem -> prover_result |
35867 | 216 |
|
38023 | 217 |
(* configuration attributes *) |
218 |
||
38991 | 219 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
220 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 221 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 222 |
|
223 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
224 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 225 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
226 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
227 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 228 |
|
38023 | 229 |
fun with_path cleanup after f path = |
230 |
Exn.capture f path |
|
231 |
|> tap (fn _ => cleanup path) |
|
232 |
|> Exn.release |
|
233 |
|> tap (after path) |
|
234 |
||
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
235 |
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
236 |
i n goal = |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
237 |
quote name ^ |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
238 |
(if verbose then |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
239 |
" with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
240 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
241 |
"") ^ |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
242 |
" 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
|
243 |
(if blocking then |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
244 |
"" |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
245 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
246 |
"\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
|
247 |
|
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
248 |
fun proof_banner auto = |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
249 |
if auto then "Sledgehammer found a proof" else "Try this command" |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
250 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
251 |
(* generic TPTP-based ATPs *) |
38023 | 252 |
|
40114 | 253 |
fun dest_Untranslated (Untranslated p) = p |
254 |
| dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" |
|
255 |
fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p |
|
256 |
| translated_axiom _ (Translated p) = p |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
257 |
|
40062 | 258 |
fun int_option_add (SOME m) (SOME n) = SOME (m + n) |
259 |
| int_option_add _ _ = NONE |
|
260 |
||
39492 | 261 |
(* Important messages are important but not so important that users want to see |
262 |
them each time. *) |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
263 |
val important_message_keep_factor = 0.1 |
39492 | 264 |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
265 |
fun run_atp auto atp_name |
38645 | 266 |
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
38997 | 267 |
known_failures, default_max_relevant, explicit_forall, |
268 |
use_conjecture_for_hypotheses} |
|
38455 | 269 |
({debug, verbose, overlord, full_types, explicit_apply, |
38998 | 270 |
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
|
271 |
minimize_command |
40065 | 272 |
({state, goal, subgoal, axioms, only, ...} : prover_problem) = |
38023 | 273 |
let |
39318 | 274 |
val ctxt = Proof.context_of state |
38998 | 275 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
276 |
val axioms = |
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
277 |
axioms |> not only ? take (the_default default_max_relevant max_relevant) |
40114 | 278 |
|> map (translated_axiom ctxt) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
279 |
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
|
280 |
else Config.get ctxt dest_dir |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
281 |
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
|
282 |
val problem_file_name = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
283 |
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
|
284 |
else problem_prefix ^ serial_string ()) |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
285 |
^ "_" ^ 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
|
286 |
val problem_path_name = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
287 |
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
|
288 |
File.tmp_path problem_file_name |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
289 |
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
|
290 |
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
|
291 |
else |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
292 |
error ("No such directory: " ^ quote dest_dir ^ ".") |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
(* write out problem file and call ATP *) |
38645 | 296 |
fun command_line complete timeout probfile = |
38023 | 297 |
let |
298 |
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
|
299 |
" " ^ File.shell_path probfile |
|
300 |
in |
|
39010 | 301 |
(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
|
302 |
else "exec " ^ core) ^ " 2>&1" |
38023 | 303 |
end |
304 |
fun split_time s = |
|
305 |
let |
|
306 |
val split = String.tokens (fn c => str c = "\n"); |
|
307 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
308 |
fun as_num f = f >> (fst o read_int); |
|
309 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
310 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
311 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
312 |
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
|
40062 | 313 |
val as_time = Scan.read Symbol.stopper time o explode |
38023 | 314 |
in (output, as_time t) end; |
315 |
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
|
316 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 317 |
(home_var, _) :: _ => |
38023 | 318 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 319 |
| [] => |
320 |
if File.exists command then |
|
321 |
let |
|
39318 | 322 |
fun run complete timeout = |
38032 | 323 |
let |
38645 | 324 |
val command = command_line complete timeout probfile |
38032 | 325 |
val ((output, msecs), res_code) = |
326 |
bash_output command |
|
327 |
|>> (if overlord then |
|
328 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
329 |
else |
|
330 |
I) |
|
40062 | 331 |
|>> (if measure_run_time then split_time else rpair NONE) |
39452 | 332 |
val (tstplike_proof, outcome) = |
333 |
extract_tstplike_proof_and_outcome complete res_code |
|
334 |
proof_delims known_failures output |
|
335 |
in (output, msecs, tstplike_proof, outcome) end |
|
38032 | 336 |
val readable_names = debug andalso overlord |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
337 |
val (atp_problem, pool, conjecture_offset, axiom_names) = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
338 |
prepare_atp_problem ctxt readable_names explicit_forall full_types |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
339 |
explicit_apply hyp_ts concl_t axioms |
39452 | 340 |
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
|
341 |
atp_problem |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
342 |
val _ = File.write_list probfile ss |
38032 | 343 |
val conjecture_shape = |
344 |
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
|
345 |
|> map single |
39318 | 346 |
val run_twice = has_incomplete_mode andalso not auto |
38645 | 347 |
val timer = Timer.startRealTimer () |
38032 | 348 |
val result = |
39318 | 349 |
run false (if run_twice then |
350 |
Time.fromMilliseconds |
|
38645 | 351 |
(2 * Time.toMilliseconds timeout div 3) |
39318 | 352 |
else |
353 |
timeout) |
|
354 |
|> run_twice |
|
38645 | 355 |
? (fn (_, msecs0, _, SOME _) => |
39318 | 356 |
run true (Time.- (timeout, Timer.checkRealTimer timer)) |
39452 | 357 |
|> (fn (output, msecs, tstplike_proof, outcome) => |
40062 | 358 |
(output, int_option_add msecs0 msecs, |
359 |
tstplike_proof, outcome)) |
|
38645 | 360 |
| result => result) |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
361 |
in ((pool, conjecture_shape, axiom_names), result) end |
38032 | 362 |
else |
363 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 364 |
|
365 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
366 |
the proof file too. *) |
|
367 |
fun cleanup probfile = |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
368 |
if dest_dir = "" then try File.rm probfile else NONE |
38023 | 369 |
fun export probfile (_, (output, _, _, _)) = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
370 |
if dest_dir = "" then |
38023 | 371 |
() |
372 |
else |
|
373 |
File.write (Path.explode (Path.implode probfile ^ "_proof")) output |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
374 |
val ((pool, conjecture_shape, axiom_names), |
39452 | 375 |
(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
|
376 |
with_path cleanup export run_on problem_path_name |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
377 |
val (conjecture_shape, axiom_names) = |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
378 |
repair_conjecture_shape_and_axiom_names output conjecture_shape |
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
379 |
axiom_names |
39492 | 380 |
val important_message = |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
381 |
if random () <= important_message_keep_factor then |
39492 | 382 |
extract_important_message output |
383 |
else |
|
384 |
"" |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
385 |
val (message, used_axioms) = |
38023 | 386 |
case outcome of |
387 |
NONE => |
|
388 |
proof_text isar_proof |
|
389 |
(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
|
390 |
(proof_banner auto, full_types, minimize_command, tstplike_proof, |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
391 |
axiom_names, goal, subgoal) |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
392 |
|>> (fn message => |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
393 |
message ^ (if verbose then |
40062 | 394 |
"\nATP real CPU time: " ^ |
395 |
string_of_int (the msecs) ^ " ms." |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
396 |
else |
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
|
397 |
"") ^ |
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
|
398 |
(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
|
399 |
"\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
|
400 |
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
|
401 |
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
|
402 |
"")) |
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset
|
403 |
| SOME failure => (string_for_failure failure, []) |
38023 | 404 |
in |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
405 |
{outcome = outcome, message = message, used_axioms = used_axioms, |
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
406 |
run_time_in_msecs = msecs} |
38023 | 407 |
end |
408 |
||
40181 | 409 |
fun failure_from_smt_failure SMT_Solver.Time_Out = TimedOut |
410 |
| failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable |
|
411 |
| failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
412 |
|
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
413 |
fun run_smt_solver ctxt remote ({timeout, ...} : params) minimize_command |
40065 | 414 |
({state, subgoal, subgoal_count, axioms, ...} |
415 |
: 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
|
416 |
let |
40181 | 417 |
val {outcome, used_facts, run_time_in_msecs} = |
418 |
SMT_Solver.smt_filter remote timeout state |
|
419 |
(map_filter (try dest_Untranslated) axioms) subgoal |
|
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
420 |
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
|
421 |
val message = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
422 |
case outcome of |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
423 |
NONE => |
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset
|
424 |
try_command_line (proof_banner false) |
40065 | 425 |
(apply_on_subgoal subgoal subgoal_count ^ |
40181 | 426 |
command_call smtN (map fst used_facts)) ^ |
427 |
minimize_line minimize_command (map fst used_facts) |
|
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
428 |
| SOME (SMT_Solver.Other_Failure message) => message |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
429 |
| SOME _ => string_for_failure (the outcome') |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
430 |
in |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
431 |
{outcome = outcome', used_axioms = used_facts, |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
432 |
run_time_in_msecs = SOME run_time_in_msecs, message = message} |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
433 |
end |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
434 |
|
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
435 |
fun get_prover ctxt auto name = |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
436 |
let val thy = ProofContext.theory_of ctxt in |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
437 |
if is_smt_prover name then |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
438 |
run_smt_solver ctxt (String.isPrefix remote_prefix name) |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
439 |
else |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
440 |
run_atp auto name (get_atp thy name) |
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
441 |
end |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
442 |
|
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
443 |
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) |
40065 | 444 |
auto minimize_command |
445 |
(problem as {state, goal, subgoal, subgoal_count, axioms, ...}) |
|
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
446 |
name = |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
447 |
let |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
448 |
val thy = Proof.theory_of state |
39318 | 449 |
val ctxt = Proof.context_of state |
37584 | 450 |
val birth_time = Time.now () |
451 |
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
|
452 |
val max_relevant = |
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
453 |
the_default (default_max_relevant_for_prover thy name) max_relevant |
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
454 |
val num_axioms = Int.min (length axioms, max_relevant) |
40065 | 455 |
val desc = |
456 |
prover_description ctxt params name num_axioms subgoal subgoal_count goal |
|
39318 | 457 |
fun go () = |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
458 |
let |
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
459 |
fun really_go () = |
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset
|
460 |
get_prover ctxt auto name params (minimize_command name) problem |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
461 |
|> (fn {outcome, message, ...} => |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
462 |
(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
|
463 |
val (outcome_code, message) = |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
464 |
if debug then |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
465 |
really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
466 |
else |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
467 |
(really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
468 |
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
|
469 |
| 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
|
470 |
ML_Compiler.exn_message exn ^ "\n")) |
39318 | 471 |
val _ = |
472 |
if expect = "" orelse outcome_code = expect then |
|
473 |
() |
|
474 |
else if blocking then |
|
475 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
476 |
else |
|
477 |
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
478 |
in (outcome_code = "some", message) end |
|
479 |
in |
|
480 |
if auto then |
|
481 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
482 |
(success, state |> success ? Proof.goal_message (fn () => |
|
483 |
Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite |
|
39327 | 484 |
(Pretty.str message)])) |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
485 |
end |
39318 | 486 |
else if blocking then |
487 |
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
|
488 |
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
|
489 |
(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
|
490 |
(success, state) |
39318 | 491 |
end |
492 |
else |
|
493 |
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); |
|
494 |
(false, state)) |
|
37584 | 495 |
end |
28582 | 496 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
497 |
fun run_sledgehammer (params as {blocking, provers, full_types, |
40069 | 498 |
relevance_thresholds, max_relevant, ...}) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
499 |
auto i (relevance_override as {only, ...}) minimize_command |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
500 |
state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
501 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
502 |
error "No prover is set." |
39318 | 503 |
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
|
504 |
0 => (Output.urgent_message "No subgoal!"; (false, state)) |
39318 | 505 |
| n => |
506 |
let |
|
39364 | 507 |
val _ = Proof.assert_backward state |
39318 | 508 |
val thy = Proof.theory_of state |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
509 |
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
510 |
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
|
511 |
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
|
512 |
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
|
513 |
val (smts, atps) = provers |> List.partition is_smt_prover |
40114 | 514 |
fun run_provers full_types irrelevant_consts relevance_fudge |
515 |
maybe_translate provers (res as (success, state)) = |
|
40065 | 516 |
if success orelse null provers then |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
517 |
res |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
518 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
519 |
let |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
520 |
val max_max_relevant = |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
521 |
case max_relevant of |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
522 |
SOME n => n |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
523 |
| NONE => |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
524 |
0 |> fold (Integer.max o default_max_relevant_for_prover thy) |
40065 | 525 |
provers |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
526 |
|> auto ? (fn n => n div auto_max_relevant_divisor) |
40065 | 527 |
val axioms = |
528 |
relevant_facts ctxt full_types relevance_thresholds |
|
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
|
529 |
max_max_relevant irrelevant_consts 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
|
530 |
relevance_override chained_ths hyp_ts concl_t |
40114 | 531 |
|> map maybe_translate |
40062 | 532 |
val problem = |
40065 | 533 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
534 |
axioms = axioms, only = only} |
|
535 |
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
|
536 |
in |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
537 |
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
|
538 |
fold (fn prover => fn (true, state) => (true, state) |
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset
|
539 |
| (false, _) => run_prover problem prover) |
40065 | 540 |
provers (false, state) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
541 |
else |
40065 | 542 |
provers |> (if blocking then Par_List.map else map) |
543 |
(run_prover problem) |
|
544 |
|> exists fst |> rpair state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
545 |
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
|
546 |
val run_atps = |
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
|
547 |
run_provers full_types atp_irrelevant_consts atp_relevance_fudge |
40114 | 548 |
(Translated o translate_axiom 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
|
549 |
val run_smts = |
40114 | 550 |
run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated |
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
|
551 |
smts |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
552 |
fun run_atps_and_smt_solvers () = |
40065 | 553 |
[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
|
554 |
in |
40065 | 555 |
(false, state) |
556 |
|> (if blocking then run_atps #> not auto ? run_smts |
|
557 |
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
|
558 |
end |
38044 | 559 |
|
38023 | 560 |
val setup = |
561 |
dest_dir_setup |
|
562 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
563 |
#> measure_run_time_setup |
38023 | 564 |
|
28582 | 565 |
end; |