| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:44:57 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
| base
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 23 May 2012 16:03:38 +0200 |
boehmes |
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 02 Feb 2011 14:01:09 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 09:41:48 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 09:06:37 +0100 |
boehmes |
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:54:29 +0100 |
boehmes |
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 17:55:56 +0100 |
boehmes |
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 08:33:02 +0100 |
boehmes |
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
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
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
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
|