| Mon, 06 Jun 2011 23:46:02 +0200 |
blanchet |
slighly more reasonable Vampire slices (until new monomorphizer is used)
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
file |
diff |
annotate
|
| Tue, 24 May 2011 18:04:23 +0200 |
blanchet |
ensure that the argument of logical negation is enclosed in parentheses in THF mode
|
file |
diff |
annotate
|
| Tue, 24 May 2011 13:29:32 +0200 |
blanchet |
further reduce the number of facts passed to less used remote ATPs
|
file |
diff |
annotate
|
| Tue, 24 May 2011 10:03:15 +0200 |
blanchet |
pass fewer relevant facts to less used remote systems
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
slightly gracefuller handling of LEO-II and Satallax output
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
identify HOL functions with THF functions
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
started adding support for THF output (but no lambdas)
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
clearer SystemOnTPTP errors
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
give fewer equations to Waldmeister
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
detect inappropriate problems and crashes better in Waldmeister
|
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
|
| Sun, 22 May 2011 14:51:41 +0200 |
blanchet |
fish out axioms in Waldmeister output
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:04 +0200 |
blanchet |
recognize one more SystemOnTPTP error
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:01 +0200 |
blanchet |
added support for remote Waldmeister
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:50:32 +0200 |
blanchet |
added Waldmeister
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:49:35 +0200 |
blanchet |
reorganized ATP formats a little bit
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
make sure the Vampire incomplete proof detection code kicks in
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
renamed "simple_types" to "simple"
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
tweaked ATP type systems further based on Judgment Day
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
better error reporting: detect missing E proofs and remove Vampire native format error
|
file |
diff |
annotate
|
| Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
tweak E slices
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
|
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
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
allow each slice to have its own type system
|
file |
diff |
annotate
|
| Fri, 06 May 2011 13:35:00 +0200 |
blanchet |
further improved type system setup based on Judgment Days
|
file |
diff |
annotate
|
| Fri, 06 May 2011 13:34:59 +0200 |
blanchet |
allow each prover to specify its own formula kind for symbols occurring in the conjecture
|
file |
diff |
annotate
|
| Fri, 06 May 2011 13:34:59 +0200 |
blanchet |
better type system setup, based on Judgment Day
|
file |
diff |
annotate
|
| Thu, 05 May 2011 09:43:39 +0200 |
blanchet |
improve suggested type system list based on evaluation
|
file |
diff |
annotate
|
| Wed, 04 May 2011 22:56:33 +0200 |
blanchet |
renamed "many_typed" to "simple" (as in simple types)
|
file |
diff |
annotate
|
| Wed, 04 May 2011 22:47:13 +0200 |
blanchet |
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
|
file |
diff |
annotate
|
| Tue, 03 May 2011 08:52:32 +0200 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
| Tue, 03 May 2011 00:10:22 +0200 |
blanchet |
replaced some Unsynchronized.refs with Config.Ts
|
file |
diff |
annotate
|
| Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
better default type systems for SNARK and ToFoF
|
file |
diff |
annotate
|
| Mon, 02 May 2011 14:40:57 +0200 |
blanchet |
use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
|
file |
diff |
annotate
|
| Mon, 02 May 2011 14:22:34 +0200 |
blanchet |
supply type-system defaults for major ATPs
|
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 |
pick up GaveUp error on SystemOnTPTP
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
implement the new ATP type system in Sledgehammer
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
define type system in ATP module so that ATPs can suggest a type system
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
recognize more SystemOnTPTP errors
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
better known failure recognition for ToFoF-E
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:23 +0200 |
blanchet |
get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
|
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 |
implemented general slicing for ATPs, especially E 1.2w and above
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 15:17:39 +0100 |
blanchet |
adjust fudge factors
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 12:32:55 +0100 |
blanchet |
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
|
file |
diff |
annotate
|
| Tue, 15 Feb 2011 18:32:58 +0100 |
blanchet |
make experimental "Z3 ATP" work on Linux as well
|
file |
diff |
annotate
|
| Tue, 15 Feb 2011 10:03:10 +0100 |
blanchet |
adjusted fudge factors (based on Judgment Day runs)
|
file |
diff |
annotate
|
| Thu, 10 Feb 2011 10:09:38 +0100 |
blanchet |
make minimizer verbose
|
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
|
| Wed, 09 Feb 2011 17:18:58 +0100 |
blanchet |
added "Z3 as an ATP" support to Sledgehammer locally
|
file |
diff |
annotate
|
| Wed, 09 Feb 2011 17:18:57 +0100 |
blanchet |
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 16:10:10 +0100 |
blanchet |
available_provers ~> supported_provers (for clarity)
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 16:10:08 +0100 |
blanchet |
added support for bleeding-edge E weighting function "SymOffsetsWeight"
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 03:56:51 +0100 |
blanchet |
added "smt_triggers" option to experiment with triggers in Sledgehammer;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 01:12:17 +0100 |
blanchet |
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 14:17:49 +0100 |
blanchet |
disable feature that was enabled by mistake
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 13:52:44 +0100 |
blanchet |
use the options provided by Stephan Schulz -- much better
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 12:12:35 +0100 |
blanchet |
optionally supply constant weights to E -- turned off by default until properly parameterized
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 14:02:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:01:49 +0100 |
blanchet |
fewer facts to SInE-E
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
added timeout max for remote server invocation
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 22:37:16 +0100 |
blanchet |
more precise error handling for Z3;
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 10:52:38 +0100 |
blanchet |
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 09:10:44 +0100 |
blanchet |
recognize Vampire error
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 23:01:30 +0100 |
blanchet |
give E one more second, to prevent cases where it finds a proof but has no time to print it
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 16:25:40 +0200 |
blanchet |
first step in adding support for an SMT backend to Sledgehammer
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 14:55:09 +0200 |
blanchet |
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 15:16:08 +0200 |
blanchet |
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 23:37:34 +0200 |
blanchet |
prefer version 0.6 of Vampire, now that we can parse its output
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 12:30:50 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 10:22:52 +0200 |
blanchet |
change order of default ATPs;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 16:27:36 +0200 |
blanchet |
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 16:06:11 +0200 |
blanchet |
better error reporting when the Sledgehammer minimizer is interrupted
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:20:52 +0200 |
blanchet |
improve SInE-E failure message
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:17:56 +0200 |
blanchet |
SNARK doesn't like facts
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:15:53 +0200 |
blanchet |
show real CPU time
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 22:31:45 +0200 |
blanchet |
add dependency of "spass" script
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 18:42:31 +0200 |
blanchet |
lower number of facts given to SInE
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 17:27:10 +0200 |
blanchet |
got rid of the "theory_relevant" option;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 13:55:30 +0200 |
blanchet |
fix Vampire version numbers
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 17:49:52 +0200 |
blanchet |
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:05:22 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 21:40:03 +0200 |
blanchet |
better workaround for E's off-by-one-second issue
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 15:06:47 +0200 |
blanchet |
use a soft time limit for E
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 14:36:29 +0200 |
blanchet |
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 21:11:30 +0200 |
blanchet |
adjust fudge factors in the light of experiments
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 17:53:49 +0200 |
blanchet |
revert unintended change
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 16:12:41 +0200 |
blanchet |
prevent double inclusion of the fact "True_or_False" in TPTP problems
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 09:04:37 +0200 |
blanchet |
play with fudge factor + parse one more Vampire error
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 00:09:25 +0200 |
blanchet |
fiddle a bit with the SPASS fudge number
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 22:47:03 +0200 |
blanchet |
be more generous towards SPASS's -SOS mode
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 09:43:10 +0200 |
blanchet |
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 13:04:37 +0200 |
blanchet |
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:29:53 +0200 |
blanchet |
added remote SInE and remote SNARK
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 20:53:55 +0200 |
blanchet |
don't get confused by wrong slice
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 17:09:05 +0200 |
blanchet |
added "max_relevant_per_iter" option to Sledgehammer
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 16:42:37 +0200 |
blanchet |
thank Andrei instead of Tanya
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 12:04:00 +0200 |
blanchet |
rename enum values
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 18:14:50 +0200 |
blanchet |
tweaking
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 17:01:31 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 14:35:44 +0200 |
blanchet |
improve detection of old Vampire versions
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:47:19 +0200 |
wenzelm |
made 9043eefe8d71 actually compile;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 13:59:04 +0200 |
blanchet |
detect old Vampire and give a nicer error message
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 09:39:05 +0200 |
blanchet |
Geoff's formatter now needs closed formulas
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 11:05:45 +0200 |
blanchet |
fiddle some more with "max_new_relevant_facts_per_iter"
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 20:02:02 +0200 |
blanchet |
avoid "ATP Error: Error: blah" style messages
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 19:26:42 +0200 |
blanchet |
better error and minimizer output
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 18:45:41 +0200 |
blanchet |
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 16:54:46 +0200 |
blanchet |
fiddle with the fudge factors, to get similar results as before
|
file |
diff |
annotate
|