SSoelvsten/adiar

Add `zdd_ispoint` and `zdd_point`

SSoelvsten opened this issue · 0 comments

This is the ZDD continuation of #533 .

  • Declare zdd_point in src/adiar/zdd.h. It is implemented in src/adiar/zdd.build.cpp as an alias for zdd_vars.
  • Declare zdd_ispoint in src/adiar/zdd.h. It is implemented in src/adiar/zdd/pred.cpp as the ZDD version of bdd_iscube. Due to the suppression rules of ZDDs, it can be implemented as a test for the width being 1 and the number of arcs to true is also 1 (making it faster than bdd_iscube as no I/Os are necessary). Both of these values are precomputed and can be fetched from the levelized_file<node>.

Of course, there should be unit tests for both.

Additional context
Why is it point and not a cube as in #533 ? Consider zdd_change with the second argument being symbolic ( cf. #519 ): if it was not a single point then the result would a much more complex operation (effectively XOR'ing each pair of sets). This would of course be interesting, but in this case it is a widely different algorithm. Hence, we need the zdd_ispoint anyway to change its behaviour.