src/HOL/Tools/SMT/smt_normalize.ML
2013-11-10 haftmann 2013-11-10 simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
2013-10-02 blanchet 2013-10-02 make SMT integration slacker w.r.t. bad apples (facts)
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-28 boehmes 2013-03-28 new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code
2012-12-21 boehmes 2012-12-21 refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
2012-03-30 huffman 2012-03-30 move lemmas from Nat_Numeral to Int.thy and Num.thy
2012-03-27 boehmes 2012-03-27 dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
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-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-05 boehmes 2011-09-05 tuned
2011-05-31 boehmes 2011-05-31 use new monomorphizer for SMT; simplify the monomorphizer by inlining functions and proper passing of arguments
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-01 boehmes 2011-04-01 make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-03-31 boehmes 2011-03-31 provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2010-12-20 boehmes 2010-12-20 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-20 boehmes 2010-12-20 added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
2010-12-20 boehmes 2010-12-20 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
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-17 wenzelm 2010-12-17 tuned;
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 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 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 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-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-24 boehmes 2010-11-24 swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)
2010-11-24 boehmes 2010-11-24 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
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 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-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 eta-expand built-in constants; also rewrite partially applied natural number terms
2010-10-29 boehmes 2010-10-29 optionally drop assumptions which cannot be preprocessed
2010-10-29 boehmes 2010-10-29 tuned
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-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-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-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-07-13 boehmes 2010-07-13 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
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