| 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
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
regenerate SMT example certificates, to reflect "set" type constructor
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:11 +0100 |
haftmann |
commented out examples which choke on strict set/pred distinction
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:54:38 +0100 |
boehmes |
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 18:52:52 +0200 |
boehmes |
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
fixed eta-expansion: use correct order to apply new bound variables
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
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
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 09:19:44 +0100 |
boehmes |
added test cases with quantifier occurring in first-order term positions
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 09:31:47 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:55:21 +0100 |
boehmes |
updated SMT certificates
|
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
|
| 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:06 +0200 |
boehmes |
updated SMT certificates
|
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
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
file |
diff |
annotate
|