diff options
Diffstat (limited to 'src/opt/xyz/xyzInt.h')
| -rw-r--r-- | src/opt/xyz/xyzInt.h | 631 |
1 files changed, 631 insertions, 0 deletions
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h new file mode 100644 index 00000000..22950bfd --- /dev/null +++ b/src/opt/xyz/xyzInt.h @@ -0,0 +1,631 @@ +/**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 int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +/*=== xyzMinSop.c ==========================================================*/ +extern void Min_SopMinimize( Min_Man_t * p ); +extern int 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_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); +extern void Min_CoverCheck( Min_Man_t * p ); +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 ); + 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 [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 [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + int i; + // check identity + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesAreEqual( pCube, pNew ) ) + return 1; + // check containment + for ( i = 0; i < (int)pNew->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pCube ) + if ( Min_CubeIsContained( pCube, pNew ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesDistOne( pCube, pNew, NULL ) ) + return pCube; + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |