blanchet [Mon, 08 Nov 2010 14:33:54 +0100] rev 40440
merge
blanchet [Mon, 08 Nov 2010 14:33:30 +0100] rev 40439
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
huffman [Mon, 08 Nov 2010 05:07:18 -0800] rev 40438
merged
huffman [Sat, 06 Nov 2010 10:01:00 -0700] rev 40437
merged
huffman [Fri, 05 Nov 2010 15:15:28 -0700] rev 40436
(infixl "<<" 55) -> (infix "<<" 50)
huffman [Wed, 03 Nov 2010 17:22:25 -0700] rev 40435
simplify some proofs
huffman [Wed, 03 Nov 2010 17:06:21 -0700] rev 40434
remove unnecessary stuff from Discrete.thy
huffman [Wed, 03 Nov 2010 16:39:23 -0700] rev 40433
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
huffman [Wed, 03 Nov 2010 15:57:39 -0700] rev 40432
add lemma eq_imp_below
huffman [Wed, 03 Nov 2010 15:47:46 -0700] rev 40431
discontinue a bunch of legacy theorem names
huffman [Wed, 03 Nov 2010 15:31:24 -0700] rev 40430
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman [Wed, 03 Nov 2010 15:03:16 -0700] rev 40429
simplify some proofs
blanchet [Mon, 08 Nov 2010 13:53:18 +0100] rev 40428
compile -- 7550b2cba1cb broke the build
blanchet [Mon, 08 Nov 2010 13:25:00 +0100] rev 40427
merge
blanchet [Mon, 08 Nov 2010 09:10:44 +0100] rev 40426
recognize Vampire error
boehmes [Mon, 08 Nov 2010 12:13:51 +0100] rev 40425
return the process return code along with the process outputs
boehmes [Mon, 08 Nov 2010 12:13:44 +0100] rev 40424
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)
haftmann [Mon, 08 Nov 2010 11:49:28 +0100] rev 40423
merged
haftmann [Mon, 08 Nov 2010 10:56:48 +0100] rev 40422
corrected slip: must keep constant map, not type map; tuned code
haftmann [Mon, 08 Nov 2010 10:43:24 +0100] rev 40421
constructors to datatypes in code_reflect can be globbed; dropped unused code
bulwahn [Mon, 08 Nov 2010 09:25:43 +0100] rev 40420
adding code and theory for smallvalue generators, but do not setup the interpretation yet
blanchet [Mon, 08 Nov 2010 02:33:48 +0100] rev 40419
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet [Mon, 08 Nov 2010 02:32:27 +0100] rev 40418
better detection of completely irrelevant facts
blanchet [Sun, 07 Nov 2010 18:19:04 +0100] rev 40417
always use a hard timeout in Mirabelle
blanchet [Sun, 07 Nov 2010 18:15:13 +0100] rev 40416
use "smt" (rather than "metis") to reconstruct SMT proofs
blanchet [Sun, 07 Nov 2010 18:03:24 +0100] rev 40415
don't pass too many facts on the first iteration of the SMT solver
blanchet [Sun, 07 Nov 2010 18:02:02 +0100] rev 40414
catch TimeOut exception
blanchet [Sun, 07 Nov 2010 17:56:07 +0100] rev 40413
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
blanchet [Sun, 07 Nov 2010 17:51:25 +0100] rev 40412
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
blanchet [Sun, 07 Nov 2010 13:29:59 +0100] rev 40411
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