blanchet [Thu, 05 Aug 2010 12:58:57 +0200] rev 38201
make nitpick accept "==" for "nitpick_(p)simp"s
blanchet [Thu, 05 Aug 2010 12:40:12 +0200] rev 38200
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
blanchet [Thu, 05 Aug 2010 11:54:53 +0200] rev 38199
deal correctly with Pure.conjunction in mono check
blanchet [Thu, 05 Aug 2010 09:49:46 +0200] rev 38198
rename internal functions
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