69 p->fUseEsop = fUseEsop;
90 printf(
"Abc_NtkCov: The network check has failed.\n" );
127 printf(
"Iter %d : ", i+1 );
222 printf(
"Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ",
287 assert( vSupp0 && vSupp1 );
288 Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
289 Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
294 for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
296 if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
305 else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
318 for ( ; k0 < vSupp0->nSize; k0++ )
323 for ( ; k1 < vSupp1->nSize; k1++ )
361 Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
362 Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
365 int fCompl0, fCompl1;
379 if ( vSupp->nSize > p->nFaninMax )
395 if ( pCov0 && pCov1 )
400 else if ( pCov0 && pCov0->
nLits == 0 )
401 pCover0 = pCov0->
pNext;
403 pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->
pNext = pCov0;
408 else if ( pCov1 && pCov1->
nLits == 0 )
409 pCover1 = pCov1->
pNext;
411 pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->
pNext = pCov1;
424 if ( pCover0 && pCover1 )
431 if ( pCover0 && pCover1 )
436 if ( !pCoverX && !pCoverP && !pCoverN )
452 p->nSuppsMax =
Abc_MaxInt( p->nSuppsMax, p->nSupps );
474 assert( pCover0 && pCover1 );
483 for ( i = 0; i < p->vPairs0->nSize; i++ )
487 if ( (Val0 & Val1) == 0 )
491 if ( i < p->vPairs0->nSize )
494 if ( p->pManMin->nCubes > p->nCubesMax )
507 for ( i = 0; i < nSupp; i++ )
509 if ( p->vComTo0->pArray[i] == -1 )
514 if ( p->vComTo1->pArray[i] == -1 )
519 if ( (Val0 & Val1) == 3 )
578 assert( pCover0 && pCover1 );
587 for ( i = 0; i < p->vComTo0->nSize; i++ )
589 if ( p->vComTo0->pArray[i] == -1 )
597 if ( p->pManMin->nCubes > p->nCubesMax )
614 for ( i = 0; i < p->vComTo1->nSize; i++ )
616 if ( p->vComTo1->pArray[i] == -1 )
624 if ( p->pManMin->nCubes > p->nCubesMax )
676 Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1;
688 if ( vSupp->nSize > p->nFaninMax )
701 else if ( pCov0 && pCov0->
nLits == 0 )
702 pCover0 = pCov0->
pNext;
704 pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->
pNext = pCov0;
709 else if ( pCov1 && pCov1->
nLits == 0 )
710 pCover1 = pCov1->
pNext;
712 pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->
pNext = pCov1;
715 if ( !Abc_NodeCovProductEsop( p, pCover0, pCover1, vSupp->nSize ) )
737 p->nSuppsMax =
Abc_MaxInt( p->nSuppsMax, p->nSupps );
759 Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1;
761 int fCompl0, fCompl1;
772 if ( vSupp->nSize > p->nFaninMax )
787 if ( !pCover0 || !pCover1 )
789 else if ( !Abc_NodeCovProductSop( p, pCover0, pCover1, vSupp->nSize ) )
812 if ( !pCover0 || !pCover1 )
814 else if ( !Abc_NodeCovUnionSop( p, pCover0, pCover1, vSupp->nSize ) )
832 if ( pCoverP == NULL && pCoverN == NULL )
840 p->nSuppsMax =
Abc_MaxInt( p->nSuppsMax, p->nSupps );
869 if ( pCover0 == NULL || pCover1 == NULL )
877 for ( i = 0; i < p->vPairs0->nSize; i++ )
881 if ( (Val0 & Val1) == 0 )
885 if ( i < p->vPairs0->nSize )
888 if ( p->pManMin->nCubes >= p->nCubesMax )
896 for ( i = 0; i < nSupp; i++ )
898 if ( p->vComTo0->pArray[i] == -1 )
903 if ( p->vComTo1->pArray[i] == -1 )
908 if ( (Val0 & Val1) == 3 )
963 for ( i = 0; i < p->vComTo0->nSize; i++ )
965 if ( p->vComTo0->pArray[i] == -1 )
973 if ( p->pManMin->nCubes >= p->nCubesMax )
986 for ( i = 0; i < p->vComTo1->nSize; i++ )
988 if ( p->vComTo1->pArray[i] == -1 )
996 if ( p->pManMin->nCubes >= p->nCubesMax )
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
static Vec_Int_t * Abc_ObjGetSupp(Abc_Obj_t *pObj)
static void Min_CubeXorVar(Min_Cube_t *p, int Var, int Value)
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Vec_Int_t * Abc_NodeCovSupport(Cov_Man_t *p, Vec_Int_t *vSupp0, Vec_Int_t *vSupp1)
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
static ABC_NAMESPACE_IMPL_START void Abc_NtkCovCovers(Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
#define Abc_NtkForEachCo(pNtk, pCo, i)
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
static abctime Abc_Clock()
static int Abc_MaxInt(int a, int b)
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Cov_Man_t * Cov_ManAlloc(Abc_Ntk_t *pNtk, int nFaninMax)
DECLARATIONS ///.
Abc_Ntk_t * Abc_NtkCovDeriveRegular(Cov_Man_t *p, Abc_Ntk_t *pNtk)
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
static Min_Cube_t * Abc_ObjGetCover2(Abc_Obj_t *pObj)
static int Abc_NtkCovCoversOne(Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
static void Abc_ObjSetCover(Abc_Obj_t *pObj, Min_Cube_t *pCov, int Pol)
void Cov_ManFree(Cov_Man_t *p)
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
static Min_Cube_t * Abc_NodeCovProduct(Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
static int Min_CubeGetVar(Min_Cube_t *p, int Var)
void Min_EsopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
static void Abc_ObjSetCover2(Abc_Obj_t *pObj, Min_Cube_t *pCov)
#define ABC_NAMESPACE_IMPL_END
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
static int Min_CoverCountCubes(Min_Cube_t *pCover)
static void Vec_IntPush(Vec_Int_t *p, int Entry)
#define ABC_NAMESPACE_IMPL_START
static Min_Cube_t * Abc_NodeCovSum(Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
#define Abc_NtkForEachCi(pNtk, pCi, i)
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
#define Min_CoverForEachCube(pCover, pCube)
typedefABC_NAMESPACE_HEADER_START struct Cov_Man_t_ Cov_Man_t
DECLARATIONS ///.
static Min_Cube_t * Min_CubeAlloc(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts(Abc_Ntk_t *pNtk)
static void Abc_NtkCovCovers_rec(Cov_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vBoundary)
static void Min_CoverRecycle(Min_Man_t *p, Min_Cube_t *pCover)
Abc_Ntk_t * Abc_NtkSopEsopCover(Abc_Ntk_t *pNtk, int nFaninMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose)
FUNCTION DEFINITIONS ///.
static int Abc_NodeCovPropagate(Cov_Man_t *p, Abc_Obj_t *pObj)
void Min_SopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
static void Vec_IntFree(Vec_Int_t *p)
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
static void Abc_ObjSetSupp(Abc_Obj_t *pObj, Vec_Int_t *vVec)
static void Vec_IntClear(Vec_Int_t *p)
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
static Min_Cube_t * Abc_ObjGetCover(Abc_Obj_t *pObj, int Pol)
void Min_EsopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
void Min_SopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
void Min_ManClean(Min_Man_t *p, int nSupp)
static void Vec_PtrFree(Vec_Ptr_t *p)