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