From 4b9e690f1642d45b54995701a39508b197e73247 Mon Sep 17 00:00:00 2001 From: CazSaa Date: Fri, 7 Mar 2025 09:58:36 +0100 Subject: [PATCH 1/5] BUG: fix return type of Cudd_addLeq --- dd/cudd_add.pyx | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/dd/cudd_add.pyx b/dd/cudd_add.pyx index 4f75ee80..71b4a44b 100644 --- a/dd/cudd_add.pyx +++ b/dd/cudd_add.pyx @@ -295,7 +295,7 @@ cdef extern from 'cudd.h': DdManager *dd, DD_MAOP op, DdNode *f) # arithmetic operators - cdef DdNode *Cudd_addLeq( + cdef int Cudd_addLeq( DdManager *dd, DdNode *f, DdNode *g) cdef DdNode *Cudd_addLog( @@ -1909,23 +1909,13 @@ cdef class ADD: elif op == '<': # TODO: is there any better function # for this available in CUDD ? - leq = Cudd_addLeq( - mgr, v.node, u.node) - v_leq_u = wrap(self, leq) - r = Cudd_addCmpl( - mgr, v_leq_u.node) + raise NotImplementedError('<') elif op == '<=': - r = Cudd_addLeq( - mgr, u.node, v.node) + raise NotImplementedError('<=') elif op == '>': - leq = Cudd_addLeq( - mgr, u.node, v.node) - u_leq_v = wrap(self, leq) - r = Cudd_addCmpl( - mgr, u_leq_v.node) + raise NotImplementedError('>') elif op == '>=': - r = Cudd_addLeq( - mgr, v.node, u.node) + raise NotImplementedError('>=') elif op == '==': raise NotImplementedError('==') elif op == '=': From 9a157b8269341c715d13aab2814e4c8ce0ad2c74 Mon Sep 17 00:00:00 2001 From: CazSaa Date: Fri, 7 Mar 2025 10:04:53 +0100 Subject: [PATCH 2/5] BUG: render value of ADD constants in .dot graph --- dd/cudd_add.pyx | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/dd/cudd_add.pyx b/dd/cudd_add.pyx index 71b4a44b..81e44083 100644 --- a/dd/cudd_add.pyx +++ b/dd/cudd_add.pyx @@ -2259,7 +2259,7 @@ cdef class ADD: **kw ) -> None: """Write BDDs to `filename` as figure.""" - raise NotImplementedError() + # raise NotImplementedError() g = _to_dot(roots) g.dump( filename, @@ -2425,6 +2425,15 @@ cdef class Function: return None return self.agd._var_with_index[self._index] + @property + def value(self) -> float: + """Return value of leaf `node`. + + Raise `ValueError` if `node` + is nonleaf. + """ + return self.agd.value_of(self) + @property def level( self @@ -2979,7 +2988,7 @@ def _to_dot_recurse( return u_nd = umap.setdefault(u_int, len(umap)) if u.var is None: - label = 'FALSE' if u == u.agd.zero else 'TRUE' + label = str(u.value) else: label = u.var h = subgraphs[u.level] From d44e05c482ead6ba0cbecedad29e2e2857a71def Mon Sep 17 00:00:00 2001 From: CazSaa Date: Fri, 7 Mar 2025 10:09:03 +0100 Subject: [PATCH 3/5] remove redundant taillabels on edges --- dd/cudd_add.pyx | 2 -- 1 file changed, 2 deletions(-) diff --git a/dd/cudd_add.pyx b/dd/cudd_add.pyx index 81e44083..e9750e5a 100644 --- a/dd/cudd_add.pyx +++ b/dd/cudd_add.pyx @@ -3010,11 +3010,9 @@ def _to_dot_recurse( w_nd = umap[w_int] g.add_edge( u_nd, v_nd, - taillabel='0', style='dashed') g.add_edge( u_nd, w_nd, - taillabel='1', style='solid') From 334307e5eaa0f7f60cadefc3cc4613b6ab09d8d1 Mon Sep 17 00:00:00 2001 From: CazSaa Date: Fri, 7 Mar 2025 10:50:23 +0100 Subject: [PATCH 4/5] allow .dot output --- dd/cudd_add.pyx | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/dd/cudd_add.pyx b/dd/cudd_add.pyx index e9750e5a..09f1d42c 100644 --- a/dd/cudd_add.pyx +++ b/dd/cudd_add.pyx @@ -2200,7 +2200,7 @@ cdef class ADD: roots: list[Function], filetype: - _dd_abc.ImageFileType | + _dd_abc.ImageFileType | _ty.Literal['dot'] | None=None): """Write ADD as a diagram to file `filename`. @@ -2233,12 +2233,14 @@ cdef class ADD: filetype = 'png' elif name.endswith('.svg'): filetype = 'svg' + elif name.endswith('.dot'): + filetype = 'dot' else: raise ValueError( 'cannot infer file type ' 'from extension of file ' f'name "{filename}"') - if filetype in ('pdf', 'png', 'svg'): + if filetype in ('pdf', 'png', 'svg', 'dot'): self._dump_figure( roots, filename, filetype) else: @@ -2255,7 +2257,7 @@ cdef class ADD: filename: str, filetype: - _dd_abc.ImageFileType, + _dd_abc.ImageFileType | _ty.Literal['dot'], **kw ) -> None: """Write BDDs to `filename` as figure.""" From a14f348bff23cc3dbf3a92e08ee618451350bcee Mon Sep 17 00:00:00 2001 From: CazSaa Date: Fri, 7 Mar 2025 13:08:23 +0100 Subject: [PATCH 5/5] BUG: remove erroneous shortcut in `find_or_add` --- dd/cudd_add.pyx | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/dd/cudd_add.pyx b/dd/cudd_add.pyx index 09f1d42c..1db46d09 100644 --- a/dd/cudd_add.pyx +++ b/dd/cudd_add.pyx @@ -1605,16 +1605,13 @@ cdef class ADD: if level >= high.level: raise ValueError( level, high.level, 'high.level') - r: DdRef index = self._index_of_var[var] - if high == self.zero: - r = low.node - else: - r = cuddUniqueInter( - self.manager, index, - high.node, low.node) - if r is NULL: - raise CouldNotCreateNode() + + r = cuddUniqueInter( + self.manager, index, + high.node, low.node) + if r is NULL: + raise CouldNotCreateNode() f = wrap(self, r) if level > f.level: raise AssertionError( @@ -1636,8 +1633,6 @@ cdef class ADD: raise AssertionError('`low is NULL`') if high is NULL: raise AssertionError('`high is NULL`') - if high == Cudd_ReadZero(self.manager): - return low r = cuddUniqueInter( self.manager, index, high, low) if r is NULL: