cofactor x = False ?

[johnyf]

I was trying to use sylvan_compose to rename variables. That appears to work. However, trying to use sylvan_compose to cofactor BDDs doesn't appear to work correctly.

Cofactoring the node for x with dict(x=True) works correctly:

BDD x, u;
x = sylvan_ithvar(0);
printf("%d\n", x);
BDDMAP map;
map = sylvan_map_empty();
map = sylvan_map_add(map, 0, sylvan_true);
u = sylvan_compose(x, map);
assert(u == sylvan_true);

But cofactoring x with dict(x=False) returns an incorrect result:

map = sylvan_map_empty();
map = sylvan_map_add(map, 0, sylvan_false);
u = sylvan_compose(x, map);
printf("%d\n", u);
assert(u == sylvan_false);

The assertion fails, with u equal to x (node 2), instead of sylvan_false ((BDD)0x0). My understanding of the cause is that sylvan_false serves the dual purpose of logical False and empty variable mapping (BDDMAP), as indicated by sylvan_map_isempty.

Is this the case?

If no, then an explanation of what is going wrong, or a bugfix suggestion would be greatly appreciated. If this is intended, then:

1. If someone substitutes False for a variable, then sylvan_compose will silently return an incorrect result. Since this is a valid call of compose, it would be considered a bug. For example, this is not the case with Cudd_bddCompose.

2. Is there any other way to efficiently cofactor with false non-top variable(s)? The only other way I can think of is sylvan_and_exists. It appears that the algorithm for and_exists reduces, in this special case, essentially to that of compose (which is essentially the same for cofactoring and renaming). Is this the case, or are there any details that would support to implement substitution with False within sylvan_compose?

   To describe the similarity, suppose that we want to cofactor node u with x = False (and no other variables, though that's possible too, with a suitable conjunction of literals). Applying and_exists will unzip u down to the level of x, while keeping the node for v (== ! x) as is. Reaching the level of x, both u and v will be unzipped. This will lead to the terminal cases for v, so the conjunction will escape at that level, and stop the recursion, starting returning. The first zip will skip x (existentially quantified), and the conjunctions just below that level will have effectively applied the selection x = False. The rest of the returning recursion will be as if we called compose.

[johnyf]

This appears to be a bug that affects the addition of dict(x=False) to an empty map. In contrast, the following assertion passes:

map = sylvan_map_empty();
map = sylvan_map_add(map, 1, sylvan_true);
map = sylvan_map_add(map, 0, sylvan_false);
u = sylvan_compose(x, map);
printf("%d\n", u);
assert(u == sylvan_false);

It seems that the culprit may be this line, because sylvan_makenode(key, sylvan_map_empty(), value) will in this case be sylvan_makenode(key, sylvan_false, sylvan_false), which reduces to sylvan_false, instead of the map from variable x to sylvan_false.

[trolando]

You are quite correct that there is a design flaw here, and also that the problem is related to the use of makenode here.

More general, if a map_add is called and the "value" is identical to the existing (sub)map (sub, at the level of the variable) then the map is not updated.

A fix would involve removing the "redundant node" (low == high) check for the specific case of creating a BDD map (or MTBDD map).

[trolando]

I have committed a fix in 1ac9f686b277052033598ba27ddc6a513d08a073 and 232b472ed048d96e7b27ad770ad12a58c3d6b651

[johnyf]

Thank you for addressing this issue. For posterity, the test of dd.sylvan whose failure resulted in this issue is line sylvan_test.py#L141. The failure occurred with 73a69dd3541b01955ca08d4517d5c392d4da8dd2 and the traceback is:

ipython sylvan_test.py
---------------------------------------------------------------------------
AssertionError                            Traceback (most recent call last)
~/dd/tests/sylvan_test.py in <module>()
    167
    168 if __name__ == '__main__':
--> 169     test_cofactor()

~/dd/tests/sylvan_test.py in test_cofactor()
    139     u = bdd.compose(x, dict(x=bdd.false))
    140     u_ = bdd.false
--> 141     assert u == u_, (u, u_)
    142     del x, u, u_
    143

AssertionError: (<dd.sylvan.Function object at 0x7fe5840acfd0>, <dd.sylvan.Function object at 0x7fe584583030>)

With 01df1f129859290ac90ac684744c98598d5c4e56 all tests in sylvan_test.py pass.