| Fri, 29 Oct 2010 18:17:09 +0200 |
boehmes |
optionally drop assumptions which cannot be preprocessed
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:05 +0200 |
boehmes |
tuned
|
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: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
|
| 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
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
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 16:29:33 +0200 |
boehmes |
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
|
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
|