| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 17:47:50 +0200 |
blanchet |
added experimental configuration options to tune use of builtin symbols in SMT
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 16:28:54 +0200 |
blanchet |
added possibility to reset builtins (for experimentation)
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 16:07:56 +0200 |
blanchet |
just one data slot (record) per program unit
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 15:54:37 +0100 |
wenzelm |
comments;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:30:05 +0100 |
wenzelm |
Ord_List.merge convenience;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 11:05:30 +0100 |
boehmes |
also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 04:33:17 +0100 |
blanchet |
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
|
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
|
| 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
|