Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
Thu, 17 Mar 2011 11:18:31 +0100 |
blanchet |
add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
|
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, 17 Feb 2011 12:14:47 +0100 |
blanchet |
export more functionality of Sledgehammer to applications (for experiments)
|
file |
diff |
annotate
|
Wed, 16 Feb 2011 19:07:53 +0100 |
blanchet |
export useful function (needed in a Sledgehammer-related experiment)
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
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
|
Sun, 19 Dec 2010 13:25:18 +0100 |
blanchet |
escape backticks in altstrings
|
file |
diff |
annotate
|
Sat, 18 Dec 2010 21:07:34 +0100 |
blanchet |
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
|
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 |
reintroduce the higher penalty for skolems
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
comment tuning
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
make it more likely that induction rules are picked up by Sledgehammer
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
instantiate induction rules automatically
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 16:42:06 +0100 |
blanchet |
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
|
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 |
make Sledgehammer's relevance filter include the "ext" rule when appropriate
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
Tue, 07 Dec 2010 16:27:07 +0100 |
blanchet |
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
|
file |
diff |
annotate
|
Mon, 08 Nov 2010 02:32:27 +0100 |
blanchet |
better detection of completely irrelevant facts
|
file |
diff |
annotate
|
Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
always honor the max relevant constraint
|
file |
diff |
annotate
|
Fri, 05 Nov 2010 09:49:03 +0100 |
blanchet |
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
|
file |
diff |
annotate
|
Thu, 04 Nov 2010 15:31:26 +0100 |
blanchet |
pass proper type to SMT_Builtin.is_builtin
|
file |
diff |
annotate
|
Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
ignore facts with only theory constants in them
|
file |
diff |
annotate
|
Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
use the SMT integration's official list of built-ins
|
file |
diff |
annotate
|
Fri, 29 Oct 2010 10:40:36 +0200 |
blanchet |
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
|
file |
diff |
annotate
|
Thu, 28 Oct 2010 12:33:24 +0200 |
blanchet |
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 21:34:01 +0200 |
blanchet |
if "debug" is on, print list of relevant facts (poweruser request);
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 21:01:28 +0200 |
blanchet |
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 14:49:48 +0200 |
blanchet |
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 15:02:27 +0200 |
blanchet |
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 14:47:43 +0200 |
blanchet |
replaced references with proper record that's threaded through
|
file |
diff |
annotate
|
Tue, 05 Oct 2010 12:50:45 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
Thu, 30 Sep 2010 20:44:53 +0200 |
blanchet |
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
|
file |
diff |
annotate
|
Mon, 27 Sep 2010 09:14:39 +0200 |
blanchet |
remove needless flag
|
file |
diff |
annotate
|
Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
Tue, 14 Sep 2010 17:23:16 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 14 Sep 2010 16:34:26 +0200 |
blanchet |
handle relevance filter corner cases more gracefully;
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 18:22:04 +0200 |
blanchet |
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 16:32:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 00:50:51 +0200 |
blanchet |
cosmetics
|
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
|
Wed, 01 Sep 2010 11:59:04 +0200 |
blanchet |
fiddled with fudge factor (based on Mirabelle)
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 11:36:02 +0200 |
blanchet |
give priority to assumptions in structured proofs
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 10:26:54 +0200 |
blanchet |
introduce fudge factors to deal with "theory const"
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 23:50:59 +0200 |
blanchet |
finished renaming
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 23:46:23 +0200 |
blanchet |
shorten a few file names
|
file |
diff |
annotate
| base
|