| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't translate new Skolemizer assumptions in new Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
conceal old Skolems in new Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
properly locate helpers whose constants have several entries in the helper table
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
skip "hBOOL" in new Metis path finder
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't pass "~ " to new Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
clean up unnecessary machinery -- helpers work also with monomorphic type encodings
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added support for helpers in new Metis, so far only for polymorphic type encodings
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
implemented missing hAPP and ti cases of new path finder
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
support lightweight tags in new Metis
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
distinguish different kinds of typing informations in the fact name
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
monomorphize in the new Metis if the type system calls for it
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed new path finder for type information tag
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use ":" for type information (looks good in Metis's output) and handle it in new path finder
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
parse optional type system specification
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
proper handling of type variable classes in new Metis
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
don't preprocess twice
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new Metis
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
removed obscure option
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added new metis mode, with no implementation yet
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|