extraUtilSupp.c File Reference

#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"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Extra_PrintBinary (FILE *pFile, unsigned Sign[], int nBits)
	DECLARATIONS ///. More...
static int	Abc_SuppCountOnes (unsigned i)
	FUNCTION DEFINITIONS ///. More...
Vec_Wrd_t *	Abc_SuppGen (int m, int n)
void	Abc_SuppVerify (Vec_Wrd_t *p, word *pMatrix, int nVars, int nVarsMin)
Vec_Wrd_t *	Abc_SuppGenPairs (Vec_Wrd_t *p, int nBits)
Vec_Wrd_t *	Abc_SuppGenPairs2 (int nOnes, int nBits)
void	Abc_SuppPrintMask (word uMask, int nBits)
void	Abc_SuppGenProfile (Vec_Wrd_t *p, int nBits, int *pCounts)
void	Abc_SuppPrintProfile (Vec_Wrd_t *p, int nBits)
int	Abc_SuppGenFindBest (Vec_Wrd_t *p, int nBits, int *pMerit)
void	Abc_SuppGenSelectVar (Vec_Wrd_t *p, int nBits, int iVar)
void	Abc_SuppGenFilter (Vec_Wrd_t *p, int nBits)
word	Abc_SuppFindOne (Vec_Wrd_t *p, int nBits)
int	Abc_SuppMinimize (word *pMatrix, Vec_Wrd_t *p, int nBits, int fVerbose)
void	Abc_SuppTest (int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose)
Vec_Wrd_t *	Abc_SuppReadMin (char *pFileName, int *pnVars)
Vec_Wrd_t *	Abc_SuppDiffMatrix (Vec_Wrd_t *vCubes)
static int	Abc_SuppCountOnes64 (word i)
int	Abc_SuppFindVar (Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
void	Abc_SuppRemove (Vec_Wrd_t *p, int *pCounts, Vec_Wec_t *pS, Vec_Wec_t *pD, int iVar, int nVars)
void	Abc_SuppProfile (Vec_Wec_t *pS, Vec_Wec_t *pD, int nVars)
int	Abc_SuppSolve (Vec_Wrd_t *p, int nVars)
void	Abc_SuppReadMinTest (char *pFileName)

Function Documentation

static int Abc_SuppCountOnes ( unsigned  i )

inlinestatic

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Generate m-out-of-n vectors.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file extraUtilSupp.c.

{
    i = i - ((i >> 1) & 0x55555555);
    i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
    i = ((i + (i >> 4)) & 0x0F0F0F0F);
    return (i*(0x01010101))>>24;
}

static int Abc_SuppCountOnes64 ( word  i )

inlinestatic

Function*************************************************************

Synopsis [Solve difference matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 396 of file extraUtilSupp.c.

{
    i = i - ((i >> 1) & 0x5555555555555555);
    i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
    i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
    return (i*(0x0101010101010101))>>56;
}

Vec_Wrd_t* Abc_SuppDiffMatrix

(

Vec_Wrd_t *

vCubes

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 363 of file extraUtilSupp.c.

{
    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;    
}

word Abc_SuppFindOne	(	Vec_Wrd_t *	p,
		int	nBits
	)

Definition at line 222 of file extraUtilSupp.c.

{
    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_SuppFindVar	(	Vec_Wec_t *	pS,
		Vec_Wec_t *	pD,
		int	nVars
	)

Definition at line 403 of file extraUtilSupp.c.

{
    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;
}

Vec_Wrd_t* Abc_SuppGen	(	int	m,
		int	n
	)

Definition at line 60 of file extraUtilSupp.c.

{
    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;
}

void Abc_SuppGenFilter	(	Vec_Wrd_t *	p,
		int	nBits
	)

Definition at line 213 of file extraUtilSupp.c.

{
    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 );
}

int Abc_SuppGenFindBest	(	Vec_Wrd_t *	p,
		int	nBits,
		int *	pMerit
	)

Definition at line 195 of file extraUtilSupp.c.

{
    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;
}

Vec_Wrd_t* Abc_SuppGenPairs	(	Vec_Wrd_t *	p,
		int	nBits
	)

Function*************************************************************

Synopsis [Generate pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file extraUtilSupp.c.

{
    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
	)

Definition at line 146 of file extraUtilSupp.c.

{
    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;
}

void Abc_SuppGenProfile	(	Vec_Wrd_t *	p,
		int	nBits,
		int *	pCounts
	)

Definition at line 180 of file extraUtilSupp.c.

{
    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_SuppGenSelectVar	(	Vec_Wrd_t *	p,
		int	nBits,
		int	iVar
	)

Definition at line 205 of file extraUtilSupp.c.

{
    word * pEntry = Vec_WrdArray(p);
    word * pLimit = Vec_WrdLimit(p);
    for ( ; pEntry < pLimit; pEntry++ )
        if ( (*pEntry >> iVar) & 1 )
            *pEntry ^= (((word)1) << nBits);
}

int Abc_SuppMinimize	(	word *	pMatrix,
		Vec_Wrd_t *	p,
		int	nBits,
		int	fVerbose
	)

Definition at line 237 of file extraUtilSupp.c.

{
    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;
}

void Abc_SuppPrintMask	(	word	uMask,
		int	nBits
	)

Function*************************************************************

Synopsis [Select variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file extraUtilSupp.c.

{
    int i;
    for ( i = 0; i < nBits; i++ )
        printf( "%d", (int)((uMask >> i) & 1) );
    printf( "\n" );
}

void Abc_SuppPrintProfile	(	Vec_Wrd_t *	p,
		int	nBits
	)

Definition at line 188 of file extraUtilSupp.c.

{
    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) );
}

void Abc_SuppProfile	(	Vec_Wec_t *	pS,
		Vec_Wec_t *	pD,
		int	nVars
	)

Definition at line 442 of file extraUtilSupp.c.

{
    int v;
    for ( v = 0; v < nVars; v++ )
        printf( "%2d : S = %3d  D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) );
}

Vec_Wrd_t* Abc_SuppReadMin	(	char *	pFileName,
		int *	pnVars
	)

Function*************************************************************

Synopsis [Reads the input part of the cubes specified in MIN format.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file extraUtilSupp.c.

{
    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;
}

void Abc_SuppReadMinTest

(

char *

pFileName

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file extraUtilSupp.c.

{
//    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 );
}

void Abc_SuppRemove	(	Vec_Wrd_t *	p,
		int *	pCounts,
		Vec_Wec_t *	pS,
		Vec_Wec_t *	pD,
		int	iVar,
		int	nVars
	)

Definition at line 415 of file extraUtilSupp.c.

{
    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 );
        }        
    }
}

int Abc_SuppSolve	(	Vec_Wrd_t *	p,
		int	nVars
	)

Definition at line 448 of file extraUtilSupp.c.

{
    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;
}

void Abc_SuppTest	(	int	nOnes,
		int	nVars,
		int	fUseSimple,
		int	fCheck,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Create representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file extraUtilSupp.c.

{
    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 );
}

void Abc_SuppVerify	(	Vec_Wrd_t *	p,
		word *	pMatrix,
		int	nVars,
		int	nVarsMin
	)

Function*************************************************************

Synopsis [Perform verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file extraUtilSupp.c.

{
    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 );
}

ABC_NAMESPACE_IMPL_START void Extra_PrintBinary	(	FILE *	pFile,
		unsigned	Sign[],
		int	nBits
	)

DECLARATIONS ///.

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

]

Function*************************************************************

Synopsis [Prints the bit string.]

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file extraUtilFile.c.

{
    int Remainder, nWords;
    int w, i;

    Remainder = (nBits%(sizeof(unsigned)*8));
    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);

    for ( w = nWords-1; w >= 0; w-- )
        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
            fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );

//  fprintf( pFile, "\n" );
}