Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
adapted the Z3 proof parser to recent changes in Z3's proof format;
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 10:12:44 +0100 |
boehmes |
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
|
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
|
Wed, 24 Nov 2010 08:51:48 +0100 |
boehmes |
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
|
file |
diff |
annotate
|
Mon, 22 Nov 2010 23:37:00 +0100 |
boehmes |
added support for quantifier weight annotations
|
file |
diff |
annotate
|
Mon, 22 Nov 2010 15:45:43 +0100 |
boehmes |
share and use more utility functions;
|
file |
diff |
annotate
|
Mon, 22 Nov 2010 15:45:42 +0100 |
boehmes |
added prove reconstruction for injective functions;
|
file |
diff |
annotate
|
Wed, 17 Nov 2010 08:14:56 +0100 |
boehmes |
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)
|
file |
diff |
annotate
|
Fri, 12 Nov 2010 15:56:11 +0100 |
boehmes |
preliminary support for newer versions of Z3
|
file |
diff |
annotate
|
Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
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)
|
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:49:23 +0200 |
boehmes |
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 11:45:12 +0200 |
boehmes |
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
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 11:39:26 +0200 |
boehmes |
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
|
file |
diff |
annotate
|
Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
Wed, 26 May 2010 17:52:32 +0200 |
boehmes |
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
|
file |
diff |
annotate
|
Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
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
|