Suggested bug fix in 'resub' with ODCs.

src/base/abci/abcOdc.c

@@ -44,12 +44,13 @@ struct Odc_Obj_t_
 
 struct Odc_Man_t_
 {
-    // dont'-care parameters
+    // don't-care parameters
     int                     nVarsMax;    // the max number of cut variables
     int                     nLevels;     // the number of ODC levels
     int                     fVerbose;    // the verbosiness flag
     int                     fVeryVerbose;// the verbosiness flag to print per-node stats
     int                     nPercCutoff; // cutoff percentage
+    int                     skipQuant;
 
     // windowing
     Abc_Obj_t *             pNode;       // the node for windowing
@@ -177,6 +178,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
     p->fVerbose     = fVerbose;
     p->fVeryVerbose = fVeryVerbose;
     p->nPercCutoff  = 10;
+    p->skipQuant    = 0;
 
     // windowing
     p->vRoots    = Vec_PtrAlloc( 128 );
@@ -744,7 +746,10 @@ unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uM
     // skip visited objects
     pObj = Odc_Lit2Obj( p, Lit );
     if ( Odc_ObjIsTravIdCurrent(p, pObj) )
+    {
+        p->skipQuant = 1;
         return pObj->uData;
+    }
     Odc_ObjSetTravIdCurrent(p, pObj);
     // skip objects out of the cone
     if ( (pObj->uMask & uMask) == 0 )
@@ -764,6 +769,7 @@ unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uM
     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
     uRes1 = Odc_And( p, uLit0, uLit1 );
     // find the result
+    p->skipQuant = 0;
     return pObj->uData = ((uRes1 << 16) | uRes0);
 }
 
@@ -783,6 +789,7 @@ int Abc_NtkDontCareQuantify( Odc_Man_t * p )
     Odc_Lit_t uRes0, uRes1;
     unsigned uData;
     int i;
+    p->skipQuant = 0;
     assert( p->iRoot < 0xffff );
     assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
     for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
@@ -790,6 +797,8 @@ int Abc_NtkDontCareQuantify( Odc_Man_t * p )
         // compute the cofactors w.r.t. this variable
         Odc_ManIncrementTravId( p );
         uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
+        if ( p->skipQuant ) 
+            continue;
         uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
         uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16),    Odc_IsComplement(p->iRoot) );
         // quantify this variable existentially