src/HOL/Tools/SMT/z3_proof_reconstruction.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-10-31 blanchet 2012-10-31 soft SMT timeout
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;
2012-02-14 wenzelm 2012-02-14 normalized aliases;
2011-11-07 boehmes 2011-11-07 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
2011-11-07 boehmes 2011-11-07 replace higher-order matching against schematic theorem with dedicated reconstruction method
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-25 boehmes 2011-08-25 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-07-18 boehmes 2011-07-18 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
2011-05-26 boehmes 2011-05-26 iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 boehmes 2011-04-08 corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
2011-04-01 boehmes 2011-04-01 save reflexivity steps in discharging Z3 Skolemization hypotheses
2011-04-01 boehmes 2011-04-01 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
2011-03-09 boehmes 2011-03-09 finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
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-15 boehmes 2010-12-15 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
2010-12-15 boehmes 2010-12-15 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
2010-12-15 boehmes 2010-12-15 adapted the Z3 proof parser to recent changes in Z3's proof format; keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)
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-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-24 boehmes 2010-11-24 be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
2010-11-22 boehmes 2010-11-22 added support for quantifier weight annotations
2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-22 boehmes 2010-11-22 added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions
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-12 boehmes 2010-11-12 preliminary support for newer versions of Z3
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 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 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
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-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-01 haftmann 2010-09-01 replaced Table.map' by Table.map
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-05-26 boehmes 2010-05-26 try logical and theory abstraction before full abstraction (avoids warnings of linarith)
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