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, 07 Apr 2010 20:40:42 +0200 |
boehmes |
buffered output (faster than direct output)
|
file |
diff |
annotate
|
Fri, 26 Mar 2010 23:57:35 +0100 |
boehmes |
made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
|
file |
diff |
annotate
|
Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
Tue, 08 Dec 2009 18:44:12 +0100 |
boehmes |
made SML/NJ happy
|
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
|
Fri, 13 Nov 2009 15:47:37 +0100 |
boehmes |
removed unused code and unused arguments,
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 10:52:05 +0100 |
boehmes |
simplified method syntax of "smt",
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 14:22:02 +0200 |
boehmes |
eliminated extraneous wrapping of public records,
|
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
|