Wed, 12 Dec 2012 16:28:18 +0100 wenzelm prevent dedicated MacOSX plugin from switching off vital workarounds;
Wed, 12 Dec 2012 14:54:48 +0100 wenzelm improved coupling of zoom_box and scale;
Wed, 12 Dec 2012 13:28:23 +0100 blanchet really all facts means really all facts (well, almost)
Wed, 12 Dec 2012 13:28:01 +0100 blanchet tuning
Wed, 12 Dec 2012 11:56:07 +0100 blanchet use modern SAT solvers with modern Kodkod versions
Wed, 12 Dec 2012 11:18:06 +0100 blanchet got rid of support for Kodkodi < 1.2.14
Wed, 12 Dec 2012 03:47:02 +0100 blanchet made MaSh evaluation driver work with SMT solvers
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
Wed, 12 Dec 2012 00:14:58 +0100 blanchet better name for SMT solver files
Wed, 12 Dec 2012 00:14:58 +0100 blanchet updated version of MaSh learner engine
Wed, 12 Dec 2012 00:14:58 +0100 blanchet push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
Tue, 11 Dec 2012 22:19:39 +0100 wenzelm disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
Tue, 11 Dec 2012 22:16:23 +0100 wenzelm less massive arrow heads;
Tue, 11 Dec 2012 22:09:22 +0100 wenzelm added explicit zoom box;
Tue, 11 Dec 2012 21:55:56 +0100 wenzelm some attempts at more discrete scale factor;
Tue, 11 Dec 2012 21:28:37 +0100 wenzelm more official graphics context with font metrics;
Tue, 11 Dec 2012 21:05:38 +0100 wenzelm just one class with parameters;
Tue, 11 Dec 2012 12:17:20 +0100 wenzelm initial layout coordinates more like old browser;
Tue, 11 Dec 2012 10:35:42 +0100 wenzelm added speculative options for jEdit;
Mon, 10 Dec 2012 21:55:57 +0100 wenzelm separate instance of class Parameters for each Main_Panel -- avoid global program state;
Mon, 10 Dec 2012 21:28:01 +0100 wenzelm discontinued long names flag -- better done via entity markup, without affecting layout;
Mon, 10 Dec 2012 20:52:57 +0100 wenzelm tuned;
Mon, 10 Dec 2012 20:32:13 +0100 wenzelm tuned;
Mon, 10 Dec 2012 19:58:45 +0100 wenzelm tuned min/max;
Mon, 10 Dec 2012 19:42:58 +0100 wenzelm tuned;
Mon, 10 Dec 2012 19:28:56 +0100 wenzelm keep diagnostic command -- avoid confusion when it disappears;
Mon, 10 Dec 2012 19:17:16 +0100 wenzelm tuned;
Mon, 10 Dec 2012 17:44:17 +0100 wenzelm tuned signature;
Mon, 10 Dec 2012 17:05:51 +0100 wenzelm removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;
Mon, 10 Dec 2012 16:38:20 +0100 blanchet merge
Mon, 10 Dec 2012 16:26:23 +0100 blanchet merged
Mon, 10 Dec 2012 16:20:04 +0100 blanchet merge
Mon, 10 Dec 2012 13:33:06 +0100 blanchet changed capitalization of MeSh filter
Mon, 10 Dec 2012 13:02:56 +0100 blanchet (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
Mon, 10 Dec 2012 16:27:03 +0100 wenzelm further clarification for Windows;
Mon, 10 Dec 2012 16:07:29 +0100 wenzelm merged
Mon, 10 Dec 2012 16:06:57 +0100 wenzelm more generous tracing limit -- rescaled in MB;
Mon, 10 Dec 2012 15:46:50 +0100 wenzelm recovered title property from bfb5964e3041;
Mon, 10 Dec 2012 15:39:20 +0100 wenzelm some clarification for Windows;
Mon, 10 Dec 2012 15:17:47 +0100 wenzelm stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
Mon, 10 Dec 2012 15:13:13 +0100 wenzelm tuned;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Mon, 10 Dec 2012 14:45:47 +0100 wenzelm merged
Mon, 10 Dec 2012 10:29:52 +0100 blanchet have MaSh evaluator keep all raw problem/solution files in a directory
Mon, 10 Dec 2012 10:41:29 +0100 wenzelm clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
Sun, 09 Dec 2012 14:05:21 +0100 wenzelm always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
Sun, 09 Dec 2012 14:01:09 +0100 wenzelm added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
Sat, 08 Dec 2012 22:41:39 +0100 wenzelm merged
Sat, 08 Dec 2012 22:15:44 +0100 blanchet merge
Sat, 08 Dec 2012 21:54:28 +0100 blanchet don't blacklist "case" theorems -- this causes problems in MaSh later
Sat, 08 Dec 2012 13:55:26 +0100 blanchet more changes to MaSh Python program (by Daniel K.)
Sat, 08 Dec 2012 00:48:51 +0100 blanchet don't have MaSh pretend it knows facts it doesn't know
Sat, 08 Dec 2012 00:48:51 +0100 blanchet reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
Sat, 08 Dec 2012 00:48:50 +0100 blanchet fixed embarrassing off-by-one bug in MaSh's Mesh
Sat, 08 Dec 2012 00:48:50 +0100 blanchet store evaluation output in a file
Sat, 08 Dec 2012 00:48:50 +0100 blanchet use parallel map
Sat, 08 Dec 2012 00:48:50 +0100 blanchet tweak MaSh fudge factors
Sat, 08 Dec 2012 00:48:50 +0100 blanchet more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
Sat, 08 Dec 2012 22:19:24 +0100 wenzelm basic monitor panel, using the powerful jfreechart library;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip