| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 19:24:37 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 22:36:41 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 20:56:44 +0200 |
wenzelm |
tuned: prefer antiquotation for try-catch;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2023 15:23:50 +0200 |
blanchet |
tuned Sledgehammer messages
|
file |
diff |
annotate
|
| Tue, 05 Sep 2023 15:23:48 +0200 |
blanchet |
respect timeout better
|
file |
diff |
annotate
|
| Fri, 10 Mar 2023 11:56:52 +0100 |
blanchet |
don't try to falisfy goals with schematics
|
file |
diff |
annotate
|
| Fri, 03 Mar 2023 11:25:29 +0100 |
blanchet |
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked Sledgehammer interaction
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
adopt terminology suggested by Larry Paulson
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
avoid double 'Warning:' in Sledgehammer messages
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
renamed new Sledgehammer option
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
don't apply abduction and consistency checking to goals of the form 'False'
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| Wed, 23 Nov 2022 11:26:50 +0100 |
blanchet |
correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output
|
file |
diff |
annotate
|
| Thu, 18 Aug 2022 09:29:11 +0200 |
blanchet |
reintroduced SPASS to the mix
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 15:09:53 +0200 |
blanchet |
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s
|
file |
diff |
annotate
|
| Tue, 16 Aug 2022 17:24:58 +0200 |
blanchet |
revived 'try0' and 'smart' Isar proofs in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 11 Jul 2022 15:03:42 +0200 |
blanchet |
milder Sledgehammer messages
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 11:30:28 +0200 |
blanchet |
tuned slices to get the fifth Zipperposition slice in a typical run
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 18:12:38 +0200 |
desharna |
tuned sledehammer to return best succeeding preplay method
|
file |
diff |
annotate
|
| Wed, 30 Mar 2022 10:37:38 +0200 |
desharna |
expanded sledgehammer's expect option with some_preplayed
|
file |
diff |
annotate
|
| Tue, 29 Mar 2022 17:12:15 +0200 |
desharna |
added preplay results to sledgehammer_output
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
further modernized E setup
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
|
file |
diff |
annotate
|
| Mon, 14 Feb 2022 16:41:48 +0100 |
blanchet |
print outcome of Sledgehammer search in panel
|
file |
diff |
annotate
|
| Mon, 14 Feb 2022 16:34:56 +0100 |
blanchet |
print Sledgehammer error message
|
file |
diff |
annotate
|
| Mon, 07 Feb 2022 15:26:22 +0100 |
blanchet |
added possibility of extra options to SMT slices
|
file |
diff |
annotate
|
| Wed, 02 Feb 2022 13:43:48 +0100 |
blanchet |
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 17:11:26 +0100 |
blanchet |
propagate right result when enough proofs have been found
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 14:54:31 +0100 |
blanchet |
don't lose error messages
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 09:21:50 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweaked Auto Sledgehammer's behavior and output
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
print more verbose information
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
run all installed provers by default
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
update slice options centrally
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
further work on new Sledgehammer slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweaked verbose output
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweak padding of prover slice schedule to include all provers
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
implemented 'max_proofs' mechanism
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
document new option 'max_proofs'
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalize slicing format
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
thread slices through
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalized output for forthcoming slicing model
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
disable slicing within SMT (in preparation for factoring it out)
|
file |
diff |
annotate
|
| Sat, 22 Jan 2022 11:33:31 +0100 |
desharna |
added spying of fact filtering timing
|
file |
diff |
annotate
|
| Fri, 21 Jan 2022 16:17:42 +0100 |
desharna |
added syping of fact filtering time to sledgehammer
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 23:11:49 +0100 |
desharna |
tuned run_sledgehammer and called it directly from Mirabelle
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 14:30:13 +0100 |
desharna |
exported Sledgehammer.launch_prover and use it in Mirabelle
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 13:27:42 +0100 |
desharna |
proper filtering inf induction rules in Mirabelle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2021 09:57:22 +0100 |
desharna |
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
|
file |
diff |
annotate
|
| Tue, 13 Jul 2021 10:57:15 +0200 |
blanchet |
revisited ac28714b7478: more faithful preplaying with chained facts
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 17:23:01 +0200 |
desharna |
refactored Sledgehammer option "induction_rules"
|
file |
diff |
annotate
|