| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| Mon, 30 May 2011 15:30:05 +0100 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| Mon, 30 May 2011 13:57:59 +0200 |
bulwahn |
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
|
changeset |
files
|
| Mon, 30 May 2011 12:20:04 +0100 |
paulson |
merged multiple heads
|
changeset |
files
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
changeset |
files
|
| Fri, 27 May 2011 21:11:44 +0200 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| Fri, 27 May 2011 16:45:24 +0200 |
boehmes |
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
|
changeset |
files
|
| Fri, 27 May 2011 10:41:09 +0200 |
blanchet |
document new "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:33:16 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
show time taken for reconstruction
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
unbreak "max_potential" logic
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more concise output
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
repaired theory merging and defined/used helpers
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
make Sledgehammer a little bit less verbose in "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try cases gracefully in Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Solve Direct
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
update SML section of documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Nitpick
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case of Sledgehammer better
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "Auto_Tools" "Try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "metis_timeout" to "preplay_timeout" and continued implementation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor fixes to Sledgehammer docs
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
shorten minimizer command further, exploiting until-now-undocumented syntax
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor tweaks to the Nitpick documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
added syntax for specifying Metis timeout (currently used only by SMT solvers)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
readded Waldmeister as default to the documentation and other minor changes
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
reintroduced Waldmeister but limit the number of remote threads created
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor doc adjustments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
mention contributions from LCP and explain metis and metisFT encodings
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fixed trivial fact detection
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
changeset |
files
|