blanchet [Thu, 05 Aug 2010 14:45:27 +0200] rev 38205
handle inductive predicates correctly after change in "def" semantics
blanchet [Thu, 05 Aug 2010 14:32:24 +0200] rev 38204
don't specialize built-ins or constructors
blanchet [Thu, 05 Aug 2010 14:20:34 +0200] rev 38203
more docs
blanchet [Thu, 05 Aug 2010 14:10:18 +0200] rev 38202
prevent the expansion of too large definitions -- use equations for these instead
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