src/HOL/SMT.thy
Thu, 20 Nov 2014 17:29:18 +0100 blanchet removed explicit '--quant-cf' option to CVC4, now that it's the default
Wed, 19 Nov 2014 10:31:15 +0100 blanchet parse CVC4 unsat cores
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 24 Oct 2014 15:07:51 +0200 hoelzl use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
Mon, 06 Oct 2014 19:19:16 +0200 blanchet strengthened 'moura' method
Mon, 29 Sep 2014 14:32:30 +0200 blanchet made 'moura' tactic more powerful
Thu, 25 Sep 2014 13:30:57 +0200 blanchet added useful options to CVC4
Wed, 17 Sep 2014 16:53:39 +0200 blanchet added interface for CVC4 extensions
Thu, 28 Aug 2014 16:58:26 +0200 blanchet tuned method description
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Sat, 16 Aug 2014 18:31:47 +0200 wenzelm updated to named_theorems;
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies
Thu, 12 Jun 2014 01:00:49 +0200 blanchet tuning
Thu, 12 Jun 2014 01:00:49 +0200 blanchet use 'ctr_sugar' abstraction in SMT(2)
Wed, 11 Jun 2014 11:28:46 +0200 blanchet fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
Tue, 11 Mar 2014 15:34:38 +0100 blanchet full path
Sun, 19 Jan 2014 22:38:17 +0100 boehmes removed obsolete remote_cvc3 and remote_z3
Mon, 13 Jan 2014 20:20:44 +0100 wenzelm activation of Z3 via "z3_non_commercial" system option (without requiring restart);
Mon, 03 Dec 2012 16:07:28 +0100 wenzelm synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
Wed, 22 Aug 2012 23:22:57 +0200 wenzelm prefer ML_file over old uses;
Mon, 23 Apr 2012 21:44:36 +0200 wenzelm more standard method setup;
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates"
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Mon, 07 Nov 2011 17:54:35 +0100 boehmes replace higher-order matching against schematic theorem with dedicated reconstruction method
Thu, 25 Aug 2011 11:15:31 +0200 boehmes improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
Tue, 09 Aug 2011 09:05:21 +0200 blanchet load lambda-lifting structure earlier, so it can be used in Metis
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)
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)
Wed, 20 Jul 2011 09:23:09 +0200 boehmes removed old (unused) SMT monomorphizer
Tue, 07 Jun 2011 10:24:16 +0200 boehmes clarified meaning of monomorphization configuration option by renaming it
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")
less more (0) -60 tip