Structural reparametrization.

1 files changed, 312 insertions, 28 deletions

diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c
index dbd3b628..7ef314ea 100644
--- a/src/proof/abs/absRpm.c
+++ b/src/proof/abs/absRpm.c
@@ -26,12 +26,190 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int   Gia_ObjDom( Gia_Man_t * p, Gia_Obj_t * pObj )            { return Vec_IntEntry(p->vDoms, Gia_ObjId(p, pObj));   }
+static inline void  Gia_ObjSetDom( Gia_Man_t * p, Gia_Obj_t * pObj, int d )  { Vec_IntWriteEntry(p->vDoms, Gia_ObjId(p, pObj), d);  }
+
+static int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp );
+static int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
+static int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Collects non-trivial internal dominators of the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj;
+    int Level, LevelMax = 2;
+    int i, iDom, iDomNext;
+    vNodes = Vec_IntAlloc( 100 );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( !pObj->fMark0 )
+            continue;
+        iDom = Gia_ObjDom(p, pObj);
+        if ( iDom == Gia_ObjId(p, pObj) )
+            continue;
+        for ( Level = 0; Level < LevelMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Level++ )
+        {
+            Vec_IntPush( vNodes, iDom );
+            iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom) );
+            if ( iDomNext == iDom )
+                break;
+            iDom = iDomNext;
+        }
+    }
+    Vec_IntUniqify( vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes one-node dominators.]
+
+  Description [For each node, computes the closest one-node dominator,
+  which can be the node itself if the node has no other dominators.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManAddDom( Gia_Man_t * p, Gia_Obj_t * pObj, int iDom0 )
+{
+    int iDom1, iDomNext;
+    if ( Gia_ObjDom(p, pObj) == -1 )
+    {
+        Gia_ObjSetDom( p, pObj, iDom0 );
+        return;
+    }
+    iDom1 = Gia_ObjDom( p, pObj );
+    while ( 1 )
+    {
+        if ( iDom0 > iDom1 )
+        {
+            iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom1) );
+            if ( iDomNext == iDom1 )
+                break;
+            iDom1 = iDomNext;
+            continue;
+        }
+        if ( iDom1 > iDom0 )
+        {
+            iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom0) );
+            if ( iDomNext == iDom0 )
+                break;
+            iDom0 = iDomNext;
+            continue;
+        }
+        assert( iDom0 == iDom1 );
+        Gia_ObjSetDom( p, pObj, iDom0 );
+        return;
+    }
+    Gia_ObjSetDom( p, pObj, Gia_ObjId(p, pObj) );
+}
+void Gia_ManComputeDoms( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->vDoms == NULL )
+        p->vDoms = Vec_IntAlloc( 0 );
+    Vec_IntFill( p->vDoms, Gia_ManObjNum(p), -1 );
+    Gia_ManForEachObjReverse( p, pObj, i )
+    {
+        if ( i == 0 || Gia_ObjIsCi(pObj) )
+            continue;
+        if ( pObj->fMark0 || (p->pRefs && Gia_ObjRefs(p, pObj) == 0) )
+            continue;
+        if ( Gia_ObjIsCo(pObj) )
+        {
+            Gia_ObjSetDom( p, pObj, i );
+            Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
+            continue;
+        }
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
+        Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i );
+    }
+}
+void Gia_ManTestDoms2( Gia_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj, * pDom;
+    clock_t clk = clock();
+    int i;
+    assert( p->vDoms == NULL );
+    Gia_ManComputeDoms( p );
+/*
+    Gia_ManForEachPi( p, pObj, i )
+        if ( Gia_ObjId(p, pObj) != Gia_ObjDom(p, pObj) )
+            printf( "PI =%6d  Id =%8d. Dom =%8d.\n", i, Gia_ObjId(p, pObj), Gia_ObjDom(p, pObj) );
+*/
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
+    Gia_ManCleanMark0( p );
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->fMark0 = 1;
+    vNodes = Vec_IntAlloc( 100 );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        if ( Gia_ObjId(p, pObj) == Gia_ObjDom(p, pObj) )
+            continue;
+
+        pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj));
+        if ( Gia_ObjIsCo(pDom) )
+        {
+            assert( Gia_ObjFanin0(pDom) == pObj );
+            continue;
+        }
+        assert( Gia_ObjIsAnd(pDom) );
+        Abs_GiaObjDeref_rec( p, pDom );
+        Abs_ManSupport( p, pDom, vNodes );
+        Abs_GiaObjRef_rec( p, pDom );
+
+        if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) == -1 )
+            printf( "FAILURE.\n" );
+//        else
+//            printf( "Success.\n" );
+    }
+    Vec_IntFree( vNodes );
+    Gia_ManCleanMark0( p );
+}
+
+void Gia_ManTestDoms( Gia_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->vDoms == NULL );
+    Gia_ManComputeDoms( p );
+    // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
+    Gia_ManCleanMark0( p );
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->fMark0 = 1;
+    vNodes = Gia_ManCollectDoms( p );
+//    Vec_IntPrint( vNodes );
+    printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) );
+    Vec_IntFree( vNodes );
+    Gia_ManCleanMark0( p );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -41,22 +219,22 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnPis, int * pnNodes )
+void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPis, Vec_Int_t * vAnds )
 {
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
         return;
     Gia_ObjSetTravIdCurrent(p, pObj);
     if ( pObj->fMark0 )
     {
-        (*pnPis)++;
+        Vec_IntPush( vPis, Gia_ObjId(p, pObj) );
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes );
-    Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), pnPis, pnNodes );
-    (*pnNodes)++;
+    Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds );
+    Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), vPis, vAnds );
+    Vec_IntPush( vAnds, Gia_ObjId(p, pObj) );
 }
-void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
+void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds )
 {
     Gia_Obj_t * pObj;
     int i;
@@ -66,9 +244,10 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
     Gia_ManForEachRo( p, pObj, i )
         Gia_ObjSetTravIdCurrent( p, pObj );
     // count PIs and internal nodes reachable from COs
-    *pnPis = *pnNodes = 0;
+    Vec_IntClear( vPis );
+    Vec_IntClear( vAnds );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes );
+        Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds );
 }
 
 /**Function*************************************************************
@@ -82,7 +261,7 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
+void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
 {
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
         return;
@@ -93,6 +272,40 @@ void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
+    Abs_ManSupport2_rec( p, Gia_ObjFanin0(pObj), vSupp );
+    Abs_ManSupport2_rec( p, Gia_ObjFanin1(pObj), vSupp );
+}
+int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+    assert( Gia_ObjIsAnd(pObj) );
+    Vec_IntClear( vSupp );
+    Gia_ManIncrementTravId( p );
+    Abs_ManSupport2_rec( p, pObj, vSupp );
+    return Vec_IntSize(vSupp);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( pObj->fMark0 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 )
+    {
+        Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
     Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
     Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
 }
@@ -101,7 +314,8 @@ int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
     assert( Gia_ObjIsAnd(pObj) );
     Vec_IntClear( vSupp );
     Gia_ManIncrementTravId( p );
-    Abs_ManSupport_rec( p, pObj, vSupp );
+    Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp );
+    Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp );
     return Vec_IntSize(vSupp);
 }
 
@@ -167,7 +381,10 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
     int i, RetValue;
     Gia_ManForEachObjVec( vSupp, p, pObj, i )
         if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves
+        {
+            assert( pObj->fMark0 );
             Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
+        }
     RetValue = Vec_IntSize(vSupp) - nSize;
     Gia_ManForEachObjVec( vSupp, p, pObj, i )
         if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves
@@ -296,16 +513,18 @@ word Abs_GiaComputeTruth( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Ve
 ***********************************************************************/
 void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
 {
-    Vec_Int_t * vSupp;
+    Vec_Int_t * vSupp, * vPis, * vAnds;
     Vec_Wrd_t * vTruths;
     Gia_Obj_t * pObj;
     word uTruth;
-    int Iter, i, nPis, nNodes, nSize0;
+    int Iter, i, nSize0;
     int fChanges = 1;
     Gia_ManCreateRefs( p );
     Gia_ManCleanMark0( p );
     Gia_ManForEachPi( p, pObj, i )
         pObj->fMark0 = 1;
+    vPis = Vec_IntAlloc( 100 );
+    vAnds = Vec_IntAlloc( 100 );
     vSupp = Vec_IntAlloc( 100 );
     vTruths = Vec_WrdAlloc( 100 );
     for ( Iter = 0; fChanges; Iter++ )
@@ -313,16 +532,16 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
         // count the number of PIs and internal nodes
         if ( fVerbose )
         {
-            Gia_ManCountPisNodes( p, &nPis, &nNodes );
+            Gia_ManCountPisNodes( p, vPis, vAnds );
             printf( "Iter %3d : ", Iter );
-            printf( "PI = %5d  ",  nPis );
-            printf( "And = %6d  ", nNodes );
+            printf( "PI = %5d  ",  Vec_IntSize(vPis) );
+            printf( "And = %6d  ", Vec_IntSize(vAnds) );
             printf( "\n" );
         }
 
         fChanges = 0;
         Gia_ManCleanMark1( p );
-//        pObj = Gia_ObjFanin0( Gia_ManPo(p, 0) );
+//        pObj = Gia_ObjFanin0( Gia_ManPo(p, 1) );
         Gia_ManForEachAnd( p, pObj, i )
         {
             if ( pObj->fMark0 )
@@ -334,18 +553,22 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
                 pObj->fMark1 = 1;
                 continue;
             }
-            if ( Abs_ManSupport(p, pObj, vSupp) > nCutMax )
+
+            // dereference nodes
+            Abs_GiaObjDeref_rec( p, pObj );
+            // compute support
+            Abs_ManSupport( p, pObj, vSupp );
+            // check support size
+            if ( Vec_IntSize(vSupp) > nCutMax )
             {
+                Abs_GiaObjRef_rec( p, pObj );
                 pObj->fMark1 = 1;
                 continue;
             }
-
-            // pObj has structural support no more than nCutMax
-            Abs_GiaObjDeref_rec( p, pObj );
-            // sort support nodes by ref count
+            // order nodes by their ref counts
             nSize0 = Abs_GiaSortNodes( p, vSupp );
-            // check how many support nodes have ref count 0
-            if ( nSize0 == 0 )
+            // quit if there is no removable or too many
+            if ( nSize0 == 0 || nSize0 > nCutMax )
             {
                 Abs_GiaObjRef_rec( p, pObj );
                 continue;
@@ -358,30 +581,91 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
             if ( !Abs_GiaCheckTruth( &uTruth, Vec_IntSize(vSupp), nSize0 ) ) // has const
             {
                 Abs_GiaObjRef_rec( p, pObj );
-//            printf( "  no\n" );
+/*
+                if ( Iter == 1 )
+                {
+                    printf( "Node = %8d   Supp = %2d   Supp0 = %2d   ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 );
+                    Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) );
+                    printf( "  no\n" );
+                }
+*/
                 continue;
             }
+/*
             printf( "Node = %8d   Supp = %2d   Supp0 = %2d   ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 );
             Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) );
             printf( "  yes\n" );
-
+*/
             // pObj can be reparamed
             pObj->fMark0 = 1;
             fChanges = 1;
         }
     }
+    Vec_IntFree( vPis );
+    Vec_IntFree( vAnds );
     Vec_IntFree( vSupp );
     Vec_WrdFree( vTruths );
     ABC_FREE( p->pRefs );
-    Gia_ManCleanMark0( p ); // temp
+//    Gia_ManCleanMark0( p ); // temp
     Gia_ManCleanMark1( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Assumed that fMark0 marks the internal PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p )
+{
+    Vec_Int_t * vPis, * vAnds;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    vPis = Vec_IntAlloc( 100 );
+    vAnds = Vec_IntAlloc( 100 );
+    Gia_ManCountPisNodes( p, vPis, vAnds );
+
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Gia_ManForEachObjVec( vPis, p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // create flops
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create COs
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+
+    Vec_IntFree( vPis );
+    Vec_IntFree( vAnds );
+    return pNew;
+}
+
 Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose )
 {
-//    Abs_GiaTest( p, nCutMax, fVerbose );
-    Abs_RpmPerformMark( p, nCutMax, 1 );
+    Gia_Man_t * pNew;
+
+    Gia_ManTestDoms( p );
     return NULL;
+
+    Abs_RpmPerformMark( p, nCutMax, 1 );
+    pNew = Gia_ManDupRpm( p );
+    Gia_ManCleanMark0( p );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////