summaryrefslogtreecommitdiffstats
path: root/src/aig/cec/cecClass.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec/cecClass.c')
-rw-r--r--src/aig/cec/cecClass.c887
1 files changed, 287 insertions, 600 deletions
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 65fa2e9b..aaa85ffa 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -24,39 +24,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Cec_ObjRepr( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iRepr; }
-static inline void Cec_ObjSetRepr( Cec_ManCsw_t * p, int Id, int Num ) { p->pObjs[Id].iRepr = Num; }
-
-static inline int Cec_ObjProved( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iProved; }
-static inline void Cec_ObjSetProved( Cec_ManCsw_t * p, int Id ) { p->pObjs[Id].iProved = 1; }
-
-static inline int Cec_ObjFailed( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iFailed; }
-static inline void Cec_ObjSetFailed( Cec_ManCsw_t * p, int Id ) { p->pObjs[Id].iFailed = 1; }
-
-static inline int Cec_ObjNext( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iNext; }
-static inline void Cec_ObjSetNext( Cec_ManCsw_t * p, int Id, int Num ) { p->pObjs[Id].iNext = Num; }
-
-static inline unsigned Cec_ObjSim( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].SimNum; }
-static inline unsigned * Cec_ObjSimP1( Cec_ManCsw_t * p, int Id ) { return &p->pObjs[Id].SimNum; }
-static inline unsigned * Cec_ObjSimP( Cec_ManCsw_t * p, int Id ) { return p->pMems + Cec_ObjSim(p, Id) + 1; }
-static inline void Cec_ObjSetSim( Cec_ManCsw_t * p, int Id, unsigned n ) { p->pObjs[Id].SimNum = n; }
-
-static inline int Cec_ObjIsConst( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) == 0; }
-static inline int Cec_ObjIsHead( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) > 0; }
-static inline int Cec_ObjIsNone( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) == 0; }
-static inline int Cec_ObjIsTail( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) > 0 && Cec_ObjNext(p, Id) == 0; }
-static inline int Cec_ObjIsClass( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) > 0 || Cec_ObjNext(p, Id) > 0; }
-
-#define Cec_ManForEachObj( p, i ) \
- for ( i = 0; i < Gia_ManObjNum(p->pAig); i++ )
-#define Cec_ManForEachObj1( p, i ) \
- for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
-#define Cec_ManForEachClass( p, i ) \
- for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) if ( !Cec_ObjIsHead(p, i) ) {} else
-#define Cec_ClassForEachObj( p, i, iObj ) \
- for ( assert(Cec_ObjIsHead(p, i)), iObj = i; iObj; iObj = Cec_ObjNext(p, iObj) )
-#define Cec_ClassForEachObj1( p, i, iObj ) \
- for ( assert(Cec_ObjIsHead(p, i)), iObj = Cec_ObjNext(p, i); iObj; iObj = Cec_ObjNext(p, iObj) )
+static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id ) { return p->pMems + p->pSimInfo[Id] + 1; }
+static inline void Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n ) { p->pSimInfo[Id] = n; }
+
+static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -64,30 +35,7 @@ static inline int Cec_ObjIsClass( Cec_ManCsw_t * p, int Id ) {
/**Function*************************************************************
- Synopsis [Creates the set of representatives.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
-{
- int i, * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
- for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
- if ( Cec_ObjProved(p, i) )
- {
- assert( Cec_ObjRepr(p, i) >= 0 );
- pReprs[i] = Cec_ObjRepr(p, i);
- }
- return pReprs;
-}
-
-/**Function*************************************************************
-
- Synopsis []
+ Synopsis [Compares simulation info of one node with constant 0.]
Description []
@@ -96,250 +44,28 @@ int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p )
+int Cec_ManSimCompareConst( unsigned * p, int nWords )
{
- Gia_Man_t * pNew, * pTemp;
- Gia_Obj_t * pObj, * pRepr;
- int iRes0, iRes1, iRepr, iNode;
- int i, fCompl, * piCopies;
- Vec_IntClear( p->vXorNodes );
- Gia_ManLevelNum( p->pAig );
- pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
- Gia_ManHashAlloc( pNew );
- piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
- piCopies[0] = 0;
- Gia_ManForEachObj1( p->pAig, pObj, i )
- {
- if ( Gia_ObjIsCi(pObj) )
- {
- piCopies[i] = Gia_ManAppendCi( pNew );
- continue;
- }
- iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
- if ( Gia_ObjIsCo(pObj) )
- {
- Gia_ManAppendCo( pNew, iRes0 );
- continue;
- }
- iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
- iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
- if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
- continue;
- assert( Cec_ObjRepr(p, i) < i );
- iRepr = piCopies[Cec_ObjRepr(p, i)];
- if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
- continue;
- pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
- fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
- piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
- }
- ABC_FREE( piCopies );
- Gia_ManHashStop( pNew );
- Gia_ManSetRegNum( pNew, 0 );
- pNew = Gia_ManCleanup( pTemp = pNew );
- Gia_ManStop( pTemp );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p )
-{
- Gia_Man_t * pNew, * pTemp;
- Gia_Obj_t * pObj, * pRepr;
- int iRes0, iRes1, iRepr, iNode, iMiter;
- int i, fCompl, * piCopies, * pDepths;
- Vec_IntClear( p->vXorNodes );
-// Gia_ManLevelNum( p->pAig );
- pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
- Gia_ManHashAlloc( pNew );
- piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
- pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
- piCopies[0] = 0;
- Gia_ManForEachObj1( p->pAig, pObj, i )
- {
- if ( Gia_ObjIsCi(pObj) )
- {
- piCopies[i] = Gia_ManAppendCi( pNew );
- continue;
- }
- if ( Gia_ObjIsCo(pObj) )
- continue;
- if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
- piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
- continue;
- 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)] );
- if ( Cec_ObjRepr(p, i) < 0 || Cec_ObjFailed(p, i) )
- continue;
- assert( Cec_ObjRepr(p, i) < i );
- iRepr = piCopies[Cec_ObjRepr(p, i)];
- if ( iRepr == -1 )
- continue;
- if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
- continue;
- pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
- fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
- piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
- if ( Cec_ObjProved(p, i) )
- continue;
-// if ( p->pPars->nLevelMax &&
-// (Gia_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax ||
-// Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
-// continue;
- // produce speculative miter
- iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
- Gia_ManAppendCo( pNew, iMiter );
- Vec_IntPush( p->vXorNodes, Cec_ObjRepr(p, i) );
- Vec_IntPush( p->vXorNodes, i );
- // add to the depth of this node
- pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Cec_ObjRepr(p, i)] );
- if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
- piCopies[i] = -1;
- }
- ABC_FREE( piCopies );
- ABC_FREE( pDepths );
- Gia_ManHashStop( pNew );
- Gia_ManSetRegNum( pNew, 0 );
- pNew = Gia_ManCleanup( pTemp = pNew );
- Gia_ManStop( pTemp );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p )
-{
- Gia_Man_t * pNew, * pTemp;
- Gia_Obj_t * pObj, * pRepr;
- int iRes0, iRes1, iRepr, iNode, iMiter;
- int i, fCompl, * piCopies;
- Vec_IntClear( p->vXorNodes );
- Gia_ManLevelNum( p->pAig );
- pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
- Gia_ManHashAlloc( pNew );
- piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
- piCopies[0] = 0;
- Gia_ManForEachObj1( p->pAig, pObj, i )
+ int w;
+ if ( p[0] & 1 )
{
- if ( Gia_ObjIsCi(pObj) )
- {
- piCopies[i] = Gia_ManAppendCi( pNew );
- continue;
- }
- if ( Gia_ObjIsCo(pObj) )
- continue;
- 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 );
- if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
- continue;
- assert( Cec_ObjRepr(p, i) < i );
- iRepr = piCopies[Cec_ObjRepr(p, i)];
- if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
- continue;
- pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
- fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
- piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
- // add speculative miter
- iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
- Gia_ManAppendCo( pNew, iMiter );
+ for ( w = 0; w < nWords; w++ )
+ if ( p[w] != ~0 )
+ return 0;
+ return 1;
}
- ABC_FREE( piCopies );
- Gia_ManHashStop( pNew );
- Gia_ManSetRegNum( pNew, 0 );
- pNew = Gia_ManCleanup( pTemp = pNew );
- Gia_ManStop( pTemp );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManCswCountOne( Cec_ManCsw_t * p, int i )
-{
- int Ent, nLits = 1;
- Cec_ClassForEachObj1( p, i, Ent )
+ else
{
- assert( Cec_ObjRepr(p, Ent) == i );
- nLits++;
+ for ( w = 0; w < nWords; w++ )
+ if ( p[w] != 0 )
+ return 0;
+ return 1;
}
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p )
-{
- int i, nLits = 0;
- Cec_ManForEachObj( p, i )
- nLits += (Cec_ObjRepr(p, i) >= 0);
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
-{
- int Ent;
- printf( "Class %4d : Num = %2d {", Counter, Cec_ManCswCountOne(p, i) );
- Cec_ClassForEachObj( p, i, Ent )
- printf(" %d", Ent );
- printf( " }\n" );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Compares simulation info of two nodes.]
Description []
@@ -348,32 +74,28 @@ void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
SeeAlso []
***********************************************************************/
-void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
+int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords )
{
- int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
- Cec_ManForEachObj1( p, i )
+ int w;
+ if ( (p0[0] & 1) == (p1[0] & 1) )
{
- if ( Cec_ObjIsHead(p, i) )
- Counter++;
- else if ( Cec_ObjIsConst(p, i) )
- Counter1++;
- else if ( Cec_ObjIsNone(p, i) )
- CounterX++;
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != p1[w] )
+ return 0;
+ return 1;
}
- nLits = Cec_ManCswCountLitsAll( p );
- printf( "Class =%7d. Const =%7d. Unsed =%7d. Lits =%8d. All =%8d. Mem = %5.2f Mb\n",
- Counter, Counter1, CounterX, nLits-Counter1, nLits, 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20) );
- if ( fVerbose )
+ else
{
- Counter = 0;
- Cec_ManForEachClass( p, i )
- Cec_ManCswPrintOne( p, i, ++Counter );
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != ~p1[w] )
+ return 0;
+ return 1;
}
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Returns the number of the first non-equal bit.]
Description []
@@ -382,28 +104,28 @@ void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords )
+int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
{
int w;
- if ( (p0[0] & 1) == (p1[0] & 1) )
+ if ( p[0] & 1 )
{
for ( w = 0; w < nWords; w++ )
- if ( p0[w] != p1[w] )
- return 0;
- return 1;
+ if ( p[w] != ~0 )
+ return 32*w + Aig_WordFindFirstBit( ~p[w] );
+ return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
- if ( p0[w] != ~p1[w] )
- return 0;
- return 1;
+ if ( p[w] != 0 )
+ return 32*w + Aig_WordFindFirstBit( p[w] );
+ return -1;
}
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Compares simulation info of two nodes.]
Description []
@@ -412,28 +134,28 @@ int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords )
SeeAlso []
***********************************************************************/
-int Cec_ManCswCompareConst( unsigned * p, int nWords )
+int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
{
int w;
- if ( p[0] & 1 )
+ if ( (p0[0] & 1) == (p1[0] & 1) )
{
for ( w = 0; w < nWords; w++ )
- if ( p[w] != ~0 )
- return 0;
- return 1;
+ if ( p0[w] != p1[w] )
+ return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] );
+ return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
- if ( p[w] != 0 )
- return 0;
- return 1;
+ if ( p0[w] != ~p1[w] )
+ return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] );
+ return -1;
}
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Creates equivalence class.]
Description []
@@ -442,31 +164,31 @@ int Cec_ManCswCompareConst( unsigned * p, int nWords )
SeeAlso []
***********************************************************************/
-void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
+void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
{
- int Repr = -1, EntPrev = -1, Ent, i;
+ int Repr = GIA_VOID, EntPrev = -1, Ent, i;
assert( Vec_IntSize(vClass) > 0 );
Vec_IntForEachEntry( vClass, Ent, i )
{
if ( i == 0 )
{
Repr = Ent;
- Cec_ObjSetRepr( p, Ent, -1 );
+ Gia_ObjSetRepr( p, Ent, GIA_VOID );
EntPrev = Ent;
}
else
{
- Cec_ObjSetRepr( p, Ent, Repr );
- Cec_ObjSetNext( p, EntPrev, Ent );
+ Gia_ObjSetRepr( p, Ent, Repr );
+ Gia_ObjSetNext( p, EntPrev, Ent );
EntPrev = Ent;
}
}
- Cec_ObjSetNext( p, EntPrev, 0 );
+ Gia_ObjSetNext( p, EntPrev, 0 );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Refines one equivalence class.]
Description []
@@ -475,34 +197,34 @@ void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
SeeAlso []
***********************************************************************/
-int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
+int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
{
unsigned * pSim0, * pSim1;
int Ent;
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
- pSim0 = fFirst? Cec_ObjSimP1(p, i) : Cec_ObjSimP(p, i);
- Cec_ClassForEachObj1( p, i, Ent )
+ pSim0 = Cec_ObjSim(p, i);
+ Gia_ClassForEachObj1( p->pAig, i, Ent )
{
- pSim1 = fFirst? Cec_ObjSimP1(p, Ent) : Cec_ObjSimP(p, Ent);
- if ( Cec_ManCswCompareEqual( pSim0, pSim1, p->nWords ) )
+ pSim1 = Cec_ObjSim(p, Ent);
+ if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
- Cec_ManCswClassCreate( p, p->vClassOld );
- Cec_ManCswClassCreate( p, p->vClassNew );
+ Cec_ManSimClassCreate( p->pAig, p->vClassOld );
+ Cec_ManSimClassCreate( p->pAig, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
- return 1 + Cec_ManCswClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), fFirst );
+ return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Computes hash key of the simuation info.]
Description []
@@ -511,7 +233,7 @@ int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
SeeAlso []
***********************************************************************/
-int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
+int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize )
{
static int s_Primes[16] = {
1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
@@ -530,7 +252,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Resets pointers to the simulation memory.]
Description []
@@ -539,90 +261,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
SeeAlso []
***********************************************************************/
-void Cec_ManCswClassesCreate( Cec_ManCsw_t * p )
-{
- int * pTable, nTableSize, i, Key;
- p->nWords = 1;
- nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p->pAig) / 10 );
- pTable = ABC_CALLOC( int, nTableSize );
- Cec_ObjSetRepr( p, 0, -1 );
- Cec_ManForEachObj1( p, i )
- {
- if ( Gia_ObjIsCo(Gia_ManObj(p->pAig, i)) )
- {
- Cec_ObjSetRepr( p, i, -1 );
- continue;
- }
- if ( Cec_ManCswCompareConst( Cec_ObjSimP1(p, i), p->nWords ) )
- {
- Cec_ObjSetRepr( p, i, 0 );
- continue;
- }
- Key = Cec_ManCswHashKey( Cec_ObjSimP1(p, i), p->nWords, nTableSize );
- if ( pTable[Key] == 0 )
- Cec_ObjSetRepr( p, i, -1 );
- else
- {
- Cec_ObjSetNext( p, pTable[Key], i );
- Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
- if ( Cec_ObjRepr(p, i) == -1 )
- Cec_ObjSetRepr( p, i, pTable[Key] );
- }
- pTable[Key] = i;
- }
- ABC_FREE( pTable );
- if ( p->pPars->fVeryVerbose )
- Cec_ManCswPrintClasses( p, 0 );
- // refine classes
- Cec_ManForEachClass( p, i )
- Cec_ManCswClassRefineOne( p, i, 1 );
- // clean memory
- Cec_ManForEachObj( p, i )
- Cec_ObjSetSim( p, i, 0 );
- if ( p->pPars->fVeryVerbose )
- Cec_ManCswPrintClasses( p, 0 );
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCswSimulateSimple( Cec_ManCsw_t * p )
-{
- Gia_Obj_t * pObj;
- unsigned Res0, Res1;
- int i;
- Gia_ManForEachCi( p->pAig, pObj, i )
- Cec_ObjSetSim( p, i, Aig_ManRandom(0) );
- Gia_ManForEachAnd( p->pAig, pObj, i )
- {
- Res0 = Cec_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
- Res1 = Cec_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
- Cec_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
- (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [References simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
+void Cec_ManSimMemRelink( Cec_ManSim_t * p )
{
unsigned * pPlace, Ent;
pPlace = &p->MemFree;
@@ -634,6 +273,7 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
pPlace = p->pMems + Ent;
}
*pPlace = 0;
+ p->nWordsOld = p->nWords;
}
/**Function*************************************************************
@@ -647,10 +287,10 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
SeeAlso []
***********************************************************************/
-unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
+unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i )
{
unsigned * pSim;
- assert( p->pObjs[i].SimNum == 0 );
+ assert( p->pSimInfo[i] == 0 );
if ( p->MemFree == 0 )
{
if ( p->nWordsAlloc == 0 )
@@ -661,9 +301,9 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
}
p->nWordsAlloc *= 2;
p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
- Cec_ManCswSimMemRelink( p );
+ Cec_ManSimMemRelink( p );
}
- p->pObjs[i].SimNum = p->MemFree;
+ p->pSimInfo[i] = p->MemFree;
pSim = p->pMems + p->MemFree;
p->MemFree = pSim[0];
pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
@@ -675,7 +315,7 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
/**Function*************************************************************
- Synopsis [Dereference simulaton info.]
+ Synopsis [Dereferences simulaton info.]
Description []
@@ -684,16 +324,16 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
SeeAlso []
***********************************************************************/
-unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
+unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i )
{
unsigned * pSim;
- assert( p->pObjs[i].SimNum > 0 );
- pSim = p->pMems + p->pObjs[i].SimNum;
+ assert( p->pSimInfo[i] > 0 );
+ pSim = p->pMems + p->pSimInfo[i];
if ( --pSim[0] == 0 )
{
pSim[0] = p->MemFree;
- p->MemFree = p->pObjs[i].SimNum;
- p->pObjs[i].SimNum = 0;
+ p->MemFree = p->pSimInfo[i];
+ p->pSimInfo[i] = 0;
p->nMems--;
}
return pSim;
@@ -701,7 +341,7 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Refines nodes belonging to candidate constant class.]
Description []
@@ -710,52 +350,145 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
SeeAlso []
***********************************************************************/
-void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
+void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
{
unsigned * pSim;
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
- nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
+ nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
- if ( i == 7720 )
- {
- int s = 0;
- }
- pSim = Cec_ObjSimP( p, i );
- assert( !Cec_ManCswCompareConst( pSim, p->nWords ) );
- Key = Cec_ManCswHashKey( pSim, p->nWords, nTableSize );
+ pSim = Cec_ObjSim( p, i );
+ assert( !Cec_ManSimCompareConst( pSim, p->nWords ) );
+ Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize );
if ( pTable[Key] == 0 )
{
- assert( Cec_ObjRepr(p, i) == 0 );
- assert( Cec_ObjNext(p, i) == 0 );
- Cec_ObjSetRepr( p, i, -1 );
+ assert( Gia_ObjRepr(p->pAig, i) == 0 );
+ assert( Gia_ObjNext(p->pAig, i) == 0 );
+ Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
}
else
{
- Cec_ObjSetNext( p, pTable[Key], i );
- Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
- if ( Cec_ObjRepr(p, i) == -1 )
- Cec_ObjSetRepr( p, i, pTable[Key] );
- assert( Cec_ObjRepr(p, i) > 0 );
+ Gia_ObjSetNext( p->pAig, pTable[Key], i );
+ Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
+ if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
+ Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
+ assert( Gia_ObjRepr(p->pAig, i) > 0 );
}
pTable[Key] = i;
}
Vec_IntForEachEntry( vRefined, i, k )
{
- if ( Cec_ObjIsHead( p, i ) )
- Cec_ManCswClassRefineOne( p, i, 0 );
+ if ( Gia_ObjIsHead( p->pAig, i ) )
+ Cec_ManSimClassRefineOne( p, i );
}
Vec_IntForEachEntry( vRefined, i, k )
- Cec_ManCswSimDeref( p, i );
+ Cec_ManSimSimDeref( p, i );
ABC_FREE( pTable );
}
/**Function*************************************************************
+ Synopsis [Saves the input pattern with the given number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
+{
+ unsigned * pInfo;
+ int i;
+ 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)) );
+ 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 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if computation should stop.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
+{
+ unsigned * pInfo, * pInfo2;
+ int i;
+ if ( p->vCoSimInfo == NULL )
+ return 0;
+ // compare outputs with 0
+ if ( p->pPars->fDoubleOuts )
+ {
+ assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
+ for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+ {
+ pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
+ pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
+ if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
+ {
+ if ( p->iOut == -1 )
+ {
+ p->iOut = i/2;
+ Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
+ }
+ if ( p->pCexes == NULL )
+ p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 );
+ if ( p->pCexes[i/2] == NULL )
+ {
+ p->nOuts++;
+ p->pCexes[i/2] = (void *)1;
+ }
+ }
+ }
+ }
+ else
+ {
+ for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+ {
+ pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
+ if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
+ {
+ if ( p->iOut == -1 )
+ {
+ p->iOut = i;
+ Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
+ }
+ if ( p->pCexes == NULL )
+ p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) );
+ if ( p->pCexes[i] == NULL )
+ {
+ p->nOuts++;
+ p->pCexes[i] = (void *)1;
+ }
+ }
+ }
+ }
+ return p->pCexes != NULL && p->pPars->fFirstStop;
+}
+
+/**Function*************************************************************
+
Synopsis [Simulates one round.]
Description [Returns the number of PO entry if failed; 0 otherwise.]
@@ -765,17 +498,20 @@ void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
SeeAlso []
***********************************************************************/
-void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, int iSeries, int fRandomize )
+int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
{
- static int nCountRand = 0;
Gia_Obj_t * pObj;
unsigned * pRes0, * pRes1, * pRes;
int i, k, w, Ent, iCiId = 0, iCoId = 0;
+ // prepare internal storage
+ if ( p->nWordsOld != p->nWords )
+ Cec_ManSimMemRelink( p );
p->nMemsMax = 0;
+ // simulate nodes
Vec_IntClear( p->vRefinedC );
if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
{
- pRes = Cec_ManCswSimRef( p, 0 );
+ pRes = Cec_ManSimSimRef( p, 0 );
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = 0;
}
@@ -788,16 +524,12 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
iCiId++;
continue;
}
- pRes = Cec_ManCswSimRef( p, i );
+ pRes = Cec_ManSimSimRef( p, i );
if ( vInfoCis )
{
pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
for ( w = 1; w <= p->nWords; w++ )
- {
- pRes[w] = pRes0[iSeries*p->nWords+w-1];
- if ( fRandomize )
- pRes[w] ^= (1 << (nCountRand++ & 0x1f));
- }
+ pRes[w] = pRes0[w-1];
}
else
{
@@ -810,7 +542,7 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
}
if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
{
- pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+ pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
if ( vInfoCos )
{
pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
@@ -824,9 +556,9 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
continue;
}
assert( Gia_ObjValue(pObj) );
- pRes = Cec_ManCswSimRef( p, i );
- pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
- pRes1 = Cec_ManCswSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+ pRes = Cec_ManSimSimRef( p, i );
+ pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+ pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
@@ -847,47 +579,50 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
}
references:
// if this node is candidate constant, collect it
- if ( Cec_ObjIsConst(p, i) && !Cec_ManCswCompareConst(pRes + 1, p->nWords) )
+ if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
{
pRes[0]++;
Vec_IntPush( p->vRefinedC, i );
}
// if the node belongs to a class, save it
- if ( Cec_ObjIsClass(p, i) )
+ if ( Gia_ObjIsClass(p->pAig, i) )
pRes[0]++;
// if this is the last node of the class, process it
- if ( Cec_ObjIsTail(p, i) )
+ if ( Gia_ObjIsTail(p->pAig, i) )
{
Vec_IntClear( p->vClassTemp );
- Cec_ClassForEachObj( p, Cec_ObjRepr(p, i), Ent )
+ Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
Vec_IntPush( p->vClassTemp, Ent );
- Cec_ManCswClassRefineOne( p, Cec_ObjRepr(p, i), 0 );
+ Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
Vec_IntForEachEntry( p->vClassTemp, Ent, k )
- Cec_ManCswSimDeref( p, Ent );
+ Cec_ManSimSimDeref( p, Ent );
}
}
if ( Vec_IntSize(p->vRefinedC) > 0 )
- Cec_ManCswProcessRefined( p, p->vRefinedC );
+ Cec_ManSimProcessRefined( p, p->vRefinedC );
assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
assert( p->nMems == 1 );
+ if ( p->nMems != 1 )
+ printf( "Cec_ManSimSimulateRound(): Memory management error!\n" );
if ( p->pPars->fVeryVerbose )
- Cec_ManCswPrintClasses( p, 0 );
+ Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
/*
- if ( p->nMems > 1 )
- {
+ if ( p->nMems > 1 ) {
for ( i = 1; i < p->nObjs; i++ )
- if ( p->pSims[i] )
- {
+ if ( p->pSims[i] ) {
int x = 0;
}
}
*/
+ return Cec_ManSimAnalyzeOutputs( p );
}
+
+
/**Function*************************************************************
- Synopsis []
+ Synopsis [Creates simulation info for this round.]
Description []
@@ -896,28 +631,41 @@ references:
SeeAlso []
***********************************************************************/
-int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
+void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
{
- int i;
- Gia_ManSetRefs( p->pAig );
- Cec_ManCswSimulateSimple( p );
- Cec_ManCswClassesCreate( p );
- for ( i = 0; i < p->pPars->nRounds; i++ )
+ unsigned * pRes0, * pRes1;
+ int i, w;
+ if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 )
{
- p->nWords = i + 1;
- Cec_ManCswSimMemRelink( p );
- Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
+ assert( vInfoCis && vInfoCos );
+ for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+ {
+ pRes0 = Vec_PtrEntry( vInfoCis, i );
+ for ( w = 0; w < p->nWords; w++ )
+ pRes0[w] = Aig_ManRandom( 0 );
+ }
+ for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+ {
+ pRes0 = Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
+ pRes1 = Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
+ for ( w = 0; w < p->nWords; w++ )
+ pRes0[w] = pRes1[w];
+ }
+ }
+ else
+ {
+ for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+ {
+ pRes0 = Vec_PtrEntry( vInfoCis, i );
+ for ( w = 0; w < p->nWords; w++ )
+ pRes0[w] = Aig_ManRandom( 0 );
+ }
}
- p->nWords = p->pPars->nWords;
- Cec_ManCswSimMemRelink( p );
- for ( i = 0; i < p->pPars->nRounds; i++ )
- Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
- return 1;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Returns 1 if the bug is found.]
Description []
@@ -926,21 +674,37 @@ int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
SeeAlso []
***********************************************************************/
-int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
+int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
{
- int Result;
- if ( pObj->fMark0 )
- return 1;
- if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
- return 0;
- Result = (Cec_ManCswClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
- Cec_ManCswClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
- return pObj->fMark0 = Result;
+ Gia_Obj_t * pObj;
+ int i;
+ assert( p->pAig->pReprs == NULL );
+ // allocate representation
+ p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
+ p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+ Gia_ManForEachObj( p->pAig, pObj, i )
+ Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID );
+ // perform simulation
+ Gia_ManSetRefs( p->pAig );
+ p->nWords = 1;
+ do {
+ if ( p->pPars->fVerbose )
+ Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+ for ( i = 0; i < 4; i++ )
+ {
+ Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+ if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+ return 1;
+ }
+ p->nWords = 2 * p->nWords + 1;
+ }
+ while ( p->nWords <= p->pPars->nWords );
+ return 0;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Returns 1 if the bug is found.]
Description []
@@ -949,100 +713,23 @@ int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
+int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
{
- Vec_Ptr_t * vInfo;
- Gia_Obj_t * pObj, * pObjOld, * pReprOld;
- int i, k, iRepr, iNode;
- vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), p->pPars->nWords );
- if ( vInfo != NULL )
- {
- for ( i = 0; i < pPat->nSeries; i++ )
- Cec_ManCswSimulateRound( p, vInfo, NULL, i, 0 );
- Vec_PtrFree( vInfo );
- }
- assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
- // mark the transitive fanout of failed nodes
- if ( p->pPars->nDepthMax != 1 )
+ int i;
+ Gia_ManSetRefs( p->pAig );
+ p->nWords = p->pPars->nWords;
+ for ( i = 0; i < p->pPars->nRounds; i++ )
{
- Gia_ManCleanMark0( p->pAig );
- Gia_ManCleanMark1( p->pAig );
- Gia_ManForEachCo( pNew, pObj, k )
- {
- iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
- iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
- if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
- continue;
-// Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
- Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
- }
- // mark the nodes reachable through the failed nodes
- Gia_ManForEachAnd( p->pAig, pObjOld, k )
- pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
- // unmark the disproved nodes
- Gia_ManForEachCo( pNew, pObj, k )
- {
- iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
- iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
- if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
- continue;
- pObjOld = Gia_ManObj(p->pAig, iNode);
- assert( pObjOld->fMark0 == 1 );
- if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
- pObjOld->fMark1 = 1;
- }
- // clean marks
- Gia_ManForEachAnd( p->pAig, pObjOld, k )
- if ( pObjOld->fMark1 )
- {
- pObjOld->fMark0 = 0;
- pObjOld->fMark1 = 0;
- }
+ if ( (i % 4) == 0 && p->pPars->fVerbose )
+ Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+ Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+ if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+ return 1;
}
- // set the results
- Gia_ManForEachCo( pNew, pObj, k )
- {
- iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
- iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
- pReprOld = Gia_ManObj(p->pAig, iRepr);
- pObjOld = Gia_ManObj(p->pAig, iNode);
- if ( pObj->fMark1 )
- { // proved
- assert( pObj->fMark0 == 0 );
- assert( !Cec_ObjProved(p, iNode) );
- if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
-// if ( pObjOld->fMark0 == 0 )
- {
- assert( iRepr == Cec_ObjRepr(p, iNode) );
- Cec_ObjSetProved( p, iNode );
- p->nAllProved++;
- }
- }
- else if ( pObj->fMark0 )
- { // disproved
- assert( pObj->fMark1 == 0 );
- if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
-// if ( pObjOld->fMark0 == 0 )
- {
- if ( iRepr == Cec_ObjRepr(p, iNode) )
- printf( "Cec_ManCswClassesUpdate(): Error! Node is not refined!\n" );
- p->nAllDisproved++;
- }
- }
- else
- { // failed
- assert( pObj->fMark0 == 0 );
- assert( pObj->fMark1 == 0 );
- assert( !Cec_ObjFailed(p, iNode) );
- assert( !Cec_ObjProved(p, iNode) );
- Cec_ObjSetFailed( p, iNode );
- p->nAllFailed++;
- }
- }
+ if ( p->pPars->fVerbose )
+ Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
return 0;
}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 18:13:10 +0000