mvc.h

主要进行大规模的电路综合

        pList->pHead = pCube->pNext;\
    else\
        pPrev->pNext = pCube->pNext;\
    if ( pList->pTail == pCube )\
    {\
        assert( pCube->pNext == NULL );\
        pList->pTail = pPrev;\
    }\
    pList->nItems--;\
}

// managing linked lists inside the cover
#define Mvc_CoverAddCubeHead( pCover, pCube )\
{\
    Mvc_List_t * pList = &pCover->lCubes;\
    Mvc_ListAddCubeHead( pList, pCube );\
}
#define Mvc_CoverAddCubeTail( pCover, pCube )\
{\
    Mvc_List_t * pList = &pCover->lCubes;\
    Mvc_ListAddCubeTail( pList, pCube );\
}
#define Mvc_CoverDeleteCube( pCover, pPrev, pCube )\
{\
    Mvc_List_t * pList = &pCover->lCubes;\
    Mvc_ListDeleteCube( pList, pPrev, pCube );\
}






// iterator through the cubes in the cube list
#define Mvc_ListForEachCube( List, Cube )\
    for ( Cube = List->pHead;\
          Cube;\
          Cube = Cube->pNext )
#define Mvc_ListForEachCubeSafe( List, Cube, Cube2 )\
    for ( Cube = List->pHead, Cube2 = (Cube? Cube->pNext: NULL);\
          Cube;\
          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )

// iterator through cubes in the cover
#define Mvc_CoverForEachCube( Cover, Cube )\
    for ( Cube = (Cover)->lCubes.pHead;\
          Cube;\
          Cube = Cube->pNext )
#define Mvc_CoverForEachCubeWithIndex( Cover, Cube, Index )\
    for ( Index = 0, Cube = (Cover)->lCubes.pHead;\
          Cube;\
          Index++, Cube = Cube->pNext )
#define Mvc_CoverForEachCubeSafe( Cover, Cube, Cube2 )\
    for ( Cube = (Cover)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
          Cube;\
          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )

// iterator which starts from the given cube
#define Mvc_CoverForEachCubeStart( Start, Cube )\
    for ( Cube = Start;\
          Cube;\
          Cube = Cube->pNext )
#define Mvc_CoverForEachCubeStartSafe( Start, Cube, Cube2 )\
    for ( Cube = Start, Cube2 = (Cube? Cube->pNext: NULL);\
          Cube;\
          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )


// iterator through literals of the cube
#define Mvc_CubeForEachLiteral( Cover, Cube, Lit, Value )\
    for ( Lit = 0;\
          Lit < Cover->nBits && ((Value = Mvc_CubeBitValue(Cube,Lit))>=0);\
          Lit++ )


// macros which work with memory
// MEM_ALLOC: allocate the given number (Size) of items of type (Type)
// MEM_FREE:  deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
#define MEM_ALLOC( Manager, Type, Size )          ((Type *)malloc( (Size) * sizeof(Type) ))
#define MEM_FREE( Manager, Type, Size, Pointer )  if ( Pointer ) { free(Pointer); Pointer = NULL; }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFITIONS                           ///
////////////////////////////////////////////////////////////////////////

/*=== mvcApi.c ====================================================*/
extern int              Mvc_CoverReadWordNum( Mvc_Cover_t * pCover );
extern int              Mvc_CoverReadBitNum( Mvc_Cover_t * pCover );
extern int              Mvc_CoverReadCubeNum( Mvc_Cover_t * pCover );
extern Mvc_Cube_t *     Mvc_CoverReadCubeHead( Mvc_Cover_t * pCover );
extern Mvc_Cube_t *     Mvc_CoverReadCubeTail( Mvc_Cover_t * pCover );
extern Mvc_List_t *     Mvc_CoverReadCubeList( Mvc_Cover_t * pCover );
extern int              Mvc_ListReadCubeNum( Mvc_List_t * pList );
extern Mvc_Cube_t *     Mvc_ListReadCubeHead( Mvc_List_t * pList );
extern Mvc_Cube_t *     Mvc_ListReadCubeTail( Mvc_List_t * pList );
extern void             Mvc_CoverSetCubeNum( Mvc_Cover_t * pCover,int nItems );
extern void             Mvc_CoverSetCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverSetCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverSetCubeList( Mvc_Cover_t * pCover, Mvc_List_t * pList );
extern bool             Mvc_CoverIsEmpty( Mvc_Cover_t * pCover );
extern bool             Mvc_CoverIsTautology( Mvc_Cover_t * pCover );
extern bool             Mvc_CoverIsBinaryBuffer( Mvc_Cover_t * pCover );
extern void             Mvc_CoverMakeEmpty( Mvc_Cover_t * pCover );
extern void             Mvc_CoverMakeTautology( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverCreateEmpty( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverCreateTautology( Mvc_Cover_t * pCover );
/*=== mvcCover.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverAlloc( Mvc_Manager_t * pMem, int nBits );
extern Mvc_Cover_t *    Mvc_CoverCreateConst( Mvc_Manager_t * pMem, int nBits, bool Phase );
extern Mvc_Cover_t *    Mvc_CoverClone( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverDup( Mvc_Cover_t * pCover );
extern void             Mvc_CoverFree( Mvc_Cover_t * pCover );
extern void             Mvc_CoverAllocateMask( Mvc_Cover_t * pCover );
extern void             Mvc_CoverAllocateArrayLits( Mvc_Cover_t * pCover );
extern void             Mvc_CoverAllocateArrayCubes( Mvc_Cover_t * pCover );
extern void             Mvc_CoverDeallocateMask( Mvc_Cover_t * pCover );
extern void             Mvc_CoverDeallocateArrayLits( Mvc_Cover_t * pCover );
/*=== mvcCube.c ====================================================*/
extern Mvc_Cube_t *     Mvc_CubeAlloc( Mvc_Cover_t * pCover );
extern Mvc_Cube_t *     Mvc_CubeDup( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CubeBitRemoveDcs( Mvc_Cube_t * pCube );
/*=== mvcCompare.c ====================================================*/
extern int              Mvc_CubeCompareInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
extern int              Mvc_CubeCompareSizeAndInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
extern int              Mvc_CubeCompareIntUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
extern int              Mvc_CubeCompareIntOutsideMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
extern int              Mvc_CubeCompareIntOutsideAndUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
/*=== mvcDivisor.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverDivisor( Mvc_Cover_t * pCover );
/*=== mvcDivide.c ====================================================*/
extern void             Mvc_CoverDivide( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
extern void             Mvc_CoverDivideInternal( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
extern void             Mvc_CoverDivideByLiteral( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
extern void             Mvc_CoverDivideByCube( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
extern void             Mvc_CoverDivideByLiteralQuo( Mvc_Cover_t * pCover, int iLit );
/*=== mvcList.c ====================================================*/
// these functions are available as macros
extern void             Mvc_ListAddCubeHead_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
extern void             Mvc_ListAddCubeTail_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
extern void             Mvc_ListDeleteCube_( Mvc_List_t * pList, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
extern void             Mvc_CoverAddCubeHead_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverAddCubeTail_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverDeleteCube_( Mvc_Cover_t * pCover, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
extern void             Mvc_CoverAddDupCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverAddDupCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
// other functions
extern void             Mvc_CoverAddLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverDeleteLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
extern void             Mvc_CoverList2Array( Mvc_Cover_t * pCover );
extern void             Mvc_CoverArray2List( Mvc_Cover_t * pCover );
extern Mvc_Cube_t *     Mvc_ListGetTailFromHead( Mvc_Cube_t * pHead );
/*=== mvcPrint.c ====================================================*/
extern void             Mvc_CoverPrint( Mvc_Cover_t * pCover );
extern void             Mvc_CubePrint( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
/*=== mvcSort.c ====================================================*/
extern void             Mvc_CoverSort( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) );
/*=== mvcUtils.c ====================================================*/
extern void             Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp );
extern void             Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube );
extern bool             Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover );
extern void             Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverCommonCubeCover( Mvc_Cover_t * pCover );
extern bool             Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
extern int              Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover );
extern int              Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] );
extern Mvc_Cover_t *    Mvc_CoverRemap( Mvc_Cover_t * pCover, int * pVarsRem, int nVarsRem );
extern void             Mvc_CoverInverse( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverRemoveDontCareLits( Mvc_Cover_t * pCover );
extern Mvc_Cover_t *    Mvc_CoverCofactor( Mvc_Cover_t * pCover, int iValue, int iValueOther );
extern Mvc_Cover_t *    Mvc_CoverFlipVar( Mvc_Cover_t * pCover, int iValue0, int iValue1 );
extern Mvc_Cover_t *    Mvc_CoverUnivQuantify( Mvc_Cover_t * p, int iValueA0, int iValueA1, int iValueB0, int iValueB1 );
extern Mvc_Cover_t **   Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar );
extern int              Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue );
extern Mvc_Cover_t *    Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew );
/*=== mvcLits.c ====================================================*/
extern int              Mvc_CoverAnyLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
extern int              Mvc_CoverBestLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
extern Mvc_Cover_t *    Mvc_CoverBestLiteralCover( Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
extern int              Mvc_CoverFirstCubeFirstLit( Mvc_Cover_t * pCover );
extern int              Mvc_CoverCountLiterals( Mvc_Cover_t * pCover );
extern bool             Mvc_CoverIsOneLiteral( Mvc_Cover_t * pCover );
/*=== mvcOpAlg.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverAlgebraicMultiply( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
extern Mvc_Cover_t *    Mvc_CoverAlgebraicSubtract( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
extern bool             Mvc_CoverAlgebraicEqual( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
/*=== mvcOpBool.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverBooleanOr( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
extern Mvc_Cover_t *    Mvc_CoverBooleanAnd( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
extern bool             Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );

/*=== mvcContain.c ====================================================*/
extern bool             Mvc_CoverContain( Mvc_Cover_t * pCover );
/*=== mvcTau.c ====================================================*/
extern bool             Mvc_CoverTautology( Mvc_Data_t * p, Mvc_Cover_t * pCover );
/*=== mvcCompl.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverComplement( Mvc_Data_t * p, Mvc_Cover_t * pCover );
/*=== mvcSharp.c ====================================================*/
extern Mvc_Cover_t *    Mvc_CoverSharp( Mvc_Data_t * p, Mvc_Cover_t * pA, Mvc_Cover_t * pB );
extern bool             Mvc_CoverDist0Cubes( Mvc_Data_t * pData, Mvc_Cube_t * pA, Mvc_Cube_t * pB );
extern void             Mvc_CoverIntersectCubes( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
extern bool             Mvc_CoverIsIntersecting( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
extern void             Mvc_CoverAppendCubes( Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
extern void             Mvc_CoverRemoveCubes( Mvc_Cover_t * pC );

/*=== mvcMerge.c ====================================================*/
extern void             Mvc_CoverDist1Merge( Mvc_Data_t * p, Mvc_Cover_t * pCover );

/*=== mvcData.c ====================================================*/
extern Mvc_Data_t *     Mvc_CoverDataAlloc( Vm_VarMap_t * pVm, Mvc_Cover_t * pCover );
extern void             Mvc_CoverDataFree( Mvc_Data_t * p, Mvc_Cover_t * pCover );

/*=== mvcMan.c ====================================================*/
extern void             Mvc_ManagerFree( Mvc_Manager_t * p );
extern Mvc_Manager_t *  Mvc_ManagerStart();
extern Mvc_Manager_t *  Mvc_ManagerAllocCover();
extern Mvc_Manager_t *  Mvc_ManagerAllocCube( int nWords );
extern Mvc_Manager_t *  Mvc_ManagerFreeCover( Mvc_Cover_t * pCover );
extern Mvc_Manager_t *  Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords );

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

#endif