Skip to content

A
abc
Commit e2411552 by Alan Mishchenko
Options

Experiments with cofactoring variables.

parent 1e76ebdf
Showing with 127 additions and 15 deletions
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 );
......
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) );
......
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 ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment