Allow non-monotonic BDD functions
mskala mskala Turns out this isn't a good idea. It makes the BDDs much bigger (exponentially so, unless we're very careful about the variable ordering) and that kills whatever speed advantage might result from tighter filters. However, the work isn't totally wasted because the improved definitions of the push-to-children operations seem independently useful; and the variable ordering probably won't hurt either.
mskala Nope, it's a wash.
The enhanced push-to-children operations made it necessary to increase the number of variables from 128 to 160, and that was surprisingly costly, slowing down all BDD operations even on BDDs that did not touch the extra variables. And the variable ordering I chose (interleaving bits from the 32-bit words), even though it was beneficial with the non-monotonic functions, actually slowed things down compared to bog-standard default ordering for the non-monotonic functions. There is something very special about non-monotonic functions, evidently. So I have now rolled back almost all of these changes. Maybe some other reordering could help, but I don't have a lot of hope. Subject for further research...
Tsukurimashou Font Family and IDSgrep
At present all our BDDs represent monotonic functions. Setting a bit in the input will never change the output from one to zero. We look for bits in the vector that must be one on any matching haystack; we never depend on a bit being zero. That principle follows from the original Bloom filters, in which other inserted elements could always make a bit one and a saturated filter contains everything. However, we can extract a little more information out of our vectors because we can limit the total number of things inserted in some words of the filter. Suppose the needle has a head. The current rule is that if the three bits corresponding to the needle's head are set, then we have a hit, or if the three bits corresponding to no head and the three bits corresponding to the functor are all set, as well as any other bits associated with recursive matching of the children, then we have a hit. We don't look at any bits that are not required to be set. But we could look at other bits: if the three bits for the needle's head are not set, then any other bits among the first 32 that are NOT associated with the "no head" condition nor the needle's functor, had better be zero. The only way those other bits could be set would be if the haystack had a bad functor or head. Looking for these to be zero tightens the filter a bit at the cost of making it non-monotonic.
It's not clear that we really win much because of the hidden background assumption that at most six bits in the first word can be set by any haystack. On that first word, allowing non-monotonicity will only have an effect when there are collisions between the functor and the "no head" bits (probability roughly 25%) so that it becomes possible for all the bits we want to be present, but also an extra bit indicating we don't really have a match. But in haystack trees that are two or three levels deep, we may be able to go non-monotonic on some of the bits in the fourth (middle children, grandchildren, and deeper descendants) word, and that could be quite valuable.
Allowing BDDs to represent non-monotonic functions will require more careful attention to the current "move needle from root to child" transformations, which will probably end up needing to use generalized cofactor or something. Their current definitions assume monotonic inputs and outputs.