Experiments with cofactoring variables.

3 files changed, 127 insertions, 15 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f7e27a08..ac0529ce 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1031,7 +1031,8 @@ extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
-extern Gia_Man_t *         Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value );  
+extern Gia_Man_t *         Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value );  
+extern Gia_Man_t *         Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value );  
 extern Gia_Man_t *         Gia_ManDupExist( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 86d8039f..269c2215 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1192,7 +1192,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG in the DFS order while rehashing.]
+  Synopsis    [Cofactors w.r.t. a primary input variable.]
 
   Description []
                
@@ -1201,16 +1201,16 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManDupCofactor_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManDupCofactorVar_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin1(pObj) );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
-Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
+Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -1227,7 +1227,7 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
     Gia_ManPi( p, iVar )->Value = Value; // modification!
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
@@ -1239,6 +1239,47 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
 
 /**Function*************************************************************
 
+  Synopsis    [Cofactors w.r.t. an internal node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, iObjValue = -1;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( iObj > 0 && iObj < Gia_ManObjNum(p) );
+    assert( Gia_ObjIsCand(Gia_ManObj(p, iObj)) );
+    assert( Value == 0 || Value == 1 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), iObjValue) );
+        if ( i == iObj )
+            iObjValue = Abc_LitNotCond(pObj->Value, !Value), pObj->Value = Value;
+    }
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Existentially quantified given variable.]
 
   Description []
@@ -1312,7 +1353,7 @@ Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
     // first part
     Gia_ManPi( p, iVar )->Value = 0; // modification!
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ObjFanin0Copy(pObj);
     // second part
@@ -1320,7 +1361,7 @@ Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
     Gia_ManForEachAnd( p, pObj, i )
         pObj->Value = ~0;
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
     // combination
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 9060a6d3..e5e9a9a4 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -228,11 +228,11 @@ int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost
     LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
     for ( i = 0; i < LookAhead; i++ )
     {
-        pPart = Gia_ManDupCofactor( p, pOrder[i], 0 );
+        pPart = Gia_ManDupCofactorVar( p, pOrder[i], 0 );
         Cost0 = Gia_ManAndNum(pPart);
         Gia_ManStop( pPart );
 
-        pPart = Gia_ManDupCofactor( p, pOrder[i], 1 );
+        pPart = Gia_ManDupCofactorVar( p, pOrder[i], 1 );
         Cost1 = Gia_ManAndNum(pPart);
         Gia_ManStop( pPart );
 
@@ -434,7 +434,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
         int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
         int nFanouts, Cost, iVar  = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
         // cofactor
-        Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
+        Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
         if ( pLast->vCofVars == NULL )
             pLast->vCofVars = Vec_IntAlloc( 100 );
         // print results
@@ -470,7 +470,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
         else               // UNDEC
             Vec_PtrPush( vStack, pPart );
         // cofactor
-        pPart = Gia_ManDupCofactor( pLast, iVar, 1 );
+        pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
         // create variable
         pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
         Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
@@ -644,7 +644,7 @@ int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax,
                     // determine cofactoring variable
                     int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
                     // cofactor
-                    Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
+                    Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
                     pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
                     Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
                     Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
@@ -658,7 +658,7 @@ int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax,
 //                        Cec_GiaSplitPrintRefs( pPart );
                     }
                     // cofactor
-                    pPart = Gia_ManDupCofactor( pLast, iVar, 1 );
+                    pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
                     pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
                     Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
                     Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
@@ -752,6 +752,76 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Print stats about cofactoring variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_GiaPrintCofStats( Gia_Man_t * p )
+{
+    Gia_Man_t * pCof0, * pCof1;
+    Gia_Obj_t * pObj, * pFan0, * pFan1, * pCtrl;
+    Vec_Int_t * vMarks;
+    int i, Count = 0;
+    vMarks = Vec_IntStart( Gia_ManObjNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjIsMuxType(pObj) )
+            continue;
+        if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        pCtrl = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
+        pCtrl = Gia_Regular(pCtrl);
+        Vec_IntAddToEntry( vMarks, Gia_ObjId(p, pCtrl), 1 );
+    }
+    printf( "The AIG with %d candidate nodes (PI+AND) has %d unique MUX control drivers:\n", 
+        Gia_ManCandNum(p), Vec_IntCountPositive(vMarks) );
+    Gia_ManLevelNum( p );
+    Gia_ManForEachCand( p, pObj, i )
+    {
+        if ( !Vec_IntEntry(vMarks, i) )
+            continue;
+        pCof0 = Gia_ManDupCofactorObj( p, i, 0 );
+        pCof1 = Gia_ManDupCofactorObj( p, i, 1 );
+        printf( "%6d :   ",          Count++ );
+        printf( "Obj = %6d   ",      i );
+        printf( "MUX refs = %5d   ", Vec_IntEntry(vMarks, i) );
+        printf( "Level = %5d   ",    Gia_ObjLevelId(p, i) );
+        printf( "Cof0 = %7d   ",     Gia_ManAndNum(pCof0) );
+        printf( "Cof1 = %7d   ",     Gia_ManAndNum(pCof1) );
+        printf( "\n" );
+        Gia_ManStop( pCof0 );
+        Gia_ManStop( pCof1 );
+    }
+    Vec_IntFree( vMarks );
+}
+void Cec_GiaPrintCofStats2( Gia_Man_t * p )
+{
+    Gia_Man_t * pCof0, * pCof1;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManLevelNum( p );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        pCof0 = Gia_ManDupCofactorVar( p, i, 0 );
+        pCof1 = Gia_ManDupCofactorVar( p, i, 1 );
+        printf( "PI %5d :   ",   i );
+        printf( "Refs = %5d   ", Gia_ObjRefNum(p, pObj) );
+        printf( "Cof0 = %7d   ", Gia_ManAndNum(pCof0) );
+        printf( "Cof1 = %7d   ", Gia_ManAndNum(pCof1) );
+        printf( "\n" );
+        Gia_ManStop( pCof0 );
+        Gia_ManStop( pCof1 );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////