Adding frontier comptuation based on reversed CO order in &ps.

src/aig/gia/gia.h

@@ -906,7 +906,7 @@ extern int                 Gia_ManLevelNum( Gia_Man_t * p );
 extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
-extern int                 Gia_ManCrossCut( Gia_Man_t * p );
+extern int                 Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );

src/aig/gia/giaFront.c

@@ -103,13 +103,54 @@ void Gia_ManFrontTransform( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManCrossCutSimple( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nCutCur = 0, nCutMax = 0;
+    Gia_ManCreateValueRefs( p );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( pObj->Value )
+            nCutCur++;
+        if ( nCutMax < nCutCur )
+            nCutMax = nCutCur;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+                nCutCur--;
+            if ( --Gia_ObjFanin1(pObj)->Value == 0 )
+                nCutCur--;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+                nCutCur--;
+        }
+    }
+//    Gia_ManForEachObj( p, pObj, i )
+//        assert( pObj->Value == 0 );
+    return nCutMax;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
     char * pFront;    // places used for the frontier
     int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
-    int nCrossCutMaxInit = Gia_ManCrossCut( p );
+    int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
     int iFront = 0;//, clk = clock(); 
     // set references for all objects
     Gia_ManCreateValueRefs( p );

src/aig/gia/giaMan.c

@@ -271,7 +271,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
         printf( "  ff =%7d", Gia_ManRegNum(p) );
     printf( "  and =%8d", Gia_ManAndNum(p) );
     printf( "  lev =%5d", Gia_ManLevelNum(p) ); Vec_IntFreeP( &p->vLevels );
-    printf( "  cut =%5d", Gia_ManCrossCut(p) );
+    printf( "  cut = %d(%d)", Gia_ManCrossCut(p, 0), Gia_ManCrossCut(p, 1) );
 //    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
     printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
     if ( Gia_ManHasDangling(p) )

src/aig/gia/giaUtil.c

@@ -574,7 +574,7 @@ void Gia_ManDfsForCrossCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNo
     Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
     Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
 }
-Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p )
+Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p, int fReverse )
 {
     Vec_Int_t * vNodes;
     Gia_Obj_t * pObj;
@@ -582,17 +582,26 @@ Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p )
     Gia_ManCleanValue( p );
     vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
     Gia_ManIncrementTravId( p );
-    Gia_ManForEachCo( p, pObj, i )
-        if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
-            Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
+    if ( fReverse )
+    {
+        Gia_ManForEachCoReverse( p, pObj, i )
+            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
+    }
+    else
+    {
+        Gia_ManForEachCo( p, pObj, i )
+            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
+    }
     return vNodes;
 }
-int Gia_ManCrossCut( Gia_Man_t * p )
+int Gia_ManCrossCut( Gia_Man_t * p, int fReverse )
 {
     Vec_Int_t * vNodes;
     Gia_Obj_t * pObj;
     int i, nCutCur = 0, nCutMax = 0;
-    vNodes = Gia_ManDfsForCrossCut( p );
+    vNodes = Gia_ManDfsForCrossCut( p, fReverse );
     Gia_ManForEachObjVec( vNodes, p, pObj, i )
     {
         if ( pObj->Value )