Version abc80921

2 files changed, 10 insertions, 5 deletions

diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index 66c7f7b9..07196259 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -50,13 +50,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     assert( !Aig_IsComplement(pOld) );
     assert( pNew != pOld );
 
-//    p->nCallsSince++;  // experiment with this!!!
+    p->nCallsSince++;  // experiment with this!!!
     
     // check if SAT solver needs recycling
     if ( p->pSat == NULL || 
         (p->pPars->nSatVarMax && 
          p->nSatVars > p->pPars->nSatVarMax && 
-         ++p->nCallsSince > p->pPars->nCallsRecycle) )
+         p->nCallsSince > p->pPars->nCallsRecycle) )
         Dch_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 7a6865bd..61d2ab93 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -60,10 +60,10 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vSimRoots, pObj );
         return;
     }
-    // pRepr is the representative of the equivalence class
-    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
+    // pRepr is the representative of an equivalence class
+    if ( pRepr->fMarkA )
         return;
-    Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
+    pRepr->fMarkA = 1;
     Vec_PtrPush( p->vSimClasses, pRepr );
 }
 
@@ -80,6 +80,8 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
 {
+    Aig_Obj_t * pObj;
+    int i;
     Vec_PtrClear( p->vSimRoots );
     Vec_PtrClear( p->vSimClasses );
     Aig_ManIncrementTravId( p->pAigTotal );
@@ -88,6 +90,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
     Dch_ManCollectTfoCands_rec( p, pObj2 );
     Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
     Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
+    Vec_PtrForEachEntry( p->vSimClasses, pObj, i )
+        pObj->fMarkA = 0;
 }
 
 /**Function*************************************************************
@@ -116,6 +120,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
         // get the value from the SAT solver
         // (account for the fact that some vars may be minimized away)
         pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+//        pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
         return;
     }
     Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );