| 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, 17 Mar 2011 11:18:31 +0100 |
blanchet |
add option to function to keep trivial ATP formulas, needed for some experiments
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:29:00 +0100 |
blanchet |
added a timeout around SMT preprocessing (notably monomorphization)
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 16:30:44 +0100 |
blanchet |
gracious timeout in "blocking" mode
|
file |
diff |
annotate
|
| Thu, 10 Feb 2011 16:15:43 +0100 |
blanchet |
run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
|
file |
diff |
annotate
|
| Wed, 09 Feb 2011 17:18:58 +0100 |
blanchet |
tuning
|
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
|
| 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 03:56:51 +0100 |
blanchet |
added "smt_triggers" option to experiment with triggers in Sledgehammer;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 14:10:40 +0100 |
blanchet |
make exceptions more transparent in "debug" mode
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 14:02:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 13:43:46 +0100 |
blanchet |
lower threshold where the binary algorithm kick in and use the same value for automatic minimization
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 13:34:32 +0100 |
blanchet |
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 12:53:56 +0100 |
blanchet |
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 12:46:58 +0100 |
blanchet |
factored out running a prover with (optionally) an implicit minimizer phrase
|
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 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 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:55:27 +0100 |
blanchet |
export experimental options
|
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
|
| 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 19:41:24 +0100 |
blanchet |
make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 18:10:32 +0100 |
blanchet |
facilitate debugging
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:53 +0100 |
blanchet |
implicitly call the minimizer for SMT solvers that don't return an unsat core
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
renamings
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
moved function to later module
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
clarified terminology
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
|
file |
diff |
annotate
| base
|