| Wed, 12 May 2010 23:54:00 +0200 |
boehmes |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:57 +0200 |
boehmes |
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:54 +0200 |
boehmes |
normalize numerals: also rewrite Numeral0 into 0
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:53 +0200 |
boehmes |
added missing rewrite rules for natural min and max
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:52 +0200 |
boehmes |
rewrite bool case expressions as if expression
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:51 +0200 |
boehmes |
simplified normalize_rule and moved it further down in the code
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:50 +0200 |
boehmes |
merged addition of rules into one function
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:49 +0200 |
boehmes |
added simplification for distinctness of small lists
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:40:42 +0200 |
boehmes |
shortened interface (do not export unused options and functions)
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:40:42 +0200 |
boehmes |
always unfold definitions of specific constants (including special binders)
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:40:42 +0200 |
boehmes |
shorten the code by conditional function application
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 17:48:55 +0100 |
boehmes |
unfold quantifiers (Ball, Bex, Ex1)
|
file |
diff |
annotate
|
| Thu, 03 Dec 2009 15:56:06 +0100 |
boehmes |
faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 12:30:54 +0100 |
boehmes |
only add nat/int conversion rules if necessary
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:47:37 +0100 |
boehmes |
removed unused code and unused arguments,
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 11:31:34 +0100 |
boehmes |
abstract over variables in reversed order (application uses given order)
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 10:52:05 +0100 |
boehmes |
simplified method syntax of "smt",
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 10:11:30 +0200 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 18:13:19 +0200 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|