src/HOL/SMT.thy
2015-11-10 fleury 2015-11-10 fixing premises in veriT proof reconstruction
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-25 blanchet 2015-04-25 made CVC4 support work also without unsat cores
2015-04-08 blanchet 2015-04-08 updated SMT module and Sledgehammer to fully open source Z3
2015-01-16 boehmes 2015-01-16 more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
2014-11-24 blanchet 2014-11-24 added one more CVC4 option that helps Judgment Day (10 theory version)
2014-11-24 blanchet 2014-11-24 added Z3 reconstruction rule suggested by F. Maric
2014-11-24 blanchet 2014-11-24 one more CVC4 option that helps
2014-11-24 blanchet 2014-11-24 renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
2014-11-20 blanchet 2014-11-20 added CVC4 option that helps on JD
2014-11-20 blanchet 2014-11-20 removed explicit '--quant-cf' option to CVC4, now that it's the default
2014-11-19 blanchet 2014-11-19 parse CVC4 unsat cores
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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