/**CFile****************************************************************
FileName [extraUtilSupp.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Support minimization.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: extraUtilSupp.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "misc/vec/vecWec.h"
#include "extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Generate m-out-of-n vectors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_SuppCountOnes( unsigned i )
{
i = i - ((i >> 1) & 0x55555555);
i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
i = ((i + (i >> 4)) & 0x0F0F0F0F);
return (i*(0x01010101))>>24;
}
Vec_Wrd_t * Abc_SuppGen( int m, int n )
{
Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
int i, Size = (1 << n);
for ( i = 0; i < Size; i++ )
if ( Abc_SuppCountOnes(i) == m )
Vec_WrdPush( vRes, i );
return vRes;
}
/**Function*************************************************************
Synopsis [Perform verification.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppVerify( Vec_Wrd_t * p, word * pMatrix, int nVars, int nVarsMin )
{
Vec_Wrd_t * pNew;
word * pLimit, * pEntry1, * pEntry2;
word Entry, EntryNew;
int i, k, v, Value, Counter = 0;
pNew = Vec_WrdAlloc( Vec_WrdSize(p) );
Vec_WrdForEachEntry( p, Entry, i )
{
EntryNew = 0;
for ( v = 0; v < nVarsMin; v++ )
{
Value = 0;
for ( k = 0; k < nVars; k++ )
if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) )
Value ^= 1;
if ( Value )
EntryNew |= (((word)1) << v);
}
Vec_WrdPush( pNew, EntryNew );
}
// check that they are disjoint
pLimit = Vec_WrdLimit(pNew);
pEntry1 = Vec_WrdArray(pNew);
for ( ; pEntry1 < pLimit; pEntry1++ )
for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
if ( *pEntry1 == *pEntry2 )
Counter++;
if ( Counter )
printf( "The total of %d pairs fail verification.\n", Counter );
else
printf( "Verification successful.\n" );
Vec_WrdFree( pNew );
}
/**Function*************************************************************
Synopsis [Generate pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wrd_t * Abc_SuppGenPairs( Vec_Wrd_t * p, int nBits )
{
Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) );
word * pLimit = Vec_WrdLimit(p);
word * pEntry1 = Vec_WrdArray(p);
word * pEntry2, Value;
for ( ; pEntry1 < pLimit; pEntry1++ )
for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
{
Value = *pEntry1 ^ *pEntry2;
if ( Abc_InfoHasBit(pMap, (int)Value) )
continue;
Abc_InfoXorBit( pMap, (int)Value );
Vec_WrdPush( vRes, Value );
}
ABC_FREE( pMap );
return vRes;
}
Vec_Wrd_t * Abc_SuppGenPairs2( int nOnes, int nBits )
{
Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
int i, k, Size = (1 << nBits), Value;
for ( i = 0; i < Size; i++ )
{
Value = Abc_SuppCountOnes(i);
for ( k = 1; k <= nOnes; k++ )
if ( Value == 2*k )
break;
if ( k <= nOnes )
Vec_WrdPush( vRes, i );
}
return vRes;
}
/**Function*************************************************************
Synopsis [Select variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppPrintMask( word uMask, int nBits )
{
int i;
for ( i = 0; i < nBits; i++ )
printf( "%d", (int)((uMask >> i) & 1) );
printf( "\n" );
}
void Abc_SuppGenProfile( Vec_Wrd_t * p, int nBits, int * pCounts )
{
word Ent;
int i, k, b;
Vec_WrdForEachEntry( p, Ent, i )
for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ )
pCounts[k] += ((Ent >> k) & 1) ^ b;
}
void Abc_SuppPrintProfile( Vec_Wrd_t * p, int nBits )
{
int k, Counts[64] = {0};
Abc_SuppGenProfile( p, nBits, Counts );
for ( k = 0; k < nBits; k++ )
printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_WrdSize(p) );
}
int Abc_SuppGenFindBest( Vec_Wrd_t * p, int nBits, int * pMerit )
{
int k, kBest = 0, Counts[64] = {0};
Abc_SuppGenProfile( p, nBits, Counts );
for ( k = 1; k < nBits; k++ )
if ( Counts[kBest] < Counts[k] )
kBest = k;
*pMerit = Counts[kBest];
return kBest;
}
void Abc_SuppGenSelectVar( Vec_Wrd_t * p, int nBits, int iVar )
{
word * pEntry = Vec_WrdArray(p);
word * pLimit = Vec_WrdLimit(p);
for ( ; pEntry < pLimit; pEntry++ )
if ( (*pEntry >> iVar) & 1 )
*pEntry ^= (((word)1) << nBits);
}
void Abc_SuppGenFilter( Vec_Wrd_t * p, int nBits )
{
word Ent;
int i, k = 0;
Vec_WrdForEachEntry( p, Ent, i )
if ( ((Ent >> nBits) & 1) == 0 )
Vec_WrdWriteEntry( p, k++, Ent );
Vec_WrdShrink( p, k );
}
word Abc_SuppFindOne( Vec_Wrd_t * p, int nBits )
{
word uMask = 0;
int Prev = -1, This, Var;
while ( 1 )
{
Var = Abc_SuppGenFindBest( p, nBits, &This );
if ( Prev >= This )
break;
Prev = This;
Abc_SuppGenSelectVar( p, nBits, Var );
uMask |= (((word)1) << Var);
}
return uMask;
}
int Abc_SuppMinimize( word * pMatrix, Vec_Wrd_t * p, int nBits, int fVerbose )
{
int i;
for ( i = 0; Vec_WrdSize(p) > 0; i++ )
{
// Abc_SuppPrintProfile( p, nBits );
pMatrix[i] = Abc_SuppFindOne( p, nBits );
Abc_SuppGenFilter( p, nBits );
if ( !fVerbose )
continue;
// print stats
printf( "%2d : ", i );
printf( "%6d ", Vec_WrdSize(p) );
Abc_SuppPrintMask( pMatrix[i], nBits );
// printf( "\n" );
}
return i;
}
/**Function*************************************************************
Synopsis [Create representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose )
{
int nVarsMin;
word Matrix[64];
abctime clk = Abc_Clock();
// create the problem
Vec_Wrd_t * vRes = Abc_SuppGen( nOnes, nVars );
Vec_Wrd_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars );
assert( nVars < 100 );
printf( "M = %2d N = %2d : ", nOnes, nVars );
printf( "K = %6d ", Vec_WrdSize(vRes) );
printf( "Total = %12.0f ", 0.5 * Vec_WrdSize(vRes) * (Vec_WrdSize(vRes) - 1) );
printf( "Distinct = %8d ", Vec_WrdSize(vPairs) );
Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
// solve the problem
clk = Abc_Clock();
nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose );
printf( "Solution with %d variables found. ", nVarsMin );
Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
if ( fCheck )
Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin );
Vec_WrdFree( vPairs );
Vec_WrdFree( vRes );
}
/**Function*************************************************************
Synopsis [Reads the input part of the cubes specified in MIN format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wrd_t * Abc_SuppReadMin( char * pFileName, int * pnVars )
{
Vec_Wrd_t * vRes; word uCube;
int nCubes = 0, nVars = -1, iVar;
char * pCur, * pToken, * pStart = "INPUT F-COVER";
char * pStr = Extra_FileReadContents( pFileName );
if ( pStr == NULL )
{ printf( "Cannot open input file (%s).\n", pFileName ); return NULL; }
pCur = strstr( pStr, pStart );
if ( pCur == NULL )
{ printf( "Cannot find beginning of cube cover (%s).\n", pStart ); return NULL; }
pToken = strtok( pCur + strlen(pStart), " \t\r\n," );
nCubes = atoi( pToken );
if ( nCubes < 1 || nCubes > 1000000 )
{ printf( "The number of cubes in not in the range [1; 1000000].\n" ); return NULL; }
vRes = Vec_WrdAlloc( 1000 );
uCube = 0; iVar = 0;
while ( (pToken = strtok(NULL, " \t\r\n,")) != NULL )
{
if ( strlen(pToken) > 2 )
{
if ( !strncmp(pToken, "INPUT", strlen("INPUT")) )
break;
if ( iVar > 64 )
{ printf( "The number of inputs (%d) is too high.\n", iVar ); Vec_WrdFree(vRes); return NULL; }
if ( nVars == -1 )
nVars = iVar;
else if ( nVars != iVar )
{ printf( "The number of inputs (%d) does not match declaration (%d).\n", nVars, iVar ); Vec_WrdFree(vRes); return NULL; }
Vec_WrdPush( vRes, uCube );
uCube = 0; iVar = 0;
continue;
}
if ( pToken[1] == '0' && pToken[0] == '1' ) // value 1
uCube |= (((word)1) << iVar);
else if ( pToken[1] != '1' || pToken[0] != '0' ) // value 0
{ printf( "Strange literal representation (%s) of cube %d.\n", pToken, nCubes ); Vec_WrdFree(vRes); return NULL; }
iVar++;
}
ABC_FREE( pStr );
if ( Vec_WrdSize(vRes) != nCubes )
{ printf( "The number of cubes (%d) does not match declaration (%d).\n", Vec_WrdSize(vRes), nCubes ); Vec_WrdFree(vRes); return NULL; }
else
printf( "Successfully parsed function with %d inputs and %d cubes.\n", nVars, nCubes );
*pnVars = nVars;
return vRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wrd_t * Abc_SuppDiffMatrix( Vec_Wrd_t * vCubes )
{
abctime clk = Abc_Clock();
word * pEnt2, * pEnt = Vec_WrdArray( vCubes );
word * pLimit = Vec_WrdLimit( vCubes );
Vec_Wrd_t * vRes, * vPairs = Vec_WrdAlloc( Vec_WrdSize(vCubes) * (Vec_WrdSize(vCubes) - 1) / 2 );
word * pStore = Vec_WrdArray( vPairs );
for ( ; pEnt < pLimit; pEnt++ )
for ( pEnt2 = pEnt+1; pEnt2 < pLimit; pEnt2++ )
*pStore++ = *pEnt ^ *pEnt2;
vPairs->nSize = Vec_WrdCap(vPairs);
assert( pStore == Vec_WrdLimit(vPairs) );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// vRes = Vec_WrdUniqifyHash( vPairs, 1 );
vRes = Vec_WrdDup( vPairs );
printf( "Successfully generated diff matrix with %10d rows (%6.2f %%). ",
Vec_WrdSize(vRes), 100.0 * Vec_WrdSize(vRes) / Vec_WrdSize(vPairs) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_WrdFree( vPairs );
return vRes;
}
/**Function*************************************************************
Synopsis [Solve difference matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_SuppCountOnes64( word i )
{
i = i - ((i >> 1) & 0x5555555555555555);
i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
return (i*(0x0101010101010101))>>56;
}
int Abc_SuppFindVar( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
{
int v, vBest = -1, dBest = -1;
for ( v = 0; v < nVars; v++ )
{
if ( Vec_WecLevelSize(pS, v) )
continue;
if ( vBest == -1 || dBest > Vec_WecLevelSize(pD, v) )
vBest = v, dBest = Vec_WecLevelSize(pD, v);
}
return vBest;
}
void Abc_SuppRemove( Vec_Wrd_t * p, int * pCounts, Vec_Wec_t * pS, Vec_Wec_t * pD, int iVar, int nVars )
{
word Entry; int i, v;
assert( Vec_WecLevelSize(pS, iVar) == 0 );
Vec_IntClear( Vec_WecEntry(pD, iVar) );
Vec_WrdForEachEntry( p, Entry, i )
{
if ( ((Entry >> iVar) & 1) == 0 )
continue;
pCounts[i]--;
if ( pCounts[i] == 1 )
{
for ( v = 0; v < nVars; v++ )
if ( (Entry >> v) & 1 )
{
Vec_IntRemove( Vec_WecEntry(pD, v), i );
Vec_WecPush( pS, v, i );
}
}
else if ( pCounts[i] == 2 )
{
for ( v = 0; v < nVars; v++ )
if ( (Entry >> v) & 1 )
Vec_WecPush( pD, v, i );
}
}
}
void Abc_SuppProfile( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
{
int v;
for ( v = 0; v < nVars; v++ )
printf( "%2d : S = %3d D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) );
}
int Abc_SuppSolve( Vec_Wrd_t * p, int nVars )
{
abctime clk = Abc_Clock();
Vec_Wrd_t * pNew = Vec_WrdDup( p );
Vec_Wec_t * vSingles = Vec_WecStart( 64 );
Vec_Wec_t * vDoubles = Vec_WecStart( 64 );
word Entry; int i, v, iVar, nVarsNew = nVars;
int * pCounts = ABC_ALLOC( int, Vec_WrdSize(p) );
Vec_WrdForEachEntry( p, Entry, i )
{
pCounts[i] = Abc_SuppCountOnes64( Entry );
if ( pCounts[i] == 1 )
{
for ( v = 0; v < nVars; v++ )
if ( (Entry >> v) & 1 )
Vec_WecPush( vSingles, v, i );
}
else if ( pCounts[i] == 2 )
{
for ( v = 0; v < nVars; v++ )
if ( (Entry >> v) & 1 )
Vec_WecPush( vDoubles, v, i );
}
}
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// Abc_SuppProfile( vSingles, vDoubles, nVars );
// find variable in 0 singles and the smallest doubles
while ( 1 )
{
iVar = Abc_SuppFindVar( vSingles, vDoubles, nVars );
if ( iVar == -1 )
break;
// printf( "Selected variable %d.\n", iVar );
Abc_SuppRemove( pNew, pCounts, vSingles, vDoubles, iVar, nVars );
// Abc_SuppProfile( vSingles, vDoubles, nVars );
nVarsNew--;
}
// printf( "Result = %d (out of %d)\n", nVarsNew, nVars );
Vec_WecFree( vSingles );
Vec_WecFree( vDoubles );
Vec_WrdFree( pNew );
ABC_FREE( pCounts );
return nVarsNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppReadMinTest( char * pFileName )
{
// int fVerbose = 0;
abctime clk = Abc_Clock();
// word Matrix[64];
int nVars, nVarsMin;
Vec_Wrd_t * vPairs, * vCubes;
vCubes = Abc_SuppReadMin( pFileName, &nVars );
if ( vCubes == NULL )
return;
vPairs = Abc_SuppDiffMatrix( vCubes );
Vec_WrdFreeP( &vCubes );
// solve the problem
clk = Abc_Clock();
// nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose );
nVarsMin = Abc_SuppSolve( vPairs, nVars );
printf( "Solution with %d variables found. ", nVarsMin );
Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
Vec_WrdFreeP( &vPairs );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END