| Wed, 11 Apr 2018 10:59:13 +0200 |
boehmes |
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
file |
diff |
annotate
|
| Wed, 30 Aug 2017 23:36:21 +0200 |
blanchet |
added options to make veriT more complete
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 18:30:23 +0200 |
blanchet |
towards support for HO SMT-LIB
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 23:43:17 +0200 |
blanchet |
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
|
file |
diff |
annotate
|
| Fri, 28 Jul 2017 15:36:32 +0100 |
blanchet |
introduced option for nat-as-int in SMT
|
file |
diff |
annotate
|
| 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
|