3 files changed, 28 insertions, 6 deletions

diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 6dd308f9..49ca963b 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -353,7 +353,18 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     // make sure the balanced node is not assigned
 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
     assert( pObjOld->pData == NULL );
-    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
+    if ( pNew->pManHaig != NULL )
+    {
+        Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
+//        printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
+//            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
+        assert( pObjNewR->pHaig != NULL );
+//        assert( pObjNewR->pHaig->pHaig == NULL );
+        assert( !Aig_IsComplement(pObjNewR->pHaig) );
+        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+    }
+    else
+        Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
     return pObjOld->pData = pObjNew;
 }
 
@@ -383,6 +394,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  p->pManHaig = NULL;
+        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig);
+    }
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -401,6 +418,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 // copy the PI
                 pObjNew = Aig_ObjCreatePi(pNew); 
                 pObj->pData = pObjNew;
+                pObjNew->pHaig = pObj->pHaig;
                 // set the arrival time of the new PI
                 arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
                 pObjNew->Level = (int)arrTime;
@@ -411,10 +429,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-                Aig_ObjCreatePo( pNew, pObjNew );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
                 Tim_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+                // create PO
+                pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
+                pObjNew->pHaig = pObj->pHaig;
             }
             else
                 assert( 0 );
@@ -429,13 +449,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             pObjNew = Aig_ObjCreatePi(pNew); 
             pObjNew->Level = pObj->Level;
             pObj->pData = pObjNew;
+            pObjNew->pHaig = pObj->pHaig;
         }
         Aig_ManForEachPo( p, pObj, i )
         {
             pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
             pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-            Aig_ObjCreatePo( pNew, pObjNew );
+            pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
+            pObjNew->pHaig = pObj->pHaig;
         }
     }
     Vec_VecFree( vStore );
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index b13c7313..e82cce22 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -133,7 +133,7 @@ p->timeCuts += clock() - clk;
             // remove the old cuts
             Dar_ObjSetCuts( pObj, NULL );
             // replace the node
-            Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+            Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
             continue;
         }
 
@@ -156,7 +156,7 @@ p->timeCuts += clock() - clk;
         pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+        Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 09b9b3a4..d19d48e4 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -582,7 +582,7 @@ p->timeEval += clock() - clk;
         pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+        Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );