Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
specify timeout for "sledgehammer_tac"
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 22:44:08 +0200 |
blanchet |
don't select facts when using sledgehammer_tac for reconstruction
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 20:35:41 +0200 |
blanchet |
don't perform a triviality check if the goal is skipped anyway
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 19:50:25 +0200 |
blanchet |
optional reconstructor
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 19:00:48 +0200 |
blanchet |
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 18:42:05 +0200 |
blanchet |
beef up "sledgehammer_tac" reconstructor
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:14:19 +0200 |
blanchet |
clearer separator in generated file names
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
support local HOATPs
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 09:24:34 +0200 |
blanchet |
add line number prefix to output file name
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 09:07:59 +0200 |
blanchet |
added "sound" option to Mirabelle
|
file |
diff |
annotate
|
Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
remove offset from Mirabelle output
|
file |
diff |
annotate
|
Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
file |
diff |
annotate
|
Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
file |
diff |
annotate
|
Fri, 08 Jul 2011 17:04:38 +0200 |
wenzelm |
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
|
file |
diff |
annotate
|
Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
renamed "type_sys" to "type_enc", which is more accurate
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
|
file |
diff |
annotate
|
Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
|
file |
diff |
annotate
|
Tue, 07 Jun 2011 08:52:35 +0200 |
blanchet |
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:36 +0200 |
blanchet |
enable new Metis
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more preparations towards hijacking Metis
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
show what failed to play
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case of Sledgehammer better
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
detect inappropriate problems and crashes better in Waldmeister
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
tuning -- the "appropriate" terminology is inspired from TPTP
|
file |
diff |
annotate
|
Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
|
file |
diff |
annotate
|
Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
have each ATP filter out dangerous facts for themselves, based on their type system
|
file |
diff |
annotate
|
Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
|
file |
diff |
annotate
|
Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
implement the new ATP type system in Sledgehammer
|
file |
diff |
annotate
|
Thu, 21 Apr 2011 22:18:28 +0200 |
blanchet |
detect some unsound proofs before showing them to the user
|
file |
diff |
annotate
|
Thu, 21 Apr 2011 18:39:22 +0200 |
blanchet |
cleanup: get rid of "may_slice" arguments without changing semantics
|
file |
diff |
annotate
|
Thu, 21 Apr 2011 18:39:22 +0200 |
blanchet |
implemented general slicing for ATPs, especially E 1.2w and above
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Thu, 31 Mar 2011 11:16:51 +0200 |
blanchet |
added support for "dest:" to "try"
|
file |
diff |
annotate
|
Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
Fri, 11 Feb 2011 11:54:24 +0100 |
blanchet |
added option to Mirabelle Sledgehammer
|
file |
diff |
annotate
|
Wed, 09 Feb 2011 17:18:58 +0100 |
blanchet |
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
|
file |
diff |
annotate
|
Wed, 09 Feb 2011 17:18:58 +0100 |
blanchet |
renamed field
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 10:18:56 +0100 |
blanchet |
added "sledgehammer_tac" as possible reconstructor in Mirabelle
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 06:53:20 +0100 |
blanchet |
avoid weird symbols in path
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 06:06:28 +0100 |
blanchet |
mechanism to keep SMT input and output files around in Mirabelle
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 23:31:22 +0100 |
blanchet |
two layers of timeouts seem to be less reliable than a single layer
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 22:15:39 +0100 |
blanchet |
move relevance filter into hard timeout
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 21:24:34 +0100 |
blanchet |
handle timeouts in Mirabelle more gracefully
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 13:48:24 +0100 |
blanchet |
higher hard timeout
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 13:38:14 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 12:55:33 +0100 |
blanchet |
use minimizing prover in Mirabelle
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 23:09:53 +0100 |
blanchet |
remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 18:23:56 +0100 |
blanchet |
added debugging option to find out how good the relevance filter was at identifying relevant facts
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 16:20:02 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|