src/HOL/Tools/SMT/smt_builtin.ML
21 months ago blanchet 2017-08-29 towards support for HO SMT-LIB
22 months ago blanchet 2017-07-28 introduced option for nat-as-int in SMT
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-09-30 blanchet 2013-09-30 added experimental configuration options to tune use of builtin symbols in SMT
2013-09-30 blanchet 2013-09-30 added possibility to reset builtins (for experimentation)
2013-09-30 blanchet 2013-09-30 just one data slot (record) per program unit
2011-12-29 wenzelm 2011-12-29 comments;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-08 wenzelm 2011-01-08 Ord_List.merge convenience;
2010-12-21 boehmes 2010-12-21 also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
2010-12-21 blanchet 2010-12-21 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
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-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-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 moved SMT classes and dictionary functions to SMT_Utils
2010-12-08 boehmes 2010-12-08 built-in numbers are also built-in terms
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-25 blanchet 2010-11-25 fix check for builtinness of 0 and 1 -- these aren't functions
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 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-23 blanchet 2010-11-23 more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-22 boehmes 2010-11-22 added support for quantifier weight annotations
2010-10-29 boehmes 2010-10-29 added crafted list of SMT built-in constants