| Sun, 27 Jul 2014 21:11:35 +0200 |
blanchet |
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
adapted examples to changes in SMT triggers
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
adapted SMT examples to new, corrected handling of 'typedef'
|
file |
diff |
annotate
|
| Tue, 03 Jun 2014 16:02:41 +0200 |
blanchet |
disable hard-to-reconstruct Z3 feature
|
file |
diff |
annotate
|
| Tue, 03 Jun 2014 11:43:07 +0200 |
blanchet |
removed SMT weights -- their impact was very inconclusive anyway
|
file |
diff |
annotate
|
| Mon, 05 May 2014 10:03:43 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Thu, 01 May 2014 23:04:07 +0200 |
boehmes |
disable bad Z3 proof
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 22:13:17 +0200 |
blanchet |
use Z3 4.3.2 to fix most FIXMEs
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:21:09 +0100 |
blanchet |
updated SMT2 examples and certificates
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
use 'smt2' in SMT examples as much as currently possible
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:31:25 +0100 |
blanchet |
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 01 Nov 2012 11:34:00 +0100 |
blanchet |
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| 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"
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
renamed "smt_fixed" to "smt_read_only_certificates"
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 11:01:04 +0200 |
blanchet |
reintroduced broken proofs and regenerated certificates
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 09:46:59 +0200 |
boehmes |
observe distinction between sets and predicates
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 18:07:44 +0200 |
boehmes |
added some examples for pattern and weight annotations
|
file |
diff |
annotate
|
| Wed, 09 Mar 2011 21:40:38 +0100 |
boehmes |
finished and tested Z3 proof reconstruction for injective functions;
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:49:28 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:22:08 +0100 |
boehmes |
re-implemented support for datatypes (including records and typedefs);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 10:52:43 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 10:39:58 +0100 |
boehmes |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
file |
diff |
annotate
|
| Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:46:19 +0200 |
boehmes |
changed SMT configuration options; updated SMT certificates
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 02:29:05 +0200 |
boehmes |
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:16:54 +0200 |
boehmes |
added function update examples and set examples
|
file |
diff |
annotate
|
| Thu, 27 May 2010 14:55:53 +0200 |
boehmes |
use Z3's builtin support for div and mod
|
file |
diff |
annotate
|
| Wed, 26 May 2010 15:34:47 +0200 |
boehmes |
hide constants and types introduced by SMT,
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|