src/HOL/SMT.thy
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-06 blanchet 2014-10-06 strengthened 'moura' method
2014-09-29 blanchet 2014-09-29 made 'moura' tactic more powerful
2014-09-25 blanchet 2014-09-25 added useful options to CVC4
2014-09-17 blanchet 2014-09-17 added interface for CVC4 extensions
2014-08-28 blanchet 2014-08-28 tuned method description
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized setup; tuned;
2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 use 'ctr_sugar' abstraction in SMT(2)
2014-06-11 blanchet 2014-06-11 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-03-11 blanchet 2014-03-11 full path
2014-01-19 boehmes 2014-01-19 removed obsolete remote_cvc3 and remote_z3
2014-01-13 wenzelm 2014-01-13 activation of Z3 via "z3_non_commercial" system option (without requiring restart);
2012-12-03 wenzelm 2012-12-03 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-23 wenzelm 2012-04-23 more standard method setup;
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-11-07 boehmes 2011-11-07 replace higher-order matching against schematic theorem with dedicated reconstruction method
2011-08-25 boehmes 2011-08-25 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
2011-08-09 blanchet 2011-08-09 load lambda-lifting structure earlier, so it can be used in Metis
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-20 boehmes 2011-07-20 removed old (unused) SMT monomorphizer
2011-06-07 boehmes 2011-06-07 clarified meaning of monomorphization configuration option by renaming it
2011-02-14 boehmes 2011-02-14 limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate
2011-01-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2011-01-07 boehmes 2011-01-07 tuned text
2011-01-07 boehmes 2011-01-07 added hints about licensing restrictions and how to enable Z3
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
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-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 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