| Tue, 26 Jun 2012 11:14:39 +0200 |
added type arguments to "ATerm" constructor -- but don't use them yet
|
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 |
| Tue, 26 Jun 2012 11:14:39 +0200 |
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
|
file | diff | annotate |
| Mon, 28 May 2012 20:25:38 +0200 |
don't generate definitions for LEO-II -- this cuases more harm than good
|
file | diff | annotate |
| Wed, 23 May 2012 21:19:48 +0200 |
tuned names
|
file | diff | annotate |
| Sun, 13 May 2012 16:31:01 +0200 |
extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"
|
file | diff | annotate |
| Wed, 25 Apr 2012 22:00:33 +0200 |
don't use the native choice operator if the type encoding isn't higher-order
|
file | diff | annotate |
| Tue, 27 Mar 2012 16:59:13 +0300 |
tuning (in particular, Symtab instead of AList)
|
file | diff | annotate |
| Tue, 27 Mar 2012 16:59:13 +0300 |
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
|
file | diff | annotate |
| Tue, 27 Mar 2012 16:59:13 +0300 |
avoid DL
|
file | diff | annotate |
| Wed, 21 Mar 2012 16:53:24 +0100 |
generate weights and precedences for predicates as well
|
file | diff | annotate |
| Tue, 20 Mar 2012 18:42:45 +0100 |
removed obsolete temporary hack
|
file | diff | annotate |
| Tue, 20 Mar 2012 18:42:45 +0100 |
tweaks
|
file | diff | annotate |
| Tue, 20 Mar 2012 10:45:52 +0100 |
don't generate new SPASS constructs for old SPASS
|
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 |
internal renamings
|
file | diff | annotate |
| Fri, 24 Feb 2012 11:23:35 +0100 |
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
|
file | diff | annotate |
| Thu, 09 Feb 2012 14:42:18 +0100 |
minor DFG fix
|
file | diff | annotate |
| Thu, 09 Feb 2012 14:04:17 +0100 |
improved KBO weights -- beware of explicit applications
|
file | diff | annotate |
| Thu, 09 Feb 2012 12:57:59 +0100 |
added possibility of generating KBO weights to DFG problems
|
file | diff | annotate |
| Sat, 04 Feb 2012 12:08:18 +0100 |
improved hashing w.r.t. Mirabelle, to help debugging
|
file | diff | annotate |
| Sat, 04 Feb 2012 12:08:18 +0100 |
tuned SPASS DFG output
|
file | diff | annotate |
| Fri, 03 Feb 2012 18:00:55 +0100 |
extended SPASS/DFG output with ranks
|
file | diff | annotate |
| Thu, 02 Feb 2012 01:55:17 +0100 |
tuning
|
file | diff | annotate |
| Wed, 01 Feb 2012 17:16:55 +0100 |
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
|
file | diff | annotate |
| Tue, 31 Jan 2012 15:13:18 +0100 |
avoid name clash, really
|
file | diff | annotate |
| Tue, 31 Jan 2012 15:10:03 +0100 |
fixed syntax bug in DFG output
|
file | diff | annotate |
| Tue, 31 Jan 2012 14:39:21 +0100 |
new SPASS setup
|
file | diff | annotate |
| Tue, 31 Jan 2012 12:43:48 +0100 |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
file | diff | annotate |
| Tue, 31 Jan 2012 10:29:05 +0100 |
nicer keyword class avoidance scheme
|
file | diff | annotate |
| Thu, 26 Jan 2012 20:49:54 +0100 |
better handling of individual type for DFG format (SPASS)
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Tue, 20 Dec 2011 18:59:50 +0100 |
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
|
file | diff | annotate |
| Tue, 20 Dec 2011 18:59:50 +0100 |
one more SPASS identifier
|
file | diff | annotate |
| Tue, 13 Dec 2011 14:55:42 +0100 |
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
added DFG unsorted support (like in the old days)
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
added sorted DFG output for coming version of SPASS
|
file | diff | annotate |
| Wed, 07 Sep 2011 13:50:17 +0200 |
fixed THF type constructor syntax
|
file | diff | annotate |
| Tue, 06 Sep 2011 18:13:36 +0200 |
added dummy polymorphic THF system
|
file | diff | annotate |
| Tue, 06 Sep 2011 09:11:08 +0200 |
tuning
|
file | diff | annotate |
| Fri, 02 Sep 2011 14:43:20 +0200 |
use new syntax for Pi binder in TFF1 output
|
file | diff | annotate |
| Wed, 31 Aug 2011 08:49:10 +0200 |
fixed explicit declaration of TFF1 types
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:46 +0200 |
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
added type abstractions (for declaring polymorphic constants) to TFF syntax
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
implement more of the polymorphic simply typed format TFF(1)
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:34 +0200 |
first step towards polymorphic TFF + changed defaults for Vampire
|
file | diff | annotate |
| Thu, 25 Aug 2011 23:38:09 +0200 |
make polymorphic encodings more complete
|
file | diff | annotate |
| Thu, 25 Aug 2011 22:05:18 +0200 |
make TFF output less explicit where possible
|
file | diff | annotate |
| Thu, 25 Aug 2011 13:55:52 +0100 |
added choice operator output for
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
tuning ATP problem output
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
clearer terminology
|
file | diff | annotate |
| Wed, 17 Aug 2011 10:03:58 +0200 |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
further worked around LEO-II parser limitation, with eta-expansion
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
added option to control which lambda translation to use (for experiments)
|
file | diff | annotate |
| Thu, 14 Jul 2011 15:14:38 +0200 |
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
|
file | diff | annotate |
| Wed, 06 Jul 2011 17:19:34 +0100 |
make SML/NJ happy + tuning
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
improved translation of lambdas in THF
|
file | diff | annotate |