2011-02-21 boehmes 2011-02-21 wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
2011-01-03 boehmes 2011-01-03 re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs
2010-12-20 boehmes 2010-12-20 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-19 boehmes 2010-12-19 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions); removed odd retyping during folify (instead, keep all terms well-typed)
2010-12-17 wenzelm 2010-12-17 merged
2010-12-17 boehmes 2010-12-17 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; fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)
2010-12-17 wenzelm 2010-12-17 tuned;
2010-12-16 boehmes 2010-12-16 merged
2010-12-16 boehmes 2010-12-16 fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope
2010-12-16 boehmes 2010-12-16 fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term
2010-12-16 boehmes 2010-12-16 fixed eta-expansion: introduce a couple of abstractions at once
2010-12-16 paulson 2010-12-16 merged
2010-12-16 paulson 2010-12-16 made sml/nj happy
2010-12-15 boehmes 2010-12-15 fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
2010-12-15 boehmes 2010-12-15 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
2010-12-15 blanchet 2010-12-15 workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor
2010-12-15 boehmes 2010-12-15 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure); abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context); proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions); built-in functions carry additionally their arity and their most general type; slightly generalized the definition of fun_app
2010-12-15 boehmes 2010-12-15 tuned
2010-12-07 boehmes 2010-12-07 centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
2010-12-06 boehmes 2010-12-06 tuned
2010-11-25 blanchet 2010-11-25 eta-reduce on the fly to prevent an exception
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-22 boehmes 2010-11-22 added support for quantifier weight annotations
2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-17 boehmes 2010-11-17 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)
2010-10-29 boehmes 2010-10-29 introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
2010-10-26 boehmes 2010-10-26 keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
2010-09-19 boehmes 2010-09-19 do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
2010-09-17 boehmes 2010-09-17 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
2010-09-16 boehmes 2010-09-16 reverse order of datatype declarations so that declarations only depend on already declared datatypes
2010-09-13 boehmes 2010-09-13 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
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image