Fixes for algebraic cudd

.github/workflows/main.yml

@@ -35,6 +35,7 @@ jobs:
                     DD_FETCH=1 \
                     DD_CUDD=1 \
                     DD_CUDD_ZDD=1 \
+                    DD_CUDD_ADD=1 \
                     DD_SYLVAN=1
                 pip install . \
                     --verbose \

Makefile

@@ -60,7 +60,7 @@ wheel_deps:
 wheel: clean wheel_deps
 	-rm dist/*.whl
 	-rm wheelhouse/*.whl
-	export DD_CUDD=1 DD_CUDD_ZDD=1; \
+	export DD_CUDD=1 DD_CUDD_ZDD=1 DD_CUDD_ADD=1; \
 	pip wheel . \
 	    -vvv \
 	    --wheel-dir dist \
@@ -77,15 +77,15 @@ install: wheel_deps
 	pip install . -vvv --use-pep517 --no-build-isolation
 
 reinstall: uninstall wheel_deps
-	export DD_CUDD=1 DD_CUDD_ZDD DD_SYLVAN; \
+	export DD_CUDD=1 DD_CUDD_ZDD DD_CUDD_ADD=1 DD_SYLVAN; \
 	pip install . -vvv --use-pep517 --no-build-isolation
 
 reinstall_buddy: uninstall wheel_deps
 	export DD_BUDDY=1; \
 	pip install . -vvv --use-pep517 --no-build-isolation
 
 reinstall_cudd: uninstall wheel_deps
-	export DD_CUDD=1 DD_CUDD_ZDD=1; \
+	export DD_CUDD=1 DD_CUDD_ZDD=1 DD_CUDD_ADD=1; \
 	pip install . -vvv --use-pep517 --no-build-isolation
 
 reinstall_sylvan: uninstall wheel_deps
@@ -167,6 +167,7 @@ clean:
 	-rm dd/buddy.c
 	-rm dd/cudd.c
 	-rm dd/cudd_zdd.c
+	-rm dd/cudd_add.c
 	-rm dd/sylvan.c
 	-rm *.pyc */*.pyc
 	-rm -rf __pycache__ */__pycache__

dd/_abc.py

@@ -127,10 +127,43 @@ def _literals_of_recurse(
     *TERNARY_OPERATOR_SYMBOLS}
 if len(BDD_OPERATOR_SYMBOLS) != 3 + 23 + 1:
     raise AssertionError(BDD_OPERATOR_SYMBOLS)
+_AgdUnaryOperatorSymbol: _ty.TypeAlias = (
+    _UnaryOperatorSymbol |
+    _ty.Literal['log'])
+ADD_UNARY_OPERATOR_SYMBOLS: _ty.Final = _literals_of(
+    _AgdUnaryOperatorSymbol)
+if len(ADD_UNARY_OPERATOR_SYMBOLS) != 3 + 1:
+    raise AssertionError(ADD_UNARY_OPERATOR_SYMBOLS)
+_AgdBinaryOperatorSymbol: _ty.TypeAlias = (
+    _BinaryOperatorSymbol |
+    _ty.Literal[
+        '+',
+        '*',
+        '/',
+        'nand'])
+ADD_BINARY_OPERATOR_SYMBOLS: _ty.Final = _literals_of(
+    _AgdBinaryOperatorSymbol)
+if len(ADD_BINARY_OPERATOR_SYMBOLS) != 23 + 4:
+    # `'-' in BINARY_OPERATOR_SYMBOLS`
+    raise AssertionError(ADD_BINARY_OPERATOR_SYMBOLS)
+ADD_TERNARY_OPERATOR_SYMBOLS: _ty.Final = {
+    *TERNARY_OPERATOR_SYMBOLS}
+if len(ADD_TERNARY_OPERATOR_SYMBOLS) != 1:
+    raise AssertionError(ADD_TERNARY_OPERATOR_SYMBOLS)
+ADD_OPERATOR_SYMBOLS: _ty.Final = {
+    *ADD_UNARY_OPERATOR_SYMBOLS,
+    *ADD_BINARY_OPERATOR_SYMBOLS,
+    *ADD_TERNARY_OPERATOR_SYMBOLS}
+if len(ADD_OPERATOR_SYMBOLS) != 4 + 27 + 1:
+    raise AssertionError(ADD_OPERATOR_SYMBOLS)
 OperatorSymbol: _ty.TypeAlias = (
     _UnaryOperatorSymbol |
     _BinaryOperatorSymbol |
     _TernaryOperatorSymbol)
+AgdOperatorSymbol: _ty.TypeAlias = (
+    _AgdUnaryOperatorSymbol |
+    _AgdBinaryOperatorSymbol |
+    _TernaryOperatorSymbol)
 ImageFileType: _ty.TypeAlias = _ty.Literal[
     'pdf',
     'png',

dd/_utils.py

@@ -267,7 +267,12 @@ def total_memory(
         unary=dd._abc.UNARY_OPERATOR_SYMBOLS,
         binary=dd._abc.BINARY_OPERATOR_SYMBOLS,
         ternary=dd._abc.TERNARY_OPERATOR_SYMBOLS,
-        all=dd._abc.BDD_OPERATOR_SYMBOLS))
+        all=dd._abc.BDD_OPERATOR_SYMBOLS),
+    agd=dict(
+        unary=dd._abc.ADD_UNARY_OPERATOR_SYMBOLS,
+        binary=dd._abc.ADD_BINARY_OPERATOR_SYMBOLS,
+        ternary=dd._abc.ADD_TERNARY_OPERATOR_SYMBOLS,
+        all=dd._abc.ADD_OPERATOR_SYMBOLS))
 
 
 def assert_operator_arity(
@@ -281,7 +286,8 @@ def assert_operator_arity(
             None,
         diagram_type:
             _ty.Literal[
-                'bdd']
+                'bdd',
+                'agd']
         ) -> None:
     """Raise `ValueError` if unexpected values.