| Fri, 18 Oct 2013 00:05:31 +0200 |
blanchet |
make sure add: doesn't add duplicates, and works for [no_atp] facts
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 23:41:00 +0200 |
blanchet |
no fact subsumption -- this only confuses later code, e.g. 'add:'
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 01:03:59 +0200 |
blanchet |
fast track -- avoid domain error in 0 case
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 15:26:58 +0200 |
blanchet |
drop only real duplicates, not subsumed facts -- this confuses MaSh
|
file |
diff |
annotate
|
| Thu, 10 Oct 2013 01:17:37 +0200 |
blanchet |
simplify fudge factor code
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 15:58:02 +0200 |
blanchet |
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 15:39:34 +0200 |
blanchet |
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 10:47:43 +0200 |
blanchet |
minor performance tuning
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 09:53:18 +0200 |
blanchet |
use plain types instead of dedicated type pattern
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 09:51:24 +0200 |
blanchet |
duplicate term and type patterns
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 22:20:45 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 22:20:45 +0200 |
blanchet |
get rid of another complication in relevance filter
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 22:20:43 +0200 |
blanchet |
renamed config option
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 18:38:23 +0200 |
blanchet |
kick out totally hopeless facts after 5 iterations to speed things up
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 09:51:19 +0200 |
blanchet |
got rid of currently unused data structure, to speed up relevance filter
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 23:55:35 +0200 |
blanchet |
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 16:14:26 +0200 |
blanchet |
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 14:54:25 +0200 |
blanchet |
weight MaSh constants by frequency
|
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
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
tuned indent
|
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
|
| Sat, 19 Jan 2013 17:42:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 20 Dec 2012 15:51:27 +0100 |
blanchet |
better weight functions for MePo/MaSh etc.
|
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
|
| Mon, 12 Nov 2012 14:46:42 +0100 |
blanchet |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:43:51 +0200 |
blanchet |
tune Mesh filter
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML files
|
file |
diff |
annotate
| base
|