Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
fixed format selection logic for Waldmeister
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 17:49:01 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
minor optimization
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly extensionalize
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
tuned
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
slightly faster/cleaner accumulation of polymorphic consts
|
file |
diff |
annotate
|
Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
|
file |
diff |
annotate
|
Tue, 07 Jun 2011 06:58:52 +0200 |
blanchet |
pass props not thms to ATP translator
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
removed old optimization that isn't one anyone
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
generate less type information in polymorphic case
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
made "explicit_apply"'s smart mode (more) complete
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed type helper indices in new Metis
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
improved ATP clausifier so it can deal with "x => (y <=> z)"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
avoid renumbering hypotheses
|
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 |
fixed detection of Skolem constants in type construction detection code
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't stumble on Skolem names
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
|
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:34 +0200 |
blanchet |
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
|
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
|