src/HOL/SMT_Examples/SMT_Tests.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-18 blanchet 2014-09-18 more meaningful record tests
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-08-19 blanchet 2014-08-19 avoid old 'smt' method in examples
2014-07-27 blanchet 2014-07-27 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-06-12 blanchet 2014-06-12 adapted examples to changes in SMT triggers
2014-06-11 blanchet 2014-06-11 adapted SMT examples to new, corrected handling of 'typedef'
2014-06-03 blanchet 2014-06-03 disable hard-to-reconstruct Z3 feature
2014-06-03 blanchet 2014-06-03 removed SMT weights -- their impact was very inconclusive anyway
2014-05-05 blanchet 2014-05-05 tuned comment
2014-05-01 boehmes 2014-05-01 disable bad Z3 proof
2014-04-25 blanchet 2014-04-25 use Z3 4.3.2 to fix most FIXMEs
2014-03-13 blanchet 2014-03-13 updated SMT2 examples and certificates
2014-03-13 blanchet 2014-03-13 use 'smt2' in SMT examples as much as currently possible
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-01-02 blanchet 2013-01-02 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
2013-01-01 blanchet 2013-01-01 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
2012-11-01 blanchet 2012-11-01 regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-06-04 boehmes 2012-06-04 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
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-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-26 blanchet 2012-03-26 reintroduced broken proofs and regenerated certificates
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-09-14 boehmes 2011-09-14 observe distinction between sets and predicates
2011-09-06 boehmes 2011-09-06 added some examples for pattern and weight annotations
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-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2011-01-03 boehmes 2011-01-03 updated SMT certificates
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-15 boehmes 2010-12-15 updated SMT certificates
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-12 boehmes 2010-11-12 look for certificates relative to the theory
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 changed SMT configuration options; updated SMT certificates
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-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 added function update examples and set examples
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 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable