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
|
Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
always measure time for ATPs -- auto minimization relies on it
|
file |
diff |
annotate
|
Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
make "sound" sound and "unsound" more sound, based on evaluation
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:25:10 +0200 |
blanchet |
fixed just introduced silly bug
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:11:42 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
flip logic of boolean option so it's off by default
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 10:25:13 +0200 |
blanchet |
added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:07:01 +0200 |
blanchet |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
file |
diff |
annotate
|