| Wed, 15 Dec 2010 11:07:13 +0100 |
boehmes |
merged
|
changeset |
files
|
| Wed, 15 Dec 2010 10:52:43 +0100 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
|
changeset |
files
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
adapted the Z3 proof parser to recent changes in Z3's proof format;
|
changeset |
files
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
also show function definitions for higher-order free variables in Z3 models
|
changeset |
files
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
always add pair rules and function update rules automatically (Boogie provides pairs and function update as built-in concepts and does not generate background axioms for them)
|
changeset |
files
|
| 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);
|
changeset |
files
|
| 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);
|
changeset |
files
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to enable trigger inference;
|
changeset |
files
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
moved SMT classes and dictionary functions to SMT_Utils
|
changeset |
files
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
tuned
|
changeset |
files
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
|
changeset |
files
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to modify the random seed of SMT solvers
|
changeset |
files
|
| Wed, 15 Dec 2010 08:34:01 +0100 |
bulwahn |
adding an Isar version of the MacLaurin theorem from some students' work in 2005
|
changeset |
files
|
| Tue, 14 Dec 2010 00:16:30 +0100 |
krauss |
Admin/contributed_components tries to formalize compatibility with external components (for use e.g. by testing tools), guessing from the content of TUM contrib_devel directory
|
changeset |
files
|