Thu, 05 Aug 2010 14:10:18 +0200 prevent the expansion of too large definitions -- use equations for these instead
blanchet [Thu, 05 Aug 2010 14:10:18 +0200] rev 38202
prevent the expansion of too large definitions -- use equations for these instead
Thu, 05 Aug 2010 12:58:57 +0200 make nitpick accept "==" for "nitpick_(p)simp"s
blanchet [Thu, 05 Aug 2010 12:58:57 +0200] rev 38201
make nitpick accept "==" for "nitpick_(p)simp"s
Thu, 05 Aug 2010 12:40:12 +0200 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
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
Thu, 05 Aug 2010 11:54:53 +0200 deal correctly with Pure.conjunction in mono check
blanchet [Thu, 05 Aug 2010 11:54:53 +0200] rev 38199
deal correctly with Pure.conjunction in mono check
Thu, 05 Aug 2010 09:49:46 +0200 rename internal functions
blanchet [Thu, 05 Aug 2010 09:49:46 +0200] rev 38198
rename internal functions
Thu, 05 Aug 2010 01:12:12 +0200 remove buggy and needless condition
blanchet [Thu, 05 Aug 2010 01:12:12 +0200] rev 38197
remove buggy and needless condition
Thu, 05 Aug 2010 00:21:11 +0200 renamed internal function
blanchet [Thu, 05 Aug 2010 00:21:11 +0200] rev 38196
renamed internal function
Wed, 04 Aug 2010 23:27:27 +0200 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
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
Wed, 04 Aug 2010 22:47:52 +0200 avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
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)
Wed, 04 Aug 2010 21:56:17 +0200 improve datatype symmetry breaking;
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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip