src/HOL/SMT.thy
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);
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again
Fri, 07 Jan 2011 17:58:51 +0100 boehmes tuned text
Fri, 07 Jan 2011 15:39:13 +0100 boehmes added hints about licensing restrictions and how to enable Z3
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
Mon, 03 Jan 2011 16:22:08 +0100 boehmes re-implemented support for datatypes (including records and typedefs);
Mon, 20 Dec 2010 22:02:57 +0100 boehmes avoid ML structure aliases (especially single-letter abbreviations)
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);
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);
Wed, 15 Dec 2010 18:18:56 +0100 boehmes fixed trigger inference: testing if a theorem already has a trigger was too strict;
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);
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);
Wed, 15 Dec 2010 08:39:24 +0100 boehmes added option to enable trigger inference;
Wed, 15 Dec 2010 08:39:24 +0100 boehmes moved SMT classes and dictionary functions to SMT_Utils
Wed, 15 Dec 2010 08:39:24 +0100 boehmes added option to modify the random seed of SMT solvers
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
Mon, 29 Nov 2010 23:41:09 +0100 boehmes also support higher-order rules for Z3 proof reconstruction
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in
Mon, 22 Nov 2010 23:37:00 +0100 boehmes added support for quantifier weight annotations
Mon, 22 Nov 2010 15:45:42 +0100 boehmes added prove reconstruction for injective functions;
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)
Fri, 29 Oct 2010 18:17:08 +0200 boehmes added crafted list of SMT built-in constants
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
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
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
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
Wed, 14 Jul 2010 14:16:12 +0200 haftmann load cache_io before code generator; moved adhoc-overloading to generic tools
Thu, 27 May 2010 18:16:54 +0200 boehmes added function update examples and set examples
Thu, 27 May 2010 16:29:33 +0200 boehmes renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
Thu, 27 May 2010 14:55:53 +0200 boehmes use Z3's builtin support for div and mod
Wed, 26 May 2010 15:34:47 +0200 boehmes hide constants and types introduced by SMT,
Wed, 12 May 2010 22:33:10 -0700 huffman use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip