2010-12-15 boehmes 2010-12-15 fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically)
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 re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level); added simple trigger inference mechanism; added syntactic checks for triggers and quantifier weights; factored out the normalization of special quantifiers (used to be in the eta-normalization part); normalization now unfolds abs/min/max (not SMT-LIB-specific); rules for pairs and function update are not anymore added automatically to the problem; more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions); normalizations are now managed in a class-based manner (similar to built-in symbols)
2010-12-15 boehmes 2010-12-15 added option to enable trigger inference; better documentation of triggers and SMT available options
2010-12-15 boehmes 2010-12-15 moved SMT classes and dictionary functions to SMT_Utils
2010-12-15 boehmes 2010-12-15 added option to modify the random seed of SMT solvers
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-29 boehmes 2010-11-29 also support higher-order rules for Z3 proof reconstruction
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 added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-10-29 boehmes 2010-10-29 added crafted list of SMT built-in constants
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 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
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-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-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools
2010-05-27 boehmes 2010-05-27 added function update examples and set examples
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27 boehmes 2010-05-27 use Z3's builtin support for div and mod
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 huffman 2010-05-12 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
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