| Fri, 26 Aug 2011 01:14:49 +0200 |
blanchet |
improve completeness of polymorphic encodings
|
changeset |
files
|
| Fri, 26 Aug 2011 00:19:25 +0200 |
blanchet |
mangle tag bound declarations properly
|
changeset |
files
|
| Fri, 26 Aug 2011 00:05:45 +0200 |
blanchet |
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
|
changeset |
files
|
| Thu, 25 Aug 2011 23:55:21 +0200 |
blanchet |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
changeset |
files
|
| Thu, 25 Aug 2011 23:54:57 +0200 |
blanchet |
honor TFF Implicit
|
changeset |
files
|
| Thu, 25 Aug 2011 23:38:09 +0200 |
blanchet |
make polymorphic encodings more complete
|
changeset |
files
|
| Thu, 25 Aug 2011 22:06:25 +0200 |
blanchet |
make default unsound mode less unsound
|
changeset |
files
|
| Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
changeset |
files
|
| Thu, 25 Aug 2011 19:09:39 +0200 |
blanchet |
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
|
changeset |
files
|
| Thu, 25 Aug 2011 19:05:40 +0200 |
blanchet |
added one more known Z3 failure
|
changeset |
files
|
| Thu, 25 Aug 2011 19:02:47 +0200 |
blanchet |
added config options to control two aspects of the translation, for evaluation purposes
|
changeset |
files
|
| Thu, 25 Aug 2011 13:55:52 +0100 |
nik |
added choice operator output for
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:06 +0200 |
blanchet |
fixed bang encoding detection of which types to encode
|
changeset |
files
|
| Thu, 25 Aug 2011 14:06:34 +0200 |
krauss |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
avoid variable clashes by properly incrementing indices
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
changeset |
files
|
| Thu, 25 Aug 2011 00:00:36 +0200 |
blanchet |
include chained facts for minimizer, otherwise it won't work
|
changeset |
files
|
| Wed, 24 Aug 2011 22:12:30 +0200 |
blanchet |
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
|
changeset |
files
|
| Fri, 26 Aug 2011 22:25:41 +0200 |
wenzelm |
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
|
changeset |
files
|
| Fri, 26 Aug 2011 22:14:12 +0200 |
wenzelm |
tuned Session.edit_node: update_perspective based on last_exec_offset;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:27:58 +0200 |
wenzelm |
tuned signature -- iterate subsumes both fold and get_first;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:18:42 +0200 |
wenzelm |
further clarification of Document.updated, based on last_common and after_entry;
|
changeset |
files
|
| Fri, 26 Aug 2011 16:06:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:56:30 +0200 |
wenzelm |
improved Document.edit: more accurate update_start and no_execs;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:09:54 +0200 |
wenzelm |
refined document state assignment: observe perspective, more explicit assignment message;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
changeset |
files
|
| Thu, 25 Aug 2011 17:38:12 +0200 |
wenzelm |
maintain last_execs assignment on Scala side;
|
changeset |
files
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
changeset |
files
|
| Thu, 25 Aug 2011 13:24:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:20:05 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:19:40 +0200 |
wenzelm |
tuned syntax -- avoid ambiguities;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:00:53 +0200 |
wenzelm |
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
|
changeset |
files
|
| Wed, 24 Aug 2011 09:23:26 -0700 |
huffman |
delete commented-out dead code
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:07 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
changeset |
files
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
changeset |
files
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
changeset |
files
|
| Wed, 24 Aug 2011 17:30:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 15:25:39 +0200 |
blanchet |
make sure that all facts are passed to ATP from minimizer
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
specify timeout for "sledgehammer_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 24 Aug 2011 10:59:22 +0900 |
Cezary Kaliszyk |
Quotient Package: add mem_rsp, mem_prs, tune proofs.
|
changeset |
files
|
| Tue, 23 Aug 2011 15:46:53 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
changeset |
files
|
| Tue, 23 Aug 2011 07:12:05 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 18:15:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 16:49:45 -0700 |
huffman |
comment out dead code to avoid compiler warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 10:43:10 -0700 |
huffman |
legacy theorem names
|
changeset |
files
|
| Mon, 22 Aug 2011 10:19:39 -0700 |
huffman |
remove duplicate lemma
|
changeset |
files
|
| Tue, 23 Aug 2011 23:18:13 +0200 |
blanchet |
fixed "hBOOL" of existential variables, and generate more helpers
|
changeset |
files
|
| Tue, 23 Aug 2011 22:44:08 +0200 |
blanchet |
don't select facts when using sledgehammer_tac for reconstruction
|
changeset |
files
|
| Tue, 23 Aug 2011 20:35:41 +0200 |
blanchet |
don't perform a triviality check if the goal is skipped anyway
|
changeset |
files
|
| Tue, 23 Aug 2011 19:50:25 +0200 |
blanchet |
optional reconstructor
|
changeset |
files
|
| Wed, 24 Aug 2011 17:25:45 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 24 Aug 2011 17:16:48 +0200 |
wenzelm |
tuned pri: prefer purging of canceled execution;
|
changeset |
files
|
| Wed, 24 Aug 2011 17:14:31 +0200 |
wenzelm |
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
|
changeset |
files
|
| Wed, 24 Aug 2011 16:49:48 +0200 |
wenzelm |
clarified Document.Node.clear -- retain header (cf. ML version);
|
changeset |
files
|
| Wed, 24 Aug 2011 16:27:27 +0200 |
wenzelm |
clarified norm_header/header_edit -- disallow update of loaded theories;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:55:43 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:30:43 +0200 |
wenzelm |
ignore irrelevant timings;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:40:10 +0200 |
wenzelm |
print state only for visible command, to avoid wasting resources for the larger part of the text;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:38:07 +0200 |
wenzelm |
early filtering of unchanged perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:37:43 +0200 |
wenzelm |
more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
|
changeset |
files
|
| Wed, 24 Aug 2011 13:03:39 +0200 |
wenzelm |
update_perspective without actual edits, bypassing the full state assignment protocol;
|
changeset |
files
|
| Tue, 23 Aug 2011 21:19:24 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 23 Aug 2011 21:14:59 +0200 |
wenzelm |
handle potentially more approriate BufferUpdate.LOADED event;
|
changeset |
files
|
| Mon, 22 Aug 2011 23:39:05 +0200 |
wenzelm |
special treatment of structure index 1 in Pure, including legacy warning;
|
changeset |
files
|
| Tue, 23 Aug 2011 19:49:21 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 23 Aug 2011 19:00:48 +0200 |
blanchet |
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
|
changeset |
files
|
| Tue, 23 Aug 2011 18:42:05 +0200 |
blanchet |
beef up "sledgehammer_tac" reconstructor
|
changeset |
files
|
| Tue, 23 Aug 2011 18:42:05 +0200 |
blanchet |
clean up Sledgehammer tactic
|
changeset |
files
|
| Tue, 23 Aug 2011 17:44:31 +0200 |
wenzelm |
fixed document;
|
changeset |
files
|
| Tue, 23 Aug 2011 17:43:06 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 23 Aug 2011 17:12:54 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 16:37:23 +0200 |
blanchet |
always use TFF if possible
|
changeset |
files
|
| Tue, 23 Aug 2011 16:14:19 +0200 |
blanchet |
clearer separator in generated file names
|
changeset |
files
|
| Tue, 23 Aug 2011 16:07:01 +0200 |
blanchet |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
changeset |
files
|
| Tue, 23 Aug 2011 15:50:27 +0200 |
blanchet |
updated known failures for Z3 3.0 TPTP
|
changeset |
files
|
| Tue, 23 Aug 2011 15:18:46 +0200 |
blanchet |
updated Z3 docs
|
changeset |
files
|
| Tue, 23 Aug 2011 15:15:43 +0200 |
blanchet |
avoid TFF format with older Vampire versions
|
changeset |
files
|
| Tue, 23 Aug 2011 14:57:16 +0200 |
blanchet |
update the Vampire related parts of the documentation
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
fixed TFF slicing
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
kindly ask Vampire to output axiom names
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
added formats to the slice and use TFF for remote Vampire
|
changeset |
files
|
| Tue, 23 Aug 2011 07:14:09 +0200 |
haftmann |
tuned specifications, syntax and proofs
|
changeset |
files
|
| Mon, 22 Aug 2011 22:00:36 +0200 |
haftmann |
tuned specifications and syntax
|
changeset |
files
|
| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
include all encodings in tests, now that the incompleteness of some encodings has been addressed
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
change Metis's default settings if type information axioms are generated
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
we must tag any type whose ground types intersect a nonmonotonic type
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning ATP problem output
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
revert guard logic -- make sure that typing information is generated for existentials
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
generate tag equations for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning, plus started implementing tag equation generation for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
clearer terminology
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
removed unused configuration option
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
remove needless typing information
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
cleaner handling of polymorphic monotonicity inference
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
more precise warning
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added option to control soundness of encodings more precisely, for evaluation purposes
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
make sound mode more sound (and clean up code)
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
gracefully handle empty SPASS problems
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
pass sound option to Sledgehammer tactic
|
changeset |
files
|
| Tue, 23 Aug 2011 16:53:05 +0200 |
wenzelm |
tuned signature -- contrast physical output primitives versus Output.raw_message;
|
changeset |
files
|
| Tue, 23 Aug 2011 16:41:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 23 Aug 2011 16:39:21 +0200 |
wenzelm |
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
|
changeset |
files
|