summaryrefslogtreecommitdiffstats
path: root/src/aig/cec
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec')
-rw-r--r--src/aig/cec/cecCec.c3
-rw-r--r--src/aig/cec/cecClass.c26
-rw-r--r--src/aig/cec/cecCore.c12
-rw-r--r--src/aig/cec/cecCorr.c148
-rw-r--r--src/aig/cec/cecIso.c4
-rw-r--r--src/aig/cec/cecPat.c22
-rw-r--r--src/aig/cec/cecSeq.c16
-rw-r--r--src/aig/cec/cecSolve.c6
-rw-r--r--src/aig/cec/cecSweep.c6
9 files changed, 185 insertions, 58 deletions
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 82df6008..ee9f6d3c 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "cecInt.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -44,7 +45,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
int i;
assert( p->pCexComb == NULL );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) );
+ sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) );
p->pCexComb->iPo = iOut;
p->pCexComb->nPis = Gia_ManCiNum(p);
p->pCexComb->nBits = Gia_ManCiNum(p);
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 49930836..5a52e913 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -111,14 +111,14 @@ int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != ~0 )
- return 32*w + Aig_WordFindFirstBit( ~p[w] );
+ return 32*w + Gia_WordFindFirstBit( ~p[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != 0 )
- return 32*w + Aig_WordFindFirstBit( p[w] );
+ return 32*w + Gia_WordFindFirstBit( p[w] );
return -1;
}
}
@@ -141,14 +141,14 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != p1[w] )
- return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] );
+ return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != ~p1[w] )
- return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] );
+ return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
return -1;
}
}
@@ -467,7 +467,7 @@ void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
- nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
+ nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
@@ -519,15 +519,15 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
assert( p->pCexComb == NULL );
assert( iPat >= 0 && iPat < 32 * p->nWords );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) );
+ sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) );
p->pCexComb->iPo = p->iOut;
p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, i );
- if ( Aig_InfoHasBit( pInfo, iPat ) )
- Aig_InfoSetBit( p->pCexComb->pData, i );
+ if ( Gia_InfoHasBit( pInfo, iPat ) )
+ Gia_InfoSetBit( p->pCexComb->pData, i );
}
}
@@ -560,8 +560,8 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
- if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) )
- Aig_InfoXorBit( p->pBestState->pData, i );
+ if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) )
+ Gia_InfoXorBit( p->pBestState->pData, i );
}
p->pBestState->iPo = ScoreBest;
}
@@ -686,7 +686,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
else
{
for ( w = 1; w <= p->nWords; w++ )
- pRes[w] = Aig_ManRandom( 0 );
+ pRes[w] = Gia_ManRandom( 0 );
}
// make sure the first pattern is always zero
pRes[1] ^= (pRes[1] & 1);
@@ -798,7 +798,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
- pRes0[w] = Aig_ManRandom( 0 );
+ pRes0[w] = Gia_ManRandom( 0 );
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
@@ -814,7 +814,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
- pRes0[w] = Aig_ManRandom( 0 );
+ pRes0[w] = Gia_ManRandom( 0 );
}
}
}
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 7759428e..ca0a3665 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -246,7 +246,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
if ( pPars->fSeqSimulate )
printf( "Performing sequential simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nWords );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
pSim = Cec_ManSimStart( pAig, pPars );
if ( pAig->pReprs == NULL )
RetValue = Cec_ManSimClassesPrepare( pSim );
@@ -283,7 +283,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
double clkTotal = clock();
// duplicate AIG and transfer equivalence classes
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
pIni = Gia_ManDup(pAig);
pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
@@ -420,7 +420,8 @@ p->timeSat += clock() - clk;
printf( "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
- if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
+// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
+ else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
{
if ( p->pPars->fVerbose )
printf( "Switching into normal mode.\n" );
@@ -431,6 +432,11 @@ p->timeSat += clock() - clk;
finalize:
if ( p->pPars->fVerbose )
{
+ printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
+ 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
+ Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
+ 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal );
ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 05259bc7..dccd90b0 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -49,6 +49,11 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
}
+ if ( f == 0 )
+ {
+ assert( Gia_ObjIsRo(p, pObj) );
+ return Gia_ObjCopyF(p, f, pObj);
+ }
assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
@@ -107,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
@@ -202,6 +207,74 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
/**Function*************************************************************
+ Synopsis [Derives SRM for signal correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pRepr;
+ Vec_Int_t * vXorLits;
+ int f, i, iPrevNew, iObjNew;
+ assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) );
+ assert( Gia_ManRegNum(p) > 0 );
+ assert( p->pReprs != NULL );
+ p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+ Gia_ManSetPhase( p );
+ pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ Gia_ManAppendCi(pNew);
+ Gia_ObjSetCopyF( p, 0, pObj, 0 );
+ }
+ for ( f = 0; f < nFrames+fScorr; f++ )
+ {
+ Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+ Gia_ManForEachPi( p, pObj, i )
+ Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+ }
+ *pvOutputs = Vec_IntAlloc( 1000 );
+ vXorLits = Vec_IntAlloc( 1000 );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ continue;
+ iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f );
+ iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+ if ( iPrevNew != iObjNew )
+ {
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+ }
+ }
+ }
+ Vec_IntForEachEntry( vXorLits, iObjNew, i )
+ Gia_ManAppendCo( pNew, iObjNew );
+ Vec_IntFree( vXorLits );
+ Gia_ManHashStop( pNew );
+ ABC_FREE( p->pCopies );
+//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description []
@@ -227,7 +300,7 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
}
@@ -351,17 +424,17 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- if ( Aig_InfoHasBit( pPres, iBit ) &&
- Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ if ( Gia_InfoHasBit( pPres, iBit ) &&
+ Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- Aig_InfoSetBit( pPres, iBit );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- Aig_InfoXorBit( pInfo, iBit );
+ Gia_InfoSetBit( pPres, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@@ -403,7 +476,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
break;
}
@@ -443,8 +516,8 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
- Aig_InfoXorBit( pInfo, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
+ Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
@@ -591,7 +664,11 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
- printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits );
+ if ( iIter == -1 )
+ printf( "BMC : " );
+ else
+ printf( "%3d : ", iIter );
+ printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
@@ -638,7 +715,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return NULL;
}
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
@@ -704,14 +781,57 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
+ // check the base case
+ if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
+ {
+ int fChanges = 1;
+ while ( fChanges )
+ {
+ int clkBmc = clock();
+ fChanges = 0;
+ pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+ if ( Gia_ManPoNum(pSrm) == 0 )
+ {
+ Gia_ManStop( pSrm );
+ Vec_IntFree( vOutputs );
+ break;
+ }
+ pParsSat->nBTLimit *= 10;
+ if ( pPars->fUseCSat )
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ else
+ vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+ // refine classes with these counter-examples
+ if ( Vec_IntSize(vCexStore) )
+ {
+ clk2 = clock();
+ RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
+ clkSim += clock() - clk2;
+ Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+ fChanges = 1;
+ }
+ if ( pPars->fVerbose )
+ Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+ // recycle
+ Vec_IntFree( vCexStore );
+ Vec_StrFree( vStatus );
+ Gia_ManStop( pSrm );
+ Vec_IntFree( vOutputs );
+ }
+ }
+ else
+ {
+ if ( pPars->fVerbose )
+ Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
+ }
+ // check the overflow
if ( r == 100000 )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
- if ( pPars->fVerbose )
- Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
+ Gia_ManEquivImprove( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
index ddb539c2..d9aa5240 100644
--- a/src/aig/cec/cecIso.c
+++ b/src/aig/cec/cecIso.c
@@ -125,7 +125,7 @@ static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords )
unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
int w;
for ( w = 0; w < nWords; w++ )
- pInfo0[w] = Aig_ManRandom( 0 );
+ pInfo0[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -314,7 +314,7 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
// start simulation info
pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
// simulate and create table
- nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
+ nTableSize = Gia_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
pTable = ABC_CALLOC( int, nTableSize );
Gia_ManCleanValue( p );
Gia_ManForEachObj1( p, pObj, i )
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index a5be4c1c..8537fe4a 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -414,17 +414,17 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int *
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- if ( Aig_InfoHasBit( pPres, iBit ) &&
- Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ if ( Gia_InfoHasBit( pPres, iBit ) &&
+ Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- Aig_InfoSetBit( pPres, iBit );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- Aig_InfoXorBit( pInfo, iBit );
+ Gia_InfoSetBit( pPres, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
int nBits = 32 * nWords;
int clk = clock();
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
- Aig_ManRandomInfo( vInfo, 0, 0, nWords );
+ Gia_ManRandomInfo( vInfo, 0, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
@@ -460,11 +460,11 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
- Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
+ Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
nWords *= 2;
@@ -511,7 +511,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vInfo, 0, nWords );
- Aig_ManRandomInfo( vInfo, nRegs, 0, nWords );
+ Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
@@ -538,12 +538,12 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
// RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
// assert( RetValue == 1 );
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
- Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
+ Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 3d05172f..28f3a637 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -51,7 +51,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+ pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0;
}
*/
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
@@ -65,16 +65,16 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k++ );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom(0);
+ pInfo[w] = Gia_ManRandom(0);
// set simulation pattern and make sure it is second (first will be erased during simulation)
- pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i );
+ pInfo[0] = (pInfo[0] << 1) | Gia_InfoHasBit( pCex->pData, i );
pInfo[0] <<= 1;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom(0);
+ pInfo[w] = Gia_ManRandom(0);
}
}
@@ -100,14 +100,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0;
+ pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
}
@@ -229,7 +229,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
}
if ( pPars->fVerbose )
printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
@@ -275,7 +275,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
return -1;
}
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
// prepare starting pattern
pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
pState->iFrame = -1;
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index fc2d5d7f..5f032b59 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -369,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
Cec_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
+// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
@@ -636,8 +636,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
if ( Gia_ObjIsCi(pObj) )
{
unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
- if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
- Aig_InfoXorBit( pInfo, iPat );
+ if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) )
+ Gia_InfoXorBit( pInfo, iPat );
pSat->nCexLits++;
// Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
return;
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index f5e5bd06..1b68efe0 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -50,7 +50,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
if ( p->pPars->nLevelMax )
Gia_ManLevelNum( p->pAig );
pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+ pNew->pName = Gia_UtilStrsav( p->pAig->pName );
Gia_ManHashAlloc( pNew );
piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
@@ -70,7 +70,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
- pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
+ pDepths[i] = ABC_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
continue;
assert( Gia_ObjRepr(p->pAig, i) < i );
@@ -109,7 +109,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
Vec_IntPush( p->vXorNodes, i );
// add to the depth of this node
- pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
+ pDepths[i] = 1 + ABC_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
piCopies[i] = -1;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-23 04:00:21 +0000