Enabling AIGs without structural hashing.

This commit is contained in:
Alan Mishchenko 2016-05-20 16:23:48 -07:00
parent 27c44fd644
commit 3b62ee4575
9 changed files with 41 additions and 27 deletions

View File

@ -1204,7 +1204,7 @@ extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p );

View File

@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
}
}
pInit[i] = 0;
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );

View File

@ -2618,7 +2618,7 @@ Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@ -2635,6 +2635,7 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->fGiaSimple = fGiaSimple;
Gia_ManConst0(p)->Value = 0;
// create primary inputs
Gia_ManForEachPi( p, pObj, i )
@ -2707,7 +2708,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
assert( pInit[i] == 'x' || pInit[i] == 'X' );
// normalize the manager
pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), fVerbose );
pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose );
// create new init string
pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )

View File

@ -666,10 +666,15 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
{
int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
if ( p->fGiaSimple )
return Gia_ManHashOr(p, Gia_ManHashAnd(p, iLit0, Abc_LitNot(iLit1)), Gia_ManHashAnd(p, Abc_LitNot(iLit0), iLit1) );
else
{
int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
}
}
/**Function*************************************************************
@ -685,14 +690,19 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
{
int iTemp0, iTemp1, fCompl = 0;
if ( iData0 > iData1 )
iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
if ( Abc_LitIsCompl(iData1) )
iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
if ( p->fGiaSimple )
return Gia_ManHashOr(p, Gia_ManHashAnd(p, iCtrl, iData1), Gia_ManHashAnd(p, Abc_LitNot(iCtrl), iData0) );
else
{
int iTemp0, iTemp1, fCompl = 0;
if ( iData0 > iData1 )
iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
if ( Abc_LitIsCompl(iData1) )
iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
}
}
/**Function*************************************************************

View File

@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose )
Gia_ManStop( pTemp );
// add initial state
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 );
Gia_ManStop( pTemp );
Vec_StrFree( vInit );
/*

View File

@ -871,7 +871,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
pInit[i] = 'X';
}
pInit[i] = 0;
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );

View File

@ -26761,7 +26761,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
Aig_ManStop( pAig );
// perform undc/zero
pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, fVerbose );
pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose );
Gia_ManStop( pTemp );
ABC_FREE( pInits );
}
@ -32141,7 +32141,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp;
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
pTemp = Gia_ManTransformToDual( pAbc->pGia );
pTemp = Gia_ManDemiterToDual( pAbc->pGia );
pAbc->Status = Cec_ManVerify( pTemp, pPars );
ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
Gia_ManStop( pTemp );

View File

@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
{
Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
Vec_StrPush( vInit, '\0' );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
Vec_StrFreeP( &vInit );

View File

@ -274,10 +274,10 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
{
int And1 = Gia_ManHashAnd(pNew, a, b);
int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b));
int Xor = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_));
int Xor = Gia_ManHashAnd(pNew, Abc_LitNot(And1), Abc_LitNot(And1_));
int And2 = Gia_ManHashAnd(pNew, c, Xor);
int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor));
*ps = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_));
*ps = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
*pc = Gia_ManHashOr (pNew, And1, And2);
}
}
@ -1209,9 +1209,12 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
assert( nFFins == nFFouts );
Gia_ManSetRegNum( pNew, nFFins );
// finalize AIG
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
if ( !fGiaSimple )
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
// transform AIG with init state
if ( p->pInits )
{
@ -1222,7 +1225,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
}
else
{
pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}