Creating dedicated choice representation for GIA.

7 files changed, 122 insertions, 23 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d573afdc..4473921c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -117,6 +117,7 @@ struct Gia_Man_t_
     int *          pReprsOld;     // representatives (for CIs and ANDs)
     Gia_Rpr_t *    pReprs;        // representatives (for CIs and ANDs)
     int *          pNexts;        // next nodes in the equivalence classes
+    int *          pSibls;        // next nodes in the choice nodes
     int *          pIso;          // pairs of structurally isomorphic nodes
     int            nTerLoop;      // the state where loop begins  
     int            nTerStates;    // the total number of ternary states
@@ -570,6 +571,8 @@ static inline void        Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ a
 static inline void        Gia_ObjUnsetRepr( Gia_Man_t * p, int Id )          { p->pReprs[Id].iRepr = GIA_VOID;                                            }
 static inline int         Gia_ObjHasRepr( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr != GIA_VOID;                                    }
 static inline int         Gia_ObjReprSelf( Gia_Man_t * p, int Id )           { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id;                    }
+static inline int         Gia_ObjSibl( Gia_Man_t * p, int Id )               { return p->pSibls ? p->pSibls[Id] : 0;                                      }
+static inline Gia_Obj_t * Gia_ObjSiblObj( Gia_Man_t * p, int Id )            { return (p->pSibls && p->pSibls[Id]) ? Gia_ManObj(p, p->pSibls[Id]) : NULL; }
 
 static inline int         Gia_ObjProved( Gia_Man_t * p, int Id )             { return p->pReprs[Id].fProved;       }
 static inline void        Gia_ObjSetProved( Gia_Man_t * p, int Id )          { p->pReprs[Id].fProved = 1;          }
@@ -920,6 +923,7 @@ extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManPrint( Gia_Man_t * p );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
+extern void                Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 224d3bda..5dcc6038 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -42,7 +42,7 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Derives combinational miter of the two AIGs.]
+  Synopsis    [Duplicates AIG in the DFS order.]
 
   Description []
                
@@ -70,6 +70,34 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
             pNew->pNexts[iObjNew] = iNextNew;        
     }
 }
+Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Gia_ManStart( Aig_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
+    // create room to store equivalences
+    if ( p->pEquivs )
+        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->iData = 1;
+    Aig_ManForEachCi( p, pObj, i )
+        pObj->iData = Gia_ManAppendCi( pNew );
+    // add logic for the POs
+    Aig_ManForEachCo( p, pObj, i )
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+    Aig_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    if ( pNew->pNexts )
+        Gia_ManDeriveReprs( pNew );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -82,19 +110,38 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj == NULL || pObj->iData )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
+    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+    if ( Aig_ObjEquiv(p, pObj) )
+    {
+        int iObjNew, iNextNew;
+        iObjNew  = Abc_Lit2Var(pObj->iData);
+        iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
+        assert( iObjNew > iNextNew );
+        assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
+        pNew->pSibls[iObjNew] = iNextNew;        
+    }
+}
+Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
+    assert( p->pEquivs != NULL );
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
-    if ( p->pEquivs )
-        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+    pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
@@ -102,12 +149,11 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
         pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachCo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    if ( pNew->pNexts )
-        Gia_ManDeriveReprs( pNew );
+    assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
     return pNew;
 }
 
@@ -195,7 +241,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives combinational miter of the two AIGs.]
+  Synopsis    [Duplicates AIG in the DFS order.]
 
   Description []
                
@@ -228,18 +274,6 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
             pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
     }
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates AIG in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
 {
     Aig_Man_t * pNew;
@@ -541,7 +575,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
     Aig_Man_t * pNew;
     pNew = Gia_ManToAig( p, 0 );
     pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
-    pGia = Gia_ManFromAig( pNew );
+//    pGia = Gia_ManFromAig( pNew );
+    pGia = Gia_ManFromAigChoices( pNew );
     Aig_ManStop( pNew );
     return pGia;
 }
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index b72f6415..6498ec52 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -51,6 +51,7 @@ ABC_NAMESPACE_HEADER_START
 
 /*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t *         Gia_ManFromAigChoices( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSimple( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 494f9a1c..f82e7952 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -107,6 +107,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pReprsOld );
     ABC_FREE( p->pReprs );
     ABC_FREE( p->pNexts );
+    ABC_FREE( p->pSibls );
     ABC_FREE( p->pRefs );
 //    ABC_FREE( p->pNodeRefs );
     ABC_FREE( p->pHTable );
@@ -260,6 +261,35 @@ void Gia_ManPrintTents( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManPrintChoiceStats( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nEquivs = 0, nChoices = 0;
+    Gia_ManMarkFanoutDrivers( p );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjSibl(p, i) )
+            continue;
+        nEquivs++;
+        if ( pObj->fMark0 )
+            nChoices++;
+        assert( !Gia_ObjSiblObj(p, i)->fMark0 );
+        assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
+    }
+    Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
 {
     if ( p->pName )
@@ -289,6 +319,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
 //    Gia_ManSatExperiment( p );
     if ( p->pReprs && p->pNexts )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
+    if ( p->pSibls )
+        Gia_ManPrintChoiceStats( p );
     if ( p->pMapping )
         Gia_ManPrintMappingStats( p );
     if ( p->pPlacement )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index b0f25864..8389a9b0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1243,6 +1243,31 @@ int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Marks nodes that appear as faninis of other nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManCleanMark0( p );
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 783202e2..3f097ecc 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -95,7 +95,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
         pEquiv = Aig_ObjEquiv( pAig, pObj );
         if ( pEquiv == NULL )
             continue;
-        assert( pEquiv->Id > pObj->Id );
+        assert( pEquiv->Id < pObj->Id );
         nEquivs++;
     }
     return nEquivs;
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0d2e8c0d..b92de8a6 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -111,7 +111,9 @@ p->timeTotal = clock() - clkTotal;
     pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
     // count the number of representatives
     if ( pPars->fVerbose ) 
-        Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
+        Abc_Print( 1, "STATS:  Ands:%8d  ->%8d.  Reprs:%7d  ->%7d.  Choices =%7d.\n", 
+               Aig_ManNodeNum(pAig), 
+               Aig_ManNodeNum(pResult), 
                Dch_DeriveChoiceCountReprs( pAig ),
                Dch_DeriveChoiceCountEquivs( pResult ),
                Aig_ManChoiceNum( pResult ) );