Version abc70202

3 files changed, 101 insertions, 15 deletions

diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 9e944028..6aa7fa9f 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -152,6 +152,7 @@ struct Ivy_FraigParams_t_
 typedef struct Ivy_Cut_t_ Ivy_Cut_t;
 struct Ivy_Cut_t_
 {
+    int         nLatches;
     short       nSize;
     short       nSizeMax;
     int         pArray[IVY_CUT_INPUT];
@@ -541,6 +542,7 @@ extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj
 extern Ivy_Obj_t *     Ivy_ObjReal( Ivy_Obj_t * pObj );
 extern void            Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
 extern void            Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
+extern int             Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c
index 263a4398..0ee29fee 100644
--- a/src/aig/ivy/ivySeq.c
+++ b/src/aig/ivy/ivySeq.c
@@ -41,6 +41,11 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+//int nMoves;
+//int nMovesS;
+//int nClauses;
+//int timeInv;
+
 /**Function*************************************************************
 
   Synopsis    [Performs incremental rewriting of the AIG.]
@@ -58,6 +63,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
     int clk, clkStart = clock();
+
     // set the DC latch values
     Ivy_ManForEachLatch( p, pNode, i )
         pNode->Init = IVY_INIT_DC;
@@ -81,7 +87,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
 //        if ( Ivy_ObjIsBuf(pNode) )
 //            continue;
         // stop if all nodes have been tried once
-        if ( i > nNodes )
+        if ( i > nNodes ) 
             break;
         // for each cut, try to resynthesize it
         nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
@@ -114,6 +120,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
     return 1;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs rewriting for one node.]
@@ -140,11 +147,11 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
     Ivy_Cut_t * pCut;
     Ivy_Obj_t * pFanin;//, * pFanout;
     Vec_Ptr_t * vFanout;
-    unsigned uPhase, uTruthBest, uTruth;
+    unsigned uPhase, uTruthBest, uTruth;//, nNewClauses;
     char * pPerm;
     int nNodesSaved, nNodesSaveCur;
     int i, c, GainCur, GainBest = -1;
-    int clk, clk2;
+    int clk, clk2;//, clk3;
 
     p->nNodesConsidered++;
     // get the node's cuts
@@ -201,18 +208,6 @@ clk2 = clock();
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
 p->timeMffc += clock() - clk2;
-/*
-if ( pNode->Id == 8648 )
-{
-    int i;
-    printf( "Trying cut : {" );
-    for ( i = 0; i < pCut->nSize; i++ )
-        printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
-//    printf( " }\n" );
-    printf( " }   " );
-    Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
-}
-*/
 
         // evaluate the cut
 clk2 = clock();
@@ -252,6 +247,15 @@ p->timeRes += clock() - clk;
     }
 */
 
+//clk3 = clock();
+//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
+//timeInv += clock() - clk;
+
+//    nClauses += nNewClauses;
+//    nMoves++;
+//    if ( nNewClauses > 0 )
+//        nMovesS++;
+
     // copy the leaves
     Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
 
diff --git a/src/aig/ivy/ivyUtil.c b/src/aig/ivy/ivyUtil.c
index 0e44c216..ab62a276 100644
--- a/src/aig/ivy/ivyUtil.c
+++ b/src/aig/ivy/ivyUtil.c
@@ -731,6 +731,86 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
+{
+    int i;
+    printf( "Trying cut : {" );
+    for ( i = 0; i < pCut->nSize; i++ )
+        printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+    printf( " }   " );
+    Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
+{
+    Vec_Ptr_t * vArray;
+    Ivy_Obj_t * pObj, * pFanout;
+    int nLatches = 0;
+    int nPresent = 0;
+    int i, k;
+    int fVerbose = 0;
+
+    if ( fVerbose )
+        printf( "Trying cut : {" );
+    for ( i = 0; i < pCut->nSize; i++ )
+    {
+        if ( fVerbose )
+            printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+        nLatches += Ivy_LeafLat(pCut->pArray[i]);
+    }
+    if ( fVerbose )
+        printf( " }   " );
+    if ( fVerbose )
+        printf( "Latches = %d. ", nLatches );
+
+    // check if there are latches on the fanout edges
+    vArray = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < pCut->nSize; i++ )
+    {
+        pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
+        Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
+        {
+            if ( Ivy_ObjIsLatch(pFanout) )
+            {
+                nPresent++;
+                break;
+            }
+        }
+    }
+    Vec_PtrSize( vArray );
+    if ( fVerbose )
+    {
+        printf( "Present = %d. ", nPresent );
+        if ( nLatches > nPresent )
+            printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
+        printf( "\n" );
+    }
+    return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////