| Thu, 17 Jan 2013 13:11:44 +0100 |
blanchet |
tweaked defaults
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 12:46:11 +0100 |
blanchet |
honor fact range for MePo as well
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:48:01 +0100 |
blanchet |
removed debugging code
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:19 +0100 |
blanchet |
export MeSh data as well
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:34:32 +0100 |
blanchet |
MaSh exporter can now export subsets of the facts, as consecutive ranges
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 22:49:06 +0100 |
blanchet |
parallelized MaSh exporter
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:59:03 +0100 |
blanchet |
tuning
|
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
|
| 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 16:49:48 +0100 |
blanchet |
export ATP and Isar commands separately
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:12:30 +0100 |
blanchet |
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:12:29 +0100 |
blanchet |
generalized MaSh exporter to sets of theories
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 23:43:52 +0100 |
blanchet |
tweaked MaSh exporter
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
don't export technical theorems for MaSh
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
generate fact name in queries again + use ATP dependencies when possible
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed "iter" fact filter to "MePo" (Meng--Paulson)
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
repair MaSh exporter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more work on MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
started implementing MaSh client-side I/O
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
gracefully handle the case of empty theories when going up the accessibility chain
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
dependency tuning
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
add Isabelle dependencies to tweak relevance filter
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
generate ATP dependencies
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate Meng--Paulson facts for evaluation purposes
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
MaSh evaluation driver
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
moved MaSh into own files
|
file |
diff |
annotate
|