| 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:24 +0200 |
blanchet |
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
make sure the minimizer monomorphizes when it should
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
move type declarations to the front, for TFF-compliance
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added (without implementation yet) new type encodings for Sledgehammer/ATP
|
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
|
| Fri, 22 Apr 2011 00:57:59 +0200 |
blanchet |
iterate the unsound-fact-set removal process to recover even more unsound proofs
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 00:00:05 +0200 |
blanchet |
automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 22:32:00 +0200 |
blanchet |
automatically retry with full-types upon unsound proof
|
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 21:14:06 +0200 |
blanchet |
tuning -- local semicolon consistency
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 18:51:22 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 18:39:22 +0200 |
blanchet |
fixed interaction between monomorphization and slicing for ATPs
|
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
|
| Fri, 01 Apr 2011 13:21:21 +0200 |
blanchet |
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 11:54:51 +0200 |
boehmes |
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 14:02:03 +0200 |
boehmes |
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:54 +0200 |
blanchet |
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:53 +0200 |
blanchet |
temporary workaround: filter out spurious monomorphic instances
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:52 +0200 |
blanchet |
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more precise failure reporting in Sledgehammer/SMT
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 17:20:54 +0100 |
blanchet |
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 17:20:53 +0100 |
blanchet |
make Minimizer honor "verbose" and "debug" options better
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 11:18:31 +0100 |
blanchet |
add option to function to keep trivial ATP formulas, needed for some experiments
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 13:59:44 +0100 |
blanchet |
exit code 127 can mean many things -- not just (and probably not) Perl missing
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:31:48 +0100 |
blanchet |
give more weight to Frees than to Consts in relevance filter
|
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
|
| Tue, 08 Feb 2011 16:10:10 +0100 |
blanchet |
available_provers ~> supported_provers (for clarity)
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 16:10:06 +0100 |
blanchet |
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 17:51:56 +0100 |
boehmes |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 04:33:17 +0100 |
blanchet |
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
|
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
|
| Mon, 20 Dec 2010 14:55:24 +0100 |
blanchet |
run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 14:09:45 +0100 |
blanchet |
remove spurious line
|
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
|
| Fri, 17 Dec 2010 22:15:08 +0100 |
blanchet |
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 21:31:19 +0100 |
blanchet |
put the SMT weights back where they belong, so that they're also used by Mirabelle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 15:30:43 +0100 |
blanchet |
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:10:08 +0100 |
blanchet |
make timeout part of the SMT filter's tail
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:02:46 +0100 |
blanchet |
split "smt_filter" into head and tail
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 09:56:04 +0100 |
blanchet |
trap one more Z3 error
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 00:27:40 +0100 |
blanchet |
more precise/correct SMT error handling
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 22:45:02 +0100 |
blanchet |
discriminate SMT errors a bit better
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:46:54 +0100 |
blanchet |
no need to do a super-duper atomization if Metis fails afterwards anyway
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
robustly handle SMT exceptions in Sledgehammer
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 18:10:32 +0100 |
blanchet |
facilitate debugging
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 17:14:44 +0100 |
blanchet |
clean up fudge factors a little bit
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 16:42:07 +0100 |
blanchet |
added weights to SMT problems
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 12:08:41 +0100 |
blanchet |
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
crank up Metis's timeout for SMT solvers, since users love Metis
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|