1 files changed, 77 insertions, 0 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 932ed525..7d806ec7 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -719,6 +719,83 @@ DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode **
     return bResult;
 }  /* end of Extra_bddBitsToCube */
 
+/**Function********************************************************************
+
+  Synopsis    [Finds the support as a negative polarity cube.]
+
+  Description [Finds the variables on which a DD depends. Returns a BDD 
+  consisting of the product of the variables in the negative polarity 
+  if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_VectorSupport Cudd_Support]
+
+******************************************************************************/
+DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
+{
+    int *support;
+    DdNode *res, *tmp, *var;
+    int i, j;
+    int size;
+
+    /* Allocate and initialize support array for ddSupportStep. */
+    size = ddMax( dd->size, dd->sizeZ );
+    support = ALLOC( int, size );
+    if ( support == NULL )
+    {
+        dd->errorCode = CUDD_MEMORY_OUT;
+        return ( NULL );
+    }
+    for ( i = 0; i < size; i++ )
+    {
+        support[i] = 0;
+    }
+
+    /* Compute support and clean up markers. */
+    ddSupportStep( Cudd_Regular( f ), support );
+    ddClearFlag( Cudd_Regular( f ) );
+
+    /* Transform support from array to cube. */
+    do
+    {
+        dd->reordered = 0;
+        res = DD_ONE( dd );
+        cuddRef( res );
+        for ( j = size - 1; j >= 0; j-- )
+        {                        /* for each level bottom-up */
+            i = ( j >= dd->size ) ? j : dd->invperm[j];
+            if ( support[i] == 1 )
+            {
+                var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) );
+                //////////////////////////////////////////////////////////////////
+                var = Cudd_Not(var);
+                //////////////////////////////////////////////////////////////////
+                cuddRef( var );
+                tmp = cuddBddAndRecur( dd, res, var );
+                if ( tmp == NULL )
+                {
+                    Cudd_RecursiveDeref( dd, res );
+                    Cudd_RecursiveDeref( dd, var );
+                    res = NULL;
+                    break;
+                }
+                cuddRef( tmp );
+                Cudd_RecursiveDeref( dd, res );
+                Cudd_RecursiveDeref( dd, var );
+                res = tmp;
+            }
+        }
+    }
+    while ( dd->reordered == 1 );
+
+    FREE( support );
+    if ( res != NULL )
+        cuddDeref( res );
+    return ( res );
+
+}                                /* end of Extra_SupportNeg */
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/