src/HOL/SMT_Examples/SMT_Tests.thy
Mon, 05 May 2014 10:03:43 +0200 blanchet tuned comment
Thu, 01 May 2014 23:04:07 +0200 boehmes disable bad Z3 proof
Fri, 25 Apr 2014 22:13:17 +0200 blanchet use Z3 4.3.2 to fix most FIXMEs
Thu, 13 Mar 2014 16:21:09 +0100 blanchet updated SMT2 examples and certificates
Thu, 13 Mar 2014 13:18:13 +0100 blanchet use 'smt2' in SMT examples as much as currently possible
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Wed, 02 Jan 2013 09:31:25 +0100 blanchet actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
Tue, 01 Jan 2013 11:36:30 +0100 blanchet regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
Thu, 01 Nov 2012 11:34:00 +0100 blanchet regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Mon, 04 Jun 2012 09:07:23 +0200 boehmes 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"
Tue, 27 Mar 2012 17:11:02 +0200 boehmes 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
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates"
Mon, 26 Mar 2012 11:01:04 +0200 blanchet reintroduced broken proofs and regenerated certificates
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Wed, 14 Sep 2011 09:46:59 +0200 boehmes observe distinction between sets and predicates
Tue, 06 Sep 2011 18:07:44 +0200 boehmes added some examples for pattern and weight annotations
Wed, 09 Mar 2011 21:40:38 +0100 boehmes finished and tested Z3 proof reconstruction for injective functions;
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again
Mon, 03 Jan 2011 16:49:28 +0100 boehmes updated SMT certificates
Mon, 03 Jan 2011 16:22:08 +0100 boehmes re-implemented support for datatypes (including records and typedefs);
Wed, 15 Dec 2010 10:52:43 +0100 boehmes updated SMT certificates
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
Tue, 26 Oct 2010 11:46:19 +0200 boehmes changed SMT configuration options; updated SMT certificates
Fri, 17 Sep 2010 10:52:35 +0200 boehmes 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
Tue, 13 Jul 2010 02:29:05 +0200 boehmes fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
Thu, 27 May 2010 18:16:54 +0200 boehmes added function update examples and set examples
Thu, 27 May 2010 14:55:53 +0200 boehmes use Z3's builtin support for div and mod
Wed, 26 May 2010 15:34:47 +0200 boehmes hide constants and types introduced by SMT,
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
less more (0) tip