| Thu, 26 Aug 2010 09:23:21 +0200 |
blanchet |
add a bonus for chained facts, since they are likely to be relevant;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 01:03:08 +0200 |
blanchet |
add a penalty for lambda-abstractions;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 00:49:04 +0200 |
blanchet |
fiddle with relevance filter
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 19:41:18 +0200 |
blanchet |
reorganize options regarding to the relevance threshold and decay
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 17:49:52 +0200 |
blanchet |
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:42:28 +0200 |
blanchet |
simplify more code
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:34:28 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:32:43 +0200 |
blanchet |
get rid of "defs_relevant" feature;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:02:07 +0200 |
blanchet |
renamed "relevance_convergence" to "relevance_decay"
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 22:57:22 +0200 |
blanchet |
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 19:19:28 +0200 |
blanchet |
compute names lazily;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 18:03:43 +0200 |
blanchet |
clean handling of whether a fact is chained or not;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 16:43:52 +0200 |
blanchet |
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 16:24:11 +0200 |
blanchet |
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 15:07:54 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:32:11 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:24:24 +0200 |
blanchet |
optimize fact filter some more
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:00:57 +0200 |
blanchet |
cache previous iteration's weights, and keep track of what's dirty and what's clean;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 21:55:52 +0200 |
blanchet |
modified relevance filter
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:53:11 +0200 |
blanchet |
invert semantics of "relevance_convergence", to make it more intuitive
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:39:12 +0200 |
blanchet |
if no facts were selected on first iteration, try again with a lower threshold
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:25:49 +0200 |
blanchet |
weed out junk in relevance filter
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:04:31 +0200 |
blanchet |
no need for "eq" facts -- good old "=" is good enough for us
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 17:49:18 +0200 |
blanchet |
destroy elim rules before checking for finite exhaustive facts
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 14:54:17 +0200 |
blanchet |
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 16:56:05 +0200 |
blanchet |
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 08:26:09 +0200 |
blanchet |
more work on finite axiom detection
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:52:26 +0200 |
blanchet |
make sure minimizer facts go through "transform_elim_theorems"
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 16:44:48 +0200 |
blanchet |
unbreak "only" option of Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 16:22:51 +0200 |
blanchet |
improve "x = A | x = B | x = C"-style axiom detection
|
file |
diff |
annotate
|