| 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
|
| Tue, 08 Oct 2013 22:33:05 +0200 |
blanchet |
higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 17:47:50 +0200 |
blanchet |
added experimental configuration options to tune use of builtin symbols in SMT
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:59:07 +0200 |
blanchet |
minor tweak to error message
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
merged "isar_try0" and "isar_minimize" options
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hardcoded obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hard-coded an obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
use configuration mechanism for low-level tracing
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 22:10:57 +0200 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 22:20:45 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 09:51:30 +0200 |
blanchet |
speed up often-called function
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
don't be so verbose about SMT solver failures
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 23:54:59 +0200 |
blanchet |
since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
limit the number of instances of a single theorem
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
use new monomorphizer in Sledgehammer
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 08:42:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 19:13:28 +0200 |
wenzelm |
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 11:34:50 +0200 |
wenzelm |
more explicit sendback propertries based on mode;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 11:34:56 +0200 |
blanchet |
added flag for jEdit/PIDE asynchronous mode
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:30:31 +0200 |
blanchet |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
file |
diff |
annotate
|
| 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
|
| Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:45:06 +0200 |
smolkas |
completely rewrote SH compress; added two parameters for experimentation/fine grained control
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
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
|
| Sun, 26 May 2013 12:56:37 +0200 |
blanchet |
handle lambda-lifted problems in Isar construction code
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 May 2013 14:58:30 +0200 |
blanchet |
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
|
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
|
| Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
added preplay tracing
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 16:36:19 +0100 |
blanchet |
tuned misleading message
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 12:22:26 +0100 |
blanchet |
generate Isar proof if Metis appears to be too slow
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:12:38 +0100 |
blanchet |
don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 14:10:51 +0100 |
blanchet |
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 15:37:42 +0100 |
blanchet |
interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:55 +0100 |
blanchet |
implement (more) accurate computation of parents
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
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
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
also have SMT solvers alternate fact filter
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
use the right filter in each slice
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
store fact filter along with ATP slice
|
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 |
thread through fact triple component from which used facts come, for accurate index output
|
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, 17 Jan 2013 14:01:45 +0100 |
blanchet |
added E-Par support
|
file |
diff |
annotate
|
| Mon, 07 Jan 2013 19:44:40 +0100 |
blanchet |
cleaner context threading
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:42:57 +0100 |
blanchet |
added 112 to list of known Z3 error codes
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:26:10 +0100 |
blanchet |
avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 13:42:14 +0100 |
blanchet |
tuned debugging file names
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 03:47:02 +0100 |
blanchet |
made MaSh evaluation driver work with SMT solvers
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 16:16:48 +0100 |
blanchet |
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:41:15 +0200 |
blanchet |
tuned Isar output
|
file |
diff |
annotate
|