6 files changed, 63 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                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h
index 7bfded4a..451724d6 100644
--- a/src/misc/vec/vecFan.h
+++ b/src/misc/vec/vecFan.h
@@ -57,6 +57,8 @@ struct Vec_Fan_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_FanForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_FanSize(vVec)) && (((Entry) = Vec_FanEntry(vVec, i)), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 8cca2b29..975b61cf 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -48,6 +48,9 @@ struct Vec_Int_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_IntForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 0ba1bdc5..eb551d1c 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -48,6 +48,9 @@ struct Vec_Ptr_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
+    for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -418,6 +421,29 @@ static inline void * Vec_PtrPop( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Moves the first nItems to the end.]
 
   Description []
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 367304d4..33be5f1d 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -48,6 +48,9 @@ struct Vec_Str_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_StrForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ )   
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////