Tue, 26 Oct 2010 13:16:43 +0200 |
blanchet |
integrated "smt" proof method with Sledgehammer
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 10:39:52 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 09:40:20 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
Mon, 25 Oct 2010 09:29:43 +0200 |
blanchet |
make "sledgehammer_params" work on single-threaded platforms
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 16:11:43 +0200 |
blanchet |
more robust handling of "remote_" vs. non-"remote_" provers
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 14:10:32 +0200 |
blanchet |
fixed signature of "is_smt_solver_installed";
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 13:49:44 +0200 |
blanchet |
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 11:11:34 +0200 |
blanchet |
make Sledgehammer minimizer fully work with SMT
|
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
|
Mon, 13 Sep 2010 13:12:33 +0200 |
blanchet |
use 30 s instead of 60 s as the default Sledgehammer timeout;
|
file |
diff |
annotate
|
Sat, 11 Sep 2010 12:31:42 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sat, 11 Sep 2010 10:35:00 +0200 |
blanchet |
finished renaming "Auto_Counterexample" to "Auto_Tools"
|
file |
diff |
annotate
|
Sat, 11 Sep 2010 10:21:52 +0200 |
blanchet |
implemented Auto Sledgehammer
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 17:27:10 +0200 |
blanchet |
got rid of the "theory_relevant" option;
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 16:46:11 +0200 |
blanchet |
generalize theorem argument parsing syntax
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 23:50:59 +0200 |
blanchet |
finished renaming
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 23:43:23 +0200 |
blanchet |
added "expect" feature of Nitpick to Sledgehammer, for regression testing
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 22:27:33 +0200 |
blanchet |
added "blocking" option to Sledgehammer to run in synchronous mode;
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 20:19:58 +0200 |
blanchet |
add a penalty for being higher-order
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 15:39:41 +0200 |
blanchet |
make Sledgehammer's relevance filter somewhat slacker
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 19:41:18 +0200 |
blanchet |
reorganize options regarding to the relevance threshold and decay
|
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:32:43 +0200 |
blanchet |
get rid of "defs_relevant" feature;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 09:02:07 +0200 |
blanchet |
renamed "relevance_convergence" to "relevance_decay"
|
file |
diff |
annotate
|
Mon, 23 Aug 2010 18:53:11 +0200 |
blanchet |
invert semantics of "relevance_convergence", to make it more intuitive
|
file |
diff |
annotate
|
Mon, 23 Aug 2010 18:39:12 +0200 |
blanchet |
if no facts were selected on first iteration, try again with a lower threshold
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 17:16:37 +0200 |
blanchet |
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 17:09:05 +0200 |
blanchet |
added "max_relevant_per_iter" option to Sledgehammer
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 12:05:48 +0200 |
blanchet |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
|
file |
diff |
annotate
|
Thu, 29 Jul 2010 22:43:46 +0200 |
blanchet |
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 19:01:07 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 18:54:18 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 19:41:19 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 17:56:01 +0200 |
blanchet |
rename "ATP_Manager" ML module to "Sledgehammer";
|
file |
diff |
annotate
|
Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 17:32:28 +0200 |
blanchet |
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 17:31:38 +0200 |
blanchet |
always perform relevance filtering on original formulas
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 18:34:06 +0200 |
blanchet |
factor out thread creation
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 17:26:14 +0200 |
blanchet |
got rid of "respect_no_atp" option, which even I don't use
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 16:15:03 +0200 |
blanchet |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 15:08:03 +0200 |
blanchet |
further reduce dependencies on "sledgehammer_fact_filter.ML"
|
file |
diff |
annotate
|
Wed, 23 Jun 2010 09:40:06 +0200 |
blanchet |
killed legacy "neg_clausify" and "clausify"
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
Fri, 11 Jun 2010 17:10:23 +0200 |
blanchet |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 15:07:50 +0200 |
blanchet |
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 15:41:27 +0200 |
blanchet |
made "clausify" attribute a legacy feature;
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 15:21:46 +0200 |
blanchet |
made "neg_clausify" a legacy feature
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 15:09:37 +0200 |
blanchet |
kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
|
file |
diff |
annotate
|
Fri, 28 May 2010 13:49:21 +0200 |
blanchet |
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
file |
diff |
annotate
|
Fri, 14 May 2010 11:20:09 +0200 |
blanchet |
delect installed ATPs dynamically, _not_ at image built time
|
file |
diff |
annotate
|
Sat, 01 May 2010 21:29:03 +0200 |
krauss |
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 13:00:30 +0200 |
blanchet |
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 17:44:33 +0200 |
blanchet |
make Sledgehammer more friendly if no subgoal is left
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:17:04 +0200 |
blanchet |
rename options
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 15:04:20 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|