19 months ago blanchet 2017-10-01 properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
20 months ago blanchet 2017-08-29 towards support for HO SMT-LIB
23 months ago blanchet 2017-06-20 tuning
23 months ago blanchet 2017-06-20 correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
2015-12-04 blanchet 2015-12-04 removed needless complication for modern SMT solvers
2014-09-24 blanchet 2014-09-24 interleave (co)datatypes in the right order w.r.t. dependencies
2014-09-17 blanchet 2014-09-17 added codatatype support for CVC4
2014-09-17 blanchet 2014-09-17 added interface for CVC4 extensions
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2012-04-18 blanchet 2012-04-18 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
2012-02-18 boehmes 2012-02-18 corrected treatment of applications of built-in functions to higher-order terms
2011-07-20 boehmes 2011-07-20 removed debugging facilities accidentally left in the committed code
2011-07-20 boehmes 2011-07-20 generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
2011-07-20 boehmes 2011-07-20 moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
2011-07-14 blanchet 2011-07-14 allow lambda-lifting without triggers
2011-06-26 boehmes 2011-06-26 generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem); maintain extra-logical information when introducing explicit application; handle let-expressions properly
2011-06-22 boehmes 2011-06-22 export lambda-lifting code as there is potential use for it within Sledgehammer
2011-06-14 boehmes 2011-06-14 slightly more general treatment of mutually recursive datatypes; treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)
2011-06-05 boehmes 2011-06-05 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
2011-04-08 boehmes 2011-04-08 fixed eta-expansion: use correct order to apply new bound variables
2011-04-08 boehmes 2011-04-08 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
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