| 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
|