| Mon, 29 Jul 2013 15:30:31 +0200 |
blanchet |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:45:06 +0200 |
smolkas |
completely rewrote SH compress; added two parameters for experimentation/fine grained control
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
| Sun, 26 May 2013 12:56:37 +0200 |
blanchet |
handle lambda-lifted problems in Isar construction code
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 May 2013 14:58:30 +0200 |
blanchet |
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
added preplay tracing
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 16:36:19 +0100 |
blanchet |
tuned misleading message
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 12:22:26 +0100 |
blanchet |
generate Isar proof if Metis appears to be too slow
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:12:38 +0100 |
blanchet |
don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 14:10:51 +0100 |
blanchet |
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 15:37:42 +0100 |
blanchet |
interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:55 +0100 |
blanchet |
implement (more) accurate computation of parents
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
also have SMT solvers alternate fact filter
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
use the right filter in each slice
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
store fact filter along with ATP slice
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 14:01:45 +0100 |
blanchet |
added E-Par support
|
file |
diff |
annotate
|
| Mon, 07 Jan 2013 19:44:40 +0100 |
blanchet |
cleaner context threading
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:42:57 +0100 |
blanchet |
added 112 to list of known Z3 error codes
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:26:10 +0100 |
blanchet |
avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 13:42:14 +0100 |
blanchet |
tuned debugging file names
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 03:47:02 +0100 |
blanchet |
made MaSh evaluation driver work with SMT solvers
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 16:16:48 +0100 |
blanchet |
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:41:15 +0200 |
blanchet |
tuned Isar output
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 18:50:53 +0200 |
blanchet |
added proof minimization code from Steffen Smolka
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 15:26:45 +0200 |
blanchet |
fixed then-else confusion
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 15:18:11 +0200 |
blanchet |
improved set of reconstructor methods
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 14:07:53 +0200 |
blanchet |
warn users about unused "using" facts
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 13:20:59 +0200 |
blanchet |
be less aggressive at kicking out chained facts
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 12:54:26 +0200 |
blanchet |
recognize bus errors as crash
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 14:29:18 +0200 |
blanchet |
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 09:51:28 +0200 |
blanchet |
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
make the monomorphizer more predictable by making the cutoff independent on the number of facts
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
use async manager to manage MaSh learners to make sure they get killed cleanly
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
added option to control which fact filter is used
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
renamed experimental option
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 17:50:06 +0200 |
blanchet |
less confusing error message
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
killed most unsound encodings
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Wed, 23 May 2012 13:28:20 +0200 |
blanchet |
lower the monomorphization thresholds for less scalable provers
|
file |
diff |
annotate
|
| Mon, 21 May 2012 10:39:32 +0200 |
blanchet |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
file |
diff |
annotate
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 20:55:09 +0200 |
blanchet |
made "split_last" more robust in the face of obscure low-level errors
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 17:49:08 +0200 |
blanchet |
true delayed evaluation of "SPASS_VERSION" environment variable
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 10:53:28 +0200 |
blanchet |
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 18:42:45 +0100 |
blanchet |
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
continued implementation of term ordering attributes
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
implement term order attribute (for experiments)
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
internal renamings
|
file |
diff |
annotate
|
| Thu, 09 Feb 2012 12:57:59 +0100 |
blanchet |
added possibility of generating KBO weights to DFG problems
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 12:27:10 +0100 |
blanchet |
cleaned up new SPASS parsing
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| Fri, 03 Feb 2012 18:00:55 +0100 |
blanchet |
optimization: slice caching in case two consecutive slices are nearly identical
|
file |
diff |
annotate
|
| Fri, 03 Feb 2012 18:00:55 +0100 |
blanchet |
try to pass fewer options to Metis
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
separate orthogonal components
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
cleanly separate each Metis encoding
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:14 +0100 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:13 +0100 |
blanchet |
renamed "slicing" to "slice"
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 12:42:21 +0100 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
be more silent when auto minimizing
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
better threading of type encodings between Sledgehammer and "metis"
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
quiet down SMT
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
more aggressive lambda hiding (if we anyway need to pass an option to Metis)
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't pass "lam_lifted" option to "metis" unless there's a good reason
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
no needless reconstructors
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed more clutter
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed needless baggage
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:06:14 +0100 |
blanchet |
give each time slice its own lambda translation
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:15:51 +0100 |
blanchet |
rename configuration option to more reasonable length
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
more millisecond cleanup
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
try "smt" as a fallback for ATPs if "metis" fails/times out
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
more detailed preplay output
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 13:57:17 +0100 |
blanchet |
use "Time.time" rather than milliseconds internally
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 13:46:26 +0100 |
blanchet |
tune: no need for option
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
check "sound" flag before doing something unsound...
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 11:24:58 +0200 |
blanchet |
simplified unsound proof detection by removing impossible case
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
continue with minimization in debug mode in spite of unsoundness
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
fewer TPTP important messages
|
file |
diff |
annotate
|