diff options
Diffstat (limited to 'src/aig/gia/giaEra2.c')
| -rw-r--r-- | src/aig/gia/giaEra2.c | 1954 |
1 files changed, 1954 insertions, 0 deletions
diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c new file mode 100644 index 00000000..64464832 --- /dev/null +++ b/src/aig/gia/giaEra2.c @@ -0,0 +1,1954 @@ +/**CFile**************************************************************** + + FileName [gia.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + +/* + Limitations of this package: + - no more than (1<<31)-1 state cubes and internal nodes + - no more than MAX_VARS_NUM state variables + - no more than MAX_CALL_NUM transitions from a state + - cube list rebalancing happens when cube count reaches MAX_CUBE_NUM +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define MAX_CALL_NUM (1000000) // the max number of recursive calls +#define MAX_ITEM_NUM (1<<20) // the number of items on a page +#define MAX_PAGE_NUM (1<<11) // the max number of memory pages +#define MAX_VARS_NUM (1<<14) // the max number of state vars allowed +#define MAX_CUBE_NUM 63 // the max number of cubes before rebalancing + +// pointer to the tree node or state cube +typedef struct Gia_PtrAre_t_ Gia_PtrAre_t; +struct Gia_PtrAre_t_ +{ + unsigned nItem : 20; // item number (related to MAX_ITEM_NUM) + unsigned nPage : 11; // page number (related to MAX_PAGE_NUM) + unsigned fMark : 1; // user mark +}; + +// tree nodes +typedef struct Gia_ObjAre_t_ Gia_ObjAre_t; +struct Gia_ObjAre_t_ +{ + unsigned iVar : 14; // variable (related to MAX_VARS_NUM) + unsigned nStas0 : 6; // cube counter (related to MAX_CUBE_NUM) + unsigned nStas1 : 6; // cube counter (related to MAX_CUBE_NUM) + unsigned nStas2 : 6; // cube counter (related to MAX_CUBE_NUM) + Gia_PtrAre_t F[3]; // branches +}; + +// state cube +typedef struct Gia_StaAre_t_ Gia_StaAre_t; +struct Gia_StaAre_t_ +{ + Gia_PtrAre_t iPrev; // previous state + Gia_PtrAre_t iNext; // next cube in the list + unsigned pData[0]; // state bits +}; + +// explicit state reachability manager +typedef struct Gia_ManAre_t_ Gia_ManAre_t; +struct Gia_ManAre_t_ +{ + Gia_Man_t * pAig; // user's AIG manager + Gia_Man_t * pNew; // temporary AIG manager + unsigned ** ppObjs; // storage for objects (MAX_PAGE_NUM pages) + unsigned ** ppStas; // storage for states (MAX_PAGE_NUM pages) +// unsigned * pfUseless; // to label useless cubes +// int nUselessAlloc; // the number of useless alloced + // internal flags + int fMiter; // stops when a bug is discovered + int fStopped; // set high when reachability is stopped + int fTree; // working in the tree mode + // internal parametesr + int nWords; // the size of bit info in words + int nSize; // the size of state structure in words + int nObjPages; // the number of pages used for objects + int nStaPages; // the number of pages used for states + int nObjs; // the number of objects + int nStas; // the number of states + int iStaCur; // the next state to be explored + Gia_PtrAre_t Root; // root of the tree + Vec_Vec_t * vCiTfos; // storage for nodes in the CI TFOs + Vec_Vec_t * vCiLits; // storage for literals of these nodes + Vec_Int_t * vCubesA; // checked cubes + Vec_Int_t * vCubesB; // unchecked cubes + // deriving counter-example + void * pSat; // SAT solver + Vec_Int_t * vSatNumCis; // SAT variables for CIs + Vec_Int_t * vSatNumCos; // SAT variables for COs + Vec_Int_t * vCofVars; // variables used to cofactor + Vec_Int_t * vAssumps; // temporary storage for assumptions + Gia_StaAre_t * pTarget; // state that needs to be reached + int iOutFail; // the number of the failed output + // statistics + int nChecks; // the number of timea cube was checked + int nEquals; // total number of equal + int nCompares; // the number of compares + int nRecCalls; // the number of rec calls + int nDisjs; // the number of disjoint cube pairs + int nDisjs2; // the number of disjoint cube pairs + int nDisjs3; // the number of disjoint cube pairs + // time + int timeAig; // AIG cofactoring time + int timeCube; // cube checking time +}; + +static inline Gia_PtrAre_t Gia_Int2Ptr( unsigned n ) { return *(Gia_PtrAre_t *)(&n); } +static inline unsigned Gia_Ptr2Int( Gia_PtrAre_t n ) { return (*(int *)(&n)) & 0x7fffffff; } + +static inline int Gia_ObjHasBranch0( Gia_ObjAre_t * q ) { return !q->nStas0 && (q->F[0].nPage || q->F[0].nItem); } +static inline int Gia_ObjHasBranch1( Gia_ObjAre_t * q ) { return !q->nStas1 && (q->F[1].nPage || q->F[1].nItem); } +static inline int Gia_ObjHasBranch2( Gia_ObjAre_t * q ) { return !q->nStas2 && (q->F[2].nPage || q->F[2].nItem); } + +static inline Gia_ObjAre_t * Gia_ManAreObj( Gia_ManAre_t * p, Gia_PtrAre_t n ) { return (Gia_ObjAre_t *)(p->ppObjs[n.nPage] + (n.nItem << 2)); } +static inline Gia_StaAre_t * Gia_ManAreSta( Gia_ManAre_t * p, Gia_PtrAre_t n ) { return (Gia_StaAre_t *)(p->ppStas[n.nPage] + n.nItem * p->nSize); } +static inline Gia_ObjAre_t * Gia_ManAreObjInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreObj( p, Gia_Int2Ptr(n) ); } +static inline Gia_StaAre_t * Gia_ManAreStaInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreSta( p, Gia_Int2Ptr(n) ); } +static inline Gia_ObjAre_t * Gia_ManAreObjLast( Gia_ManAre_t * p ) { return Gia_ManAreObjInt( p, p->nObjs-1 ); } +static inline Gia_StaAre_t * Gia_ManAreStaLast( Gia_ManAre_t * p ) { return Gia_ManAreStaInt( p, p->nStas-1 ); } + +static inline Gia_ObjAre_t * Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[0] ); } +static inline Gia_ObjAre_t * Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[1] ); } +static inline Gia_ObjAre_t * Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[2] ); } + +static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, iReg << 1 ); } +static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, (iReg << 1) + 1 ); } + +static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, iReg << 1 ); } +static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, (iReg << 1) + 1 ); } + +static inline Gia_StaAre_t * Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iPrev); } +static inline Gia_StaAre_t * Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iNext); } +static inline int Gia_StaIsGood( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return ((unsigned *)pS) != p->ppStas[0]; } + +static inline void Gia_StaSetUnused( Gia_StaAre_t * pS ) { pS->iPrev.fMark = 1; } +static inline int Gia_StaIsUnused( Gia_StaAre_t * pS ) { return pS->iPrev.fMark; } +static inline int Gia_StaIsUsed( Gia_StaAre_t * pS ) { return !pS->iPrev.fMark; } + +#define Gia_ManAreForEachCubeList( p, pList, pCube ) \ + for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) ) +#define Gia_ManAreForEachCubeList2( p, iList, pCube, iCube ) \ + for ( iCube = Gia_Ptr2Int(iList), pCube = Gia_ManAreSta(p, iList); \ + Gia_StaIsGood(p, pCube); \ + iCube = Gia_Ptr2Int(pCube->iNext), pCube = Gia_StaNext(p, pCube) ) +#define Gia_ManAreForEachCubeStore( p, pCube, i ) \ + for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ ) +#define Gia_ManAreForEachCubeVec( vVec, p, pCube, i ) \ + for ( i = 0; i < Vec_IntSize(vVec) && (pCube = Gia_ManAreStaInt(p, Vec_IntEntry(vVec,i))); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Count state minterms contained in a cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pStore ) +{ + unsigned Mint, Mask = 0; + int i, m, nMints, nDashes = 0, Dashes[32]; + // count the number of dashes + for ( i = 0; i < nVars; i++ ) + { + if ( Gia_StaHasValue0( pCube, i ) ) + continue; + if ( Gia_StaHasValue1( pCube, i ) ) + Mask |= (1 << i); + else + Dashes[nDashes++] = i; + } + // fill in the miterms + nMints = (1 << nDashes); + for ( m = 0; m < nMints; m++ ) + { + Mint = Mask; + for ( i = 0; i < nVars; i++ ) + if ( m & (1 << i) ) + Mint |= (1 << Dashes[i]); + Gia_InfoSetBit( pStore, Mint ); + } +} + +/**Function************************************************************* + + Synopsis [Count state minterms contains in the used cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCountMinterms( Gia_ManAre_t * p ) +{ + Gia_StaAre_t * pCube; + unsigned * pMemory; + int i, nMemSize, Counter = 0; + if ( Gia_ManRegNum(p->pAig) > 30 ) + return -1; + nMemSize = Gia_BitWordNum( 1 << Gia_ManRegNum(p->pAig) ); + pMemory = ABC_CALLOC( unsigned, nMemSize ); + Gia_ManAreForEachCubeStore( p, pCube, i ) + if ( Gia_StaIsUsed(pCube) ) + Gia_ManCountMintermsInCube( pCube, Gia_ManRegNum(p->pAig), pMemory ); + for ( i = 0; i < nMemSize; i++ ) + Counter += Gia_WordCountOnes( pMemory[i] ); + ABC_FREE( pMemory ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Derives the TFO of one CI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManDeriveCiTfo_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRes ) +{ + if ( Gia_ObjIsCi(pObj) ) + return pObj->fMark0; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return pObj->fMark0; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes ); + Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin1(pObj), vRes ); + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 | Gia_ObjFanin1(pObj)->fMark0; + if ( pObj->fMark0 ) + Vec_IntPush( vRes, Gia_ObjId(p, pObj) ); + return pObj->fMark0; +} + + +/**Function************************************************************* + + Synopsis [Derives the TFO of one CI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDeriveCiTfoOne( Gia_Man_t * p, Gia_Obj_t * pPivot ) +{ + Vec_Int_t * vRes; + Gia_Obj_t * pObj; + int i; + assert( pPivot->fMark0 == 0 ); + pPivot->fMark0 = 1; + vRes = Vec_IntAlloc( 100 ); + Vec_IntPush( vRes, Gia_ObjId(p, pPivot) ); + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Gia_ManForEachCo( p, pObj, i ) + { + Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes ); + if ( Gia_ObjFanin0(pObj)->fMark0 ) + Vec_IntPush( vRes, Gia_ObjId(p, pObj) ); + } + pPivot->fMark0 = 0; + return vRes; +} + +/**Function************************************************************* + + Synopsis [Derives the TFO of each CI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Gia_ManDeriveCiTfo( Gia_Man_t * p ) +{ + Vec_Ptr_t * vRes; + Gia_Obj_t * pPivot; + int i; + Gia_ManCleanMark0( p ); + Gia_ManIncrementTravId( p ); + vRes = Vec_PtrAlloc( Gia_ManCiNum(p) ); + Gia_ManForEachCi( p, pPivot, i ) + Vec_PtrPush( vRes, Gia_ManDeriveCiTfoOne(p, pPivot) ); + Gia_ManCleanMark0( p ); + return (Vec_Vec_t *)vRes; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if states are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreEqual( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( p1->pData[w] != p2->pData[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if states are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreDisjoint( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( ((p1->pData[w] ^ p2->pData[w]) >> 1) & (p1->pData[w] ^ p2->pData[w]) & 0x55555555 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if cube p1 contains cube p2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreContain( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( (p1->pData[w] | p2->pData[w]) != p2->pData[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns the number of dashes in p1 that are non-dashes in p2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreDashNum( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + int w, Counter = 0; + for ( w = 0; w < nWords; w++ ) + Counter += Gia_WordCountOnes( (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555 ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the number of a variable for sharping the cube.] + + Description [Counts the number of variables that have dash in p1 and + non-dash in p2. If there is exactly one such variable, returns its index. + Otherwise returns -1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreSharpVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + unsigned Word; + int w, iVar = -1; + for ( w = 0; w < nWords; w++ ) + { + Word = (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555; + if ( Word == 0 ) + continue; + if ( !Gia_WordHasOneBit(Word) ) + return -1; + // has exactly one bit + if ( iVar >= 0 ) + return -1; + // the first variable of this type + iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2; + } + return iVar; +} + +/**Function************************************************************* + + Synopsis [Returns the number of a variable for merging the cubes.] + + Description [If there is exactly one such variable, returns its index. + Otherwise returns -1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_StaAreDisjointVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords ) +{ + unsigned Word; + int w, iVar = -1; + for ( w = 0; w < nWords; w++ ) + { + Word = (p1->pData[w] ^ p2->pData[w]) & ((p1->pData[w] ^ p2->pData[w]) >> 1) & 0x55555555; + if ( Word == 0 ) + continue; + if ( !Gia_WordHasOneBit(Word) ) + return -1; + // has exactly one bit + if ( iVar >= 0 ) + return -1; + // the first variable of this type + iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2; + } + return iVar; +} + +/**Function************************************************************* + + Synopsis [Creates reachability manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig ) +{ + Gia_ManAre_t * p; + assert( sizeof(Gia_ObjAre_t) == 16 ); + p = ABC_CALLOC( Gia_ManAre_t, 1 ); + p->pAig = pAig; + p->nWords = Gia_BitWordNum( 2 * Gia_ManRegNum(pAig) ); + p->nSize = sizeof(Gia_StaAre_t)/4 + p->nWords; + p->ppObjs = ABC_CALLOC( unsigned *, MAX_PAGE_NUM ); + p->ppStas = ABC_CALLOC( unsigned *, MAX_PAGE_NUM ); + p->vCiTfos = Gia_ManDeriveCiTfo( pAig ); + p->vCiLits = Vec_VecDupInt( p->vCiTfos ); + p->vCubesA = Vec_IntAlloc( 100 ); + p->vCubesB = Vec_IntAlloc( 100 ); + p->iOutFail = -1; + return p; +} + +/**Function************************************************************* + + Synopsis [Deletes reachability manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreFree( Gia_ManAre_t * p ) +{ + int i; + Gia_ManStop( p->pAig ); + if ( p->pNew ) + Gia_ManStop( p->pNew ); + Vec_IntFree( p->vCubesA ); + Vec_IntFree( p->vCubesB ); + Vec_VecFree( p->vCiTfos ); + Vec_VecFree( p->vCiLits ); + for ( i = 0; i < p->nObjPages; i++ ) + ABC_FREE( p->ppObjs[i] ); + ABC_FREE( p->ppObjs ); + for ( i = 0; i < p->nStaPages; i++ ) + ABC_FREE( p->ppStas[i] ); + ABC_FREE( p->ppStas ); +// ABC_FREE( p->pfUseless ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Returns new object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_ObjAre_t * Gia_ManAreCreateObj( Gia_ManAre_t * p ) +{ + if ( p->nObjs == p->nObjPages * MAX_ITEM_NUM ) + { + if ( p->nObjPages == MAX_PAGE_NUM ) + { + printf( "ERA manager has run out of memory after allocating 2B internal nodes.\n" ); + return NULL; + } + p->ppObjs[p->nObjPages++] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * 4 ); + if ( p->nObjs == 0 ) + p->nObjs = 1; + } + return Gia_ManAreObjInt( p, p->nObjs++ ); +} + +/**Function************************************************************* + + Synopsis [Returns new state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_StaAre_t * Gia_ManAreCreateSta( Gia_ManAre_t * p ) +{ + if ( p->nStas == p->nStaPages * MAX_ITEM_NUM ) + { + if ( p->nStaPages == MAX_PAGE_NUM ) + { + printf( "ERA manager has run out of memory after allocating 2B state cubes.\n" ); + return NULL; + } + if ( p->ppStas[p->nStaPages] == NULL ) + p->ppStas[p->nStaPages] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * p->nSize ); + p->nStaPages++; + if ( p->nStas == 0 ) + { + p->nStas = 1; +// p->nUselessAlloc = (1 << 18); +// p->pfUseless = ABC_CALLOC( unsigned, p->nUselessAlloc ); + } +// if ( p->nStas == p->nUselessAlloc * 32 ) +// { +// p->nUselessAlloc *= 2; +// p->pfUseless = ABC_REALLOC( unsigned, p->pfUseless, p->nUselessAlloc ); +// memset( p->pfUseless + p->nUselessAlloc/2, 0, sizeof(unsigned) * p->nUselessAlloc/2 ); +// } + } + return Gia_ManAreStaInt( p, p->nStas++ ); +} + +/**Function************************************************************* + + Synopsis [Recycles new state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManAreRycycleSta( Gia_ManAre_t * p, Gia_StaAre_t * pSta ) +{ + memset( pSta, 0, p->nSize << 2 ); + if ( pSta == Gia_ManAreStaLast(p) ) + { + p->nStas--; + if ( p->nStas == (p->nStaPages-1) * MAX_ITEM_NUM ) + p->nStaPages--; + } + else + { +// Gia_StaSetUnused( pSta ); + } +} + +/**Function************************************************************* + + Synopsis [Creates new state state from the latch values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_StaAre_t * Gia_ManAreCreateStaNew( Gia_ManAre_t * p ) +{ + Gia_StaAre_t * pSta; + Gia_Obj_t * pObj; + int i; + pSta = Gia_ManAreCreateSta( p ); + Gia_ManForEachRi( p->pAig, pObj, i ) + { + if ( pObj->Value == 0 ) + Gia_StaSetValue0( pSta, i ); + else if ( pObj->Value == 1 ) + Gia_StaSetValue1( pSta, i ); + } + return pSta; +} + +/**Function************************************************************* + + Synopsis [Creates new state state with latch init values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_StaAre_t * Gia_ManAreCreateStaInit( Gia_ManAre_t * p ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachRi( p->pAig, pObj, i ) + pObj->Value = 0; + return Gia_ManAreCreateStaNew( p ); +} + + +/**Function************************************************************* + + Synopsis [Prints the state cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManArePrintCube( Gia_ManAre_t * p, Gia_StaAre_t * pSta ) +{ + Gia_Obj_t * pObj; + int i, Count0 = 0, Count1 = 0, Count2 = 0; + printf( "%4d %4d : ", p->iStaCur, p->nStas-1 ); + printf( "Prev %4d ", Gia_Ptr2Int(pSta->iPrev) ); + printf( "%p ", pSta ); + Gia_ManForEachRi( p->pAig, pObj, i ) + { + if ( Gia_StaHasValue0(pSta, i) ) + printf( "0" ), Count0++; + else if ( Gia_StaHasValue1(pSta, i) ) + printf( "1" ), Count1++; + else + printf( "-" ), Count2++; + } + printf( " 0 =%3d", Count0 ); + printf( " 1 =%3d", Count1 ); + printf( " - =%3d", Count2 ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Counts the depth of state transitions leading ot this state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreDepth( Gia_ManAre_t * p, int iState ) +{ + Gia_StaAre_t * pSta; + int Counter = 0; + for ( pSta = Gia_ManAreStaInt(p, iState); Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManAreListCountListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root ) +{ + Gia_StaAre_t * pCube; + int Counter = 0; + Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube ) + Counter += Gia_StaIsUsed(pCube); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of used cubes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreListCountUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree ) +{ + Gia_ObjAre_t * pObj; + if ( !fTree ) + return Gia_ManAreListCountListUsed( p, Root ); + pObj = Gia_ManAreObj(p, Root); + return Gia_ManAreListCountUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) + + Gia_ManAreListCountUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) + + Gia_ManAreListCountUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of used cubes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManAreListCountUsed( Gia_ManAre_t * p ) +{ + return Gia_ManAreListCountUsed_rec( p, p->Root, p->fTree ); +} + + +/**Function************************************************************* + + Synopsis [Prints used cubes in the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManArePrintListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root ) +{ + Gia_StaAre_t * pCube; + Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube ) + if ( Gia_StaIsUsed(pCube) ) + Gia_ManArePrintCube( p, pCube ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Prints used cubes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManArePrintUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree ) +{ + Gia_ObjAre_t * pObj; + if ( !fTree ) + return Gia_ManArePrintListUsed( p, Root ); + pObj = Gia_ManAreObj(p, Root); + return Gia_ManArePrintUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) + + Gia_ManArePrintUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) + + Gia_ManArePrintUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Prints used cubes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManArePrintUsed( Gia_ManAre_t * p ) +{ + return Gia_ManArePrintUsed_rec( p, p->Root, p->fTree ); +} + + +/**Function************************************************************* + + Synopsis [Best var has max weight.] + + Description [Weight is defined as the number of 0/1-lits minus the + absolute value of the diff between the number of 0-lits and 1-lits.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreFindBestVar( Gia_ManAre_t * p, Gia_PtrAre_t List ) +{ + Gia_StaAre_t * pCube; + int Count0, Count1, Count2; + int iVarThis, iVarBest = -1, WeightThis, WeightBest = -1; + for ( iVarThis = 0; iVarThis < Gia_ManRegNum(p->pAig); iVarThis++ ) + { + Count0 = Count1 = Count2 = 0; + Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, List), pCube ) + { + if ( Gia_StaIsUnused(pCube) ) + continue; + if ( Gia_StaHasValue0(pCube, iVarThis) ) + Count0++; + else if ( Gia_StaHasValue1(pCube, iVarThis) ) + Count1++; + else + Count2++; + } +// printf( "%4d : %5d %5d %5d Weight = %5d\n", iVarThis, Count0, Count1, Count2, +// Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0) ); + if ( (!Count0 && !Count1) || (!Count0 && !Count2) || (!Count1 && !Count2) ) + continue; + WeightThis = Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0); + if ( WeightBest < WeightThis ) + { + WeightBest = WeightThis; + iVarBest = iVarThis; + } + } + if ( iVarBest == -1 ) + { + Gia_ManArePrintListUsed( p, List ); + printf( "Error: Best variable not found!!!\n" ); + } + assert( iVarBest != -1 ); + return iVarBest; +} + +/**Function************************************************************* + + Synopsis [Rebalances the tree when cubes exceed the limit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManAreRebalance( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot ) +{ + Gia_ObjAre_t * pNode; + Gia_StaAre_t * pCube; + Gia_PtrAre_t iCube, iNext; + assert( pRoot->nItem || pRoot->nPage ); + pNode = Gia_ManAreCreateObj( p ); + pNode->iVar = Gia_ManAreFindBestVar( p, *pRoot ); + for ( iCube = *pRoot, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext; + Gia_StaIsGood(p, pCube); + iCube = iNext, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext ) + { + if ( Gia_StaIsUnused(pCube) ) + continue; + if ( Gia_StaHasValue0(pCube, pNode->iVar) ) + pCube->iNext = pNode->F[0], pNode->F[0] = iCube, pNode->nStas0++; + else if ( Gia_StaHasValue1(pCube, pNode->iVar) ) + pCube->iNext = pNode->F[1], pNode->F[1] = iCube, pNode->nStas1++; + else + pCube->iNext = pNode->F[2], pNode->F[2] = iCube, pNode->nStas2++; + } + *pRoot = Gia_Int2Ptr(p->nObjs - 1); + assert( pNode == Gia_ManAreObj(p, *pRoot) ); + p->fTree = 1; +} + +/**Function************************************************************* + + Synopsis [Compresses the list by removing unused cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManAreCompress( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot ) +{ + Gia_StaAre_t * pCube; + Gia_PtrAre_t iList = *pRoot; + Gia_PtrAre_t iCube, iNext; + assert( pRoot->nItem || pRoot->nPage ); + pRoot->nItem = 0; + pRoot->nPage = 0; + for ( iCube = iList, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext; + Gia_StaIsGood(p, pCube); + iCube = iNext, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext ) + { + if ( Gia_StaIsUnused(pCube) ) + continue; + pCube->iNext = *pRoot; + *pRoot = iCube; + } +} + + +/**Function************************************************************* + + Synopsis [Checks if the state exists in the list.] + + Description [The state may be sharped.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManAreCubeCheckList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta ) +{ + int fVerbose = 0; + Gia_StaAre_t * pCube; + int iVar; +if ( fVerbose ) +{ +printf( "Trying cube: " ); +Gia_ManArePrintCube( p, pSta ); +} + Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, *pRoot), pCube ) + { + p->nChecks++; + if ( Gia_StaIsUnused( pCube ) ) + continue; + if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) ) + continue; + if ( Gia_StaAreContain( pCube, pSta, p->nWords ) ) + { +if ( fVerbose ) +{ +printf( "Contained in " ); +Gia_ManArePrintCube( p, pCube ); +} + Gia_ManAreRycycleSta( p, pSta ); + return 0; + } + if ( Gia_StaAreContain( pSta, pCube, p->nWords ) ) + { +if ( fVerbose ) +{ +printf( "Contains " ); +Gia_ManArePrintCube( p, pCube ); +} + Gia_StaSetUnused( pCube ); + continue; + } + iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords ); + if ( iVar == -1 ) + continue; +if ( fVerbose ) +{ +printf( "Sharped by " ); +Gia_ManArePrintCube( p, pCube ); +Gia_ManArePrintCube( p, pSta ); +} +// printf( "%d %d\n", Gia_StaAreDashNum( pSta, pCube, p->nWords ), Gia_StaAreSharpVar( pSta, pCube, p->nWords ) ); + assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) ); + assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) ); + if ( Gia_StaHasValue0(pCube, iVar) ) + Gia_StaSetValue1( pSta, iVar ); + else + Gia_StaSetValue0( pSta, iVar ); +// return Gia_ManAreCubeCheckList( p, pRoot, pSta ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds new state to the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManAreCubeAddToList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta ) +{ + int fVerbose = 0; + pSta->iNext = *pRoot; + *pRoot = Gia_Int2Ptr( p->nStas - 1 ); + assert( pSta == Gia_ManAreSta(p, *pRoot) ); +if ( fVerbose ) +{ +printf( "Adding cube: " ); +Gia_ManArePrintCube( p, pSta ); +//printf( "\n" ); +} +} + +/**Function************************************************************* + + Synopsis [Checks if the cube like this exists in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreCubeCheckTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta ) +{ + int RetValue; + if ( Gia_StaHasValue0(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch0(pObj) ) + RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta ); + else + RetValue = Gia_ManAreCubeCheckList( p, pObj->F, pSta ); + if ( RetValue == 0 ) + return 0; + } + else if ( Gia_StaHasValue1(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch1(pObj) ) + RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta ); + else + RetValue = Gia_ManAreCubeCheckList( p, pObj->F + 1, pSta ); + if ( RetValue == 0 ) + return 0; + } + if ( Gia_ObjHasBranch2(pObj) ) + return Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta ); + return Gia_ManAreCubeCheckList( p, pObj->F + 2, pSta ); +} + +/**Function************************************************************* + + Synopsis [Adds new cube to the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreCubeAddToTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta ) +{ + if ( Gia_StaHasValue0(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch0(pObj) ) + Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta ); + else + { + Gia_ManAreCubeAddToList( p, pObj->F, pSta ); + if ( ++pObj->nStas0 == MAX_CUBE_NUM ) + { + pObj->nStas0 = Gia_ManAreListCountListUsed( p, pObj->F[0] ); + if ( pObj->nStas0 < MAX_CUBE_NUM/2 ) + Gia_ManAreCompress( p, pObj->F ); + else + { + Gia_ManAreRebalance( p, pObj->F ); + pObj->nStas0 = 0; + } + } + } + } + else if ( Gia_StaHasValue1(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch1(pObj) ) + Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta ); + else + { + Gia_ManAreCubeAddToList( p, pObj->F+1, pSta ); + if ( ++pObj->nStas1 == MAX_CUBE_NUM ) + { + pObj->nStas1 = Gia_ManAreListCountListUsed( p, pObj->F[1] ); + if ( pObj->nStas1 < MAX_CUBE_NUM/2 ) + Gia_ManAreCompress( p, pObj->F+1 ); + else + { + Gia_ManAreRebalance( p, pObj->F+1 ); + pObj->nStas1 = 0; + } + } + } + } + else + { + if ( Gia_ObjHasBranch2(pObj) ) + Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta ); + else + { + Gia_ManAreCubeAddToList( p, pObj->F+2, pSta ); + if ( ++pObj->nStas2 == MAX_CUBE_NUM ) + { + pObj->nStas2 = Gia_ManAreListCountListUsed( p, pObj->F[2] ); + if ( pObj->nStas2 < MAX_CUBE_NUM/2 ) + Gia_ManAreCompress( p, pObj->F+2 ); + else + { + Gia_ManAreRebalance( p, pObj->F+2 ); + pObj->nStas2 = 0; + } + } + } + } +} + + + +/**Function************************************************************* + + Synopsis [Collects overlapping cubes in the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManAreCubeCollectList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta ) +{ + Gia_StaAre_t * pCube; + int iCube; + Gia_ManAreForEachCubeList2( p, *pRoot, pCube, iCube ) + { + if ( Gia_StaIsUnused( pCube ) ) + continue; + if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) ) + { +/* + int iVar; + p->nDisjs++; + iVar = Gia_StaAreDisjointVar( pSta, pCube, p->nWords ); + if ( iVar >= 0 ) + { + p->nDisjs2++; + if ( iCube > p->iStaCur ) + p->nDisjs3++; + } +*/ + continue; + } +// p->nCompares++; +// p->nEquals += Gia_StaAreEqual( pSta, pCube, p->nWords ); + if ( iCube <= p->iStaCur ) + Vec_IntPush( p->vCubesA, iCube ); + else + Vec_IntPush( p->vCubesB, iCube ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Collects overlapping cubes in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreCubeCollectTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta ) +{ + int RetValue; + if ( Gia_StaHasValue0(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch0(pObj) ) + RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta ); + else + RetValue = Gia_ManAreCubeCollectList( p, pObj->F, pSta ); + if ( RetValue == 0 ) + return 0; + } + else if ( Gia_StaHasValue1(pSta, pObj->iVar) ) + { + if ( Gia_ObjHasBranch1(pObj) ) + RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta ); + else + RetValue = Gia_ManAreCubeCollectList( p, pObj->F + 1, pSta ); + if ( RetValue == 0 ) + return 0; + } + if ( Gia_ObjHasBranch2(pObj) ) + return Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta ); + return Gia_ManAreCubeCollectList( p, pObj->F + 2, pSta ); +} + +/**Function************************************************************* + + Synopsis [Checks if the cube like this exists in the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreCubeCheckTree( Gia_ManAre_t * p, Gia_StaAre_t * pSta ) +{ + Gia_StaAre_t * pCube; + int i, iVar; + assert( p->fTree ); + Vec_IntClear( p->vCubesA ); + Vec_IntClear( p->vCubesB ); + Gia_ManAreCubeCollectTree_rec( p, Gia_ManAreObj(p, p->Root), pSta ); +// if ( p->nStas > 3000 ) +// printf( "%d %d \n", Vec_IntSize(p->vCubesA), Vec_IntSize(p->vCubesB) ); +// Vec_IntSort( p->vCubesA, 0 ); +// Vec_IntSort( p->vCubesB, 0 ); + Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i ) + { + if ( Gia_StaIsUnused( pCube ) ) + continue; + if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) ) + continue; + if ( Gia_StaAreContain( pCube, pSta, p->nWords ) ) + { + Gia_ManAreRycycleSta( p, pSta ); + return 0; + } + if ( Gia_StaAreContain( pSta, pCube, p->nWords ) ) + { + Gia_StaSetUnused( pCube ); + continue; + } + iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords ); + if ( iVar == -1 ) + continue; + assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) ); + assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) ); + if ( Gia_StaHasValue0(pCube, iVar) ) + Gia_StaSetValue1( pSta, iVar ); + else + Gia_StaSetValue0( pSta, iVar ); + return Gia_ManAreCubeCheckTree( p, pSta ); + } + Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i ) + { + if ( Gia_StaIsUnused( pCube ) ) + continue; + if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) ) + continue; + if ( Gia_StaAreContain( pCube, pSta, p->nWords ) ) + { + Gia_ManAreRycycleSta( p, pSta ); + return 0; + } + if ( Gia_StaAreContain( pSta, pCube, p->nWords ) ) + { + Gia_StaSetUnused( pCube ); + continue; + } + iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords ); + if ( iVar == -1 ) + continue; + assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) ); + assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) ); + if ( Gia_StaHasValue0(pCube, iVar) ) + Gia_StaSetValue1( pSta, iVar ); + else + Gia_StaSetValue0( pSta, iVar ); + return Gia_ManAreCubeCheckTree( p, pSta ); + } +/* + if ( p->nStas > 3000 ) + { +printf( "Trying cube: " ); +Gia_ManArePrintCube( p, pSta ); + Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i ) + { +printf( "aaaaaaaaaaaa %5d ", Vec_IntEntry(p->vCubesA,i) ); +Gia_ManArePrintCube( p, pCube ); + } + Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i ) + { +printf( "bbbbbbbbbbbb %5d ", Vec_IntEntry(p->vCubesB,i) ); +Gia_ManArePrintCube( p, pCube ); + } + } +*/ + return 1; +} + +/**Function************************************************************* + + Synopsis [Processes the new cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManAreCubeProcess( Gia_ManAre_t * p, Gia_StaAre_t * pSta ) +{ + int RetValue; + p->nChecks = 0; + if ( !p->fTree && p->nStas == MAX_CUBE_NUM ) + Gia_ManAreRebalance( p, &p->Root ); + if ( p->fTree ) + { +// RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ManAreObj(p, p->Root), pSta ); + RetValue = Gia_ManAreCubeCheckTree( p, pSta ); + if ( RetValue ) + Gia_ManAreCubeAddToTree_rec( p, Gia_ManAreObj(p, p->Root), pSta ); + } + else + { + RetValue = Gia_ManAreCubeCheckList( p, &p->Root, pSta ); + if ( RetValue ) + Gia_ManAreCubeAddToList( p, &p->Root, pSta ); + } +// printf( "%d ", p->nChecks ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Returns the most used CI, or NULL if condition is met.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreMostUsedPi_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + pObj->Value++; + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Returns the most used CI, or NULL if condition is met.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p ) +{ + Gia_Obj_t * pObj, * pObjMax = NULL; + int i; + // clean CI counters + Gia_ManForEachCi( p->pNew, pObj, i ) + pObj->Value = 0; + // traverse from each register output + Gia_ManForEachRi( p->pAig, pObj, i ) + { + if ( pObj->Value <= 1 ) + continue; + Gia_ManIncrementTravId( p->pNew ); + Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Gia_Lit2Var(pObj->Value)) ); + } + // check the CI counters + Gia_ManForEachCi( p->pNew, pObj, i ) + if ( pObjMax == NULL || pObjMax->Value < pObj->Value ) + pObjMax = pObj; + // return the result + return pObjMax->Value > 1 ? pObjMax : NULL; +} + +/**Function************************************************************* + + Synopsis [Counts maximum support of primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCheckPOs_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + return 1; + assert( Gia_ObjIsAnd(pObj) ); + return Gia_ManCheckPOs_rec( p, Gia_ObjFanin0(pObj) ) + + Gia_ManCheckPOs_rec( p, Gia_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Counts maximum support of primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManCheckPOs( Gia_ManAre_t * p ) +{ + Gia_Obj_t * pObj, * pObjNew; + int i, CountCur, CountMax = 0; + Gia_ManForEachPo( p->pAig, pObj, i ) + { + pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) ); + if ( Gia_ObjIsConst0(pObjNew) ) + CountCur = 0; + else + { + Gia_ManIncrementTravId( p->pNew ); + CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew ); + } + CountMax = ABC_MAX( CountMax, CountCur ); + } + return CountMax; +} + +/**Function************************************************************* + + Synopsis [Returns the status of the primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p ) +{ + Gia_Obj_t * pObj, * pObjNew; + int i; + Gia_ManForEachPo( p->pAig, pObj, i ) + { + pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) ); + if ( Gia_ObjIsConst0(pObjNew) ) + { + if ( Gia_LitIsCompl(pObj->Value) ) + { + p->iOutFail = i; + return 1; + } + } + else + { + p->iOutFail = i; +// printf( "To fix later: PO may be assertable.\n" ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives next state cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) +{ + Gia_Obj_t * pPivot; + Vec_Int_t * vLits, * vTfos; + Gia_Obj_t * pObj; + int i, clk; + if ( ++p->nRecCalls == MAX_CALL_NUM ) + return 0; + if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL ) + { + Gia_StaAre_t * pNew; + clk = clock(); + pNew = Gia_ManAreCreateStaNew( p ); + pNew->iPrev = Sta; + p->fStopped = (p->fMiter && (Gia_ManCheckPOstatus(p) & 1)); + if ( p->fStopped ) + { + assert( p->pTarget == NULL ); + p->pTarget = pNew; + return 1; + } + Gia_ManAreCubeProcess( p, pNew ); + p->timeCube += clock() - clk; + return p->fStopped; + } + // remember values in the cone and perform update + vTfos = (Vec_Int_t *)Vec_VecEntry( p->vCiTfos, Gia_ObjCioId(pPivot) ); + vLits = (Vec_Int_t *)Vec_VecEntry( p->vCiLits, Gia_ObjCioId(pPivot) ); + assert( Vec_IntSize(vTfos) == Vec_IntSize(vLits) ); + Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i ) + { + Vec_IntWriteEntry( vLits, i, pObj->Value ); + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + else + { + assert( Gia_ObjIsCi(pObj) ); + pObj->Value = 0; + } + } + if ( Gia_ManAreDeriveNexts_rec( p, Sta ) ) + return 1; + // compute different values + Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + else + { + assert( Gia_ObjIsCi(pObj) ); + pObj->Value = 1; + } + } + if ( Gia_ManAreDeriveNexts_rec( p, Sta ) ) + return 1; + // reset the original values + Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i ) + pObj->Value = Vec_IntEntry( vLits, i ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives next state cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) +{ + Gia_StaAre_t * pSta; + Gia_Obj_t * pObj; + int i, RetValue, clk = clock(); + pSta = Gia_ManAreSta( p, Sta ); + if ( Gia_StaIsUnused(pSta) ) + return 0; + // recycle the manager + if ( p->pNew && Gia_ManObjNum(p->pNew) > 1000000 ) + { + Gia_ManStop( p->pNew ); + p->pNew = NULL; + } + // allocate the manager + if ( p->pNew == NULL ) + { + p->pNew = Gia_ManStart( 10 * Gia_ManObjNum(p->pAig) ); + Gia_ManIncrementTravId( p->pNew ); + Gia_ManHashAlloc( p->pNew ); + Gia_ManConst0(p->pAig)->Value = 0; + Gia_ManForEachCi( p->pAig, pObj, i ) + pObj->Value = Gia_ManAppendCi(p->pNew); + } + Gia_ManForEachRo( p->pAig, pObj, i ) + { + if ( Gia_StaHasValue0( pSta, i ) ) + pObj->Value = 0; + else if ( Gia_StaHasValue1( pSta, i ) ) + pObj->Value = 1; + else // don't-care literal + pObj->Value = Gia_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 ); + } + Gia_ManForEachAnd( p->pAig, pObj, i ) + pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p->pAig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + + // perform case-splitting + p->nRecCalls = 0; + RetValue = Gia_ManAreDeriveNexts_rec( p, Sta ); + if ( p->nRecCalls >= MAX_CALL_NUM ) + { + printf( "Exceeded the limit on the number of transitions from a state cube (%d).\n", MAX_CALL_NUM ); + p->fStopped = 1; + } +// printf( "%d ", p->nRecCalls ); +//printf( "%d ", Gia_ManObjNum(p->pNew) ); + p->timeAig += clock() - clk; + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Prints the report] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManArePrintReport( Gia_ManAre_t * p, int Time, int fFinal ) +{ + printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f Mb. ", + p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur), + (sizeof(Gia_ManAre_t) + 4.0*Gia_ManRegNum(p->pAig) + 8.0*MAX_PAGE_NUM + + 4.0*p->nStaPages*p->nSize*MAX_ITEM_NUM + 16.0*p->nObjPages*MAX_ITEM_NUM)/(1<<20) ); + if ( fFinal ) + { + ABC_PRT( "Time", clock() - Time ); + } + else + { + ABC_PRTr( "Time", clock() - Time ); + } +} + +/**Function************************************************************* + + Synopsis [Performs explicit reachability.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ) +{ +// extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ); + extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ); + Gia_ManAre_t * p; + int clk = clock(); + int RetValue = 1; + if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM ) + { + printf( "Currently can only handle circuit with up to %d registers.\n", MAX_VARS_NUM ); + return -1; + } + ABC_FREE( pAig->pCexSeq ); + p = Gia_ManAreCreate( Gia_ManCompress2(pAig, 0, 0) ); + p->fMiter = fMiter; + Gia_ManAreCubeProcess( p, Gia_ManAreCreateStaInit(p) ); + for ( p->iStaCur = 1; p->iStaCur < p->nStas; p->iStaCur++ ) + { +// printf( "Explored state %d. Total cubes %d.\n", p->iStaCur, p->nStas-1 ); + if ( Gia_ManAreDeriveNexts( p, Gia_Int2Ptr(p->iStaCur) ) || p->nStas > nStatesMax ) + pAig->pCexSeq = Gia_ManAreDeriveCex( p, p->pTarget ); + if ( p->fStopped ) + { + RetValue = -1; + break; + } + if ( fVerbose && p->iStaCur % 5000 == 0 ) + Gia_ManArePrintReport( p, clk, 0 ); + } + Gia_ManArePrintReport( p, clk, 1 ); + printf( "%s after finding %d state cubes (%d not contained) with depth %d. ", + p->fStopped ? "Stopped" : "Completed", + p->nStas, Gia_ManAreListCountUsed(p), + Gia_ManAreDepth(p, p->iStaCur-1) ); + ABC_PRT( "Time", clock() - clk ); + if ( pAig->pCexSeq != NULL ) +// printf( "Miter FAILED in state %d at frame %d (use \"&write_counter\" to dump a witness)\n", + printf( "Miter FAILED in state %d at frame %d (the cex is available for refinement)\n", + p->iStaCur, Gia_ManAreDepth(p, p->iStaCur)-1 ); + if ( fVerbose ) + { + ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube, clock() - clk ); + ABC_PRTP( "Containment", p->timeCube, clock() - clk ); + ABC_PRTP( "Other ", clock() - clk - p->timeAig, clock() - clk ); + ABC_PRTP( "TOTAL ", clock() - clk, clock() - clk ); + } + if ( Gia_ManRegNum(pAig) <= 30 ) + { + clk = clock(); + printf( "The number of unique state minterms in computed state cubes is %d. ", Gia_ManCountMinterms(p) ); + ABC_PRT( "Time", clock() - clk ); + } +// printf( "Compares = %d. Equals = %d. Disj = %d. Disj2 = %d. Disj3 = %d.\n", +// p->nCompares, p->nEquals, p->nDisjs, p->nDisjs2, p->nDisjs3 ); +// Gia_ManAreFindBestVar( p, Gia_ManAreSta(p, p->Root) ); +// Gia_ManArePrintUsed( p ); + Gia_ManAreFree( p ); + // verify + if ( pAig->pCexSeq ) + { + if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + printf( "Generated counter-example is INVALID. \n" ); + else + printf( "Generated counter-example verified correctly. \n" ); + return 0; + } + return RetValue; +} + +ABC_NAMESPACE_IMPL_END + +#include "giaAig.h" +#include "cnf.h" +#include "satSolver.h" + +ABC_NAMESPACE_IMPL_START + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreDeriveCexSatStart( Gia_ManAre_t * p ) +{ + Aig_Man_t * pAig2; + Cnf_Dat_t * pCnf; + assert( p->pSat == NULL ); + pAig2 = Gia_ManToAig( p->pAig, 0 ); + Aig_ManSetRegNum( pAig2, 0 ); + pCnf = Cnf_Derive( pAig2, Gia_ManCoNum(p->pAig) ); + p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + p->vSatNumCis = Cnf_DataCollectCiSatNums( pCnf, pAig2 ); + p->vSatNumCos = Cnf_DataCollectCoSatNums( pCnf, pAig2 ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pAig2 ); + p->vAssumps = Vec_IntAlloc( 100 ); + p->vCofVars = Vec_IntAlloc( 100 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreDeriveCexSatStop( Gia_ManAre_t * p ) +{ + assert( p->pSat != NULL ); + assert( p->pTarget != NULL ); + sat_solver_delete( (sat_solver *)p->pSat ); + Vec_IntFree( p->vSatNumCis ); + Vec_IntFree( p->vSatNumCos ); + Vec_IntFree( p->vAssumps ); + Vec_IntFree( p->vCofVars ); + p->pTarget = NULL; + p->pSat = NULL; +} + +/**Function************************************************************* + + Synopsis [Computes satisfying assignment in one timeframe.] + + Description [Returns the vector of integers represeting PIO ids + of the primary inputs that should be 1 in the counter-example.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t * pNext, int iOutFailed ) +{ + int i, status; + // make assuptions + Vec_IntClear( p->vAssumps ); + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + if ( Gia_StaHasValue0(pCur, i) ) + Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) ); + else if ( Gia_StaHasValue1(pCur, i) ) + Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) ); + } + if ( pNext ) + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + if ( Gia_StaHasValue0(pNext, i) ) + Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) ); + else if ( Gia_StaHasValue1(pNext, i) ) + Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) ); + } + if ( iOutFailed >= 0 ) + { + assert( iOutFailed < Gia_ManPoNum(p->pAig) ); + Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) ); + } + // solve SAT + status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps), + (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status != l_True ) + { + printf( "SAT problem is not satisfiable. Failure...\n" ); + return; + } + assert( status == l_True ); + // check the model + Vec_IntClear( p->vCofVars ); + for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) + { + if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, i) ) ) + Vec_IntPush( p->vCofVars, i ); + } + // write the current state + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + if ( Gia_StaHasValue0(pCur, i) ) + assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 ); + else if ( Gia_StaHasValue1(pCur, i) ) + assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 1 ); + // set don't-care value + if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 ) + Gia_StaSetValue0( pCur, i ); + else + Gia_StaSetValue1( pCur, i ); + } +} + +/**Function************************************************************* + + Synopsis [Returns the status of the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ) +{ + Abc_Cex_t * pCex; + Vec_Ptr_t * vStates; + Gia_StaAre_t * pSta, * pPrev; + int Var, i, v; + assert( p->iOutFail >= 0 ); + Gia_ManAreDeriveCexSatStart( p ); + // compute the trace + vStates = Vec_PtrAlloc( 1000 ); + for ( pSta = pLast; Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) ) + if ( pSta != pLast ) + Vec_PtrPush( vStates, pSta ); + assert( Vec_PtrSize(vStates) >= 1 ); + // start the counter-example + pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) ); + pCex->iFrame = Vec_PtrSize(vStates)-1; + pCex->iPo = p->iOutFail; + // compute states + pPrev = NULL; + Vec_PtrForEachEntry( Gia_StaAre_t *, vStates, pSta, i ) + { + Gia_ManAreDeriveCexSat( p, pSta, pPrev, (i == 0) ? p->iOutFail : -1 ); + pPrev = pSta; + // create the counter-example + Vec_IntForEachEntry( p->vCofVars, Var, v ) + { + assert( Var < Gia_ManPiNum(p->pAig) ); + Gia_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var ); + } + } + // free temporary things + Vec_PtrFree( vStates ); + Gia_ManAreDeriveCexSatStop( p ); + return pCex; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |