| Wed, 18 Apr 2012 10:53:28 +0200 |
blanchet |
avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
|
file |
diff |
annotate
|
| Sat, 18 Feb 2012 23:43:21 +0100 |
boehmes |
corrected treatment of applications of built-in functions to higher-order terms
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 15:09:53 +0200 |
boehmes |
removed debugging facilities accidentally left in the committed code
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 12:23:20 +0200 |
boehmes |
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 09:23:12 +0200 |
boehmes |
moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
allow lambda-lifting without triggers
|
file |
diff |
annotate
|
| Sun, 26 Jun 2011 19:10:02 +0200 |
boehmes |
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 15:07:03 +0200 |
boehmes |
export lambda-lifting code as there is potential use for it within Sledgehammer
|
file |
diff |
annotate
|
| Tue, 14 Jun 2011 13:50:54 +0200 |
boehmes |
slightly more general treatment of mutually recursive datatypes;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2011 15:00:17 +0200 |
boehmes |
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
fixed eta-expansion: use correct order to apply new bound variables
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 09:14:48 +0100 |
boehmes |
wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:22:08 +0100 |
boehmes |
re-implemented support for datatypes (including records and typedefs);
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 22:02:57 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:54:29 +0100 |
boehmes |
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:15:56 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 14:36:33 +0100 |
boehmes |
fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 13:12:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 13:54:17 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 13:34:28 +0100 |
boehmes |
fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:33:06 +0100 |
boehmes |
fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:07:36 +0100 |
boehmes |
fixed eta-expansion: introduce a couple of abstractions at once
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:19:00 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:05:00 +0000 |
paulson |
made sml/nj happy
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 16:32:45 +0100 |
boehmes |
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 16:29:56 +0100 |
boehmes |
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 14:29:04 +0100 |
blanchet |
workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor
|
file |
diff |
annotate
|
| 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 |
tuned
|
file |
diff |
annotate
|