| Wed, 15 Dec 2010 10:12:44 +0100 |
boehmes |
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
moved SMT classes and dictionary functions to SMT_Utils
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to modify the random seed of SMT solvers
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 15:55:35 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 15:01:37 +0100 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:52 +0100 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 11:25:21 +0100 |
blanchet |
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:32:39 +0100 |
blanchet |
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 18:27:21 +0100 |
blanchet |
export more information about available SMT solvers
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 18:22:43 +0100 |
boehmes |
split up Z3 models into constraints on free variables and constant definitions;
|
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
|
| Wed, 17 Nov 2010 08:14:56 +0100 |
boehmes |
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 08:14:55 +0100 |
boehmes |
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
|
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:23:26 +0100 |
boehmes |
honour timeouts which are not rounded to full seconds
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 17:35:57 +0100 |
boehmes |
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
|
file |
diff |
annotate
|
| Fri, 12 Nov 2010 17:28:43 +0100 |
boehmes |
check the return code of the SMT solver and raise an exception if the prover failed
|
file |
diff |
annotate
|
| Fri, 12 Nov 2010 15:56:10 +0100 |
boehmes |
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 12:13:51 +0100 |
boehmes |
return the process return code along with the process outputs
|
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
|
| Thu, 04 Nov 2010 18:01:55 +0100 |
boehmes |
simulate more closely the behaviour of the tactic
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 16:44:38 +0100 |
boehmes |
standardize timeout value based on reals
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:09 +0200 |
boehmes |
optionally drop assumptions which cannot be preprocessed
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:06 +0200 |
boehmes |
clarified error message
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 17:35:54 +0200 |
boehmes |
use proper context
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 17:35:52 +0200 |
boehmes |
trace assumptions before giving them to the SMT solver
|
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 17:35:49 +0200 |
boehmes |
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
|
file |
diff |
annotate
|