| Mon, 08 Nov 2010 13:53:18 +0100 |
blanchet |
compile -- 7550b2cba1cb broke the build
|
changeset |
files
|
| Mon, 08 Nov 2010 13:25:00 +0100 |
blanchet |
merge
|
changeset |
files
|
| Mon, 08 Nov 2010 09:10:44 +0100 |
blanchet |
recognize Vampire error
|
changeset |
files
|
| Mon, 08 Nov 2010 12:13:51 +0100 |
boehmes |
return the process return code along with the process outputs
|
changeset |
files
|
| Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
changeset |
files
|
| Mon, 08 Nov 2010 11:49:28 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 10:56:48 +0100 |
haftmann |
corrected slip: must keep constant map, not type map; tuned code
|
changeset |
files
|
| Mon, 08 Nov 2010 10:43:24 +0100 |
haftmann |
constructors to datatypes in code_reflect can be globbed; dropped unused code
|
changeset |
files
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
changeset |
files
|
| Mon, 08 Nov 2010 02:33:48 +0100 |
blanchet |
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
|
changeset |
files
|
| Mon, 08 Nov 2010 02:32:27 +0100 |
blanchet |
better detection of completely irrelevant facts
|
changeset |
files
|
| Sun, 07 Nov 2010 18:19:04 +0100 |
blanchet |
always use a hard timeout in Mirabelle
|
changeset |
files
|
| Sun, 07 Nov 2010 18:15:13 +0100 |
blanchet |
use "smt" (rather than "metis") to reconstruct SMT proofs
|
changeset |
files
|
| Sun, 07 Nov 2010 18:03:24 +0100 |
blanchet |
don't pass too many facts on the first iteration of the SMT solver
|
changeset |
files
|
| Sun, 07 Nov 2010 18:02:02 +0100 |
blanchet |
catch TimeOut exception
|
changeset |
files
|
| Sun, 07 Nov 2010 17:56:07 +0100 |
blanchet |
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
|
changeset |
files
|
| Sun, 07 Nov 2010 17:51:25 +0100 |
blanchet |
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
|
changeset |
files
|
| Sun, 07 Nov 2010 13:29:59 +0100 |
blanchet |
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
make Nitpick datatype tests faster to make timeout less likely
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
always honor the max relevant constraint
|
changeset |
files
|
| Mon, 08 Nov 2010 11:28:22 +0100 |
wenzelm |
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
|
changeset |
files
|
| Mon, 08 Nov 2010 00:00:47 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:32:26 +0100 |
wenzelm |
tweaked pdf setup to allow modification of \pdfminorversion;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:12:40 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:12:21 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:51:16 +0100 |
wenzelm |
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:42:49 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:26:25 +0100 |
wenzelm |
more literal appearance of antiqopen/antiqclose;
|
changeset |
files
|
| Sun, 07 Nov 2010 16:39:03 +0100 |
wenzelm |
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
|
changeset |
files
|