/**CFile****************************************************************
FileName [giaUnate.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Computation of structural unateness.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Flips the first bit in all entries of the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntFlopBit( Vec_Int_t * p )
{
int i;
for ( i = 0; i < p->nSize; i++ )
{
if ( i+1 < p->nSize && Abc_Lit2Var(p->pArray[i]) == Abc_Lit2Var(p->pArray[i+1]) )
i++; // skip variable appearing as both pos and neg literal
else
p->pArray[i] ^= 1;
}
return p;
}
/**Function*************************************************************
Synopsis [Compute unateness for all outputs in terms of inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Gia_ManCheckUnateVec( Gia_Man_t * p, Vec_Int_t * vCiIds, Vec_Int_t * vCoIds )
{
Vec_Int_t * vCiVec = vCiIds ? Vec_IntDup(vCiIds) : Vec_IntStartNatural(Gia_ManCiNum(p));
Vec_Int_t * vCoVec = vCoIds ? Vec_IntDup(vCoIds) : Vec_IntStartNatural(Gia_ManCoNum(p));
Vec_Wec_t * vUnatesCo = Vec_WecStart( Vec_IntSize(vCoVec) );
Vec_Wec_t * vUnates = Vec_WecStart( Gia_ManObjNum(p) );
Vec_Int_t * vUnate0, * vUnate1;
Gia_Obj_t * pObj; int i, CioId;
Vec_IntForEachEntry( vCiVec, CioId, i )
{
pObj = Gia_ManCi( p, CioId );
Vec_IntPush( Vec_WecEntry(vUnates, Gia_ObjId(p, pObj)), Abc_Var2Lit(CioId, 0) );
}
Gia_ManForEachAnd( p, pObj, i )
{
vUnate0 = Vec_WecEntry(vUnates, Gia_ObjFaninId0(pObj, i));
vUnate1 = Vec_WecEntry(vUnates, Gia_ObjFaninId1(pObj, i));
vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
vUnate1 = Gia_ObjFaninC1(pObj) ? Vec_IntFlopBit(vUnate1) : vUnate1;
Vec_IntTwoMerge2( vUnate0, vUnate1, Vec_WecEntry(vUnates, i) );
vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
vUnate1 = Gia_ObjFaninC1(pObj) ? Vec_IntFlopBit(vUnate1) : vUnate1;
}
Vec_IntForEachEntry( vCoVec, CioId, i )
{
pObj = Gia_ManCo( p, CioId );
vUnate0 = Vec_WecEntry(vUnates, Gia_ObjFaninId0p(p, pObj));
vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
Vec_IntAppend( Vec_WecEntry(vUnatesCo, i), vUnate0 );
vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
}
Vec_WecFree( vUnates );
Vec_IntFree( vCiVec );
Vec_IntFree( vCoVec );
return vUnatesCo;
}
/**Function*************************************************************
Synopsis [Checks unateness one function in one variable.]
Description [Returns 0 if Co is not unate in Ci.
Returns 1 if Co is neg-unate in Ci.
Returns 2 if Co is pos-unate in Ci.
Returns 3 if Co does not depend on Ci.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCheckUnate_rec( Gia_Man_t * p, int iObj )
{
Gia_Obj_t * pObj;
int Res0, Res1;
if ( p->nTravIds - p->pTravIds[iObj] <= 3 )
return p->nTravIds - p->pTravIds[iObj];
pObj = Gia_ManObj( p, iObj );
p->pTravIds[iObj] = p->nTravIds - 3;
if ( Gia_ObjIsCi(pObj) )
return 3;
Res0 = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId0(pObj, iObj) );
Res1 = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId1(pObj, iObj) );
Res0 = ((Res0 == 1 || Res0 == 2) && Gia_ObjFaninC0(pObj)) ? Res0 ^ 3 : Res0;
Res1 = ((Res1 == 1 || Res1 == 2) && Gia_ObjFaninC1(pObj)) ? Res1 ^ 3 : Res1;
p->pTravIds[iObj] = p->nTravIds - (Res0 & Res1);
assert( (Res0 & Res1) <= 3 );
return p->nTravIds - p->pTravIds[iObj];
}
int Gia_ManCheckUnate( Gia_Man_t * p, int iCiId, int iCoId )
{
int Res;
int CiObjId = Gia_ObjId(p, Gia_ManCi(p, iCiId));
int CoObjId = Gia_ObjId(p, Gia_ManCo(p, iCoId));
Gia_Obj_t * pCoObj = Gia_ManCo(p, iCoId);
Gia_ManIncrementTravId( p ); // Co does not depend on Ci.
Gia_ManIncrementTravId( p ); // Co is pos-unate in Ci
Gia_ObjSetTravIdCurrentId( p, CiObjId );
Gia_ManIncrementTravId( p ); // Co is neg-unate in Ci
Gia_ManIncrementTravId( p ); // Co is not unate in Ci
Res = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId0(pCoObj, CoObjId) );
return ((Res == 1 || Res == 2) && Gia_ObjFaninC0(pCoObj)) ? Res ^ 3 : Res;
}
/**Function*************************************************************
Synopsis [Testing procedure for all pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckUnateVecTest( Gia_Man_t * p, int fVerbose )
{
abctime clk = Abc_Clock();
Vec_Wec_t * vUnates = Gia_ManCheckUnateVec( p, NULL, NULL );
int i, o, Var, nVars = Gia_ManCiNum(p);
int nUnate = 0, nNonUnate = 0;
char * pBuffer = ABC_CALLOC( char, nVars+1 );
if ( fVerbose )
{
printf( "Inputs : " );
for ( i = 0; i < nVars; i++ )
printf( "%d", i % 10 );
printf( "\n" );
}
for ( o = 0; o < Gia_ManCoNum(p); o++ )
{
Vec_Int_t * vUnate = Vec_WecEntry( vUnates, o );
memset( pBuffer, ' ', (size_t)nVars );
Vec_IntForEachEntry( vUnate, Var, i )
if ( i+1 < Vec_IntSize(vUnate) && Abc_Lit2Var(Var) == Abc_Lit2Var(Vec_IntEntry(vUnate, i+1)) ) // both lits are present
pBuffer[Abc_Lit2Var(Var)] = '.', i++, nNonUnate++; // does not depend on this var
else
pBuffer[Abc_Lit2Var(Var)] = Abc_LitIsCompl(Var) ? 'n' : 'p', nUnate++;
if ( fVerbose )
printf( "Out%4d : %s\n", o, pBuffer );
}
ABC_FREE( pBuffer );
// print stats
printf( "Ins/Outs = %4d/%4d. Total supp = %5d. Total unate = %5d.\n",
Gia_ManCiNum(p), Gia_ManCoNum(p), nUnate+nNonUnate, nUnate );
ABC_PRT( "Total time", Abc_Clock() - clk );
//Vec_WecPrint( vUnates, 0 );
Vec_WecFree( vUnates );
}
/**Function*************************************************************
Synopsis [Testing procedure for one pair.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckUnateTest( Gia_Man_t * p, int fComputeAll, int fVerbose )
{
if ( fComputeAll )
Gia_ManCheckUnateVecTest( p, fVerbose );
else
{
abctime clk = Abc_Clock();
int i, o, nVars = Gia_ManCiNum(p);
int nUnate = 0, nNonUnate = 0;
char * pBuffer = ABC_CALLOC( char, nVars+1 );
if ( fVerbose )
{
printf( "Inputs : " );
for ( i = 0; i < nVars; i++ )
printf( "%d", i % 10 );
printf( "\n" );
}
for ( o = 0; o < Gia_ManCoNum(p); o++ )
{
for ( i = 0; i < nVars; i++ )
{
int Res = Gia_ManCheckUnate( p, i, o );
if ( Res == 3 ) pBuffer[i] = ' ';
else if ( Res == 2 ) pBuffer[i] = 'p', nUnate++;
else if ( Res == 1 ) pBuffer[i] = 'n', nUnate++;
else if ( Res == 0 ) pBuffer[i] = '.', nNonUnate++;
else assert( 0 );
}
if ( fVerbose )
printf( "Out%4d : %s\n", o, pBuffer );
}
ABC_FREE( pBuffer );
// print stats
printf( "Ins/Outs = %4d/%4d. Total supp = %5d. Total unate = %5d.\n",
Gia_ManCiNum(p), Gia_ManCoNum(p), nUnate+nNonUnate, nUnate );
ABC_PRT( "Total time", Abc_Clock() - clk );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END