Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
|
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
|
Sat, 16 Aug 2014 13:23:50 +0200 |
wenzelm |
modernized module name and setup;
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:52:48 +0200 |
blanchet |
more informative preplay failures
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
added appropriate method for skolemization of Z3 steps to the mix
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
tuned ML function name
|
file |
diff |
annotate
|
Fri, 25 Jul 2014 12:20:48 +0200 |
blanchet |
faster minimization by not adding facts that are already in the simpset
|
file |
diff |
annotate
|
Fri, 25 Jul 2014 11:31:20 +0200 |
blanchet |
added missing facts to proof method
|
file |
diff |
annotate
|
Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
fine-tuned methods
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 08:19:55 +0200 |
blanchet |
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
given two one-liners, only show the best of the two
|
file |
diff |
annotate
|
Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 16 May 2014 19:14:00 +0200 |
blanchet |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
file |
diff |
annotate
|
Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
file |
diff |
annotate
|
Thu, 15 May 2014 20:48:13 +0200 |
blanchet |
new approach to silence proof methods, to avoid weird theory/context mismatches
|
file |
diff |
annotate
|
Tue, 13 May 2014 16:18:16 +0200 |
blanchet |
transfer theorems since 'silence_methods' may change the theory
|
file |
diff |
annotate
|
Sun, 04 May 2014 21:35:04 +0200 |
blanchet |
use right meson tactic for preplaying
|
file |
diff |
annotate
|
Sun, 04 May 2014 19:01:36 +0200 |
blanchet |
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
simplified preplaying information
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:16 +0100 |
blanchet |
removed hint that is seldom useful in practice
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 01:35:48 +0100 |
blanchet |
removed legacy 'metisFT' method
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 01:03:28 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
| base
|