| 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
|
| Sun, 19 Dec 2010 17:55:56 +0100 |
boehmes |
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
|
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 |
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, 08 Dec 2010 08:33:04 +0100 |
boehmes |
built-in numbers are also built-in terms
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 08:33:02 +0100 |
boehmes |
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 00:32:30 +0100 |
blanchet |
fix check for builtinness of 0 and 1 -- these aren't functions
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 15:33:35 +0100 |
boehmes |
swap names for built-in tester functions (to better reflect the intuition of what they do);
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 10:39:58 +0100 |
boehmes |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 23:43:56 +0100 |
blanchet |
more precise characterization of built-in constants "number_of", "0", and "1"
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 23:37:00 +0100 |
boehmes |
added support for quantifier weight annotations
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:08 +0200 |
boehmes |
added crafted list of SMT built-in constants
|
file |
diff |
annotate
|