| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
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
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
simplified minimization logic
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
put faster proof methods first
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
use parallel preplay machinery also for one-line proofs
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
always minimize Sledgehammer results by default
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
added more proof methods for one-liners
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Thu, 22 May 2014 05:23:50 +0200 |
blanchet |
properly reconstruct helpers in Z3 proofs
|
file |
diff |
annotate
|
| Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 21 May 2014 14:09:42 +0200 |
blanchet |
avoid markup-generating @{make_string}
|
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
|
| Fri, 14 Mar 2014 12:09:51 +0100 |
blanchet |
delayed construction of command (and of noncommercial check) + tuning
|
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 |
honor the fact that the new Z3 can generate Isar proofs
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 10:33:57 +0100 |
blanchet |
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 16:21:43 +0100 |
blanchet |
do the right thing with provers that exist only remotely (e.g. e_sine)
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
|
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, 06 Feb 2014 01:13:44 +0100 |
blanchet |
try right bunch of methods
|
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
|
| Mon, 03 Feb 2014 23:38:33 +0100 |
blanchet |
properly overwrite replay data from one compression iteration to another
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:07:20 +0100 |
blanchet |
moved ML code around
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 13:42:47 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 13:32:13 +0100 |
blanchet |
guarded against exception
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
| base
|