| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:41:19 +0200 |
blanchet |
made "completish" mode a bit more complete
|
file |
diff |
annotate
|
| Fri, 17 May 2013 11:35:52 +0200 |
wenzelm |
tuned signature -- emphasize thread creation here;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:37:07 +0100 |
blanchet |
reintroduced crucial sorting accidentally lost in 962190eab40d
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:27:33 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:21:49 +0100 |
blanchet |
provide two modes for MaSh driver: linearized or real visibility
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:55 +0100 |
blanchet |
implement (more) accurate computation of parents
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 11:33:43 +0100 |
blanchet |
tuned code: factored out parent computation
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 10:43:36 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
avoid crude/wrong theorem comparision
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
more MaSh tracing
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 08 Feb 2013 12:22:37 +0100 |
blanchet |
added option to use SNoW as machine learning algo
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
killed deadcode
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
drop needless .0s
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
file |
diff |
annotate
|
| Tue, 05 Feb 2013 17:19:13 +0100 |
blanchet |
removed spurious trimming
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 12:09:07 +0100 |
blanchet |
adapted to new MaSh interface
|
file |
diff |
annotate
|
| Sat, 19 Jan 2013 17:42:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 16:06:45 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 00:18:11 +0100 |
blanchet |
optimization -- evaluate conversion to table only once
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 23:29:22 +0100 |
blanchet |
use correct weights in MeSh driver
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 18:43:59 +0100 |
blanchet |
evaluate more cases (cf. paper)
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 17:55:03 +0100 |
blanchet |
updated MaSh
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 09:59:50 +0100 |
blanchet |
adjust weights -- sorts are prolific, so tone them down even more
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 22:17:00 +0100 |
blanchet |
don't learn theories -- this option is very slow and not very helpful
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 20:57:48 +0100 |
blanchet |
honor unknown chained in MaSh and a few other tweaks
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 15:04:55 +0100 |
blanchet |
remove obsolete MaSh files
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 12:15:44 +0100 |
blanchet |
cleaned up hint handling
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 12:15:43 +0100 |
blanchet |
better handlig of built-ins -- at the top-level, not in subterms
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 16:49:40 +0100 |
blanchet |
honor filtering out of arguments for built-in constants (e.g. representation of numerals)
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 16:49:39 +0100 |
blanchet |
new version of MaSh Python component
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
don't learn from the proof of "psimps" etc.
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
updated MaSh Python component
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
start using MaSh hints
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
always compare theorem using the same, weaker function
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:19 +0100 |
blanchet |
export MeSh data as well
|
file |
diff |
annotate
|
| Sun, 06 Jan 2013 17:38:29 +0100 |
blanchet |
get rid of spurious "Isar" proofs
|
file |
diff |
annotate
|
| Sun, 06 Jan 2013 17:38:29 +0100 |
blanchet |
also generate queries for goals with too many Isar dependencies
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 22:31:33 +0100 |
blanchet |
tuned message
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 22:31:32 +0100 |
blanchet |
tap after, not before command invocation
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:20 +0100 |
blanchet |
refined class handling, to prevent cycles in fact graph
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:19 +0100 |
blanchet |
tweaked nicknames
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
speed up generation of local theorem nicknames
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
tweaked fudge factor
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 10:41:53 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 28 Dec 2012 23:31:51 +0100 |
blanchet |
tuned ML function name
|
file |
diff |
annotate
|
| Fri, 28 Dec 2012 21:03:39 +0100 |
blanchet |
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
|
file |
diff |
annotate
|
| Fri, 28 Dec 2012 14:13:39 +0100 |
blanchet |
tuned ML function names
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 16:49:12 +0100 |
blanchet |
improved thm order hack, in case the default names are overridden
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 15:46:27 +0100 |
blanchet |
enable theory learning in MaSh
|
file |
diff |
annotate
|
| Fri, 21 Dec 2012 14:35:29 +0100 |
blanchet |
name tuning
|
file |
diff |
annotate
|
| Thu, 20 Dec 2012 15:51:27 +0100 |
blanchet |
better weight functions for MePo/MaSh etc.
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:09:48 +0100 |
blanchet |
updated MaSh serialization number (to reflect new weights)
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
contain exponential explosion of term patterns
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
tuned weights -- keep same relative values, but use 1.0 as the least weight
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
really honor pattern depth, and use 2 by default
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 19:23:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 02:47:45 +0100 |
blanchet |
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 00:24:06 +0100 |
blanchet |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:51 +0100 |
blanchet |
don't have MaSh pretend it knows facts it doesn't know
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
fixed embarrassing off-by-one bug in MaSh's Mesh
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
tweak MaSh fudge factors
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 17:48:04 +0100 |
blanchet |
use proper entry point for MaSh in test driver
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 15:54:17 +0100 |
blanchet |
parse more liberal MaSh suggestion syntax (for the eval driver)
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
tweaked MaSh proximity
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
reduce max number of dependencies for MaSh to get rid of junk
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
more feature tweaks
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
prioritize chained facts
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
more MaSh feature tweaking
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
record free variables as a MaSh feature
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
expand type classes into their ancestors for MaSh
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
tweaked MaSh features, based on comments by Josef Urban
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
increase weight of local facts again (MaSh)
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
simplify code now that "mash.py" supports weights
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 13:25:06 +0100 |
blanchet |
take proximity into account for MaSh + fix a debilitating bug in feature generation
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 13:25:06 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 10:35:58 +0100 |
blanchet |
tweaked order of theorems to avoid forward dependencies (MaSh)
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:43:24 +0100 |
blanchet |
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:19:03 +0100 |
blanchet |
added feature weights in MaSh
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:19:02 +0100 |
blanchet |
promote local facts using a hack (for MaSh)
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 19:10:14 +0100 |
blanchet |
turned off noisy MaSh features
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 10:02:51 +0100 |
blanchet |
simplify MaSh term patterns + add missing global facts if there aren't too many
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 00:37:11 +0100 |
blanchet |
MaSh improvements: deeper patterns + more respect for chained facts
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 23:43:53 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 20:55:34 +0100 |
blanchet |
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 13:24:55 +0100 |
blanchet |
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
|
file |
diff |
annotate
|
| Sat, 01 Dec 2012 23:55:39 +0100 |
blanchet |
tuned order of functions
|
file |
diff |
annotate
|
| Sat, 01 Dec 2012 23:55:38 +0100 |
blanchet |
proper quoting of paths in MaSh
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 15:31:03 +0100 |
blanchet |
simplify code slightly
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 12:04:32 +0100 |
blanchet |
moved MaSh's Python code into Isabelle
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 11:32:22 +0100 |
blanchet |
thread context correctly when printing backquoted facts
|
file |
diff |
annotate
|
| Thu, 01 Nov 2012 15:00:48 +0100 |
blanchet |
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
|
file |
diff |
annotate
|
| Mon, 06 Aug 2012 22:12:17 +0200 |
blanchet |
optimized saving
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
remember ATP flops to avoid repeating them too quickly
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
remember which MaSh proofs were found using ATPs
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
rule out same "technical" theories for MePo as for MaSh
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
crank up max number of dependencies
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 09:51:28 +0200 |
blanchet |
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
don't export technical theorems for MaSh
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
cap the number of facts returned by MaSh
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
remove MaSh junk associated with size functions
|
file |
diff |
annotate
|