38 no zero suppressed decision diagram implemented

[oykukoc]

Summary

This PR implements a Zero-Suppressed Decision Diagram (ZDD) as a new
decision diagram type in the FrEDDY framework.

ZDDs are a variant of BDDs optimized for representing sparse sets and
combinatorial problems. While BDDs suppress redundant nodes (where
hi == lo), ZDDs suppress nodes whose positive (hi) edge leads to the
0-terminal. This makes ZDDs particularly efficient for representing
families of sets, such as cube set representations in logic minimization.

Implementation

ZDD Wrapper (zdd class)

A handle class mirroring BDD's public interface with the following methods:

• same_node, is_const, var, high, low
• is_zero, is_one, eval
• size, depth, path_count
• compose, restr, is_essential
• exist, forall
• dump_dot
• Operators: & (conjunction), | (disjunction), ~ (complement)

ZDD Manager (zdd_manager class)

• Conjunction: Follows BDD synthesis — expanded returns identity
• Disjunction: Native level-based ZDD union
• Complement: Native ZDD complement
• Reduction: ZDD-specific — suppress when hi-edge → 0-terminal
• Terminals: Two distinct leaf nodes (0 = empty family, 1 = unit family)

Key Difference from BDD

The synthesis (conjunction algorithm) is identical to BDD. The only
difference lies in the reduction rule:

• BDD: reduce when hi == lo (redundancy rule)
• ZDD: reduce when hi → 0-terminal (zero-suppression rule)

Tests

• Basic construction and set operations
• Cube set representation and subsumption
• Logic minimization example
• Wrapper method tests (path_count, compose, restr, exist, forall, etc.)