author | blanchet |
Fri, 18 Feb 2011 15:17:39 +0100 | |
changeset 41770 | a710e96583d5 |
parent 41769 | eb2e39555f98 |
child 42332 | 474790ed7b0c |
permissions | -rw-r--r-- |
38047 | 1 |
(* Title: HOL/Tools/ATP/atp_systems.ML |
28592 | 2 |
Author: Fabian Immler, TU Muenchen |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
28592 | 4 |
|
36376 | 5 |
Setup for supported ATPs. |
28592 | 6 |
*) |
7 |
||
36376 | 8 |
signature ATP_SYSTEMS = |
28592 | 9 |
sig |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
10 |
type failure = ATP_Proof.failure |
38023 | 11 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
12 |
type atp_config = |
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:
38090
diff
changeset
|
13 |
{exec: string * string, |
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:
38090
diff
changeset
|
14 |
required_execs: (string * string) list, |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
15 |
arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, |
38645 | 16 |
has_incomplete_mode: bool, |
38023 | 17 |
proof_delims: (string * string) list, |
18 |
known_failures: (failure * string) list, |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
19 |
default_max_relevant: int, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
20 |
explicit_forall: bool, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
21 |
use_conjecture_for_hypotheses: bool} |
38023 | 22 |
|
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
23 |
datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
24 |
|
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
25 |
(* for experimentation purposes -- do not use in production code *) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
26 |
val e_weight_method : e_weight_method Unsynchronized.ref |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
27 |
val e_default_fun_weight : real Unsynchronized.ref |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
28 |
val e_fun_weight_base : real Unsynchronized.ref |
41770 | 29 |
val e_fun_weight_span : real Unsynchronized.ref |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
30 |
val e_default_sym_offs_weight : real Unsynchronized.ref |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
31 |
val e_sym_offs_weight_base : real Unsynchronized.ref |
41770 | 32 |
val e_sym_offs_weight_span : real Unsynchronized.ref |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
33 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
34 |
val eN : string |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
35 |
val spassN : string |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
36 |
val vampireN : string |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
37 |
val sine_eN : string |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
38 |
val snarkN : string |
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
39 |
val z3_atpN : string |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
40 |
val remote_prefix : string |
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
41 |
val remote_atp : |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
42 |
string -> string -> string list -> (string * string) list |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
43 |
-> (failure * string) list -> int -> bool -> string * atp_config |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
44 |
val add_atp : string * atp_config -> theory -> theory |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
45 |
val get_atp : theory -> string -> atp_config |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
46 |
val supported_atps : theory -> string list |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
47 |
val is_atp_installed : theory -> string -> bool |
35867 | 48 |
val refresh_systems_on_tptp : unit -> unit |
49 |
val setup : theory -> theory |
|
28592 | 50 |
end; |
51 |
||
36376 | 52 |
structure ATP_Systems : ATP_SYSTEMS = |
28592 | 53 |
struct |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
54 |
|
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
55 |
open ATP_Proof |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
56 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
57 |
(* ATP configuration *) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
58 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
59 |
type atp_config = |
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:
38090
diff
changeset
|
60 |
{exec: string * string, |
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:
38090
diff
changeset
|
61 |
required_execs: (string * string) list, |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
62 |
arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, |
38645 | 63 |
has_incomplete_mode: bool, |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
64 |
proof_delims: (string * string) list, |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
65 |
known_failures: (failure * string) list, |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
66 |
default_max_relevant: int, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
67 |
explicit_forall: bool, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
68 |
use_conjecture_for_hypotheses: bool} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
69 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
70 |
val known_perl_failures = |
38094 | 71 |
[(CantConnect, "HTTP error"), |
72 |
(NoPerl, "env: perl"), |
|
38065 | 73 |
(NoLibwwwPerl, "Can't locate HTTP")] |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
74 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
75 |
(* named ATPs *) |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
76 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
77 |
val eN = "e" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
78 |
val spassN = "spass" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
79 |
val vampireN = "vampire" |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
80 |
val z3_atpN = "z3_atp" |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
81 |
val sine_eN = "sine_e" |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
82 |
val snarkN = "snark" |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
83 |
val remote_prefix = "remote_" |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
84 |
|
38023 | 85 |
structure Data = Theory_Data |
86 |
( |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
87 |
type T = (atp_config * stamp) Symtab.table |
38023 | 88 |
val empty = Symtab.empty |
89 |
val extend = I |
|
90 |
fun merge data : T = Symtab.merge (eq_snd op =) data |
|
91 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
|
92 |
) |
|
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
93 |
|
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
94 |
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000 |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset
|
95 |
|
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
96 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
97 |
(* E *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
98 |
|
40344
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset
|
99 |
(* Give E an extra second to reconstruct the proof. Older versions even get two |
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset
|
100 |
seconds, because the "eproof" script wrongly subtracted an entire second to |
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset
|
101 |
account for the overhead of the script itself, which is in fact much |
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset
|
102 |
lower. *) |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
103 |
fun e_bonus () = |
41334
3cb52cbf0eed
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
blanchet
parents:
41317
diff
changeset
|
104 |
if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
105 |
|
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
106 |
val tstp_proof_delims = |
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
107 |
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
108 |
|
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
109 |
datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
110 |
|
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
111 |
val e_weight_method = Unsynchronized.ref E_Fun_Weight |
41770 | 112 |
(* FUDGE *) |
113 |
val e_default_fun_weight = Unsynchronized.ref 20.0 |
|
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
114 |
val e_fun_weight_base = Unsynchronized.ref 0.0 |
41770 | 115 |
val e_fun_weight_span = Unsynchronized.ref 40.0 |
116 |
val e_default_sym_offs_weight = Unsynchronized.ref 1.0 |
|
117 |
val e_sym_offs_weight_base = Unsynchronized.ref ~20.0 |
|
118 |
val e_sym_offs_weight_span = Unsynchronized.ref 60.0 |
|
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
119 |
|
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
120 |
fun e_weight_method_case fw sow = |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
121 |
case !e_weight_method of |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
122 |
E_Auto => raise Fail "Unexpected \"E_Auto\"" |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
123 |
| E_Fun_Weight => fw |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
124 |
| E_Sym_Offset_Weight => sow |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
125 |
|
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
126 |
fun scaled_e_weight w = |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
127 |
e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base) |
41770 | 128 |
+ w * e_weight_method_case (!e_fun_weight_span) (!e_sym_offs_weight_span) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
129 |
|> Real.ceil |> signed_string_of_int |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
130 |
|
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41334
diff
changeset
|
131 |
fun e_weight_arguments weights = |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
132 |
if !e_weight_method = E_Auto orelse |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
133 |
string_ord (getenv "E_VERSION", "1.2w") = LESS then |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
134 |
"-xAutoDev" |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
135 |
else |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
136 |
"--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
137 |
\--destructive-er-aggressive --destructive-er --presat-simplify \ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
138 |
\--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
139 |
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
140 |
\-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^ |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
141 |
"(SimulateSOS, " ^ |
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41766
diff
changeset
|
142 |
(e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight) |
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41766
diff
changeset
|
143 |
|> Real.ceil |> signed_string_of_int) ^ |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
144 |
",20,1.5,1.5,1" ^ |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
145 |
(weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w) |
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
146 |
|> implode) ^ |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
147 |
"),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
148 |
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
149 |
\FIFOWeight(PreferProcessed))'" |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
150 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
151 |
val e_config : atp_config = |
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:
38090
diff
changeset
|
152 |
{exec = ("E_HOME", "eproof"), |
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:
38090
diff
changeset
|
153 |
required_execs = [], |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
154 |
arguments = fn _ => fn timeout => fn weights => |
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41334
diff
changeset
|
155 |
"--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \ |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
156 |
\--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
38645 | 157 |
has_incomplete_mode = false, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
158 |
proof_delims = [tstp_proof_delims], |
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset
|
159 |
known_failures = |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
160 |
[(Unprovable, "SZS status: CounterSatisfiable"), |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
161 |
(Unprovable, "SZS status CounterSatisfiable"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
162 |
(TimedOut, "Failure: Resource limit exceeded (time)"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
163 |
(TimedOut, "time limit exceeded"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
164 |
(OutOfResources, |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
165 |
"# Cannot determine problem status within resource limit"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
166 |
(OutOfResources, "SZS status: ResourceOut"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
167 |
(OutOfResources, "SZS status ResourceOut")], |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
168 |
default_max_relevant = 250 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
169 |
explicit_forall = false, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
170 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
171 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
172 |
val e = (eN, e_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
173 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
174 |
|
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
175 |
(* SPASS *) |
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
176 |
|
36219
16670b4f0baa
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset
|
177 |
(* The "-VarWeight=3" option helps the higher-order problems, probably by |
16670b4f0baa
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset
|
178 |
counteracting the presence of "hAPP". *) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
179 |
val spass_config : atp_config = |
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:
38090
diff
changeset
|
180 |
{exec = ("ISABELLE_ATP", "scripts/spass"), |
39002 | 181 |
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
182 |
arguments = fn complete => fn timeout => fn _ => |
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37926
diff
changeset
|
183 |
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
184 |
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
185 |
|> not complete ? prefix "-SOS=1 ", |
38645 | 186 |
has_incomplete_mode = true, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
187 |
proof_delims = [("Here is a proof", "Formulae used in the proof")], |
36289
f75b6a3e1450
set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
blanchet
parents:
36287
diff
changeset
|
188 |
known_failures = |
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
189 |
known_perl_failures @ |
37413 | 190 |
[(IncompleteUnprovable, "SPASS beiseite: Completion found"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
191 |
(TimedOut, "SPASS beiseite: Ran out of time"), |
36965 | 192 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
37413 | 193 |
(MalformedInput, "Undefined symbol"), |
37414
d0cea0796295
expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents:
37413
diff
changeset
|
194 |
(MalformedInput, "Free Variable"), |
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset
|
195 |
(SpassTooOld, "tptp2dfg"), |
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset
|
196 |
(InternalError, "Please report this error")], |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
197 |
default_max_relevant = 150 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
198 |
explicit_forall = true, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
199 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
200 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
201 |
val spass = (spassN, spass_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
202 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
203 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
204 |
(* Vampire *) |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
205 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
206 |
val vampire_config : atp_config = |
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:
38090
diff
changeset
|
207 |
{exec = ("VAMPIRE_HOME", "vampire"), |
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:
38090
diff
changeset
|
208 |
required_execs = [], |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
209 |
arguments = fn complete => fn timeout => fn _ => |
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents:
41148
diff
changeset
|
210 |
(* This would work too but it's less tested: "--proof tptp " ^ *) |
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents:
41148
diff
changeset
|
211 |
"--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ |
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents:
41148
diff
changeset
|
212 |
" --thanks \"Andrei and Krystof\" --input_file" |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
213 |
|> not complete ? prefix "--sos on ", |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
214 |
has_incomplete_mode = true, |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
215 |
proof_delims = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
216 |
[("=========== Refutation ==========", |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
217 |
"======= End of refutation ======="), |
38033 | 218 |
("% SZS output start Refutation", "% SZS output end Refutation"), |
219 |
("% SZS output start Proof", "% SZS output end Proof")], |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
220 |
known_failures = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
221 |
[(Unprovable, "UNPROVABLE"), |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
222 |
(IncompleteUnprovable, "CANNOT PROVE"), |
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:
38090
diff
changeset
|
223 |
(TimedOut, "SZS status Timeout"), |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
224 |
(Unprovable, "Satisfiability detected"), |
38647
5500241da479
play with fudge factor + parse one more Vampire error
blanchet
parents:
38646
diff
changeset
|
225 |
(Unprovable, "Termination reason: Satisfiable"), |
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset
|
226 |
(VampireTooOld, "not a valid option"), |
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset
|
227 |
(Interrupted, "Aborted by signal SIGINT")], |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
228 |
default_max_relevant = 450 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
229 |
explicit_forall = false, |
38680 | 230 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
231 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
232 |
val vampire = (vampireN, vampire_config) |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
233 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
234 |
|
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
235 |
(* Z3 with TPTP syntax *) |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
236 |
|
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
237 |
val z3_atp_config : atp_config = |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
238 |
{exec = ("Z3_HOME", "z3"), |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
239 |
required_execs = [], |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
240 |
arguments = fn _ => fn timeout => fn _ => |
41766
26dab6eca1c2
make experimental "Z3 ATP" work on Linux as well
blanchet
parents:
41765
diff
changeset
|
241 |
"MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout), |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
242 |
has_incomplete_mode = false, |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
243 |
proof_delims = [], |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
244 |
known_failures = |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
245 |
[(Unprovable, "\nsat"), |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
246 |
(IncompleteUnprovable, "\nunknown"), |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
247 |
(ProofMissing, "\nunsat")], |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
248 |
default_max_relevant = 225 (* FUDGE *), |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
249 |
explicit_forall = true, |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
250 |
use_conjecture_for_hypotheses = false} |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
251 |
|
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
252 |
val z3_atp = (z3_atpN, z3_atp_config) |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
253 |
|
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
254 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
255 |
(* Remote ATP invocation via SystemOnTPTP *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
256 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
257 |
val systems = Synchronized.var "atp_systems" ([] : string list) |
31835 | 258 |
|
259 |
fun get_systems () = |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
260 |
case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
261 |
(output, 0) => split_lines output |
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
262 |
| (output, _) => |
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
263 |
error (case extract_known_failure known_perl_failures output of |
41744 | 264 |
SOME failure => string_for_failure failure |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
265 |
| NONE => perhaps (try (unsuffix "\n")) output ^ ".") |
31835 | 266 |
|
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
267 |
fun find_system name [] systems = find_first (String.isPrefix name) systems |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
268 |
| find_system name (version :: versions) systems = |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
269 |
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
270 |
NONE => find_system name versions systems |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
271 |
| res => res |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
272 |
|
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
273 |
fun get_system name versions = |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
274 |
Synchronized.change_result systems |
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
275 |
(fn systems => (if null systems then get_systems () else systems) |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
276 |
|> `(find_system name versions)) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
277 |
|
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
278 |
fun the_system name versions = |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
279 |
case get_system name versions of |
39010 | 280 |
SOME sys => sys |
41269 | 281 |
| NONE => error ("System " ^ quote name ^ |
282 |
" is not available at SystemOnTPTP.") |
|
31835 | 283 |
|
41148 | 284 |
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) |
285 |
||
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
286 |
fun remote_config system_name system_versions proof_delims known_failures |
38997 | 287 |
default_max_relevant use_conjecture_for_hypotheses |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
288 |
: atp_config = |
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:
38090
diff
changeset
|
289 |
{exec = ("ISABELLE_ATP", "scripts/remote_atp"), |
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:
38090
diff
changeset
|
290 |
required_execs = [], |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
291 |
arguments = fn _ => fn timeout => fn _ => |
41148 | 292 |
" -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) |
293 |
^ " -s " ^ the_system system_name system_versions, |
|
38645 | 294 |
has_incomplete_mode = false, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
295 |
proof_delims = insert (op =) tstp_proof_delims proof_delims, |
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
296 |
known_failures = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
297 |
known_failures @ known_perl_failures @ |
38094 | 298 |
[(TimedOut, "says Timeout")], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
299 |
default_max_relevant = default_max_relevant, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
300 |
explicit_forall = true, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
301 |
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
302 |
|
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
303 |
fun remotify_config system_name system_versions |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
304 |
({proof_delims, known_failures, default_max_relevant, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
305 |
use_conjecture_for_hypotheses, ...} : atp_config) : atp_config = |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
306 |
remote_config system_name system_versions proof_delims known_failures |
38997 | 307 |
default_max_relevant use_conjecture_for_hypotheses |
38023 | 308 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
309 |
fun remote_atp name system_name system_versions proof_delims known_failures |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
310 |
default_max_relevant use_conjecture_for_hypotheses = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
311 |
(remote_prefix ^ name, |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
312 |
remote_config system_name system_versions proof_delims known_failures |
38997 | 313 |
default_max_relevant use_conjecture_for_hypotheses) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
314 |
fun remotify_atp (name, config) system_name system_versions = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
315 |
(remote_prefix ^ name, remotify_config system_name system_versions config) |
28592 | 316 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
317 |
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
318 |
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] |
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
319 |
val remote_z3_atp = |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
320 |
remote_atp z3_atpN "Z3---" ["2.18"] [] |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
321 |
[(IncompleteUnprovable, "SZS status Satisfiable"), |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
322 |
(ProofMissing, "SZS status Unsatisfiable")] |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
323 |
225 (* FUDGE *) false |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
324 |
val remote_sine_e = |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
325 |
remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] |
41765
d323edd12b50
adjusted fudge factors (based on Judgment Day runs)
blanchet
parents:
41744
diff
changeset
|
326 |
500 (* FUDGE *) true |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
327 |
val remote_snark = |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
328 |
remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] [] |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
329 |
250 (* FUDGE *) true |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
330 |
|
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
331 |
(* Setup *) |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
332 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
333 |
fun add_atp (name, config) thy = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
334 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
335 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
336 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
337 |
fun get_atp thy name = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
338 |
the (Symtab.lookup (Data.get thy) name) |> fst |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
339 |
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
340 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
341 |
val supported_atps = Symtab.keys o Data.get |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
342 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
343 |
fun is_atp_installed thy name = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
344 |
let val {exec, required_execs, ...} = get_atp thy name in |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
345 |
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
346 |
end |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
347 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
348 |
fun refresh_systems_on_tptp () = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
349 |
Synchronized.change systems (fn _ => get_systems ()) |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
350 |
|
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
351 |
val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
352 |
remote_sine_e, remote_snark] |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
353 |
val setup = fold add_atp atps |
35867 | 354 |
|
28592 | 355 |
end; |