Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT.thy
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t; file | diff | annotate
Tue, 10 Nov 2015 23:41:20 +0100 wenzelm recovered from a9c0572109af; file | diff | annotate
Tue, 10 Nov 2015 17:49:54 +0100 fleury fixing premises in veriT proof reconstruction file | diff | annotate
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches; file | diff | annotate
Sat, 25 Apr 2015 09:48:06 +0200 blanchet made CVC4 support work also without unsat cores file | diff | annotate
Wed, 08 Apr 2015 18:47:38 +0200 blanchet updated SMT module and Sledgehammer to fully open source Z3 file | diff | annotate
Fri, 16 Jan 2015 23:23:31 +0100 boehmes more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet added one more CVC4 option that helps Judgment Day (10 theory version) file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet added Z3 reconstruction rule suggested by F. Maric file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet one more CVC4 option that helps file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names file | diff | annotate
Thu, 20 Nov 2014 17:29:18 +0100 blanchet added CVC4 option that helps on JD file | diff | annotate
Thu, 20 Nov 2014 17:29:18 +0100 blanchet removed explicit '--quant-cf' option to CVC4, now that it's the default file | diff | annotate
Wed, 19 Nov 2014 10:31:15 +0100 blanchet parse CVC4 unsat cores file | diff | annotate
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section; file | diff | annotate
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 file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet strengthened 'moura' method file | diff | annotate
Mon, 29 Sep 2014 14:32:30 +0200 blanchet made 'moura' tactic more powerful file | diff | annotate
Thu, 25 Sep 2014 13:30:57 +0200 blanchet added useful options to CVC4 file | diff | annotate
Wed, 17 Sep 2014 16:53:39 +0200 blanchet added interface for CVC4 extensions file | diff | annotate
Thu, 28 Aug 2014 16:58:26 +0200 blanchet tuned method description file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate | base
Sat, 16 Aug 2014 18:31:47 +0200 wenzelm updated to named_theorems; file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet tuning file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet use 'ctr_sugar' abstraction in SMT(2) file | diff | annotate
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 file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle file | diff | annotate
Tue, 11 Mar 2014 15:34:38 +0100 blanchet full path file | diff | annotate
Sun, 19 Jan 2014 22:38:17 +0100 boehmes removed obsolete remote_cvc3 and remote_z3 file | diff | annotate
Mon, 13 Jan 2014 20:20:44 +0100 wenzelm activation of Z3 via "z3_non_commercial" system option (without requiring restart); file | diff | annotate
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); file | diff | annotate
Wed, 22 Aug 2012 23:22:57 +0200 wenzelm prefer ML_file over old uses; file | diff | annotate
Mon, 23 Apr 2012 21:44:36 +0200 wenzelm more standard method setup; file | diff | annotate
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates" file | diff | annotate
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure; file | diff | annotate
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
less more (0) -60 tip
isabelle