20 months ago blanchet 2017-08-29 towards support for HO SMT-LIB
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-05-23 boehmes 2012-05-23 extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-02-02 boehmes 2011-02-02 avoid ML structure aliases (especially single-letter abbreviations)
2011-01-07 boehmes 2011-01-07 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-20 boehmes 2010-12-20 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
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-19 boehmes 2010-12-19 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general); hide internal constants z3div and z3mod; rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod
2010-12-08 boehmes 2010-12-08 be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
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-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-11-12 boehmes 2010-11-12 preliminary support for newer versions of Z3
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable