/**CFile****************************************************************
FileName [covInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Mapping into network of SOPs/ESOPs.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: covInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__map__cov__covInt_h
#define ABC__map__cov__covInt_h
#include "base/abc/abc.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// 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)); }
/*=== covMinEsop.c ==========================================================*/
extern void Min_EsopMinimize( Min_Man_t * p );
extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== covMinSop.c ==========================================================*/
extern void Min_SopMinimize( Min_Man_t * p );
extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== covMinMan.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 );
/*=== covMinUtil.c ==========================================================*/
extern void Min_CoverCreate( Vec_Str_t * vCover, Min_Cube_t * pCover, char Type );
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;
}
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////