Version abc50807

2 files changed, 29 insertions, 0 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index ec4023b0..568eef7d 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -111,6 +111,7 @@ extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * suppor
 extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
 extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
 
 /*=== extraUtilFile.c ========================================================*/
 
diff --git a/src/misc/extra/extraUtilBdd.c b/src/misc/extra/extraUtilBdd.c
index 32fdca2c..38e3345c 100644
--- a/src/misc/extra/extraUtilBdd.c
+++ b/src/misc/extra/extraUtilBdd.c
@@ -656,6 +656,34 @@ DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc )
     return bRes;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
+{
+    DdNode * bTemp, * bProd;
+    int i;
+    assert( iStart <= iStop );
+    assert( iStart >= 0 && iStart <= dd->size );
+    assert( iStop >= 0  && iStop  <= dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    for ( i = iStart; i < iStop; i++ )
+    {
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/