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
|
Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
alias for people like me
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 09:17:26 +0100 |
blanchet |
killed legacy alias
|
file |
diff |
annotate
|
Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
Fri, 11 Jan 2013 14:35:28 +0100 |
smolkas |
tuned
|
file |
diff |
annotate
|
Fri, 11 Jan 2013 13:57:51 +0100 |
smolkas |
set show_markup to false in order to avoid problems in jedit
|
file |
diff |
annotate
|
Sat, 05 Jan 2013 22:31:30 +0100 |
blanchet |
nicer output
|
file |
diff |
annotate
|
Sat, 05 Jan 2013 22:31:30 +0100 |
blanchet |
pass option to minimize
|
file |
diff |
annotate
|
Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
|
file |
diff |
annotate
|
Wed, 19 Dec 2012 22:43:07 +0100 |
blanchet |
crank up default timeout for MaSh ATP learning
|
file |
diff |
annotate
|
Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
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, 12 Nov 2012 14:11:51 +0100 |
blanchet |
create temp directory if not already created
|
file |
diff |
annotate
|
Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
merged two commands
|
file |
diff |
annotate
|
Thu, 26 Jul 2012 11:07:27 +0200 |
blanchet |
detect unknown options again
|
file |
diff |
annotate
|
Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
don't relearn old facts in Isar mode
|
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:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
use CVC3 and Yices by default if they are available and there are enough cores
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
minimal maxes + tuning
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
convenience
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learning should honor the fact override and the chained facts
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
more MaSh docs
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn command in MaSh
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
optimize parent computation in MaSh + remove temporary files
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
use async manager to manage MaSh learners to make sure they get killed cleanly
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
added option to control which fact filter is used
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
make tracing an option
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more implementation 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 |
renamed Sledgehammer options
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
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, 23 May 2012 13:28:20 +0200 |
blanchet |
lower the monomorphization thresholds for less scalable provers
|
file |
diff |
annotate
|
Sat, 21 Apr 2012 11:15:49 +0200 |
blanchet |
swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
improve "remote_satallax" by exploiting unsat core
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 18:42:45 +0100 |
blanchet |
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
added "dont_preplay" alias
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
Mon, 06 Feb 2012 23:01:01 +0100 |
blanchet |
renamed type encoding
|
file |
diff |
annotate
|
Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
Thu, 02 Feb 2012 12:42:05 +0100 |
blanchet |
include new SPASS by default if available
|
file |
diff |
annotate
|
Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
lower timeout for preplay, now that we have more preplay methods
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 13:34:14 +0100 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 13:34:13 +0100 |
blanchet |
renamed "slicing" to "slice"
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
Fri, 23 Sep 2011 16:44:51 +0200 |
blanchet |
reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
|
file |
diff |
annotate
|