diff options
Diffstat (limited to 'src/temp/xyz/xyzInt.h')
| -rw-r--r-- | src/temp/xyz/xyzInt.h | 642 |
1 files changed, 0 insertions, 642 deletions
diff --git a/src/temp/xyz/xyzInt.h b/src/temp/xyz/xyzInt.h deleted file mode 100644 index 656612aa..00000000 --- a/src/temp/xyz/xyzInt.h +++ /dev/null @@ -1,642 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Min_Man_t_ Min_Man_t; -typedef struct Min_Cube_t_ Min_Cube_t; - -struct Min_Man_t_ -{ - int nVars; // the number of vars - int nWords; // the number of words - Extra_MmFixed_t * pMemMan; // memory manager for cubes - // temporary cubes - Min_Cube_t * pOne0; // tautology cube - Min_Cube_t * pOne1; // tautology cube - Min_Cube_t * pTriv0[2]; // trivial cube - Min_Cube_t * pTriv1[2]; // trivial cube - Min_Cube_t * pTemp; // cube for computing the distance - Min_Cube_t * pBubble; // cube used as a separator - // temporary storage for the new cover - int nCubes; // the number of cubes - Min_Cube_t ** ppStore; // storage for cubes by number of literals -}; - -struct Min_Cube_t_ -{ - Min_Cube_t * pNext; // the pointer to the next cube in the cover - unsigned nVars : 10; // the number of variables - unsigned nWords : 12; // the number of machine words - unsigned nLits : 10; // the number of literals in the cube - unsigned uData[1]; // the bit-data for the cube -}; - - -// iterators through the entries in the linked lists of cubes -#define Min_CoverForEachCube( pCover, pCube ) \ - for ( pCube = pCover; \ - pCube; \ - pCube = pCube->pNext ) -#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ - for ( pCube = pCover, \ - pCube2 = pCube? pCube->pNext: NULL; \ - pCube; \ - pCube = pCube2, \ - pCube2 = pCube? pCube->pNext: NULL ) -#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ - for ( pCube = pCover, \ - ppPrev = &(pCover); \ - pCube; \ - ppPrev = &pCube->pNext, \ - pCube = pCube->pNext ) - -// macros to get hold of bits and values in the cubes -static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); } -static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); } -static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); } -static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); } - -/*=== xyzMinEsop.c ==========================================================*/ -extern void Min_EsopMinimize( Min_Man_t * p ); -extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); -/*=== xyzMinSop.c ==========================================================*/ -extern void Min_SopMinimize( Min_Man_t * p ); -extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); -/*=== xyzMinMan.c ==========================================================*/ -extern Min_Man_t * Min_ManAlloc( int nVars ); -extern void Min_ManClean( Min_Man_t * p, int nSupp ); -extern void Min_ManFree( Min_Man_t * p ); -/*=== xyzMinUtil.c ==========================================================*/ -extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); -extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); -extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ); -extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); -extern void Min_CoverCheck( Min_Man_t * p ); -extern int Min_CubeCheck( Min_Cube_t * pCube ); -extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); -extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); -extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p ) -{ - Min_Cube_t * pCube; - pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan ); - pCube->pNext = NULL; - pCube->nVars = p->nVars; - pCube->nWords = p->nWords; - pCube->nLits = 0; - memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube representing elementary var.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl ) -{ - Min_Cube_t * pCube; - pCube = Min_CubeAlloc( p ); - Min_CubeXorBit( pCube, iVar*2+fCompl ); - pCube->nLits = 1; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) -{ - Min_Cube_t * pCube; - pCube = Min_CubeAlloc( p ); - memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); - pCube->nLits = pCopy->nLits; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Recycles the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); -} - -/**Function************************************************************* - - Synopsis [Recycles the cube cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube, * pCube2; - Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); -} - - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubeCountLits( Min_Cube_t * pCube ) -{ - unsigned uData; - int Count = 0, i, w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Count++; - } - return Count; -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vLits ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vLits, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CoverCountCubes( Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube; - int Count = 0; - Min_CoverForEachCube( pCover, pCube ) - Count++; - return Count; -} - - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - unsigned uData; - int i; - assert( pCube0->nVars == pCube1->nVars ); - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] & pCube1->uData[i]; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( uData != 0x55555555 ) - return 1; - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Collects the disjoint variables of the two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vVars ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; - uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); - if ( uData == 0 ) - continue; - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vVars, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp ) -{ - unsigned uData; - int i, fFound = 0; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - { - if ( pTemp ) pTemp->uData[i] = 0; - continue; - } - if ( fFound ) - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (uData & (uData-1)) > 0 ) // more than one 1 - return 0; - if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); - fFound = 1; - } - if ( fFound == 0 ) - { - printf( "\n" ); - Min_CubeWrite( stdout, pCube0 ); - Min_CubeWrite( stdout, pCube1 ); - printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 ) -{ - unsigned uData;//, uData2; - int i, k, Var0 = -1, Var1 = -1; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - continue; - if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) - return 0; - for ( k = 0; k < 32; k += 2 ) - if ( uData & (1 << k) ) - { - if ( Var0 == -1 ) - Var0 = 16 * i + k/2; - else if ( Var1 == -1 ) - Var1 = 16 * i + k/2; - else - return 0; - } - /* - if ( Var0 >= 0 ) - { - uData &= 0xFFFF; - uData2 = (uData >> 16); - if ( uData && uData2 ) - return 0; - if ( uData ) - { - } - uData }= uData2; - uData &= 0x - } - */ - } - if ( Var0 >= 0 && Var1 >= 0 ) - { - *pVar0 = Var0; - *pVar1 = Var1; - return 1; - } - if ( Var0 == -1 || Var1 == -1 ) - { - printf( "\n" ); - Min_CubeWrite( stdout, pCube0 ); - Min_CubeWrite( stdout, pCube1 ); - printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - Min_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Min_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; - pCube->nLits = Min_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - Min_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Min_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; - pCube->nLits = Min_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( pCube0->uData[i] != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; - pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); - } -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of distance-1 merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - pCube->uData[w] |= pDist->uData[w]; -} - - - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube, * pCube2, * pThis; - if ( pCover == NULL ) - { - Min_ManClean( p, p->nVars ); - return; - } - Min_ManClean( p, pCover->nVars ); - Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - { - // go through the linked list - Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - Min_CubeRecycle( p, pCube ); - break; - } - if ( pThis != NULL ) - continue; - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - } -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Min_Cube_t * pThis; - int i; -/* - // this cube cannot be equal to any cube - Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - { - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - Min_CubeWrite( stdout, pCube ); - assert( 0 ); - } - } -*/ - // try to find a containing cube - for ( i = 0; i <= (int)pCube->nLits; i++ ) - Min_CoverForEachCube( p->ppStore[i], pThis ) - { - // skip the bubble - if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) - return 1; - } - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |