blanchet [Thu, 05 Aug 2010 01:12:12 +0200] rev 38197
remove buggy and needless condition
blanchet [Thu, 05 Aug 2010 00:21:11 +0200] rev 38196
renamed internal function
blanchet [Wed, 04 Aug 2010 23:27:27 +0200] rev 38195
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
blanchet [Wed, 04 Aug 2010 22:47:52 +0200] rev 38194
avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet [Wed, 04 Aug 2010 21:56:17 +0200] rev 38193
improve datatype symmetry breaking;
all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example
blanchet [Wed, 04 Aug 2010 10:52:29 +0200] rev 38192
merged
blanchet [Wed, 04 Aug 2010 10:51:04 +0200] rev 38191
make SML/NJ happy
blanchet [Wed, 04 Aug 2010 10:39:35 +0200] rev 38190
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet [Tue, 03 Aug 2010 21:37:12 +0200] rev 38189
tuning
blanchet [Tue, 03 Aug 2010 21:20:31 +0200] rev 38188
better "Pretty" handling
blanchet [Tue, 03 Aug 2010 18:27:21 +0200] rev 38187
change formula for enumerating scopes
blanchet [Tue, 03 Aug 2010 18:14:44 +0200] rev 38186
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
blanchet [Tue, 03 Aug 2010 17:43:15 +0200] rev 38185
speed up Nitpick examples a little bit
blanchet [Tue, 03 Aug 2010 17:29:54 +0200] rev 38184
minor changes
blanchet [Tue, 03 Aug 2010 17:29:27 +0200] rev 38183
updated example timings
blanchet [Tue, 03 Aug 2010 15:15:17 +0200] rev 38182
more helpful message
blanchet [Tue, 03 Aug 2010 14:54:30 +0200] rev 38181
also mention gfp
blanchet [Tue, 03 Aug 2010 14:49:42 +0200] rev 38180
bump up the max cardinalities, to use up more of the time given to us by the user
blanchet [Tue, 03 Aug 2010 14:49:02 +0200] rev 38179
make tracing monotonicity easier
blanchet [Tue, 03 Aug 2010 14:28:44 +0200] rev 38178
more documentation, based on email discussions with a user
blanchet [Tue, 03 Aug 2010 14:06:29 +0200] rev 38177
make example easier to parse
blanchet [Tue, 03 Aug 2010 14:04:48 +0200] rev 38176
clarify attribute documentation
blanchet [Tue, 03 Aug 2010 13:40:24 +0200] rev 38175
choose better example
blanchet [Tue, 03 Aug 2010 13:29:26 +0200] rev 38174
fix newly introduced bug w.r.t. conditional equations
blanchet [Tue, 03 Aug 2010 13:17:15 +0200] rev 38173
document something I explained in an email to a poweruser
blanchet [Tue, 03 Aug 2010 12:31:30 +0200] rev 38172
make Nitpick more flexible when parsing (p)simp rules
blanchet [Tue, 03 Aug 2010 12:16:32 +0200] rev 38171
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet [Tue, 03 Aug 2010 02:18:05 +0200] rev 38170
handle free variables even more gracefully;
1. show those that only occur in assumptions as part of the constants;
2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
blanchet [Tue, 03 Aug 2010 01:16:08 +0200] rev 38169
optimize local "def"s by treating them as definitions
blanchet [Mon, 02 Aug 2010 19:15:15 +0200] rev 38168
careful about which linear inductive predicates should be starred