| Wed, 21 May 2014 14:09:42 +0200 |
blanchet |
avoid markup-generating @{make_string}
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
| base
|
| Tue, 07 Dec 2010 16:27:07 +0100 |
blanchet |
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 11:41:24 +0100 |
blanchet |
handle "max_relevant" uniformly
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 11:26:17 +0100 |
blanchet |
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:31:29 +0100 |
blanchet |
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:23:31 +0100 |
blanchet |
reraise interrupt exceptions
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 18:29:14 +0100 |
blanchet |
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:22:07 +0100 |
blanchet |
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 09:15:49 +0100 |
blanchet |
adjust Sledgehammer/SMT fudge factor
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 14:58:50 +0100 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 13:26:12 +0100 |
blanchet |
set Metis option on correct context, lest it be ignored
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 12:11:12 +0100 |
blanchet |
make "debug" mode of Sledgehammer/SMT more liberal
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 16:15:15 +0100 |
blanchet |
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 22:37:16 +0100 |
blanchet |
more precise error handling for Z3;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 21:54:03 +0100 |
blanchet |
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 18:28:09 +0100 |
blanchet |
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 22:24:08 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 22:23:28 +0100 |
boehmes |
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 22:08:01 +0100 |
blanchet |
better error message
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 21:08:48 +0100 |
blanchet |
better error message
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 18:58:30 +0100 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 18:56:31 +0100 |
blanchet |
interpret SMT_Failure.Solver_Crashed correctly
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 18:56:29 +0100 |
blanchet |
pick up SMT solver crashes and report them to the user/Mirabelle if desired
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 09:03:07 +0100 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 14:33:30 +0100 |
blanchet |
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 13:53:18 +0100 |
blanchet |
compile -- 7550b2cba1cb broke the build
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 07 Nov 2010 18:19:04 +0100 |
blanchet |
always use a hard timeout in Mirabelle
|
file |
diff |
annotate
|
| Sun, 07 Nov 2010 18:03:24 +0100 |
blanchet |
don't pass too many facts on the first iteration of the SMT solver
|
file |
diff |
annotate
|
| Sun, 07 Nov 2010 18:02:02 +0100 |
blanchet |
catch TimeOut exception
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
use the SMT integration's official list of built-ins
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 22:26:53 +0100 |
blanchet |
standardize on seconds for Nitpick and Sledgehammer timeouts
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 09:36:51 +0200 |
blanchet |
clear identification;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 21:51:04 +0200 |
blanchet |
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 21:43:50 +0200 |
blanchet |
better list of irrelevant SMT constants
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 21:34:01 +0200 |
blanchet |
if "debug" is on, print list of relevant facts (poweruser request);
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 21:01:28 +0200 |
blanchet |
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 20:09:38 +0200 |
blanchet |
merge
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 16:56:54 +0200 |
blanchet |
remove needless context argument;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 17:35:51 +0200 |
boehmes |
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 14:48:55 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 13:50:57 +0200 |
blanchet |
proper error handling for SMT solvers in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 13:16:43 +0200 |
blanchet |
integrated "smt" proof method with Sledgehammer
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:31:45 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 16:11:43 +0200 |
blanchet |
more robust handling of "remote_" vs. non-"remote_" provers
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 15:02:27 +0200 |
blanchet |
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
|
file |
diff |
annotate
|