src/HOL/Tools/SMT/smt_translate.ML
Thu, 16 Dec 2010 12:07:36 +0100 boehmes fixed eta-expansion: introduce a couple of abstractions at once
Thu, 16 Dec 2010 12:19:00 +0000 paulson merged
Thu, 16 Dec 2010 12:05:00 +0000 paulson made sml/nj happy
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)
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
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
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);
Wed, 15 Dec 2010 08:39:24 +0100 boehmes tuned
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
Mon, 06 Dec 2010 15:38:02 +0100 boehmes tuned
Thu, 25 Nov 2010 14:58:20 +0100 blanchet eta-reduce on the fly to prevent an exception
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in
Mon, 22 Nov 2010 23:37:00 +0100 boehmes added support for quantifier weight annotations
Mon, 22 Nov 2010 15:45:43 +0100 boehmes share and use more utility functions;
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)
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
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
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)
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
Thu, 16 Sep 2010 06:49:46 +0200 boehmes reverse order of datatype declarations so that declarations only depend on already declared datatypes
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
Wed, 26 May 2010 15:34:47 +0200 boehmes hide constants and types introduced by SMT,
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip