Version abc70731

5 files changed, 52 insertions, 5 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 44dd2788..923ffc12 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -85,6 +85,7 @@ extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
 /*=== darScript.c ========================================================*/
+extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 097f1a4d..9c0997b8 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -54,6 +54,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     int i;
     // create the new manager 
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index b74f570c..dec9bff7 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -42,7 +42,7 @@
 void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
 {
     memset( pPars, 0, sizeof(Dar_RwrPar_t) );
-    pPars->nCutsMax     =  8;
+    pPars->nCutsMax     =  8; // 8
     pPars->nSubgMax     =  5; // 5 is a "magic number"
     pPars->fFanout      =  1;
     pPars->fUpdateLevel =  0;
@@ -151,8 +151,8 @@ p->timeCuts += clock() - clk;
         Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
         nNodeBefore = Aig_ManNodeNum( pAig );
-        pObjNew = Dar_LibBuildBest( p );
-        pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
+        pObjNew = Dar_LibBuildBest( p ); // pObjNew can be complemented!
+        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 );
@@ -183,6 +183,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     }
     // stop the rewriting manager
     Dar_ManStop( p );
+    Aig_ManCheckPhase( pAig );
     // check
     if ( !Aig_ManCheck( pAig ) )
     {
@@ -209,9 +210,12 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, clk = 0, clkStart = clock();
+    int i, nNodes, clk = 0, clkStart = clock();
     // remove dangling nodes
-    Aig_ManCleanup( pAig );
+    if ( nNodes = Aig_ManCleanup( pAig ) )
+    {
+//        printf( "Removing %d nodes.\n", nNodes );
+    }
     // create default parameters
     Dar_ManDefaultRwrParams( pPars );
     pPars->nCutsMax = nCutsMax;
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index fbd12cae..b304fe34 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -361,6 +361,21 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         Aig_ObjCollectCut( pObj, vCut, p->vCutNodes );
         // get the truth table
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
+        if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
+        {
+            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->pGraphBest = Kit_GraphCreateConst0();
+            Vec_PtrCopy( p->vLeavesBest, vCut );
+            return p->GainBest;
+        }
+        if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
+        {
+            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->pGraphBest = Kit_GraphCreateConst1();
+            Vec_PtrCopy( p->vLeavesBest, vCut );
+            return p->GainBest;
+        }
+
         // try the positive phase
         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
         if ( RetValue > -1 )
@@ -559,6 +574,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
     // stop the rewriting manager
     Dar_ManRefStop( p );
+    Aig_ManCheckPhase( pAig );
     if ( !Aig_ManCheck( pAig ) )
     {
         printf( "Dar_ManRefactor: The network check has failed.\n" );
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 75076981..2fe39860 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -30,6 +30,30 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pTemp;
+    Dar_RwrPar_t Pars, * pPars = &Pars;
+    Dar_ManDefaultRwrParams( pPars );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    Dar_ManRewrite( pAig, pPars );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    return pAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reproduces script "compress2".]
 
   Description []