| 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
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 15:38:02 +0100 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 14:58:20 +0100 |
blanchet |
eta-reduce on the fly to prevent an exception
|
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
|
| Mon, 22 Nov 2010 23:37:00 +0100 |
boehmes |
added support for quantifier weight annotations
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 15:45:43 +0100 |
boehmes |
share and use more utility functions;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 08:14:56 +0100 |
boehmes |
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:04 +0200 |
boehmes |
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:39:26 +0200 |
boehmes |
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
|
file |
diff |
annotate
|
| Sun, 19 Sep 2010 00:29:13 +0200 |
boehmes |
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 10:52:35 +0200 |
boehmes |
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 06:49:46 +0200 |
boehmes |
reverse order of datatype declarations so that declarations only depend on already declared datatypes
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 06:02:47 +0200 |
boehmes |
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
|
file |
diff |
annotate
|
| Wed, 26 May 2010 15:34:47 +0200 |
boehmes |
hide constants and types introduced by SMT,
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
file |
diff |
annotate
|