| Wed, 18 Jul 2012 08:44:04 +0200 |
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 |
learn from minimized ATP proofs
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
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 |
added option to control which fact filter is used
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
renamed Sledgehammer options
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file | diff | annotate |
| Wed, 11 Jul 2012 21:43:19 +0200 |
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 |
renamed experimental option
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
started adding polymophic SPASS output
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
tuning
|
file | diff | annotate |
| Mon, 18 Jun 2012 17:50:06 +0200 |
less confusing error message
|
file | diff | annotate |
| Wed, 06 Jun 2012 10:35:05 +0200 |
killed most unsound encodings
|
file | diff | annotate |
| Wed, 23 May 2012 21:19:48 +0200 |
tuned names
|
file | diff | annotate |
| Wed, 23 May 2012 13:28:20 +0200 |
lower the monomorphization thresholds for less scalable provers
|
file | diff | annotate |
| Mon, 21 May 2012 10:39:32 +0200 |
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 |
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 |
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 |
made "split_last" more robust in the face of obscure low-level errors
|
file | diff | annotate |
| Thu, 19 Apr 2012 17:49:08 +0200 |
true delayed evaluation of "SPASS_VERSION" environment variable
|
file | diff | annotate |
| Wed, 18 Apr 2012 10:53:28 +0200 |
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 |
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 |
continued implementation of term ordering attributes
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
implement term order attribute (for experiments)
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
internal renamings
|
file | diff | annotate |
| Thu, 09 Feb 2012 12:57:59 +0100 |
added possibility of generating KBO weights to DFG problems
|
file | diff | annotate |
| Sun, 05 Feb 2012 12:27:10 +0100 |
cleaned up new SPASS parsing
|
file | diff | annotate |
| Sat, 04 Feb 2012 12:08:18 +0100 |
made option available to users (mostly for experiments)
|
file | diff | annotate |
| Fri, 03 Feb 2012 18:00:55 +0100 |
optimization: slice caching in case two consecutive slices are nearly identical
|
file | diff | annotate |
| Fri, 03 Feb 2012 18:00:55 +0100 |
try to pass fewer options to Metis
|
file | diff | annotate |
| Mon, 30 Jan 2012 17:15:59 +0100 |
rename lambda translation schemes
|
file | diff | annotate |
| Thu, 26 Jan 2012 20:49:54 +0100 |
separate orthogonal components
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Thu, 19 Jan 2012 21:37:12 +0100 |
renamed "sound" option to "strict"
|
file | diff | annotate |
| Thu, 19 Jan 2012 21:37:12 +0100 |
cleanly separate each Metis encoding
|
file | diff | annotate |
| Wed, 07 Dec 2011 16:03:05 +0100 |
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 |
added "minimize" option for more control over automatic minimization
|
file | diff | annotate |
| Thu, 01 Dec 2011 13:34:13 +0100 |
renamed "slicing" to "slice"
|
file | diff | annotate |
| Sat, 19 Nov 2011 12:42:21 +0100 |
made SML/NJ happy
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
be more silent when auto minimizing
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
better threading of type encodings between Sledgehammer and "metis"
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
quiet down SMT
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
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 |
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 |
no needless reconstructors
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
removed more clutter
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
removed needless baggage
|
file | diff | annotate |
| Wed, 16 Nov 2011 17:06:14 +0100 |
give each time slice its own lambda translation
|
file | diff | annotate |
| Wed, 16 Nov 2011 16:35:19 +0100 |
thread in additional options to minimizer
|
file | diff | annotate |
| Wed, 16 Nov 2011 13:22:36 +0100 |
make metis reconstruction handling more flexible
|
file | diff | annotate |
| Wed, 16 Nov 2011 09:42:27 +0100 |
parse lambda translation option in Metis
|
file | diff | annotate |
| Tue, 15 Nov 2011 22:15:51 +0100 |
rename configuration option to more reasonable length
|
file | diff | annotate |
| Tue, 15 Nov 2011 22:13:39 +0100 |
started implementing lambda-lifting in Metis
|
file | diff | annotate |
| Sun, 06 Nov 2011 22:18:54 +0100 |
more millisecond cleanup
|
file | diff | annotate |
| Sun, 06 Nov 2011 22:18:54 +0100 |
try "smt" as a fallback for ATPs if "metis" fails/times out
|
file | diff | annotate |
| Sun, 06 Nov 2011 22:18:54 +0100 |
more detailed preplay output
|
file | diff | annotate |
| Sun, 06 Nov 2011 22:18:54 +0100 |
tuning
|
file | diff | annotate |
| Sun, 06 Nov 2011 13:57:17 +0100 |
use "Time.time" rather than milliseconds internally
|
file | diff | annotate |
| Sun, 06 Nov 2011 13:46:26 +0100 |
tune: no need for option
|
file | diff | annotate |