| Mon, 07 Nov 2011 17:54:35 +0100 |
boehmes |
replace higher-order matching against schematic theorem with dedicated reconstruction method
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 09:05:21 +0200 |
blanchet |
load lambda-lifting structure earlier, so it can be used in Metis
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 12:23:20 +0200 |
boehmes |
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 09:23:12 +0200 |
boehmes |
moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 09:23:09 +0200 |
boehmes |
removed old (unused) SMT monomorphizer
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 10:24:16 +0200 |
boehmes |
clarified meaning of monomorphization configuration option by renaming it
|
file |
diff |
annotate
|
| Mon, 14 Feb 2011 12:25:26 +0100 |
boehmes |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 17:58:51 +0100 |
boehmes |
tuned text
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 15:39:13 +0100 |
boehmes |
added hints about licensing restrictions and how to enable Z3
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 17:51:56 +0100 |
boehmes |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:22:08 +0100 |
boehmes |
re-implemented support for datatypes (including records and typedefs);
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 22:02:57 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
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, 15 Dec 2010 18:18:56 +0100 |
boehmes |
fixed trigger inference: testing if a theorem already has a trigger was too strict;
|
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, 15 Dec 2010 08:39:24 +0100 |
boehmes |
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to enable trigger inference;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
moved SMT classes and dictionary functions to SMT_Utils
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to modify the random seed of SMT solvers
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 23:41:09 +0100 |
boehmes |
also support higher-order rules for Z3 proof reconstruction
|
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
|
| Mon, 22 Nov 2010 23:37:00 +0100 |
boehmes |
added support for quantifier weight annotations
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 15:45:42 +0100 |
boehmes |
added prove reconstruction for injective functions;
|
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:08 +0200 |
boehmes |
added crafted list of SMT built-in constants
|
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
|
| 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
|
| Mon, 13 Sep 2010 06:02:47 +0200 |
boehmes |
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 14:16:12 +0200 |
haftmann |
load cache_io before code generator; moved adhoc-overloading to generic tools
|
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 16:29:33 +0200 |
boehmes |
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
|
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 22:33:10 -0700 |
huffman |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
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
|