Version abc80402

3 files changed, 41 insertions, 31 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 1cc239b1..99c0276d 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -80,6 +80,7 @@ extern void            Dar_LibStart();
 extern void            Dar_LibStop();
 /*=== darBalance.c ========================================================*/
 extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
+extern Aig_Man_t *     Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
 extern void            Dar_BalancePrintStats( Aig_Man_t * p );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
@@ -94,7 +95,6 @@ extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbos
 extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
 extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
-extern Aig_Man_t *     Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 63f6f232..6e78041a 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -333,7 +333,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     if ( vSuper->nSize == 0 )
         return pObjOld->pData = Aig_ManConst0(pNew);
     if ( Vec_PtrSize(vSuper) < 2 )
-        printf( "BUG!\n" );
+        printf( "Dar_Balance_rec: Internal error!\n" );
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
     {
@@ -366,9 +366,11 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     Aig_Obj_t * pObj, * pDriver, * pObjNew;
     Vec_Vec_t * vStore;
     int i;
+    assert( Aig_ManVerifyTopoOrder(p) );
     // create the new manager 
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
@@ -439,6 +441,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
 
 /**Function*************************************************************
 
+  Synopsis    [Reproduces script "compress2".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
+{
+    Aig_Man_t * pAigXor, * pRes;
+    if ( fExor )
+    {
+        pAigXor = Aig_ManDupExor( pAig );
+        if ( fVerbose )
+            Dar_BalancePrintStats( pAigXor );
+        pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
+        Aig_ManStop( pAigXor );
+    }
+    else
+    {
+        pRes = Dar_ManBalance( pAig, fUpdateLevel );
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts a new node in the order by levels.]
 
   Description []
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 2a0aa7d5..7d78bf40 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -341,11 +341,19 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
 //Aig_ManPrintStats( pAig );
 
     Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pObj->pNext = pObj->pHaig;
         pObj->pHaig = pObj;
+    }
 
     pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
     Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
+
+    pAig = Vec_PtrEntry( vAigs, 1 );
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj->pNext;
+
     return vAigs;
 }
 
@@ -399,35 +407,6 @@ PRT( "Choicing time ", clock() - clk );
 //    return NULL;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Reproduces script "compress2".]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
-{
-    Aig_Man_t * pAigXor, * pRes;
-    if ( fExor )
-    {
-        pAigXor = Aig_ManDupExor( pAig );
-        if ( fVerbose )
-            Dar_BalancePrintStats( pAigXor );
-        pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
-        Aig_ManStop( pAigXor );
-    }
-    else
-    {
-        pRes = Dar_ManBalance( pAig, fUpdateLevel );
-    }
-    return pRes;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////