Sat, 18 Dec 2010 12:55:33 +0100 use minimizing prover in Mirabelle
blanchet [Sat, 18 Dec 2010 12:55:33 +0100] rev 41264
use minimizing prover in Mirabelle
Sat, 18 Dec 2010 12:53:56 +0100 renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet [Sat, 18 Dec 2010 12:53:56 +0100] rev 41263
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
Sat, 18 Dec 2010 12:46:58 +0100 factored out running a prover with (optionally) an implicit minimizer phrase
blanchet [Sat, 18 Dec 2010 12:46:58 +0100] rev 41262
factored out running a prover with (optionally) an implicit minimizer phrase
Fri, 17 Dec 2010 23:18:39 +0100 merged;
wenzelm [Fri, 17 Dec 2010 23:18:39 +0100] rev 41261
merged;
Fri, 17 Dec 2010 23:09:53 +0100 remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
blanchet [Fri, 17 Dec 2010 23:09:53 +0100] rev 41260
remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
Fri, 17 Dec 2010 22:15:08 +0100 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet [Fri, 17 Dec 2010 22:15:08 +0100] rev 41259
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
Fri, 17 Dec 2010 21:47:13 +0100 convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
blanchet [Fri, 17 Dec 2010 21:47:13 +0100] rev 41258
convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
Fri, 17 Dec 2010 21:32:06 +0100 merged
blanchet [Fri, 17 Dec 2010 21:32:06 +0100] rev 41257
merged
Fri, 17 Dec 2010 21:31:19 +0100 put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet [Fri, 17 Dec 2010 21:31:19 +0100] rev 41256
put the SMT weights back where they belong, so that they're also used by Mirabelle
Fri, 17 Dec 2010 18:23:56 +0100 added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet [Fri, 17 Dec 2010 18:23:56 +0100] rev 41255
added debugging option to find out how good the relevance filter was at identifying relevant facts
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip