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 macrosextern 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 functionsextern 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