extra.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/st/st.h"

Go to the source code of this file.

Typedefs
typedef unsigned short	uint16
typedef unsigned int	uint32
typedef struct Extra_BitMat_t_	Extra_BitMat_t
typedef struct Extra_FileReader_t_	Extra_FileReader_t
typedef struct Extra_MmFixed_t_	Extra_MmFixed_t
typedef struct Extra_MmFlex_t_	Extra_MmFlex_t
typedef struct Extra_MmStep_t_	Extra_MmStep_t
typedef struct Sdm_Man_t_	Sdm_Man_t
typedef struct ProgressBarStruct	ProgressBar

Functions
Extra_BitMat_t *	Extra_BitMatrixStart (int nSize)
void	Extra_BitMatrixClean (Extra_BitMat_t *p)
void	Extra_BitMatrixStop (Extra_BitMat_t *p)
void	Extra_BitMatrixPrint (Extra_BitMat_t *p)
int	Extra_BitMatrixReadSize (Extra_BitMat_t *p)
void	Extra_BitMatrixInsert1 (Extra_BitMat_t *p, int i, int k)
int	Extra_BitMatrixLookup1 (Extra_BitMat_t *p, int i, int k)
void	Extra_BitMatrixDelete1 (Extra_BitMat_t *p, int i, int k)
void	Extra_BitMatrixInsert2 (Extra_BitMat_t *p, int i, int k)
int	Extra_BitMatrixLookup2 (Extra_BitMat_t *p, int i, int k)
void	Extra_BitMatrixDelete2 (Extra_BitMat_t *p, int i, int k)
void	Extra_BitMatrixOr (Extra_BitMat_t *p, int i, unsigned *pInfo)
void	Extra_BitMatrixOrTwo (Extra_BitMat_t *p, int i, int j)
int	Extra_BitMatrixCountOnesUpper (Extra_BitMat_t *p)
int	Extra_BitMatrixIsDisjoint (Extra_BitMat_t *p1, Extra_BitMat_t *p2)
int	Extra_BitMatrixIsClique (Extra_BitMat_t *p)
char *	Extra_FileGetSimilarName (char *pFileNameWrong, char *pS1, char *pS2, char *pS3, char *pS4, char *pS5)
char *	Extra_FileNameExtension (char *FileName)
char *	Extra_FileNameAppend (char *pBase, char *pSuffix)
char *	Extra_FileNameGeneric (char *FileName)
char *	Extra_FileNameGenericAppend (char *pBase, char *pSuffix)
void	Extra_FileNameCorrectPath (char *FileName)
char *	Extra_FileNameWithoutPath (char *FileName)
char *	Extra_FilePathWithoutName (char *FileName)
char *	Extra_FileDesignName (char *pFileName)
int	Extra_FileCheck (char *pFileName)
int	Extra_FileSize (char *pFileName)
char *	Extra_FileRead (FILE *pFile)
char *	Extra_FileRead2 (FILE *pFile, FILE *pFile2)
char *	Extra_FileReadContents (char *pFileName)
char *	Extra_FileReadContents2 (char *pFileName, char *pFileName2)
int	Extra_FileIsType (char *pFileName, char *pS1, char *pS2, char *pS3)
char *	Extra_TimeStamp ()
char *	Extra_StringAppend (char *pStrGiven, char *pStrAdd)
void	Extra_StringClean (char *pStrGiven, char *pCharKeep)
unsigned	Extra_ReadBinary (char *Buffer)
void	Extra_PrintBinary (FILE *pFile, unsigned Sign[], int nBits)
int	Extra_ReadHex (unsigned Sign[], char *pString, int nDigits)
int	Extra_ReadHexadecimal (unsigned Sign[], char *pString, int nVars)
void	Extra_PrintHexadecimal (FILE *pFile, unsigned Sign[], int nVars)
void	Extra_PrintHexadecimalString (char *pString, unsigned Sign[], int nVars)
void	Extra_PrintHex (FILE *pFile, unsigned *pTruth, int nVars)
void	Extra_PrintHexReverse (FILE *pFile, unsigned *pTruth, int nVars)
void	Extra_PrintSymbols (FILE *pFile, char Char, int nTimes, int fPrintNewLine)
Extra_FileReader_t *	Extra_FileReaderAlloc (char *pFileName, char *pCharsComment, char *pCharsStop, char *pCharsClean)
	FUNCTION DEFINITIONS ///. More...
void	Extra_FileReaderFree (Extra_FileReader_t *p)
char *	Extra_FileReaderGetFileName (Extra_FileReader_t *p)
int	Extra_FileReaderGetFileSize (Extra_FileReader_t *p)
int	Extra_FileReaderGetCurPosition (Extra_FileReader_t *p)
void *	Extra_FileReaderGetTokens (Extra_FileReader_t *p)
int	Extra_FileReaderGetLineNumber (Extra_FileReader_t *p, int iToken)
Extra_MmFixed_t *	Extra_MmFixedStart (int nEntrySize)
void	Extra_MmFixedStop (Extra_MmFixed_t *p)
char *	Extra_MmFixedEntryFetch (Extra_MmFixed_t *p)
void	Extra_MmFixedEntryRecycle (Extra_MmFixed_t *p, char *pEntry)
void	Extra_MmFixedRestart (Extra_MmFixed_t *p)
int	Extra_MmFixedReadMemUsage (Extra_MmFixed_t *p)
int	Extra_MmFixedReadMaxEntriesUsed (Extra_MmFixed_t *p)
Extra_MmFlex_t *	Extra_MmFlexStart ()
void	Extra_MmFlexStop (Extra_MmFlex_t *p)
void	Extra_MmFlexPrint (Extra_MmFlex_t *p)
char *	Extra_MmFlexEntryFetch (Extra_MmFlex_t *p, int nBytes)
int	Extra_MmFlexReadMemUsage (Extra_MmFlex_t *p)
Extra_MmStep_t *	Extra_MmStepStart (int nSteps)
void	Extra_MmStepStop (Extra_MmStep_t *p)
char *	Extra_MmStepEntryFetch (Extra_MmStep_t *p, int nBytes)
void	Extra_MmStepEntryRecycle (Extra_MmStep_t *p, char *pEntry, int nBytes)
int	Extra_MmStepReadMemUsage (Extra_MmStep_t *p)
int	Extra_Base2LogDouble (double Num)
double	Extra_Power2 (int Num)
int	Extra_Power3 (int Num)
int	Extra_NumCombinations (int k, int n)
int *	Extra_DeriveRadixCode (int Number, int Radix, int nDigits)
int	Extra_CountOnes (unsigned char *pBytes, int nBytes)
int	Extra_Factorial (int n)
char **	Extra_Permutations (int n)
unsigned	Extra_TruthPermute (unsigned Truth, char *pPerms, int nVars, int fReverse)
unsigned	Extra_TruthPolarize (unsigned uTruth, int Polarity, int nVars)
unsigned	Extra_TruthCanonN (unsigned uTruth, int nVars)
unsigned	Extra_TruthCanonNN (unsigned uTruth, int nVars)
unsigned	Extra_TruthCanonP (unsigned uTruth, int nVars)
unsigned	Extra_TruthCanonNP (unsigned uTruth, int nVars)
unsigned	Extra_TruthCanonNPN (unsigned uTruth, int nVars)
void	Extra_Truth4VarNPN (unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)
void	Extra_Truth4VarN (unsigned short **puCanons, char ***puPhases, char **ppCounters, int nPhasesMax)
unsigned short	Extra_TruthPerm4One (unsigned uTruth, int Phase)
unsigned	Extra_TruthPerm5One (unsigned uTruth, int Phase)
void	Extra_TruthPerm6One (unsigned *uTruth, int Phase, unsigned *uTruthRes)
void	Extra_TruthExpand (int nVars, int nWords, unsigned *puTruth, unsigned uPhase, unsigned *puTruthR)
void **	Extra_ArrayAlloc (int nCols, int nRows, int Size)
unsigned short **	Extra_TruthPerm43 ()
unsigned **	Extra_TruthPerm53 ()
unsigned **	Extra_TruthPerm54 ()
void	Extra_BubbleSort (int Order[], int Costs[], int nSize, int fIncreasing)
int *	Extra_GreyCodeSchedule (int n)
int *	Extra_PermSchedule (int n)
word	Extra_Truth6MinimumExact (word t, int *pComp, int *pPerm)
word	Extra_Truth6MinimumHeuristic (word t)
int	Extra_TruthCanonFastN (int nVarsMax, int nVarsReal, unsigned *pt, unsigned **pptRes, char **ppfRes)
int	Sdm_ManCanRead ()
Sdm_Man_t *	Sdm_ManRead ()
void	Sdm_ManQuit ()
int	Sdm_ManComputeFunc (Sdm_Man_t *p, int iDsdLit0, int iDsdLit1, int *pCut, int uMask, int fXor)
void	Sdm_ManPrintDsdStats (Sdm_Man_t *p, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
int	Sdm_ManReadDsdVarNum (Sdm_Man_t *p, int iDsd)
int	Sdm_ManReadDsdAndNum (Sdm_Man_t *p, int iDsd)
int	Sdm_ManReadDsdClauseNum (Sdm_Man_t *p, int iDsd)
word	Sdm_ManReadDsdTruth (Sdm_Man_t *p, int iDsd)
char *	Sdm_ManReadDsdStr (Sdm_Man_t *p, int iDsd)
void	Sdm_ManReadCnfCosts (Sdm_Man_t *p, int *pCosts, int nCosts)
ProgressBar *	Extra_ProgressBarStart (FILE *pFile, int nItemsTotal)
	FUNCTION DEFINITIONS ///. More...
void	Extra_ProgressBarStop (ProgressBar *p)
void	Extra_ProgressBarUpdate_int (ProgressBar *p, int nItemsCur, char *pString)
static void	Extra_ProgressBarUpdate (ProgressBar *p, int nItemsCur, char *pString)
static int	Extra_BitWordNum (int nBits)
static int	Extra_TruthWordNum (int nVars)
static void	Extra_TruthSetBit (unsigned *p, int Bit)
static void	Extra_TruthXorBit (unsigned *p, int Bit)
static int	Extra_TruthHasBit (unsigned *p, int Bit)
static int	Extra_WordCountOnes (unsigned uWord)
static int	Extra_TruthCountOnes (unsigned *pIn, int nVars)
static int	Extra_TruthIsEqual (unsigned *pIn0, unsigned *pIn1, int nVars)
static int	Extra_TruthIsConst0 (unsigned *pIn, int nVars)
static int	Extra_TruthIsConst1 (unsigned *pIn, int nVars)
static int	Extra_TruthIsImply (unsigned *pIn1, unsigned *pIn2, int nVars)
static void	Extra_TruthCopy (unsigned *pOut, unsigned *pIn, int nVars)
static void	Extra_TruthClear (unsigned *pOut, int nVars)
static void	Extra_TruthFill (unsigned *pOut, int nVars)
static void	Extra_TruthNot (unsigned *pOut, unsigned *pIn, int nVars)
static void	Extra_TruthAnd (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Extra_TruthOr (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Extra_TruthSharp (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Extra_TruthNand (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Extra_TruthAndPhase (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars, int fCompl0, int fCompl1)
unsigned **	Extra_TruthElementary (int nVars)
void	Extra_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int Start)
void	Extra_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
void	Extra_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
int	Extra_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
int	Extra_TruthSupportSize (unsigned *pTruth, int nVars)
int	Extra_TruthSupport (unsigned *pTruth, int nVars)
void	Extra_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
void	Extra_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
void	Extra_TruthExist (unsigned *pTruth, int nVars, int iVar)
void	Extra_TruthForall (unsigned *pTruth, int nVars, int iVar)
void	Extra_TruthMux (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
void	Extra_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
int	Extra_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
void	Extra_TruthCountOnesInCofs (unsigned *pTruth, int nVars, short *pStore)
unsigned	Extra_TruthHash (unsigned *pIn, int nWords)
unsigned	Extra_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)
abctime	Extra_CpuTime ()
double	Extra_CpuTimeDouble ()
int	Extra_GetSoftDataLimit ()
	FUNCTION DEFINITIONS ///. More...
ABC_DLL void	Extra_UtilGetoptReset ()
int	Extra_UtilGetopt (int argc, char *argv[], const char *optstring)
char *	Extra_UtilPrintTime (long t)
char *	Extra_UtilStrsav (const char *s)
char *	Extra_UtilTildeExpand (char *fname)
char *	Extra_UtilFileSearch (char *file, char *path, char *mode)

Variables
ABC_NAMESPACE_HEADER_START typedef unsigned char	uint8
void(*	Extra_UtilMMoutOfMemory )(long size)
const char *	globalUtilOptarg
int	globalUtilOptind

Typedef Documentation

typedef struct Extra_BitMat_t_ Extra_BitMat_t

Definition at line 81 of file extra.h.

typedef struct Extra_FileReader_t_ Extra_FileReader_t

Definition at line 132 of file extra.h.

typedef struct Extra_MmFixed_t_ Extra_MmFixed_t

Definition at line 144 of file extra.h.

typedef struct Extra_MmFlex_t_ Extra_MmFlex_t

Definition at line 145 of file extra.h.

typedef struct Extra_MmStep_t_ Extra_MmStep_t

Definition at line 146 of file extra.h.

typedef struct ProgressBarStruct ProgressBar

Definition at line 237 of file extra.h.

typedef struct Sdm_Man_t_ Sdm_Man_t

Definition at line 222 of file extra.h.

typedef unsigned short uint16

Definition at line 72 of file extra.h.

typedef unsigned int uint32

Definition at line 73 of file extra.h.

Function Documentation

void** Extra_ArrayAlloc	(	int	nCols,
		int	nRows,
		int	Size
	)

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

Synopsis [Allocated one-memory-chunk array.]

Description []

SideEffects []

SeeAlso []

Definition at line 880 of file extraUtilMisc.c.

{
    void ** pRes;
    char * pBuffer;
    int i;
    assert( nCols > 0 && nRows > 0 && Size > 0 );
    pBuffer = ABC_ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
    pRes = (void **)pBuffer;
    pRes[0] = pBuffer + nCols * sizeof(void *);
    for ( i = 1; i < nCols; i++ )
        pRes[i] = (void *)((char *)pRes[0] + i * nRows * Size);
    return pRes;
}

int Extra_Base2LogDouble

(

double

Num

)

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

Synopsis [Finds the smallest integer larger of equal than the logarithm.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file extraUtilMisc.c.

{
    double Res;
    int ResInt;

    Res    = log(Num)/log(2.0);
    ResInt = (int)Res;
    if ( ResInt == Res )
        return ResInt;
    else 
        return ResInt+1;
}

void Extra_BitMatrixClean

(

Extra_BitMat_t *

p

)

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

Synopsis [Stops the bit matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file extraUtilBitMatrix.c.

{
    memset( p->ppData[0], 0, sizeof(unsigned) * p->nSize * p->nWords );
}

int Extra_BitMatrixCountOnesUpper

(

Extra_BitMat_t *

p

)

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

Synopsis [Counts the number of 1's in the upper rectangle.]

Description []

SideEffects []

SeeAlso []

Definition at line 349 of file extraUtilBitMatrix.c.

{
    int i, k, nTotal = 0;
    for ( i = 0; i < p->nSize; i++ )
        for ( k = i + 1; k < p->nSize; k++ )
            nTotal += ( (p->ppData[i][k>>5] & (1 << (k&31))) > 0 );
    return nTotal;
}

void Extra_BitMatrixDelete1	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file extraUtilBitMatrix.c.

{
    p->nDeletes++;
    if ( i < k )
        p->ppData[i][k>>p->nBitShift] &= ~(1<<(k & p->uMask));
    else
        p->ppData[k][i>>p->nBitShift] &= ~(1<<(i & p->uMask));
}

void Extra_BitMatrixDelete2	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file extraUtilBitMatrix.c.

{
    p->nDeletes++;
    if ( i > k )
        p->ppData[i][k>>p->nBitShift] &= ~(1<<(k & p->uMask));
    else
        p->ppData[k][i>>p->nBitShift] &= ~(1<<(i & p->uMask));
}

void Extra_BitMatrixInsert1	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 190 of file extraUtilBitMatrix.c.

{
    p->nInserts++;
    if ( i < k )
        p->ppData[i][k>>p->nBitShift] |= (1<<(k & p->uMask));
    else
        p->ppData[k][i>>p->nBitShift] |= (1<<(i & p->uMask));
}

void Extra_BitMatrixInsert2	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file extraUtilBitMatrix.c.

{
    p->nInserts++;
    if ( i > k )
        p->ppData[i][k>>p->nBitShift] |= (1<<(k & p->uMask));
    else
        p->ppData[k][i>>p->nBitShift] |= (1<<(i & p->uMask));
}

int Extra_BitMatrixIsClique

(

Extra_BitMat_t *

pMat

)

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

Synopsis [Returns 1 if the matrix is a set of cliques.]

Description [For example pairwise symmetry info should satisfy this property.]

SideEffects []

SeeAlso []

Definition at line 391 of file extraUtilBitMatrix.c.

{
    int v, u, i;
    for ( v = 0; v < pMat->nSize; v++ )
    for ( u = v+1; u < pMat->nSize; u++ )
    {
        if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
            continue;
        // v and u are symmetric
        for ( i = 0; i < pMat->nSize; i++ )
        {
            if ( i == v || i == u )
                continue;
            // i is neither v nor u
            // the symmetry status of i is the same w.r.t. to v and u
            if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
                return 0;
        }
    }
    return 1;
}

int Extra_BitMatrixIsDisjoint	(	Extra_BitMat_t *	p1,
		Extra_BitMat_t *	p2
	)

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

Synopsis [Returns 1 if the matrices have no entries in common.]

Description []

SideEffects []

SeeAlso []

Definition at line 369 of file extraUtilBitMatrix.c.

{
    int i, w;
    assert( p1->nSize == p2->nSize );
    for ( i = 0; i < p1->nSize; i++ )
        for ( w = 0; w < p1->nWords; w++ )
            if ( p1->ppData[i][w] & p2->ppData[i][w] )
                return 0;
    return 1;
}

int Extra_BitMatrixLookup1	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file extraUtilBitMatrix.c.

{
    p->nLookups++;
    if ( i < k )
        return ((p->ppData[i][k>>p->nBitShift] & (1<<(k & p->uMask))) > 0);
    else
        return ((p->ppData[k][i>>p->nBitShift] & (1<<(i & p->uMask))) > 0);
}

int Extra_BitMatrixLookup2	(	Extra_BitMat_t *	p,
		int	i,
		int	k
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file extraUtilBitMatrix.c.

{
    p->nLookups++;
    if ( i > k )
        return ((p->ppData[i][k>>p->nBitShift] & (1<<(k & p->uMask))) > 0);
    else
        return ((p->ppData[k][i>>p->nBitShift] & (1<<(i & p->uMask))) > 0);
}

void Extra_BitMatrixOr	(	Extra_BitMat_t *	p,
		int	i,
		unsigned *	pInfo
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 313 of file extraUtilBitMatrix.c.

{
    int w;
    for ( w = 0; w < p->nWords; w++ )
        p->ppData[i][w] |= pInfo[w];
}

void Extra_BitMatrixOrTwo	(	Extra_BitMat_t *	p,
		int	i,
		int	j
	)

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

Synopsis [Inserts the element into the upper part.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file extraUtilBitMatrix.c.

{
    int w;
    for ( w = 0; w < p->nWords; w++ )
        p->ppData[i][w] = p->ppData[j][w] = (p->ppData[i][w] | p->ppData[j][w]);
}

void Extra_BitMatrixPrint

(

Extra_BitMat_t *

pMat

)

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

Synopsis [Prints the bit-matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file extraUtilBitMatrix.c.

{
    int i, k, nVars;
    printf( "\n" );
    nVars = Extra_BitMatrixReadSize( pMat );
    for ( i = 0; i < nVars; i++ )
    {
        for ( k = 0; k <= i; k++ )
            printf( " " );
        for ( k = i+1; k < nVars; k++ )
            if ( Extra_BitMatrixLookup1( pMat, i, k ) )
                printf( "1" );
            else
                printf( "." );
        printf( "\n" );
    }
}

int Extra_BitMatrixReadSize

(

Extra_BitMat_t *

p

)

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

Synopsis [Reads the matrix size.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file extraUtilBitMatrix.c.

{
    return p->nSize;
}

Extra_BitMat_t* Extra_BitMatrixStart

(

int

nSize

)

AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Starts the bit matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file extraUtilBitMatrix.c.

{
    Extra_BitMat_t * p;
    int i;
    p = ABC_ALLOC( Extra_BitMat_t, 1 );
    memset( p, 0, sizeof(Extra_BitMat_t) );
    p->nSize     = nSize;
    p->nBitShift = (sizeof(unsigned) == 4) ?  5:  6;
    p->uMask     = (sizeof(unsigned) == 4) ? 31: 63;
    p->nWords    = nSize / (8 * sizeof(unsigned)) + ((nSize % (8 * sizeof(unsigned))) > 0);
    p->ppData    = ABC_ALLOC( unsigned *, nSize );
    p->ppData[0] = ABC_ALLOC( unsigned, nSize * p->nWords );
    memset( p->ppData[0], 0, sizeof(unsigned) * nSize * p->nWords );
    for ( i = 1; i < nSize; i++ )
        p->ppData[i] = p->ppData[i-1] + p->nWords;
    return p;
}

void Extra_BitMatrixStop

(

Extra_BitMat_t *

p

)

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

Synopsis [Stops the bit matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file extraUtilBitMatrix.c.

{
    ABC_FREE( p->ppData[0] );
    ABC_FREE( p->ppData );
    ABC_FREE( p );
}

static int Extra_BitWordNum ( int  nBits )

inlinestatic

Definition at line 248 of file extra.h.

{ return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }

void Extra_BubbleSort	(	int	Order[],
		int	Costs[],
		int	nSize,
		int	fIncreasing
	)

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

Synopsis [Bubble-sorts components by scores in increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 2044 of file extraUtilMisc.c.

{
    int i, Temp, fChanges;
    assert( nSize < 1000 );
    for ( i = 0; i < nSize; i++ )
        Order[i] = i;
    if ( fIncreasing )
    {
        do {
            fChanges = 0;
            for ( i = 0; i < nSize - 1; i++ )
            {
                if ( Costs[Order[i]] <= Costs[Order[i+1]] )
                    continue;
                Temp = Order[i];
                Order[i] = Order[i+1];
                Order[i+1] = Temp;
                fChanges = 1;
            }
        } while ( fChanges );
    }
    else
    {
        do {
            fChanges = 0;
            for ( i = 0; i < nSize - 1; i++ )
            {
                if ( Costs[Order[i]] >= Costs[Order[i+1]] )
                    continue;
                Temp = Order[i];
                Order[i] = Order[i+1];
                Order[i+1] = Temp;
                fChanges = 1;
            }
        } while ( fChanges );
    }
}

int Extra_CountOnes	(	unsigned char *	pBytes,
		int	nBytes
	)

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

Synopsis [Counts the number of ones in the bitstring.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file extraUtilMisc.c.

{
    static int bit_count[256] = {
      0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
      3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
    };

    int i, Counter;
    Counter = 0;
    for ( i = 0; i < nBytes; i++ )
        Counter += bit_count[ *(pBytes+i) ];
    return Counter;
}

abctime Extra_CpuTime

(

)

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

Synopsis [util_cpu_time()]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file extraUtilUtil.c.

{
    return Abc_Clock();
}

double Extra_CpuTimeDouble

(

)

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

Synopsis [util_cpu_time()]

Description []

SideEffects []

SeeAlso []

Definition at line 381 of file extraUtilUtil.c.

{
    struct rusage ru;
    getrusage(RUSAGE_SELF, &ru);
    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; 
}

int* Extra_DeriveRadixCode	(	int	Number,
		int	Radix,
		int	nDigits
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file extraUtilMisc.c.

{
    static int Code[100];
    int i;
    assert( nDigits < 100 );
    for ( i = 0; i < nDigits; i++ )
    {
        Code[i] = Number % Radix;
        Number  = Number / Radix;
    }
    assert( Number == 0 );
    return Code;
}

int Extra_Factorial

(

int

n

)

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

Synopsis [Computes the factorial.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file extraUtilMisc.c.

{
    int i, Res = 1;
    for ( i = 1; i <= n; i++ )
        Res *= i;
    return Res;
}

int Extra_FileCheck

(

char *

pFileName

)

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

Synopsis [Returns the file size.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 281 of file extraUtilFile.c.

{
    FILE * pFile;
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Extra_FileCheck():  File \"%s\" does not exist.\n", pFileName );
        return 0;
    }
    fseek( pFile, 0, SEEK_END );
    if ( ftell( pFile ) == 0 )
        printf( "Extra_FileCheck():  File \"%s\" is empty.\n", pFileName );
    fclose( pFile );
    return 1;
}

char* Extra_FileDesignName

(

char *

pFileName

)

Definition at line 250 of file extraUtilFile.c.

{
    char * pBeg, * pEnd, * pStore, * pCur;
    // find the first dot
    for ( pEnd = pFileName; *pEnd; pEnd++ )
        if ( *pEnd == '.' )
            break;
    // find the first char
    for ( pBeg = pEnd - 1; pBeg >= pFileName; pBeg-- )
        if ( !((*pBeg >= 'a' && *pBeg <= 'z') || (*pBeg >= 'A' && *pBeg <= 'Z') || (*pBeg >= '0' && *pBeg <= '9') || *pBeg == '_') )
            break;
    pBeg++;
    // fill up storage
    pStore = ABC_ALLOC( char, pEnd - pBeg + 1 );
    for ( pCur = pStore; pBeg < pEnd; pBeg++, pCur++ )
        *pCur = *pBeg;
    *pCur = 0;
    return pStore;
}

char* Extra_FileGetSimilarName	(	char *	pFileNameWrong,
		char *	pS1,
		char *	pS2,
		char *	pS3,
		char *	pS4,
		char *	pS5
	)

CFile****************************************************************

FileName [extraUtilFile.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [File management utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

extraUtilFile.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Tries to find a file name with a different extension.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file extraUtilFile.c.

{
    FILE * pFile;
    char * pFileNameOther;
    char * pFileGen;

    if ( pS1 == NULL )
        return NULL;

    // get the generic file name
    pFileGen = Extra_FileNameGeneric( pFileNameWrong );
    pFileNameOther = Extra_FileNameAppend( pFileGen, pS1 );
    pFile = fopen( pFileNameOther, "r" );
    if ( pFile == NULL && pS2 )
    { // try one more
        pFileNameOther = Extra_FileNameAppend( pFileGen, pS2 );
        pFile = fopen( pFileNameOther, "r" );
        if ( pFile == NULL && pS3 )
        { // try one more
            pFileNameOther = Extra_FileNameAppend( pFileGen, pS3 );
            pFile = fopen( pFileNameOther, "r" );
            if ( pFile == NULL && pS4 )
            { // try one more
                pFileNameOther = Extra_FileNameAppend( pFileGen, pS4 );
                pFile = fopen( pFileNameOther, "r" );
                if ( pFile == NULL && pS5 )
                { // try one more
                    pFileNameOther = Extra_FileNameAppend( pFileGen, pS5 );
                    pFile = fopen( pFileNameOther, "r" );
                }
            }
        }
    }
    ABC_FREE( pFileGen );
    if ( pFile )
    {
        fclose( pFile );
        return pFileNameOther;
    }
    // did not find :(
    return NULL;            
}

int Extra_FileIsType	(	char *	pFileName,
		char *	pS1,
		char *	pS2,
		char *	pS3
	)

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

Synopsis [Returns one if the file has a given extension.]

Description []

SideEffects []

SeeAlso []

Definition at line 420 of file extraUtilFile.c.

{
    int lenS, lenF = strlen(pFileName);
    lenS = pS1 ? strlen(pS1) : 0;
    if ( lenS && lenF > lenS && !strncmp( pFileName+lenF-lenS, pS1, lenS ) )
        return 1;
    lenS = pS2 ? strlen(pS2) : 0;
    if ( lenS && lenF > lenS && !strncmp( pFileName+lenF-lenS, pS2, lenS ) )
        return 1;
    lenS = pS3 ? strlen(pS3) : 0;
    if ( lenS && lenF > lenS && !strncmp( pFileName+lenF-lenS, pS3, lenS ) )
        return 1;
    return 0;
}

char* Extra_FileNameAppend	(	char *	pBase,
		char *	pSuffix
	)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file extraUtilFile.c.

{
    static char Buffer[500];
    assert( strlen(pBase) + strlen(pSuffix) < 500 );
    sprintf( Buffer, "%s%s", pBase, pSuffix );
    return Buffer;
}

void Extra_FileNameCorrectPath

(

char *

FileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file extraUtilFile.c.

{
    char * pStart;
    if ( FileName )
        for ( pStart = FileName; *pStart; pStart++ )
            if ( *pStart == '>' || *pStart == '\\' )
                *pStart = '/';
}

char* Extra_FileNameExtension

(

char *

FileName

)

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

Synopsis [Returns the pointer to the file extension.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file extraUtilFile.c.

{
    char * pDot;
    // find the last "dot" in the file name, if it is present
    for ( pDot = FileName + strlen(FileName)-1; pDot >= FileName; pDot-- )
        if ( *pDot == '.' )
            return pDot + 1;
   return FileName;
}

char* Extra_FileNameGeneric

(

char *

FileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file extraUtilFile.c.

{
    char * pDot, * pRes;
    pRes = Extra_UtilStrsav( FileName );
    if ( (pDot = strrchr( pRes, '.' )) )
        *pDot = 0;
    return pRes;
}

char* Extra_FileNameGenericAppend	(	char *	pBase,
		char *	pSuffix
	)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file extraUtilFile.c.

{
    static char Buffer[1000];
    char * pDot;
    assert( strlen(pBase) + strlen(pSuffix) < 1000 );
    strcpy( Buffer, pBase );
    if ( (pDot = strrchr( Buffer, '.' )) )
        *pDot = 0;
    strcat( Buffer, pSuffix );
    return Buffer;
}

char* Extra_FileNameWithoutPath

(

char *

FileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file extraUtilFile.c.

{
    char * pRes;
    for ( pRes = FileName + strlen(FileName) - 1; pRes >= FileName; pRes-- )
        if ( *pRes == '\\' || *pRes == '/' )
            return pRes + 1;
    return FileName;
}

char* Extra_FilePathWithoutName

(

char *

FileName

)

Definition at line 236 of file extraUtilFile.c.

{
    char * pRes;
    FileName = Abc_UtilStrsav( FileName );
    for ( pRes = FileName + strlen(FileName) - 1; pRes >= FileName; pRes-- )
        if ( *pRes == '\\' || *pRes == '/' )
        {
           *pRes = 0;
           Extra_FileNameCorrectPath( FileName );
           return FileName;
        }
    ABC_FREE( FileName );
    return NULL;
}

char* Extra_FileRead

(

FILE *

pFile

)

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

Synopsis [Read the file into the internal buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 336 of file extraUtilFile.c.

{
    int nFileSize;
    char * pBuffer;
    int RetValue;
    // get the file size, in bytes
    fseek( pFile, 0, SEEK_END );  
    nFileSize = ftell( pFile );  
    // move the file current reading position to the beginning
    rewind( pFile ); 
    // load the contents of the file into memory
    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
    RetValue = fread( pBuffer, nFileSize, 1, pFile );
    // terminate the string with '\0'
    pBuffer[ nFileSize + 0] = '\n';
    pBuffer[ nFileSize + 1] = '\0';
    return pBuffer;
}

char* Extra_FileRead2	(	FILE *	pFile,
		FILE *	pFile2
	)

Definition at line 354 of file extraUtilFile.c.

{
    char * pBuffer;
    int nSize, nSize2;
    int RetValue;
    // get the file size, in bytes
    fseek( pFile, 0, SEEK_END );  
    nSize = ftell( pFile );  
    rewind( pFile ); 
    // get the file size, in bytes
    fseek( pFile2, 0, SEEK_END );  
    nSize2 = ftell( pFile2 );  
    rewind( pFile2 ); 
    // load the contents of the file into memory
    pBuffer = ABC_ALLOC( char, nSize + nSize2 + 3 );
    RetValue = fread( pBuffer,         nSize,  1, pFile );
    RetValue = fread( pBuffer + nSize, nSize2, 1, pFile2 );
    // terminate the string with '\0'
    pBuffer[ nSize + nSize2 + 0] = '\n';
    pBuffer[ nSize + nSize2 + 1] = '\0';
    return pBuffer;
}

char* Extra_FileReadContents

(

char *

pFileName

)

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

Synopsis [Read the file into the internal buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 388 of file extraUtilFile.c.

{
    FILE * pFile;
    char * pBuffer;
    pFile = fopen( pFileName, "rb" );
    pBuffer = pFile ? Extra_FileRead( pFile ) : NULL;
    if ( pFile )  fclose( pFile );
    return pBuffer;
}

char* Extra_FileReadContents2	(	char *	pFileName,
		char *	pFileName2
	)

Definition at line 397 of file extraUtilFile.c.

{
    FILE * pFile, * pFile2;
    char * pBuffer;
    pFile  = fopen( pFileName, "rb" );
    pFile2 = fopen( pFileName2, "rb" );
    pBuffer = (pFile && pFile2) ? Extra_FileRead2( pFile, pFile2 ) : NULL;
    if ( pFile )  fclose( pFile );
    if ( pFile2 ) fclose( pFile2 );
    return pBuffer;
}

Extra_FileReader_t* Extra_FileReaderAlloc	(	char *	pFileName,
		char *	pCharsComment,
		char *	pCharsStop,
		char *	pCharsClean
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts the file reader.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file extraUtilReader.c.

{
    Extra_FileReader_t * p;
    FILE * pFile;
    char * pChar;
    int nCharsToRead;
    int RetValue;
    // check if the file can be opened
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Extra_FileReaderAlloc(): Cannot open input file \"%s\".\n", pFileName );
        return NULL;
    }
    // start the file reader    
    p = ABC_ALLOC( Extra_FileReader_t, 1 );
    memset( p, 0, sizeof(Extra_FileReader_t) );
    p->pFileName   = pFileName;
    p->pFile       = pFile;
    // set the character map
    memset( p->pCharMap, EXTRA_CHAR_NORMAL, 256 );
    for ( pChar = pCharsComment; *pChar; pChar++ )
        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_COMMENT;
    for ( pChar = pCharsStop; *pChar; pChar++ )
        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_STOP;
    for ( pChar = pCharsClean; *pChar; pChar++ )
        p->pCharMap[(unsigned char)*pChar] = EXTRA_CHAR_CLEAN;
    // get the file size, in bytes
    fseek( pFile, 0, SEEK_END );  
    p->nFileSize = ftell( pFile );  
    rewind( pFile ); 
    // allocate the buffer
    p->pBuffer = ABC_ALLOC( char, EXTRA_BUFFER_SIZE+1 );
    p->nBufferSize = EXTRA_BUFFER_SIZE;
    p->pBufferCur  = p->pBuffer;
    // determine how many chars to read
    nCharsToRead = EXTRA_MINIMUM(p->nFileSize, EXTRA_BUFFER_SIZE);
    // load the first part into the buffer
    RetValue = fread( p->pBuffer, nCharsToRead, 1, p->pFile );
    p->nFileRead = nCharsToRead;
    // set the ponters to the end and the stopping point
    p->pBufferEnd  = p->pBuffer + nCharsToRead;
    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + EXTRA_BUFFER_SIZE - EXTRA_OFFSET_SIZE;
    // start the arrays
    p->vTokens = Vec_PtrAlloc( 100 );
    p->vLines = Vec_IntAlloc( 100 );
    p->nLineCounter = 1; // 1-based line counting
    return p;
}

void Extra_FileReaderFree

(

Extra_FileReader_t *

p

)

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

Synopsis [Stops the file reader.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file extraUtilReader.c.

{
    if ( p->pFile )
        fclose( p->pFile );
    ABC_FREE( p->pBuffer );
    Vec_PtrFree( p->vTokens );
    Vec_IntFree( p->vLines );
    ABC_FREE( p );
}

int Extra_FileReaderGetCurPosition

(

Extra_FileReader_t *

p

)

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

Synopsis [Returns the current reading position.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file extraUtilReader.c.

{
    return p->nFileRead - (p->pBufferEnd - p->pBufferCur);
}

char* Extra_FileReaderGetFileName

(

Extra_FileReader_t *

p

)

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

Synopsis [Returns the file size.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file extraUtilReader.c.

{
    return p->pFileName;
}

int Extra_FileReaderGetFileSize

(

Extra_FileReader_t *

p

)

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

Synopsis [Returns the file size.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file extraUtilReader.c.

{
    return p->nFileSize;
}

int Extra_FileReaderGetLineNumber	(	Extra_FileReader_t *	p,
		int	iToken
	)

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

Synopsis [Returns the line number for the given token.]

Description []

SideEffects []

SeeAlso []

Definition at line 218 of file extraUtilReader.c.

{
    assert( iToken >= 0 && iToken < p->vTokens->nSize );
    return p->vLines->pArray[iToken];
}

void* Extra_FileReaderGetTokens

(

Extra_FileReader_t *

p

)

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

Synopsis [Returns the next set of tokens.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file extraUtilReader.c.

{
    Vec_Ptr_t * vTokens;
    while ( (vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens_int( p )) )
        if ( vTokens->nSize > 0 )
            break;
    return vTokens;
}

int Extra_FileSize

(

char *

pFileName

)

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

Synopsis [Returns the file size.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 308 of file extraUtilFile.c.

{
    FILE * pFile;
    int nFileSize;
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Extra_FileSize(): The file is unavailable (absent or open).\n" );
        return 0;
    }
    fseek( pFile, 0, SEEK_END );  
    nFileSize = ftell( pFile ); 
    fclose( pFile );
    return nFileSize;
}

int Extra_GetSoftDataLimit

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis [getSoftDataLimit()]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file extraUtilUtil.c.

{
    return EXTRA_RLIMIT_DATA_DEFAULT;
}

int* Extra_GreyCodeSchedule

(

int

n

)

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

Synopsis [Computes complementation schedule for 2^n Grey codes.]

Description []

SideEffects []

SeeAlso []

Definition at line 2169 of file extraUtilMisc.c.

{
    int * pRes = ABC_ALLOC( int, (1<<n) );
    int i, k, b = 0;
//    pRes[b++] = -1;
    for ( k = 0; k < n; k++ )
        for ( pRes[b++] = k, i = 1; i < (1<<k); i++ )
            pRes[b++] = pRes[i-1]; // pRes[i];
    pRes[b++] = n-1;
    assert( b == (1<<n) );

    if ( 0 )
    {
        unsigned uSign = 0;
        for ( b = 0; b < (1<<n); b++ )
        {
            uSign ^= (1 << pRes[b]);
            printf( "%3d %3d  ", b, pRes[b] );
            Extra_PrintBinary( stdout, &uSign, n );
            printf( "\n" );
        }
    }
    return pRes;
}

char* Extra_MmFixedEntryFetch

(

Extra_MmFixed_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file extraUtilMemory.c.

{
    char * pTemp;
    int i;

    // check if there are still free entries
    if ( p->nEntriesUsed == p->nEntriesAlloc )
    { // need to allocate more entries
        assert( p->pEntriesFree == NULL );
        if ( p->nChunks == p->nChunksAlloc )
        {
            p->nChunksAlloc *= 2;
            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
        }
        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
        // transform these entries into a linked list
        pTemp = p->pEntriesFree;
        for ( i = 1; i < p->nChunkSize; i++ )
        {
            *((char **)pTemp) = pTemp + p->nEntrySize;
            pTemp += p->nEntrySize;
        }
        // set the last link
        *((char **)pTemp) = NULL;
        // add the chunk to the chunk storage
        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
        // add to the number of entries allocated
        p->nEntriesAlloc += p->nChunkSize;
    }
    // incrememt the counter of used entries
    p->nEntriesUsed++;
    if ( p->nEntriesMax < p->nEntriesUsed )
        p->nEntriesMax = p->nEntriesUsed;
    // return the first entry in the free entry list
    pTemp = p->pEntriesFree;
    p->pEntriesFree = *((char **)pTemp);
    return pTemp;
}

void Extra_MmFixedEntryRecycle	(	Extra_MmFixed_t *	p,
		char *	pEntry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file extraUtilMemory.c.

{
    // decrement the counter of used entries
    p->nEntriesUsed--;
    // add the entry to the linked list of free entries
    *((char **)pEntry) = p->pEntriesFree;
    p->pEntriesFree = pEntry;
}

int Extra_MmFixedReadMaxEntriesUsed

(

Extra_MmFixed_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file extraUtilMemory.c.

{
    return p->nEntriesMax;
}

int Extra_MmFixedReadMemUsage

(

Extra_MmFixed_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file extraUtilMemory.c.

{
    return p->nMemoryAlloc;
}

void Extra_MmFixedRestart

(

Extra_MmFixed_t *

p

)

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

Synopsis []

Description [Relocates all the memory except the first chunk.]

SideEffects []

SeeAlso []

Definition at line 273 of file extraUtilMemory.c.

{
    int i;
    char * pTemp;

    // deallocate all chunks except the first one
    for ( i = 1; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    p->nChunks = 1;
    // transform these entries into a linked list
    pTemp = p->pChunks[0];
    for ( i = 1; i < p->nChunkSize; i++ )
    {
        *((char **)pTemp) = pTemp + p->nEntrySize;
        pTemp += p->nEntrySize;
    }
    // set the last link
    *((char **)pTemp) = NULL;
    // set the free entry list
    p->pEntriesFree  = p->pChunks[0];
    // set the correct statistics
    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
    p->nMemoryUsed   = 0;
    p->nEntriesAlloc = p->nChunkSize;
    p->nEntriesUsed  = 0;
}

Extra_MmFixed_t* Extra_MmFixedStart

(

int

nEntrySize

)

AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Allocates memory pieces of fixed size.]

Description [The size of the chunk is computed as the minimum of 1024 entries and 64K. Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 122 of file extraUtilMemory.c.

{
    Extra_MmFixed_t * p;

    p = ABC_ALLOC( Extra_MmFixed_t, 1 );
    memset( p, 0, sizeof(Extra_MmFixed_t) );

    p->nEntrySize    = nEntrySize;
    p->nEntriesAlloc = 0;
    p->nEntriesUsed  = 0;
    p->pEntriesFree  = NULL;

    if ( nEntrySize * (1 << 10) < (1<<16) )
        p->nChunkSize = (1 << 10);
    else
        p->nChunkSize = (1<<16) / nEntrySize;
    if ( p->nChunkSize < 8 )
        p->nChunkSize = 8;

    p->nChunksAlloc  = 64;
    p->nChunks       = 0;
    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );

    p->nMemoryUsed   = 0;
    p->nMemoryAlloc  = 0;
    return p;
}

void Extra_MmFixedStop

(

Extra_MmFixed_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file extraUtilMemory.c.

{
    int i;
    if ( p == NULL )
        return;
    for ( i = 0; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    ABC_FREE( p->pChunks );
    ABC_FREE( p );
}

char* Extra_MmFlexEntryFetch	(	Extra_MmFlex_t *	p,
		int	nBytes
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 418 of file extraUtilMemory.c.

{
    char * pTemp;
    // check if there are still free entries
    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
    { // need to allocate more entries
        if ( p->nChunks == p->nChunksAlloc )
        {
            p->nChunksAlloc *= 2;
            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
        }
        if ( nBytes > p->nChunkSize )
        {
            // resize the chunk size if more memory is requested than it can give
            // (ideally, this should never happen)
            p->nChunkSize = 2 * nBytes;
        }
        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
        p->pEnd     = p->pCurrent + p->nChunkSize;
        p->nMemoryAlloc += p->nChunkSize;
        // add the chunk to the chunk storage
        p->pChunks[ p->nChunks++ ] = p->pCurrent;
    }
    assert( p->pCurrent + nBytes <= p->pEnd );
    // increment the counter of used entries
    p->nEntriesUsed++;
    // keep track of the memory used
    p->nMemoryUsed += nBytes;
    // return the next entry
    pTemp = p->pCurrent;
    p->pCurrent += nBytes;
    return pTemp;
}

void Extra_MmFlexPrint

(

Extra_MmFlex_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 376 of file extraUtilMemory.c.

{
    printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
        p->nChunkSize, p->nChunks );
    printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
        p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
}

int Extra_MmFlexReadMemUsage

(

Extra_MmFlex_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 463 of file extraUtilMemory.c.

{
    return p->nMemoryAlloc;
}

Extra_MmFlex_t* Extra_MmFlexStart

(

)

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

Synopsis [Allocates entries of flexible size.]

Description [Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 344 of file extraUtilMemory.c.

{ 
    Extra_MmFlex_t * p;
//printf( "allocing flex\n" );
    p = ABC_ALLOC( Extra_MmFlex_t, 1 );
    memset( p, 0, sizeof(Extra_MmFlex_t) );

    p->nEntriesUsed  = 0;
    p->pCurrent      = NULL;
    p->pEnd          = NULL;

    p->nChunkSize    = (1 << 12);
    p->nChunksAlloc  = 64;
    p->nChunks       = 0;
    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );

    p->nMemoryUsed   = 0;
    p->nMemoryAlloc  = 0;
    return p;
}

void Extra_MmFlexStop

(

Extra_MmFlex_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 395 of file extraUtilMemory.c.

{
    int i;
    if ( p == NULL )
        return;
//printf( "deleting flex\n" );
    for ( i = 0; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    ABC_FREE( p->pChunks );
    ABC_FREE( p );
}

char* Extra_MmStepEntryFetch	(	Extra_MmStep_t *	p,
		int	nBytes
	)

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

Synopsis [Creates the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 555 of file extraUtilMemory.c.

{
    if ( nBytes == 0 )
        return NULL;
    if ( nBytes > p->nMapSize )
    {
//        printf( "Allocating %d bytes.\n", nBytes );
//        return ABC_ALLOC( char, nBytes );
        if ( p->nLargeChunks == p->nLargeChunksAlloc )
        {
            if ( p->nLargeChunksAlloc == 0 )
                p->nLargeChunksAlloc = 32;
            p->nLargeChunksAlloc *= 2;
            p->pLargeChunks = ABC_REALLOC( void *, p->pLargeChunks, p->nLargeChunksAlloc );
        }
        p->pLargeChunks[ p->nLargeChunks++ ] = ABC_ALLOC( char, nBytes );
        return (char *)p->pLargeChunks[ p->nLargeChunks - 1 ];
    }
    return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
}

void Extra_MmStepEntryRecycle	(	Extra_MmStep_t *	p,
		char *	pEntry,
		int	nBytes
	)

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

Synopsis [Recycles the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 of file extraUtilMemory.c.

{
    if ( nBytes == 0 )
        return;
    if ( nBytes > p->nMapSize )
    {
//        ABC_FREE( pEntry );
        return;
    }
    Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
}

int Extra_MmStepReadMemUsage

(

Extra_MmStep_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file extraUtilMemory.c.

{
    int i, nMemTotal = 0;
    for ( i = 0; i < p->nMems; i++ )
        nMemTotal += p->pMems[i]->nMemoryAlloc;
    return nMemTotal;
}

Extra_MmStep_t* Extra_MmStepStart

(

int

nSteps

)

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

Synopsis [Starts the hierarchical memory manager.]

Description [This manager can allocate entries of any size. Iternally they are mapped into the entries with the number of bytes equal to the power of 2. The smallest entry size is 8 bytes. The next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. The input parameters "nSteps" says how many fixed memory managers are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger entries are handed over to malloc() and then ABC_FREE()ed.]

SideEffects []

SeeAlso []

Definition at line 492 of file extraUtilMemory.c.

{
    Extra_MmStep_t * p;
    int i, k;
    p = ABC_ALLOC( Extra_MmStep_t, 1 );
    memset( p, 0, sizeof(Extra_MmStep_t) );
    p->nMems = nSteps;
    // start the fixed memory managers
    p->pMems = ABC_ALLOC( Extra_MmFixed_t *, p->nMems );
    for ( i = 0; i < p->nMems; i++ )
        p->pMems[i] = Extra_MmFixedStart( (8<<i) );
    // set up the mapping of the required memory size into the corresponding manager
    p->nMapSize = (4<<p->nMems);
    p->pMap = ABC_ALLOC( Extra_MmFixed_t *, p->nMapSize+1 );
    p->pMap[0] = NULL;
    for ( k = 1; k <= 4; k++ )
        p->pMap[k] = p->pMems[0];
    for ( i = 0; i < p->nMems; i++ )
        for ( k = (4<<i)+1; k <= (8<<i); k++ )
            p->pMap[k] = p->pMems[i];
//for ( i = 1; i < 100; i ++ )
//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
    return p;
}

void Extra_MmStepStop

(

Extra_MmStep_t *

p

)

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

Synopsis [Stops the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 528 of file extraUtilMemory.c.

{
    int i;
    for ( i = 0; i < p->nMems; i++ )
        Extra_MmFixedStop( p->pMems[i] );
    if ( p->pLargeChunks ) 
    {
      for ( i = 0; i < p->nLargeChunks; i++ )
          ABC_FREE( p->pLargeChunks[i] );
      ABC_FREE( p->pLargeChunks );
    }
    ABC_FREE( p->pMems );
    ABC_FREE( p->pMap );
    ABC_FREE( p );
}

int Extra_NumCombinations	(	int	k,
		int	n
	)

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

Synopsis [Finds the number of combinations of k elements out of n.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file extraUtilMisc.c.

{
    int i, Res = 1;
    for ( i = 1; i <= k; i++ )
            Res = Res * (n-i+1) / i;
    return Res;
} /* end of Extra_NumCombinations */

int* Extra_PermSchedule

(

int

n

)

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

Synopsis [Computes permutation schedule for n! permutations.]

Description []

SideEffects []

SeeAlso []

Definition at line 2205 of file extraUtilMisc.c.

{
    int nFact   = Extra_Factorial(n);
    int nGroups = nFact / n / 2;
    int * pRes = ABC_ALLOC( int, nFact );
    int * pRes0, i, k, b = 0;
    assert( n > 1 );
    if ( n == 2 )
    {
        pRes[0] = pRes[1] = 0;
        return pRes;
    }
    pRes0 = Extra_PermSchedule( n-1 );
    for ( k = 0; k < nGroups; k++ )
    {
        for ( i = n-1; i > 0; i-- )
            pRes[b++] = i-1;
        pRes[b++] = pRes0[2*k]+1;
        for ( i = 0; i < n-1; i++ )
            pRes[b++] = i;
        pRes[b++] = pRes0[2*k+1];
    }
    ABC_FREE( pRes0 );
    assert( b == nFact );

    if ( 0 )
    {
        int Perm[16];
        for ( i = 0; i < n; i++ )
            Perm[i] = i;
        for ( b = 0; b < nFact; b++ )
        {
            ABC_SWAP( int, Perm[pRes[b]], Perm[pRes[b]+1] );
            printf( "%3d %3d    ", b, pRes[b] );
            for ( i = 0; i < n; i++ )
                printf( "%d", Perm[i] );
            printf( "\n" );
        }
    }
    return pRes;
}

char** Extra_Permutations

(

int

n

)

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

Synopsis [Computes the set of all permutations.]

Description [The number of permutations in the array is n!. The number of entries in each permutation is n. Therefore, the resulting array is a two-dimentional array of the size: n! x n. To free the resulting array, call ABC_FREE() on the pointer returned by this procedure.]

SideEffects []

SeeAlso []

Definition at line 238 of file extraUtilMisc.c.

{
    char Array[50];
    char ** pRes;
    int nFact, i;
    // allocate memory
    nFact = Extra_Factorial( n );
    pRes  = (char **)Extra_ArrayAlloc( nFact, n, sizeof(char) );
    // fill in the permutations
    for ( i = 0; i < n; i++ )
        Array[i] = i;
    Extra_Permutations_rec( pRes, nFact, n, Array );
    // print the permutations
/*
    {
    int i, k;
    for ( i = 0; i < nFact; i++ )
    {
        printf( "{" );
        for ( k = 0; k < n; k++ )
            printf( " %d", pRes[i][k] );
        printf( " }\n" );
    }
    }
*/
    return pRes;
}

double Extra_Power2

(

int

Degree

)

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

Synopsis [Returns the power of two as a double.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file extraUtilMisc.c.

{
    double Res;
    assert( Degree >= 0 );
    if ( Degree < 32 )
        return (double)(01<<Degree); 
    for ( Res = 1.0; Degree; Res *= 2.0, Degree-- );
    return Res;
}

int Extra_Power3

(

int

Num

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file extraUtilMisc.c.

{
    int i;
    int Res;
    Res = 1;
    for ( i = 0; i < Num; i++ )
        Res *= 3;
    return Res;
}

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

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

void Extra_PrintHex	(	FILE *	pFile,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Prints the hex unsigned into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 620 of file extraUtilFile.c.

{
    int nMints, nDigits, Digit, k;

    // write the number into the file
    fprintf( pFile, "0x" );
    nMints  = (1 << nVars);
    nDigits = nMints / 4 + ((nMints % 4) > 0);
    for ( k = nDigits - 1; k >= 0; k-- )
    {
        Digit = ((pTruth[k/8] >> (k * 4)) & 15);
        if ( Digit < 10 )
            fprintf( pFile, "%d", Digit );
        else
            fprintf( pFile, "%c", 'A' + Digit-10 );
    }
//    fprintf( pFile, "\n" );
}

void Extra_PrintHexadecimal	(	FILE *	pFile,
		unsigned	Sign[],
		int	nVars
	)

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

Synopsis [Prints the hex unsigned into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 565 of file extraUtilFile.c.

{
    int nDigits, Digit, k;
    // write the number into the file
    nDigits = (1 << nVars) / 4;
    for ( k = nDigits - 1; k >= 0; k-- )
    {
        Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
        if ( Digit < 10 )
            fprintf( pFile, "%d", Digit );
        else
            fprintf( pFile, "%c", 'a' + Digit-10 );
    }
//    fprintf( pFile, "\n" );
}

void Extra_PrintHexadecimalString	(	char *	pString,
		unsigned	Sign[],
		int	nVars
	)

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

Synopsis [Prints the hex unsigned into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 592 of file extraUtilFile.c.

{
    int nDigits, Digit, k;
    // write the number into the file
    nDigits = (1 << nVars) / 4;
    for ( k = nDigits - 1; k >= 0; k-- )
    {
        Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
        if ( Digit < 10 )
            *pString++ = '0' + Digit;
        else
            *pString++ = 'a' + Digit-10;
    }
//    fprintf( pFile, "\n" );
    *pString = 0;
}

void Extra_PrintHexReverse	(	FILE *	pFile,
		unsigned *	pTruth,
		int	nVars
	)

Definition at line 638 of file extraUtilFile.c.

{
    int nMints, nDigits, Digit, k;

    // write the number into the file
    fprintf( pFile, "0x" );
    nMints  = (1 << nVars);
    nDigits = nMints / 4 + ((nMints % 4) > 0);
    for ( k = 0; k < nDigits; k++ )
    {
        Digit = ((pTruth[k/8] >> (k * 4)) & 15);
        if ( Digit < 10 )
            fprintf( pFile, "%d", Digit );
        else
            fprintf( pFile, "%c", 'A' + Digit-10 );
    }
//    fprintf( pFile, "\n" );
}

void Extra_PrintSymbols	(	FILE *	pFile,
		char	Char,
		int	nTimes,
		int	fPrintNewLine
	)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 668 of file extraUtilFile.c.

{
    int i;
    for ( i = 0; i < nTimes; i++ )
        printf( "%c", Char );
    if ( fPrintNewLine )
        printf( "\n" );
}

ProgressBar* Extra_ProgressBarStart	(	FILE *	pFile,
		int	nItemsTotal
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts the progress bar.]

Description [The first parameter is the output stream (pFile), where the progress is printed. The current printing position should be the first one on the given line. The second parameters is the total number of items that correspond to 100% position of the progress bar.]

SideEffects []

SeeAlso []

Definition at line 62 of file extraUtilProgress.c.

{
    ProgressBar * p;
    if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
    p = ABC_ALLOC( ProgressBar, 1 );
    memset( p, 0, sizeof(ProgressBar) );
    p->pFile       = pFile;
    p->nItemsTotal = nItemsTotal;
    p->posTotal    = 78;
    p->posCur      = 1;
    p->nItemsNext  = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
    Extra_ProgressBarShow( p, NULL );
    return p;
}

void Extra_ProgressBarStop

(

ProgressBar *

p

)

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

Synopsis [Stops the progress bar.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file extraUtilProgress.c.

{
    if ( p == NULL ) return;
    Extra_ProgressBarClean( p );
    ABC_FREE( p );
}

static void Extra_ProgressBarUpdate ( ProgressBar *  p, int  nItemsCur, char *  pString  )

inlinestatic

Definition at line 243 of file extra.h.

{  if ( p && nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); }

void Extra_ProgressBarUpdate_int	(	ProgressBar *	p,
		int	nItemsCur,
		char *	pString
	)

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

Synopsis [Updates the progress bar.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file extraUtilProgress.c.

{
    if ( p == NULL ) return;
    if ( nItemsCur < p->nItemsNext )
        return;
    if ( nItemsCur >= p->nItemsTotal )
    {
        p->posCur = 78;
        p->nItemsNext = 0x7FFFFFFF;
    }
    else
    {
        p->posCur += 7;
        p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
    }
    Extra_ProgressBarShow( p, pString );
}

unsigned Extra_ReadBinary

(

char *

Buffer

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file extraUtilFile.c.

{
    unsigned Result;
    int i;

    Result = 0;
    for ( i = 0; Buffer[i]; i++ )
        if ( Buffer[i] == '0' || Buffer[i] == '1' )
            Result = Result * 2 + Buffer[i] - '0';
        else
        {
            assert( 0 );
        }
    return Result;
}

int Extra_ReadHex	(	unsigned	Sign[],
		char *	pString,
		int	nDigits
	)

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

Synopsis [Reads the hex unsigned into the bit-string.]

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file extraUtilFile.c.

{
    int Digit, k, c;
    for ( k = 0; k < nDigits; k++ )
    {
        c = nDigits-1-k;
        if ( pString[c] >= '0' && pString[c] <= '9' )
            Digit = pString[c] - '0';
        else if ( pString[c] >= 'A' && pString[c] <= 'F' )
            Digit = pString[c] - 'A' + 10;
        else if ( pString[c] >= 'a' && pString[c] <= 'f' )
            Digit = pString[c] - 'a' + 10;
        else { assert( 0 ); return 0; }
        Sign[k/8] |= ( (Digit & 15) << ((k%8) * 4) );
    }
    return 1;
}

int Extra_ReadHexadecimal	(	unsigned	Sign[],
		char *	pString,
		int	nVars
	)

Definition at line 540 of file extraUtilFile.c.

{
    int nWords, nDigits, k;
    nWords = Extra_TruthWordNum( nVars );
    for ( k = 0; k < nWords; k++ )
        Sign[k] = 0;
    // read the number from the string
    nDigits = (1 << nVars) / 4;
    if ( nDigits == 0 )
        nDigits = 1;
    Extra_ReadHex( Sign, pString, nDigits );
    return 1;
}

char* Extra_StringAppend	(	char *	pStrGiven,
		char *	pStrAdd
	)

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

Synopsis [Appends the string.]

Description [Assumes that the given string (pStrGiven) has been allocated before using malloc(). The additional string has not been allocated. Allocs more root, appends the additional part, frees the old given string.]

SideEffects []

SeeAlso []

Definition at line 690 of file extraUtilFile.c.

{
    char * pTemp;
    if ( pStrGiven )
    {
        pTemp = ABC_ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
        sprintf( pTemp, "%s%s", pStrGiven, pStrAdd );
        ABC_FREE( pStrGiven );
    }
    else
        pTemp = Extra_UtilStrsav( pStrAdd );
    return pTemp;
}

void Extra_StringClean	(	char *	pStrGiven,
		char *	pCharKeep
	)

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

Synopsis [Only keep characters belonging to the second string.]

Description []

SideEffects []

SeeAlso []

Definition at line 715 of file extraUtilFile.c.

{
    char * pTemp, * pChar, * pSave = pStrGiven;
    for ( pTemp = pStrGiven; *pTemp; pTemp++ )
    {
        for ( pChar = pCharKeep; *pChar; pChar++ )
            if ( *pTemp == *pChar )
                break;
        if ( *pChar == 0 )
            continue;
        *pSave++ = *pTemp;
    }
    *pSave = 0;
}

char* Extra_TimeStamp

(

)

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

Synopsis [Returns the time stamp.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 446 of file extraUtilFile.c.

{
    static char Buffer[100];
    char * TimeStamp;
    time_t ltime;
    // get the current time
    time( &ltime );
    TimeStamp = asctime( localtime( &ltime ) );
    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
    strcpy( Buffer, TimeStamp );
    return Buffer;
}

void Extra_Truth4VarN	(	unsigned short **	puCanons,
		char ***	puPhases,
		char **	ppCounters,
		int	nPhasesMax
	)

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

Synopsis [Computes NPN canonical forms for 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 814 of file extraUtilMisc.c.

{
    unsigned short * uCanons;
    unsigned uTruth, uPhase;
    char ** uPhases, * pCounters;
    int nFuncs, nClasses, i;

    nFuncs  = (1 << 16);
    uCanons = ABC_ALLOC( unsigned short, nFuncs );
    memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
    pCounters = ABC_ALLOC( char, nFuncs );
    memset( pCounters, 0, sizeof(char) * nFuncs );
    uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
    nClasses = 0;
    for ( uTruth = 0; uTruth < (unsigned)nFuncs; uTruth++ )
    {
        // skip already assigned
        if ( uCanons[uTruth] )
        {
            assert( uTruth > uCanons[uTruth] );
            continue;
        }
        nClasses++;
        for ( i = 0; i < 16; i++ )
        {
            uPhase = Extra_TruthPolarize( uTruth, i, 4 );
            if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
            {
                uCanons[uPhase]    = uTruth;
                uPhases[uPhase][0] = i;
                pCounters[uPhase]  = 1;
            }
            else
            {
                assert( uCanons[uPhase] == uTruth );
                if ( pCounters[uPhase] < nPhasesMax )
                    uPhases[uPhase][ (int)pCounters[uPhase]++ ] = i;
            }
        }
    }
    if ( puCanons ) 
        *puCanons = uCanons;
    else
        ABC_FREE( uCanons );
    if ( puPhases ) 
        *puPhases = uPhases;
    else
        ABC_FREE( uPhases );
    if ( ppCounters ) 
        *ppCounters = pCounters;
    else
        ABC_FREE( pCounters );
//    printf( "The number of 4N-classes = %d.\n", nClasses );
}

void Extra_Truth4VarNPN	(	unsigned short **	puCanons,
		char **	puPhases,
		char **	puPerms,
		unsigned char **	puMap
	)

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

Synopsis [Computes NPN canonical forms for 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 642 of file extraUtilMisc.c.

{
    unsigned short * uCanons;
    unsigned char * uMap;
    unsigned uTruth, uPhase, uPerm;
    char ** pPerms4, * uPhases, * uPerms;
    int nFuncs, nClasses;
    int i, k;

    nFuncs  = (1 << 16);
    uCanons = ABC_ALLOC( unsigned short, nFuncs );
    uPhases = ABC_ALLOC( char, nFuncs );
    uPerms  = ABC_ALLOC( char, nFuncs );
    uMap    = ABC_ALLOC( unsigned char, nFuncs );
    memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
    memset( uPhases, 0, sizeof(char) * nFuncs );
    memset( uPerms,  0, sizeof(char) * nFuncs );
    memset( uMap,    0, sizeof(unsigned char) * nFuncs );
    pPerms4 = Extra_Permutations( 4 );

    nClasses = 1;
    nFuncs = (1 << 15);
    for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
    {
        // skip already assigned
        if ( uCanons[uTruth] )
        {
            assert( uTruth > uCanons[uTruth] );
            uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
            continue;
        }
        uMap[uTruth] = nClasses++;
        for ( i = 0; i < 16; i++ )
        {
            uPhase = Extra_TruthPolarize( uTruth, i, 4 );
            for ( k = 0; k < 24; k++ )
            {
                uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                if ( uCanons[uPerm] == 0 )
                {
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i;
                    uPerms[uPerm]  = k;

                    uPerm = ~uPerm & 0xFFFF;
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i | 16;
                    uPerms[uPerm]  = k;
                }
                else
                    assert( uCanons[uPerm] == uTruth );
            }
            uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, i, 4 ); 
            for ( k = 0; k < 24; k++ )
            {
                uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                if ( uCanons[uPerm] == 0 )
                {
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i;
                    uPerms[uPerm]  = k;

                    uPerm = ~uPerm & 0xFFFF;
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i | 16;
                    uPerms[uPerm]  = k;
                }
                else
                    assert( uCanons[uPerm] == uTruth );
            }
        }
    }
    uPhases[(1<<16)-1] = 16;
    assert( nClasses == 222 );
    ABC_FREE( pPerms4 );
    if ( puCanons ) 
        *puCanons = uCanons;
    else
        ABC_FREE( uCanons );
    if ( puPhases ) 
        *puPhases = uPhases;
    else
        ABC_FREE( uPhases );
    if ( puPerms ) 
        *puPerms = uPerms;
    else
        ABC_FREE( uPerms );
    if ( puMap ) 
        *puMap = uMap;
    else
        ABC_FREE( uMap );
}

word Extra_Truth6MinimumExact	(	word	t,
		int *	pComp,
		int *	pPerm
	)

Definition at line 2286 of file extraUtilMisc.c.

{
    word tMin = ~(word)0;
    word tCur, tTemp1, tTemp2;
    int i, p, c;
    for ( i = 0; i < 2; i++ )
    {
        tCur = i ? ~t : t;
        tTemp1 = tCur;
        for ( p = 0; p < 720; p++ )
        {
//            printf( "Trying perm %d:\n", p );
//            Kit_DsdPrintFromTruth( &tCur, 6 ), printf( "\n" );;
            tTemp2 = tCur;
            for ( c = 0; c < 64; c++ )
            {
                tMin = Abc_MinWord( tMin, tCur );
                tCur = Extra_Truth6ChangePhase( tCur, pComp[c] );
            }
            assert( tTemp2 == tCur );
            tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] );
        }
        assert( tTemp1 == tCur );
    }
    return tMin;
}

word Extra_Truth6MinimumHeuristic

(

word

t

)

Definition at line 2374 of file extraUtilMisc.c.

{
    word tMin1, tMin2;
    int nOnes = Extra_Truth6Ones( t );
    if ( nOnes < 32 )
        return Extra_Truth6MinimumRoundMany( t );
    if ( nOnes > 32 )
        return Extra_Truth6MinimumRoundMany( ~t );
    tMin1 = Extra_Truth6MinimumRoundMany(  t );
    tMin2 = Extra_Truth6MinimumRoundMany( ~t );
    return Abc_MinWord( tMin1, tMin2 );
}

static void Extra_TruthAnd ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 326 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] & pIn1[w];
}

static void Extra_TruthAndPhase ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars, int  fCompl0, int  fCompl1  )

inlinestatic

Definition at line 350 of file extra.h.

{
    int w;
    if ( fCompl0 && fCompl1 )
    {
        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~(pIn0[w] | pIn1[w]);
    }
    else if ( fCompl0 && !fCompl1 )
    {
        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~pIn0[w] & pIn1[w];
    }
    else if ( !fCompl0 && fCompl1 )
    {
        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] & ~pIn1[w];
    }
    else // if ( !fCompl0 && !fCompl1 )
    {
        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] & pIn1[w];
    }
}

int Extra_TruthCanonFastN	(	int	nVarsMax,
		int	nVarsReal,
		unsigned *	pt,
		unsigned **	pptRes,
		char **	ppfRes
	)

AutomaticEnd Function********************************************************************

Synopsis [Computes the N-canonical form of the Boolean function up to 6 inputs.]

Description [The N-canonical form is defined as the truth table with the minimum integer value. This function exhaustively enumerates through the complete set of 2^N phase assignments. Returns pointers to the static storage to the truth table and phases. This data should be used before the function is called again.]

SideEffects []

SeeAlso []

Definition at line 374 of file extraUtilCanon.c.

{
    static unsigned uTruthStore6[2];
    int RetValue;
    assert( nVarsMax <= 6 );
    assert( nVarsReal <= nVarsMax );
    RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 );
    if ( nVarsMax == 6 && nVarsReal < nVarsMax )
    {
        uTruthStore6[0] = **pptRes;
        uTruthStore6[1] = **pptRes;
        *pptRes = uTruthStore6;
    }
    return RetValue;
}

unsigned Extra_TruthCanonN	(	unsigned	uTruth,
		int	nVars
	)

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

Synopsis [Computes N-canonical form using brute-force methods.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file extraUtilMisc.c.

{
    unsigned uTruthMin, uPhase;
    int nMints, i;
    nMints    = (1 << nVars);
    uTruthMin = 0xFFFFFFFF;
    for ( i = 0; i < nMints; i++ )
    {
        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
        if ( uTruthMin > uPhase )
            uTruthMin = uPhase;
    }
    return uTruthMin;
}

unsigned Extra_TruthCanonNN	(	unsigned	uTruth,
		int	nVars
	)

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

Synopsis [Computes NN-canonical form using brute-force methods.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file extraUtilMisc.c.

{
    unsigned uTruthMin, uTruthC, uPhase;
    int nMints, i;
    nMints    = (1 << nVars);
    uTruthC   = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
    uTruthMin = 0xFFFFFFFF;
    for ( i = 0; i < nMints; i++ )
    {
        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
        if ( uTruthMin > uPhase )
            uTruthMin = uPhase;
        uPhase = Extra_TruthPolarize( uTruthC, i, nVars ); 
        if ( uTruthMin > uPhase )
            uTruthMin = uPhase;
    }
    return uTruthMin;
}

unsigned Extra_TruthCanonNP	(	unsigned	uTruth,
		int	nVars
	)

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

Synopsis [Computes NP-canonical form using brute-force methods.]

Description []

SideEffects []

SeeAlso []

Definition at line 538 of file extraUtilMisc.c.

{
    static int nVarsOld, nPerms;
    static char ** pPerms = NULL;

    unsigned uTruthMin, uPhase, uPerm;
    int nMints, k, i;

    if ( pPerms == NULL )
    {
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }
    else if ( nVarsOld != nVars )
    {
        ABC_FREE( pPerms );
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }

    nMints    = (1 << nVars);
    uTruthMin = 0xFFFFFFFF;
    for ( i = 0; i < nMints; i++ )
    {
        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
        for ( k = 0; k < nPerms; k++ )
        {
            uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
            if ( uTruthMin > uPerm )
                uTruthMin = uPerm;
        }
    }
    return uTruthMin;
}

unsigned Extra_TruthCanonNPN	(	unsigned	uTruth,
		int	nVars
	)

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

Synopsis [Computes NPN-canonical form using brute-force methods.]

Description []

SideEffects []

SeeAlso []

Definition at line 586 of file extraUtilMisc.c.

{
    static int nVarsOld, nPerms;
    static char ** pPerms = NULL;

    unsigned uTruthMin, uTruthC, uPhase, uPerm;
    int nMints, k, i;

    if ( pPerms == NULL )
    {
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }
    else if ( nVarsOld != nVars )
    {
        ABC_FREE( pPerms );
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }

    nMints    = (1 << nVars);
    uTruthC   = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
    uTruthMin = 0xFFFFFFFF;
    for ( i = 0; i < nMints; i++ )
    {
        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
        for ( k = 0; k < nPerms; k++ )
        {
            uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
            if ( uTruthMin > uPerm )
                uTruthMin = uPerm;
        }
        uPhase = Extra_TruthPolarize( uTruthC, i, nVars ); 
        for ( k = 0; k < nPerms; k++ )
        {
            uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
            if ( uTruthMin > uPerm )
                uTruthMin = uPerm;
        }
    }
    return uTruthMin;
}

unsigned Extra_TruthCanonP	(	unsigned	uTruth,
		int	nVars
	)

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

Synopsis [Computes P-canonical form using brute-force methods.]

Description []

SideEffects []

SeeAlso []

Definition at line 495 of file extraUtilMisc.c.

{
    static int nVarsOld, nPerms;
    static char ** pPerms = NULL;

    unsigned uTruthMin, uPerm;
    int k;

    if ( pPerms == NULL )
    {
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }
    else if ( nVarsOld != nVars )
    {
        ABC_FREE( pPerms );
        nPerms = Extra_Factorial( nVars );   
        pPerms = Extra_Permutations( nVars );
        nVarsOld = nVars;
    }

    uTruthMin = 0xFFFFFFFF;
    for ( k = 0; k < nPerms; k++ )
    {
        uPerm = Extra_TruthPermute( uTruth, pPerms[k], nVars, 0 );
        if ( uTruthMin > uPerm )
            uTruthMin = uPerm;
    }
    return uTruthMin;
}

void Extra_TruthChangePhase	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Changes phase of the function w.r.t. one variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 719 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;
    unsigned Temp;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                Temp = pTruth[i];
                pTruth[i] = pTruth[Step+i];
                pTruth[Step+i] = Temp;
            }
            pTruth += 2*Step;
        }
        return;
    }
}

static void Extra_TruthClear ( unsigned *  pOut, int  nVars  )

inlinestatic

Definition at line 308 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = 0;
}

void Extra_TruthCofactor0	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pTruth[Step+i] = pTruth[i];
            pTruth += 2*Step;
        }
        return;
    }
}

void Extra_TruthCofactor1	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pTruth[i] = pTruth[Step+i];
            pTruth += 2*Step;
        }
        return;
    }
}

static void Extra_TruthCopy ( unsigned *  pOut, unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 302 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn[w];
}

static int Extra_TruthCountOnes ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 263 of file extra.h.

{
    int w, Counter = 0;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        Counter += Extra_WordCountOnes(pIn[w]);
    return Counter;
}

void Extra_TruthCountOnesInCofs	(	unsigned *	pTruth,
		int	nVars,
		short *	pStore
	)

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

Synopsis [Counts the number of 1's in each cofactor.]

Description [The resulting numbers are stored in the array of shorts, whose length is 2*nVars. The number of 1's is counted in a different space than the original function. For example, if the function depends on k variables, the cofactors are assumed to depend on k-1 variables.]

SideEffects []

SeeAlso []

Definition at line 828 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Counter;
    memset( pStore, 0, sizeof(short) * 2 * nVars );
    if ( nVars <= 5 )
    {
        if ( nVars > 0 )
        {
            pStore[2*0+0] = Extra_WordCountOnes( pTruth[0] & 0x55555555 );
            pStore[2*0+1] = Extra_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
        }
        if ( nVars > 1 )
        {
            pStore[2*1+0] = Extra_WordCountOnes( pTruth[0] & 0x33333333 );
            pStore[2*1+1] = Extra_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
        }
        if ( nVars > 2 )
        {
            pStore[2*2+0] = Extra_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
            pStore[2*2+1] = Extra_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
        }
        if ( nVars > 3 )
        {
            pStore[2*3+0] = Extra_WordCountOnes( pTruth[0] & 0x00FF00FF );
            pStore[2*3+1] = Extra_WordCountOnes( pTruth[0] & 0xFF00FF00 );
        }
        if ( nVars > 4 )
        {
            pStore[2*4+0] = Extra_WordCountOnes( pTruth[0] & 0x0000FFFF );
            pStore[2*4+1] = Extra_WordCountOnes( pTruth[0] & 0xFFFF0000 );
        }
        return;
    }
    // nVars >= 6
    // count 1's for all other variables
    for ( k = 0; k < nWords; k++ )
    {
        Counter = Extra_WordCountOnes( pTruth[k] );
        for ( i = 5; i < nVars; i++ )
            if ( k & (1 << (i-5)) )
                pStore[2*i+1] += Counter;
            else
                pStore[2*i+0] += Counter;
    }
    // count 1's for the first five variables
    for ( k = 0; k < nWords/2; k++ )
    {
        pStore[2*0+0] += Extra_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
        pStore[2*0+1] += Extra_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >>  1) );
        pStore[2*1+0] += Extra_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
        pStore[2*1+1] += Extra_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >>  2) );
        pStore[2*2+0] += Extra_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
        pStore[2*2+1] += Extra_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >>  4) );
        pStore[2*3+0] += Extra_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
        pStore[2*3+1] += Extra_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >>  8) );
        pStore[2*4+0] += Extra_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
        pStore[2*4+1] += Extra_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
        pTruth += 2;
    }
}

unsigned** Extra_TruthElementary

(

int

nVars

)

AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Derive elementary truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file extraUtilTruth.c.

{
    unsigned ** pRes;
    int i, k, nWords;
    nWords = Extra_TruthWordNum(nVars);
    pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 );
    for ( i = 0; i < nVars; i++ )
    {
        if ( i < 5 )
        {
            for ( k = 0; k < nWords; k++ )
                pRes[i][k] = s_VarMasks[i][1];
        }
        else
        {
            for ( k = 0; k < nWords; k++ )
                if ( k & (1 << (i-5)) )
                    pRes[i][k] = ~(unsigned)0;
                else
                    pRes[i][k] = 0;
        }
    }
    return pRes;
}

void Extra_TruthExist	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pTruth[i]     |= pTruth[Step+i];
                pTruth[Step+i] = pTruth[i];
            }
            pTruth += 2*Step;
        }
        return;
    }
}

void Extra_TruthExpand	(	int	nVars,
		int	nWords,
		unsigned *	puTruth,
		unsigned	uPhase,
		unsigned *	puTruthR
	)

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

Synopsis [Computes a phase of the 8-var function.]

Description []

SideEffects []

SeeAlso []

Definition at line 1279 of file extraUtilMisc.c.

{
    // elementary truth tables
    static unsigned uTruths[8][8] = {
        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
    };
    static char Cases[256] = {
         0, // 00000000
         0, // 00000001
         1, // 00000010
         0, // 00000011
         2, // 00000100
        -1, // 00000101
        -1, // 00000110
         0, // 00000111
         3, // 00001000
        -1, // 00001001
        -1, // 00001010
        -1, // 00001011
        -1, // 00001100
        -1, // 00001101
        -1, // 00001110
         0, // 00001111
         4, // 00010000
        -1, // 00010001
        -1, // 00010010
        -1, // 00010011
        -1, // 00010100
        -1, // 00010101
        -1, // 00010110
        -1, // 00010111
        -1, // 00011000
        -1, // 00011001
        -1, // 00011010
        -1, // 00011011
        -1, // 00011100
        -1, // 00011101
        -1, // 00011110
         0, // 00011111
         5, // 00100000
        -1, // 00100001
        -1, // 00100010
        -1, // 00100011
        -1, // 00100100
        -1, // 00100101
        -1, // 00100110
        -1, // 00100111
        -1, // 00101000
        -1, // 00101001
        -1, // 00101010
        -1, // 00101011
        -1, // 00101100
        -1, // 00101101
        -1, // 00101110
        -1, // 00101111
        -1, // 00110000
        -1, // 00110001
        -1, // 00110010
        -1, // 00110011
        -1, // 00110100
        -1, // 00110101
        -1, // 00110110
        -1, // 00110111
        -1, // 00111000
        -1, // 00111001
        -1, // 00111010
        -1, // 00111011
        -1, // 00111100
        -1, // 00111101
        -1, // 00111110
         0, // 00111111
         6, // 01000000
        -1, // 01000001
        -1, // 01000010
        -1, // 01000011
        -1, // 01000100
        -1, // 01000101
        -1, // 01000110
        -1, // 01000111
        -1, // 01001000
        -1, // 01001001
        -1, // 01001010
        -1, // 01001011
        -1, // 01001100
        -1, // 01001101
        -1, // 01001110
        -1, // 01001111
        -1, // 01010000
        -1, // 01010001
        -1, // 01010010
        -1, // 01010011
        -1, // 01010100
        -1, // 01010101
        -1, // 01010110
        -1, // 01010111
        -1, // 01011000
        -1, // 01011001
        -1, // 01011010
        -1, // 01011011
        -1, // 01011100
        -1, // 01011101
        -1, // 01011110
        -1, // 01011111
        -1, // 01100000
        -1, // 01100001
        -1, // 01100010
        -1, // 01100011
        -1, // 01100100
        -1, // 01100101
        -1, // 01100110
        -1, // 01100111
        -1, // 01101000
        -1, // 01101001
        -1, // 01101010
        -1, // 01101011
        -1, // 01101100
        -1, // 01101101
        -1, // 01101110
        -1, // 01101111
        -1, // 01110000
        -1, // 01110001
        -1, // 01110010
        -1, // 01110011
        -1, // 01110100
        -1, // 01110101
        -1, // 01110110
        -1, // 01110111
        -1, // 01111000
        -1, // 01111001
        -1, // 01111010
        -1, // 01111011
        -1, // 01111100
        -1, // 01111101
        -1, // 01111110
         0, // 01111111
         7, // 10000000
        -1, // 10000001
        -1, // 10000010
        -1, // 10000011
        -1, // 10000100
        -1, // 10000101
        -1, // 10000110
        -1, // 10000111
        -1, // 10001000
        -1, // 10001001
        -1, // 10001010
        -1, // 10001011
        -1, // 10001100
        -1, // 10001101
        -1, // 10001110
        -1, // 10001111
        -1, // 10010000
        -1, // 10010001
        -1, // 10010010
        -1, // 10010011
        -1, // 10010100
        -1, // 10010101
        -1, // 10010110
        -1, // 10010111
        -1, // 10011000
        -1, // 10011001
        -1, // 10011010
        -1, // 10011011
        -1, // 10011100
        -1, // 10011101
        -1, // 10011110
        -1, // 10011111
        -1, // 10100000
        -1, // 10100001
        -1, // 10100010
        -1, // 10100011
        -1, // 10100100
        -1, // 10100101
        -1, // 10100110
        -1, // 10100111
        -1, // 10101000
        -1, // 10101001
        -1, // 10101010
        -1, // 10101011
        -1, // 10101100
        -1, // 10101101
        -1, // 10101110
        -1, // 10101111
        -1, // 10110000
        -1, // 10110001
        -1, // 10110010
        -1, // 10110011
        -1, // 10110100
        -1, // 10110101
        -1, // 10110110
        -1, // 10110111
        -1, // 10111000
        -1, // 10111001
        -1, // 10111010
        -1, // 10111011
        -1, // 10111100
        -1, // 10111101
        -1, // 10111110
        -1, // 10111111
        -1, // 11000000
        -1, // 11000001
        -1, // 11000010
        -1, // 11000011
        -1, // 11000100
        -1, // 11000101
        -1, // 11000110
        -1, // 11000111
        -1, // 11001000
        -1, // 11001001
        -1, // 11001010
        -1, // 11001011
        -1, // 11001100
        -1, // 11001101
        -1, // 11001110
        -1, // 11001111
        -1, // 11010000
        -1, // 11010001
        -1, // 11010010
        -1, // 11010011
        -1, // 11010100
        -1, // 11010101
        -1, // 11010110
        -1, // 11010111
        -1, // 11011000
        -1, // 11011001
        -1, // 11011010
        -1, // 11011011
        -1, // 11011100
        -1, // 11011101
        -1, // 11011110
        -1, // 11011111
        -1, // 11100000
        -1, // 11100001
        -1, // 11100010
        -1, // 11100011
        -1, // 11100100
        -1, // 11100101
        -1, // 11100110
        -1, // 11100111
        -1, // 11101000
        -1, // 11101001
        -1, // 11101010
        -1, // 11101011
        -1, // 11101100
        -1, // 11101101
        -1, // 11101110
        -1, // 11101111
        -1, // 11110000
        -1, // 11110001
        -1, // 11110010
        -1, // 11110011
        -1, // 11110100
        -1, // 11110101
        -1, // 11110110
        -1, // 11110111
        -1, // 11111000
        -1, // 11111001
        -1, // 11111010
        -1, // 11111011
        -1, // 11111100
        -1, // 11111101
        -1, // 11111110
         0  // 11111111
    };
    static char Perms[256][8] = {
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000000
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000001
        { 1, 0, 2, 3, 4, 5, 6, 7 }, // 00000010
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000011
        { 1, 2, 0, 3, 4, 5, 6, 7 }, // 00000100
        { 0, 2, 1, 3, 4, 5, 6, 7 }, // 00000101
        { 2, 0, 1, 3, 4, 5, 6, 7 }, // 00000110
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000111
        { 1, 2, 3, 0, 4, 5, 6, 7 }, // 00001000
        { 0, 2, 3, 1, 4, 5, 6, 7 }, // 00001001
        { 2, 0, 3, 1, 4, 5, 6, 7 }, // 00001010
        { 0, 1, 3, 2, 4, 5, 6, 7 }, // 00001011
        { 2, 3, 0, 1, 4, 5, 6, 7 }, // 00001100
        { 0, 3, 1, 2, 4, 5, 6, 7 }, // 00001101
        { 3, 0, 1, 2, 4, 5, 6, 7 }, // 00001110
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00001111
        { 1, 2, 3, 4, 0, 5, 6, 7 }, // 00010000
        { 0, 2, 3, 4, 1, 5, 6, 7 }, // 00010001
        { 2, 0, 3, 4, 1, 5, 6, 7 }, // 00010010
        { 0, 1, 3, 4, 2, 5, 6, 7 }, // 00010011
        { 2, 3, 0, 4, 1, 5, 6, 7 }, // 00010100
        { 0, 3, 1, 4, 2, 5, 6, 7 }, // 00010101
        { 3, 0, 1, 4, 2, 5, 6, 7 }, // 00010110
        { 0, 1, 2, 4, 3, 5, 6, 7 }, // 00010111
        { 2, 3, 4, 0, 1, 5, 6, 7 }, // 00011000
        { 0, 3, 4, 1, 2, 5, 6, 7 }, // 00011001
        { 3, 0, 4, 1, 2, 5, 6, 7 }, // 00011010
        { 0, 1, 4, 2, 3, 5, 6, 7 }, // 00011011
        { 3, 4, 0, 1, 2, 5, 6, 7 }, // 00011100
        { 0, 4, 1, 2, 3, 5, 6, 7 }, // 00011101
        { 4, 0, 1, 2, 3, 5, 6, 7 }, // 00011110
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00011111
        { 1, 2, 3, 4, 5, 0, 6, 7 }, // 00100000
        { 0, 2, 3, 4, 5, 1, 6, 7 }, // 00100001
        { 2, 0, 3, 4, 5, 1, 6, 7 }, // 00100010
        { 0, 1, 3, 4, 5, 2, 6, 7 }, // 00100011
        { 2, 3, 0, 4, 5, 1, 6, 7 }, // 00100100
        { 0, 3, 1, 4, 5, 2, 6, 7 }, // 00100101
        { 3, 0, 1, 4, 5, 2, 6, 7 }, // 00100110
        { 0, 1, 2, 4, 5, 3, 6, 7 }, // 00100111
        { 2, 3, 4, 0, 5, 1, 6, 7 }, // 00101000
        { 0, 3, 4, 1, 5, 2, 6, 7 }, // 00101001
        { 3, 0, 4, 1, 5, 2, 6, 7 }, // 00101010
        { 0, 1, 4, 2, 5, 3, 6, 7 }, // 00101011
        { 3, 4, 0, 1, 5, 2, 6, 7 }, // 00101100
        { 0, 4, 1, 2, 5, 3, 6, 7 }, // 00101101
        { 4, 0, 1, 2, 5, 3, 6, 7 }, // 00101110
        { 0, 1, 2, 3, 5, 4, 6, 7 }, // 00101111
        { 2, 3, 4, 5, 0, 1, 6, 7 }, // 00110000
        { 0, 3, 4, 5, 1, 2, 6, 7 }, // 00110001
        { 3, 0, 4, 5, 1, 2, 6, 7 }, // 00110010
        { 0, 1, 4, 5, 2, 3, 6, 7 }, // 00110011
        { 3, 4, 0, 5, 1, 2, 6, 7 }, // 00110100
        { 0, 4, 1, 5, 2, 3, 6, 7 }, // 00110101
        { 4, 0, 1, 5, 2, 3, 6, 7 }, // 00110110
        { 0, 1, 2, 5, 3, 4, 6, 7 }, // 00110111
        { 3, 4, 5, 0, 1, 2, 6, 7 }, // 00111000
        { 0, 4, 5, 1, 2, 3, 6, 7 }, // 00111001
        { 4, 0, 5, 1, 2, 3, 6, 7 }, // 00111010
        { 0, 1, 5, 2, 3, 4, 6, 7 }, // 00111011
        { 4, 5, 0, 1, 2, 3, 6, 7 }, // 00111100
        { 0, 5, 1, 2, 3, 4, 6, 7 }, // 00111101
        { 5, 0, 1, 2, 3, 4, 6, 7 }, // 00111110
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00111111
        { 1, 2, 3, 4, 5, 6, 0, 7 }, // 01000000
        { 0, 2, 3, 4, 5, 6, 1, 7 }, // 01000001
        { 2, 0, 3, 4, 5, 6, 1, 7 }, // 01000010
        { 0, 1, 3, 4, 5, 6, 2, 7 }, // 01000011
        { 2, 3, 0, 4, 5, 6, 1, 7 }, // 01000100
        { 0, 3, 1, 4, 5, 6, 2, 7 }, // 01000101
        { 3, 0, 1, 4, 5, 6, 2, 7 }, // 01000110
        { 0, 1, 2, 4, 5, 6, 3, 7 }, // 01000111
        { 2, 3, 4, 0, 5, 6, 1, 7 }, // 01001000
        { 0, 3, 4, 1, 5, 6, 2, 7 }, // 01001001
        { 3, 0, 4, 1, 5, 6, 2, 7 }, // 01001010
        { 0, 1, 4, 2, 5, 6, 3, 7 }, // 01001011
        { 3, 4, 0, 1, 5, 6, 2, 7 }, // 01001100
        { 0, 4, 1, 2, 5, 6, 3, 7 }, // 01001101
        { 4, 0, 1, 2, 5, 6, 3, 7 }, // 01001110
        { 0, 1, 2, 3, 5, 6, 4, 7 }, // 01001111
        { 2, 3, 4, 5, 0, 6, 1, 7 }, // 01010000
        { 0, 3, 4, 5, 1, 6, 2, 7 }, // 01010001
        { 3, 0, 4, 5, 1, 6, 2, 7 }, // 01010010
        { 0, 1, 4, 5, 2, 6, 3, 7 }, // 01010011
        { 3, 4, 0, 5, 1, 6, 2, 7 }, // 01010100
        { 0, 4, 1, 5, 2, 6, 3, 7 }, // 01010101
        { 4, 0, 1, 5, 2, 6, 3, 7 }, // 01010110
        { 0, 1, 2, 5, 3, 6, 4, 7 }, // 01010111
        { 3, 4, 5, 0, 1, 6, 2, 7 }, // 01011000
        { 0, 4, 5, 1, 2, 6, 3, 7 }, // 01011001
        { 4, 0, 5, 1, 2, 6, 3, 7 }, // 01011010
        { 0, 1, 5, 2, 3, 6, 4, 7 }, // 01011011
        { 4, 5, 0, 1, 2, 6, 3, 7 }, // 01011100
        { 0, 5, 1, 2, 3, 6, 4, 7 }, // 01011101
        { 5, 0, 1, 2, 3, 6, 4, 7 }, // 01011110
        { 0, 1, 2, 3, 4, 6, 5, 7 }, // 01011111
        { 2, 3, 4, 5, 6, 0, 1, 7 }, // 01100000
        { 0, 3, 4, 5, 6, 1, 2, 7 }, // 01100001
        { 3, 0, 4, 5, 6, 1, 2, 7 }, // 01100010
        { 0, 1, 4, 5, 6, 2, 3, 7 }, // 01100011
        { 3, 4, 0, 5, 6, 1, 2, 7 }, // 01100100
        { 0, 4, 1, 5, 6, 2, 3, 7 }, // 01100101
        { 4, 0, 1, 5, 6, 2, 3, 7 }, // 01100110
        { 0, 1, 2, 5, 6, 3, 4, 7 }, // 01100111
        { 3, 4, 5, 0, 6, 1, 2, 7 }, // 01101000
        { 0, 4, 5, 1, 6, 2, 3, 7 }, // 01101001
        { 4, 0, 5, 1, 6, 2, 3, 7 }, // 01101010
        { 0, 1, 5, 2, 6, 3, 4, 7 }, // 01101011
        { 4, 5, 0, 1, 6, 2, 3, 7 }, // 01101100
        { 0, 5, 1, 2, 6, 3, 4, 7 }, // 01101101
        { 5, 0, 1, 2, 6, 3, 4, 7 }, // 01101110
        { 0, 1, 2, 3, 6, 4, 5, 7 }, // 01101111
        { 3, 4, 5, 6, 0, 1, 2, 7 }, // 01110000
        { 0, 4, 5, 6, 1, 2, 3, 7 }, // 01110001
        { 4, 0, 5, 6, 1, 2, 3, 7 }, // 01110010
        { 0, 1, 5, 6, 2, 3, 4, 7 }, // 01110011
        { 4, 5, 0, 6, 1, 2, 3, 7 }, // 01110100
        { 0, 5, 1, 6, 2, 3, 4, 7 }, // 01110101
        { 5, 0, 1, 6, 2, 3, 4, 7 }, // 01110110
        { 0, 1, 2, 6, 3, 4, 5, 7 }, // 01110111
        { 4, 5, 6, 0, 1, 2, 3, 7 }, // 01111000
        { 0, 5, 6, 1, 2, 3, 4, 7 }, // 01111001
        { 5, 0, 6, 1, 2, 3, 4, 7 }, // 01111010
        { 0, 1, 6, 2, 3, 4, 5, 7 }, // 01111011
        { 5, 6, 0, 1, 2, 3, 4, 7 }, // 01111100
        { 0, 6, 1, 2, 3, 4, 5, 7 }, // 01111101
        { 6, 0, 1, 2, 3, 4, 5, 7 }, // 01111110
        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 01111111
        { 1, 2, 3, 4, 5, 6, 7, 0 }, // 10000000
        { 0, 2, 3, 4, 5, 6, 7, 1 }, // 10000001
        { 2, 0, 3, 4, 5, 6, 7, 1 }, // 10000010
        { 0, 1, 3, 4, 5, 6, 7, 2 }, // 10000011
        { 2, 3, 0, 4, 5, 6, 7, 1 }, // 10000100
        { 0, 3, 1, 4, 5, 6, 7, 2 }, // 10000101
        { 3, 0, 1, 4, 5, 6, 7, 2 }, // 10000110
        { 0, 1, 2, 4, 5, 6, 7, 3 }, // 10000111
        { 2, 3, 4, 0, 5, 6, 7, 1 }, // 10001000
        { 0, 3, 4, 1, 5, 6, 7, 2 }, // 10001001
        { 3, 0, 4, 1, 5, 6, 7, 2 }, // 10001010
        { 0, 1, 4, 2, 5, 6, 7, 3 }, // 10001011
        { 3, 4, 0, 1, 5, 6, 7, 2 }, // 10001100
        { 0, 4, 1, 2, 5, 6, 7, 3 }, // 10001101
        { 4, 0, 1, 2, 5, 6, 7, 3 }, // 10001110
        { 0, 1, 2, 3, 5, 6, 7, 4 }, // 10001111
        { 2, 3, 4, 5, 0, 6, 7, 1 }, // 10010000
        { 0, 3, 4, 5, 1, 6, 7, 2 }, // 10010001
        { 3, 0, 4, 5, 1, 6, 7, 2 }, // 10010010
        { 0, 1, 4, 5, 2, 6, 7, 3 }, // 10010011
        { 3, 4, 0, 5, 1, 6, 7, 2 }, // 10010100
        { 0, 4, 1, 5, 2, 6, 7, 3 }, // 10010101
        { 4, 0, 1, 5, 2, 6, 7, 3 }, // 10010110
        { 0, 1, 2, 5, 3, 6, 7, 4 }, // 10010111
        { 3, 4, 5, 0, 1, 6, 7, 2 }, // 10011000
        { 0, 4, 5, 1, 2, 6, 7, 3 }, // 10011001
        { 4, 0, 5, 1, 2, 6, 7, 3 }, // 10011010
        { 0, 1, 5, 2, 3, 6, 7, 4 }, // 10011011
        { 4, 5, 0, 1, 2, 6, 7, 3 }, // 10011100
        { 0, 5, 1, 2, 3, 6, 7, 4 }, // 10011101
        { 5, 0, 1, 2, 3, 6, 7, 4 }, // 10011110
        { 0, 1, 2, 3, 4, 6, 7, 5 }, // 10011111
        { 2, 3, 4, 5, 6, 0, 7, 1 }, // 10100000
        { 0, 3, 4, 5, 6, 1, 7, 2 }, // 10100001
        { 3, 0, 4, 5, 6, 1, 7, 2 }, // 10100010
        { 0, 1, 4, 5, 6, 2, 7, 3 }, // 10100011
        { 3, 4, 0, 5, 6, 1, 7, 2 }, // 10100100
        { 0, 4, 1, 5, 6, 2, 7, 3 }, // 10100101
        { 4, 0, 1, 5, 6, 2, 7, 3 }, // 10100110
        { 0, 1, 2, 5, 6, 3, 7, 4 }, // 10100111
        { 3, 4, 5, 0, 6, 1, 7, 2 }, // 10101000
        { 0, 4, 5, 1, 6, 2, 7, 3 }, // 10101001
        { 4, 0, 5, 1, 6, 2, 7, 3 }, // 10101010
        { 0, 1, 5, 2, 6, 3, 7, 4 }, // 10101011
        { 4, 5, 0, 1, 6, 2, 7, 3 }, // 10101100
        { 0, 5, 1, 2, 6, 3, 7, 4 }, // 10101101
        { 5, 0, 1, 2, 6, 3, 7, 4 }, // 10101110
        { 0, 1, 2, 3, 6, 4, 7, 5 }, // 10101111
        { 3, 4, 5, 6, 0, 1, 7, 2 }, // 10110000
        { 0, 4, 5, 6, 1, 2, 7, 3 }, // 10110001
        { 4, 0, 5, 6, 1, 2, 7, 3 }, // 10110010
        { 0, 1, 5, 6, 2, 3, 7, 4 }, // 10110011
        { 4, 5, 0, 6, 1, 2, 7, 3 }, // 10110100
        { 0, 5, 1, 6, 2, 3, 7, 4 }, // 10110101
        { 5, 0, 1, 6, 2, 3, 7, 4 }, // 10110110
        { 0, 1, 2, 6, 3, 4, 7, 5 }, // 10110111
        { 4, 5, 6, 0, 1, 2, 7, 3 }, // 10111000
        { 0, 5, 6, 1, 2, 3, 7, 4 }, // 10111001
        { 5, 0, 6, 1, 2, 3, 7, 4 }, // 10111010
        { 0, 1, 6, 2, 3, 4, 7, 5 }, // 10111011
        { 5, 6, 0, 1, 2, 3, 7, 4 }, // 10111100
        { 0, 6, 1, 2, 3, 4, 7, 5 }, // 10111101
        { 6, 0, 1, 2, 3, 4, 7, 5 }, // 10111110
        { 0, 1, 2, 3, 4, 5, 7, 6 }, // 10111111
        { 2, 3, 4, 5, 6, 7, 0, 1 }, // 11000000
        { 0, 3, 4, 5, 6, 7, 1, 2 }, // 11000001
        { 3, 0, 4, 5, 6, 7, 1, 2 }, // 11000010
        { 0, 1, 4, 5, 6, 7, 2, 3 }, // 11000011
        { 3, 4, 0, 5, 6, 7, 1, 2 }, // 11000100
        { 0, 4, 1, 5, 6, 7, 2, 3 }, // 11000101
        { 4, 0, 1, 5, 6, 7, 2, 3 }, // 11000110
        { 0, 1, 2, 5, 6, 7, 3, 4 }, // 11000111
        { 3, 4, 5, 0, 6, 7, 1, 2 }, // 11001000
        { 0, 4, 5, 1, 6, 7, 2, 3 }, // 11001001
        { 4, 0, 5, 1, 6, 7, 2, 3 }, // 11001010
        { 0, 1, 5, 2, 6, 7, 3, 4 }, // 11001011
        { 4, 5, 0, 1, 6, 7, 2, 3 }, // 11001100
        { 0, 5, 1, 2, 6, 7, 3, 4 }, // 11001101
        { 5, 0, 1, 2, 6, 7, 3, 4 }, // 11001110
        { 0, 1, 2, 3, 6, 7, 4, 5 }, // 11001111
        { 3, 4, 5, 6, 0, 7, 1, 2 }, // 11010000
        { 0, 4, 5, 6, 1, 7, 2, 3 }, // 11010001
        { 4, 0, 5, 6, 1, 7, 2, 3 }, // 11010010
        { 0, 1, 5, 6, 2, 7, 3, 4 }, // 11010011
        { 4, 5, 0, 6, 1, 7, 2, 3 }, // 11010100
        { 0, 5, 1, 6, 2, 7, 3, 4 }, // 11010101
        { 5, 0, 1, 6, 2, 7, 3, 4 }, // 11010110
        { 0, 1, 2, 6, 3, 7, 4, 5 }, // 11010111
        { 4, 5, 6, 0, 1, 7, 2, 3 }, // 11011000
        { 0, 5, 6, 1, 2, 7, 3, 4 }, // 11011001
        { 5, 0, 6, 1, 2, 7, 3, 4 }, // 11011010
        { 0, 1, 6, 2, 3, 7, 4, 5 }, // 11011011
        { 5, 6, 0, 1, 2, 7, 3, 4 }, // 11011100
        { 0, 6, 1, 2, 3, 7, 4, 5 }, // 11011101
        { 6, 0, 1, 2, 3, 7, 4, 5 }, // 11011110
        { 0, 1, 2, 3, 4, 7, 5, 6 }, // 11011111
        { 3, 4, 5, 6, 7, 0, 1, 2 }, // 11100000
        { 0, 4, 5, 6, 7, 1, 2, 3 }, // 11100001
        { 4, 0, 5, 6, 7, 1, 2, 3 }, // 11100010
        { 0, 1, 5, 6, 7, 2, 3, 4 }, // 11100011
        { 4, 5, 0, 6, 7, 1, 2, 3 }, // 11100100
        { 0, 5, 1, 6, 7, 2, 3, 4 }, // 11100101
        { 5, 0, 1, 6, 7, 2, 3, 4 }, // 11100110
        { 0, 1, 2, 6, 7, 3, 4, 5 }, // 11100111
        { 4, 5, 6, 0, 7, 1, 2, 3 }, // 11101000
        { 0, 5, 6, 1, 7, 2, 3, 4 }, // 11101001
        { 5, 0, 6, 1, 7, 2, 3, 4 }, // 11101010
        { 0, 1, 6, 2, 7, 3, 4, 5 }, // 11101011
        { 5, 6, 0, 1, 7, 2, 3, 4 }, // 11101100
        { 0, 6, 1, 2, 7, 3, 4, 5 }, // 11101101
        { 6, 0, 1, 2, 7, 3, 4, 5 }, // 11101110
        { 0, 1, 2, 3, 7, 4, 5, 6 }, // 11101111
        { 4, 5, 6, 7, 0, 1, 2, 3 }, // 11110000
        { 0, 5, 6, 7, 1, 2, 3, 4 }, // 11110001
        { 5, 0, 6, 7, 1, 2, 3, 4 }, // 11110010
        { 0, 1, 6, 7, 2, 3, 4, 5 }, // 11110011
        { 5, 6, 0, 7, 1, 2, 3, 4 }, // 11110100
        { 0, 6, 1, 7, 2, 3, 4, 5 }, // 11110101
        { 6, 0, 1, 7, 2, 3, 4, 5 }, // 11110110
        { 0, 1, 2, 7, 3, 4, 5, 6 }, // 11110111
        { 5, 6, 7, 0, 1, 2, 3, 4 }, // 11111000
        { 0, 6, 7, 1, 2, 3, 4, 5 }, // 11111001
        { 6, 0, 7, 1, 2, 3, 4, 5 }, // 11111010
        { 0, 1, 7, 2, 3, 4, 5, 6 }, // 11111011
        { 6, 7, 0, 1, 2, 3, 4, 5 }, // 11111100
        { 0, 7, 1, 2, 3, 4, 5, 6 }, // 11111101
        { 7, 0, 1, 2, 3, 4, 5, 6 }, // 11111110
        { 0, 1, 2, 3, 4, 5, 6, 7 }  // 11111111
    };

    assert( uPhase > 0 && uPhase < (unsigned)(1 << nVars) );

    // the same function
    if ( Cases[uPhase] == 0 )
    {
        int i;
        for ( i = 0; i < nWords; i++ )
            puTruthR[i] = puTruth[i];
        return;
    }

    // an elementary variable
    if ( Cases[uPhase] > 0 )
    {
        int i;
        for ( i = 0; i < nWords; i++ )
            puTruthR[i] = uTruths[(int)Cases[uPhase]][i];
        return;
    }

    // truth table takes one word
    if ( nWords == 1 )
    {
        int i, k, nMints, iRes;
        char * pPerm = Perms[uPhase];
        puTruthR[0] = 0;
        nMints = (1 << nVars);
        for ( i = 0; i < nMints; i++ )
            if ( puTruth[0] & (1 << i) )
            {
                for ( iRes = 0, k = 0; k < nVars; k++ )
                    if ( i & (1 << pPerm[k]) )
                        iRes |= (1 << k);
                puTruthR[0] |= (1 << iRes);
            }
        return;
    }
    else if ( nWords == 2 )
    {
        int i, k, iRes;
        char * pPerm = Perms[uPhase];
        puTruthR[0] = puTruthR[1] = 0;
        for ( i = 0; i < 32; i++ )
        {
            if ( puTruth[0] & (1 << i) )
            {
                for ( iRes = 0, k = 0; k < 6; k++ )
                    if ( i & (1 << pPerm[k]) )
                        iRes |= (1 << k);
                if ( iRes < 32 )
                    puTruthR[0] |= (1 << iRes);
                else
                    puTruthR[1] |= (1 << (iRes-32));
            }
        }
        for ( ; i < 64; i++ )
        {
            if ( puTruth[1] & (1 << (i-32)) )
            {
                for ( iRes = 0, k = 0; k < 6; k++ )
                    if ( i & (1 << pPerm[k]) )
                        iRes |= (1 << k);
                if ( iRes < 32 )
                    puTruthR[0] |= (1 << iRes);
                else
                    puTruthR[1] |= (1 << (iRes-32));
            }
        }
    }
    // truth table takes more than one word
    else
    {
        int i, k, nMints, iRes;
        char * pPerm = Perms[uPhase];
        for ( i = 0; i < nWords; i++ )
            puTruthR[i] = 0;
        nMints = (1 << nVars);
        for ( i = 0; i < nMints; i++ )
            if ( puTruth[i>>5] & (1 << (i&31)) )
            {
                for ( iRes = 0, k = 0; k < 5; k++ )
                    if ( i & (1 << pPerm[k]) )
                        iRes |= (1 << k);
                puTruthR[iRes>>5] |= (1 << (iRes&31));
            }
    }
}

static void Extra_TruthFill ( unsigned *  pOut, int  nVars  )

inlinestatic

Definition at line 314 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~(unsigned)0;
}

void Extra_TruthForall	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 556 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pTruth[i]     &= pTruth[Step+i];
                pTruth[Step+i] = pTruth[i];
            }
            pTruth += 2*Step;
        }
        return;
    }
}

static int Extra_TruthHasBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 253 of file extra.h.

{ return (p[Bit>>5] & (1<<(Bit & 31))) > 0;   }

unsigned Extra_TruthHash	(	unsigned *	pIn,
		int	nWords
	)

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 902 of file extraUtilTruth.c.

{
    // The 1,024 smallest prime numbers used to compute the hash value
    // http://www.math.utah.edu/~alfeld/math/primelist.html
    static int HashPrimes[1024] = { 2, 3, 5, 
    7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
    101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, 
    193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, 
    293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, 
    409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, 
    521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, 
    641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, 
    757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, 
    881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, 
    1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091, 
    1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193, 
    1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291, 
    1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 
    1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 
    1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, 
    1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699, 
    1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811, 
    1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931, 
    1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029, 
    2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137, 
    2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267, 
    2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357, 
    2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459, 
    2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593, 
    2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693, 
    2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791, 
    2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903, 
    2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023, 
    3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167, 
    3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271, 
    3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373, 
    3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511, 
    3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607, 
    3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709, 
    3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833, 
    3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931, 
    3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057, 
    4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177, 
    4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283, 
    4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423, 
    4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547, 
    4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657, 
    4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789, 
    4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931, 
    4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011, 
    5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147, 
    5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279, 
    5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413, 
    5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507, 
    5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647, 
    5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743, 
    5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857, 
    5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007, 
    6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121, 
    6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247, 
    6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343, 
    6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473, 
    6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607, 
    6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733, 
    6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857, 
    6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971, 
    6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103, 
    7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229, 
    7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369, 
    7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517, 
    7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
    7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
    7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
    7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
    8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
    8147, 8161 };
    int i;
    unsigned uHashKey;
    assert( nWords <= 1024 );
    uHashKey = 0;
    for ( i = 0; i < nWords; i++ )
        uHashKey ^= HashPrimes[i] * pIn[i];
    return uHashKey;
}

static int Extra_TruthIsConst0 ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 278 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn[w] )
            return 0;
    return 1;
}

static int Extra_TruthIsConst1 ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 286 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn[w] != ~(unsigned)0 )
            return 0;
    return 1;
}

static int Extra_TruthIsEqual ( unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 270 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn0[w] != pIn1[w] )
            return 0;
    return 1;
}

static int Extra_TruthIsImply ( unsigned *  pIn1, unsigned *  pIn2, int  nVars  )

inlinestatic

Definition at line 294 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn1[w] & ~pIn2[w] )
            return 0;
    return 1;
}

int Extra_TruthMinCofSuppOverlap	(	unsigned *	pTruth,
		int	nVars,
		int *	pVarMin
	)

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 775 of file extraUtilTruth.c.

{
    static unsigned uCofactor[16];
    int i, ValueCur, ValueMin, VarMin;
    unsigned uSupp0, uSupp1;
    int nVars0, nVars1;
    assert( nVars <= 9 );
    ValueMin = 32;
    VarMin   = -1;
    for ( i = 0; i < nVars; i++ )
    {
        // get negative cofactor
        Extra_TruthCopy( uCofactor, pTruth, nVars );
        Extra_TruthCofactor0( uCofactor, nVars, i );
        uSupp0 = Extra_TruthSupport( uCofactor, nVars );
        nVars0 = Extra_WordCountOnes( uSupp0 );
//Extra_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
        // get positive cofactor
        Extra_TruthCopy( uCofactor, pTruth, nVars );
        Extra_TruthCofactor1( uCofactor, nVars, i );
        uSupp1 = Extra_TruthSupport( uCofactor, nVars );
        nVars1 = Extra_WordCountOnes( uSupp1 );
//Extra_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
        // get the number of common vars
        ValueCur = Extra_WordCountOnes( uSupp0 & uSupp1 );
        if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
        {
            ValueMin = ValueCur;
            VarMin = i;
        }
        if ( ValueMin == 0 )
            break;
    }
    if ( pVarMin )
        *pVarMin = VarMin;
    return ValueMin;
}

void Extra_TruthMux	(	unsigned *	pOut,
		unsigned *	pCof0,
		unsigned *	pCof1,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pOut[i]      = pCof0[i];
                pOut[Step+i] = pCof1[Step+i];
            }
            pOut += 2*Step;
        }
        return;
    }
}

static void Extra_TruthNand ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 344 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~(pIn0[w] & pIn1[w]);
}

static void Extra_TruthNot ( unsigned *  pOut, unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 320 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~pIn[w];
}

static void Extra_TruthOr ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 332 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] | pIn1[w];
}

unsigned short** Extra_TruthPerm43

(

)

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

Synopsis [Allocated lookup table for truth table permutation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1908 of file extraUtilMisc.c.

{
    unsigned short ** pTable;
    unsigned uTruth;
    int i, k;
    pTable = (unsigned short **)Extra_ArrayAlloc( 256, 16, 2 );
    for ( i = 0; i < 256; i++ )
    {
        uTruth = (i << 8) | i;
        for ( k = 0; k < 16; k++ )
            pTable[i][k] = Extra_TruthPerm4One( uTruth, k );
    }
    return pTable;
}

unsigned short Extra_TruthPerm4One	(	unsigned	uTruth,
		int	Phase
	)

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

Synopsis [Computes a phase of the 3-var function.]

Description []

SideEffects []

SeeAlso []

Definition at line 905 of file extraUtilMisc.c.

{
    // cases
    static unsigned short Cases[16] = {
        0,      // 0000  - skip
        0,      // 0001  - skip
        0xCCCC, // 0010  - single var
        0,      // 0011  - skip
        0xF0F0, // 0100  - single var
        1,      // 0101
        1,      // 0110
        0,      // 0111  - skip
        0xFF00, // 1000  - single var
        1,      // 1001
        1,      // 1010
        1,      // 1011
        1,      // 1100
        1,      // 1101
        1,      // 1110
        0       // 1111  - skip
    };
    // permutations
    static int Perms[16][4] = {
        { 0, 0, 0, 0 }, // 0000  - skip
        { 0, 0, 0, 0 }, // 0001  - skip
        { 0, 0, 0, 0 }, // 0010  - single var
        { 0, 0, 0, 0 }, // 0011  - skip
        { 0, 0, 0, 0 }, // 0100  - single var
        { 0, 2, 1, 3 }, // 0101
        { 2, 0, 1, 3 }, // 0110
        { 0, 0, 0, 0 }, // 0111  - skip
        { 0, 0, 0, 0 }, // 1000  - single var
        { 0, 2, 3, 1 }, // 1001
        { 2, 0, 3, 1 }, // 1010
        { 0, 1, 3, 2 }, // 1011
        { 2, 3, 0, 1 }, // 1100
        { 0, 3, 1, 2 }, // 1101
        { 3, 0, 1, 2 }, // 1110
        { 0, 0, 0, 0 }  // 1111  - skip
    };
    int i, k, iRes;
    unsigned uTruthRes;
    assert( Phase >= 0 && Phase < 16 );
    if ( Cases[Phase] == 0 )
        return uTruth;
    if ( Cases[Phase] > 1 )
        return Cases[Phase];
    uTruthRes = 0;
    for ( i = 0; i < 16; i++ )
        if ( uTruth & (1 << i) )
        {
            for ( iRes = 0, k = 0; k < 4; k++ )
                if ( i & (1 << Perms[Phase][k]) )
                    iRes |= (1 << k);
            uTruthRes |= (1 << iRes);
        }
    return uTruthRes;
}

unsigned** Extra_TruthPerm53

(

)

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

Synopsis [Allocated lookup table for truth table permutation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1934 of file extraUtilMisc.c.

{
    unsigned ** pTable;
    unsigned uTruth;
    int i, k;
    pTable = (unsigned **)Extra_ArrayAlloc( 256, 32, 4 );
    for ( i = 0; i < 256; i++ )
    {
        uTruth = (i << 24) | (i << 16) | (i << 8) | i;
        for ( k = 0; k < 32; k++ )
            pTable[i][k] = Extra_TruthPerm5One( uTruth, k );
    }
    return pTable;
}

unsigned** Extra_TruthPerm54

(

)

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

Synopsis [Allocated lookup table for truth table permutation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1960 of file extraUtilMisc.c.

{
    unsigned ** pTable;
    unsigned uTruth;
    int i;
    pTable = (unsigned **)Extra_ArrayAlloc( 256*256, 4, 4 );
    for ( i = 0; i < 256*256; i++ )
    {
        uTruth = (i << 16) | i;
        pTable[i][0] = Extra_TruthPerm5One( uTruth, 31-8 );
        pTable[i][1] = Extra_TruthPerm5One( uTruth, 31-4 );
        pTable[i][2] = Extra_TruthPerm5One( uTruth, 31-2 );
        pTable[i][3] = Extra_TruthPerm5One( uTruth, 31-1 );
    }
    return pTable;
}

unsigned Extra_TruthPerm5One	(	unsigned	uTruth,
		int	Phase
	)

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

Synopsis [Computes a phase of the 3-var function.]

Description []

SideEffects []

SeeAlso []

Definition at line 975 of file extraUtilMisc.c.

{
    // cases
    static unsigned Cases[32] = {
        0,          // 00000  - skip
        0,          // 00001  - skip
        0xCCCCCCCC, // 00010  - single var
        0,          // 00011  - skip
        0xF0F0F0F0, // 00100  - single var
        1,          // 00101
        1,          // 00110
        0,          // 00111  - skip
        0xFF00FF00, // 01000  - single var
        1,          // 01001
        1,          // 01010
        1,          // 01011
        1,          // 01100
        1,          // 01101
        1,          // 01110
        0,          // 01111  - skip
        0xFFFF0000, // 10000  - skip
        1,          // 10001
        1,          // 10010
        1,          // 10011
        1,          // 10100
        1,          // 10101
        1,          // 10110
        1,          // 10111  - four var
        1,          // 11000
        1,          // 11001
        1,          // 11010
        1,          // 11011  - four var
        1,          // 11100
        1,          // 11101  - four var
        1,          // 11110  - four var
        0           // 11111  - skip
    };
    // permutations
    static int Perms[32][5] = {
        { 0, 0, 0, 0, 0 }, // 00000  - skip
        { 0, 0, 0, 0, 0 }, // 00001  - skip
        { 0, 0, 0, 0, 0 }, // 00010  - single var
        { 0, 0, 0, 0, 0 }, // 00011  - skip
        { 0, 0, 0, 0, 0 }, // 00100  - single var
        { 0, 2, 1, 3, 4 }, // 00101
        { 2, 0, 1, 3, 4 }, // 00110
        { 0, 0, 0, 0, 0 }, // 00111  - skip
        { 0, 0, 0, 0, 0 }, // 01000  - single var
        { 0, 2, 3, 1, 4 }, // 01001
        { 2, 0, 3, 1, 4 }, // 01010
        { 0, 1, 3, 2, 4 }, // 01011
        { 2, 3, 0, 1, 4 }, // 01100
        { 0, 3, 1, 2, 4 }, // 01101
        { 3, 0, 1, 2, 4 }, // 01110
        { 0, 0, 0, 0, 0 }, // 01111  - skip
        { 0, 0, 0, 0, 0 }, // 10000  - single var
        { 0, 4, 2, 3, 1 }, // 10001
        { 4, 0, 2, 3, 1 }, // 10010
        { 0, 1, 3, 4, 2 }, // 10011
        { 2, 3, 0, 4, 1 }, // 10100
        { 0, 3, 1, 4, 2 }, // 10101
        { 3, 0, 1, 4, 2 }, // 10110
        { 0, 1, 2, 4, 3 }, // 10111  - four var
        { 2, 3, 4, 0, 1 }, // 11000
        { 0, 3, 4, 1, 2 }, // 11001
        { 3, 0, 4, 1, 2 }, // 11010
        { 0, 1, 4, 2, 3 }, // 11011  - four var
        { 3, 4, 0, 1, 2 }, // 11100
        { 0, 4, 1, 2, 3 }, // 11101  - four var
        { 4, 0, 1, 2, 3 }, // 11110  - four var
        { 0, 0, 0, 0, 0 }  // 11111  - skip
    };
    int i, k, iRes;
    unsigned uTruthRes;
    assert( Phase >= 0 && Phase < 32 );
    if ( Cases[Phase] == 0 )
        return uTruth;
    if ( Cases[Phase] > 1 )
        return Cases[Phase];
    uTruthRes = 0;
    for ( i = 0; i < 32; i++ )
        if ( uTruth & (1 << i) )
        {
            for ( iRes = 0, k = 0; k < 5; k++ )
                if ( i & (1 << Perms[Phase][k]) )
                    iRes |= (1 << k);
            uTruthRes |= (1 << iRes);
        }
    return uTruthRes;
}

void Extra_TruthPerm6One	(	unsigned *	uTruth,
		int	Phase,
		unsigned *	uTruthRes
	)

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

Synopsis [Computes a phase of the 3-var function.]

Description []

SideEffects []

SeeAlso []

Definition at line 1077 of file extraUtilMisc.c.

{
    // cases
    static unsigned Cases[64] = {
        0,          // 000000  - skip
        0,          // 000001  - skip
        0xCCCCCCCC, // 000010  - single var
        0,          // 000011  - skip
        0xF0F0F0F0, // 000100  - single var
        1,          // 000101
        1,          // 000110
        0,          // 000111  - skip
        0xFF00FF00, // 001000  - single var
        1,          // 001001
        1,          // 001010
        1,          // 001011
        1,          // 001100
        1,          // 001101
        1,          // 001110
        0,          // 001111  - skip
        0xFFFF0000, // 010000  - skip
        1,          // 010001
        1,          // 010010
        1,          // 010011
        1,          // 010100
        1,          // 010101
        1,          // 010110
        1,          // 010111  - four var
        1,          // 011000
        1,          // 011001
        1,          // 011010
        1,          // 011011  - four var
        1,          // 011100
        1,          // 011101  - four var
        1,          // 011110  - four var
        0,          // 011111  - skip
        0xFFFFFFFF, // 100000  - single var
        1,          // 100001 
        1,          // 100010  
        1,          // 100011  
        1,          // 100100  
        1,          // 100101
        1,          // 100110
        1,          // 100111  
        1,          // 101000  
        1,          // 101001
        1,          // 101010
        1,          // 101011
        1,          // 101100
        1,          // 101101
        1,          // 101110
        1,          // 101111  
        1,          // 110000  
        1,          // 110001
        1,          // 110010
        1,          // 110011
        1,          // 110100
        1,          // 110101
        1,          // 110110
        1,          // 110111  
        1,          // 111000
        1,          // 111001
        1,          // 111010
        1,          // 111011  
        1,          // 111100
        1,          // 111101  
        1,          // 111110  
        0           // 111111  - skip
    };
    // permutations
    static int Perms[64][6] = {
        { 0, 0, 0, 0, 0, 0 }, // 000000  - skip
        { 0, 0, 0, 0, 0, 0 }, // 000001  - skip
        { 0, 0, 0, 0, 0, 0 }, // 000010  - single var
        { 0, 0, 0, 0, 0, 0 }, // 000011  - skip
        { 0, 0, 0, 0, 0, 0 }, // 000100  - single var
        { 0, 2, 1, 3, 4, 5 }, // 000101
        { 2, 0, 1, 3, 4, 5 }, // 000110
        { 0, 0, 0, 0, 0, 0 }, // 000111  - skip
        { 0, 0, 0, 0, 0, 0 }, // 001000  - single var
        { 0, 2, 3, 1, 4, 5 }, // 001001
        { 2, 0, 3, 1, 4, 5 }, // 001010
        { 0, 1, 3, 2, 4, 5 }, // 001011
        { 2, 3, 0, 1, 4, 5 }, // 001100
        { 0, 3, 1, 2, 4, 5 }, // 001101
        { 3, 0, 1, 2, 4, 5 }, // 001110
        { 0, 0, 0, 0, 0, 0 }, // 001111  - skip
        { 0, 0, 0, 0, 0, 0 }, // 010000  - skip
        { 0, 4, 2, 3, 1, 5 }, // 010001
        { 4, 0, 2, 3, 1, 5 }, // 010010
        { 0, 1, 3, 4, 2, 5 }, // 010011
        { 2, 3, 0, 4, 1, 5 }, // 010100
        { 0, 3, 1, 4, 2, 5 }, // 010101
        { 3, 0, 1, 4, 2, 5 }, // 010110
        { 0, 1, 2, 4, 3, 5 }, // 010111  - four var
        { 2, 3, 4, 0, 1, 5 }, // 011000
        { 0, 3, 4, 1, 2, 5 }, // 011001
        { 3, 0, 4, 1, 2, 5 }, // 011010
        { 0, 1, 4, 2, 3, 5 }, // 011011  - four var
        { 3, 4, 0, 1, 2, 5 }, // 011100
        { 0, 4, 1, 2, 3, 5 }, // 011101  - four var
        { 4, 0, 1, 2, 3, 5 }, // 011110  - four var
        { 0, 0, 0, 0, 0, 0 }, // 011111  - skip
        { 0, 0, 0, 0, 0, 0 }, // 100000  - single var
        { 0, 2, 3, 4, 5, 1 }, // 100001 
        { 2, 0, 3, 4, 5, 1 }, // 100010  
        { 0, 1, 3, 4, 5, 2 }, // 100011  
        { 2, 3, 0, 4, 5, 1 }, // 100100  
        { 0, 3, 1, 4, 5, 2 }, // 100101
        { 3, 0, 1, 4, 5, 2 }, // 100110
        { 0, 1, 2, 4, 5, 3 }, // 100111  
        { 2, 3, 4, 0, 5, 1 }, // 101000  
        { 0, 3, 4, 1, 5, 2 }, // 101001
        { 3, 0, 4, 1, 5, 2 }, // 101010
        { 0, 1, 4, 2, 5, 3 }, // 101011
        { 3, 4, 0, 1, 5, 2 }, // 101100
        { 0, 4, 1, 2, 5, 3 }, // 101101
        { 4, 0, 1, 2, 5, 3 }, // 101110
        { 0, 1, 2, 3, 5, 4 }, // 101111  
        { 2, 3, 4, 5, 0, 1 }, // 110000  
        { 0, 3, 4, 5, 1, 2 }, // 110001
        { 3, 0, 4, 5, 1, 2 }, // 110010
        { 0, 1, 4, 5, 2, 3 }, // 110011
        { 3, 4, 0, 5, 1, 2 }, // 110100
        { 0, 4, 1, 5, 2, 3 }, // 110101
        { 4, 0, 1, 5, 2, 3 }, // 110110
        { 0, 1, 2, 5, 3, 4 }, // 110111  
        { 3, 4, 5, 0, 1, 2 }, // 111000
        { 0, 4, 5, 1, 2, 3 }, // 111001
        { 4, 0, 5, 1, 2, 3 }, // 111010
        { 0, 1, 5, 2, 3, 4 }, // 111011  
        { 4, 5, 0, 1, 2, 3 }, // 111100
        { 0, 5, 1, 2, 3, 4 }, // 111101  
        { 5, 0, 1, 2, 3, 4 }, // 111110  
        { 0, 0, 0, 0, 0, 0 }  // 111111  - skip
    };
    int i, k, iRes;
    assert( Phase >= 0 && Phase < 64 );
    if ( Cases[Phase] == 0 )
    {
        uTruthRes[0] = uTruth[0];
        uTruthRes[1] = uTruth[1];
        return;
    }
    if ( Cases[Phase] > 1 )
    {
        if ( Phase == 32 )
        {
            uTruthRes[0] = 0x00000000;
            uTruthRes[1] = 0xFFFFFFFF;
        }
        else
        {
            uTruthRes[0] = Cases[Phase];
            uTruthRes[1] = Cases[Phase];
        }
        return;
    }
    uTruthRes[0] = 0;
    uTruthRes[1] = 0;
    for ( i = 0; i < 64; i++ )
    {
        if ( i < 32 )
        {
            if ( uTruth[0] & (1 << i) )
            {
                for ( iRes = 0, k = 0; k < 6; k++ )
                    if ( i & (1 << Perms[Phase][k]) )
                        iRes |= (1 << k);
                if ( iRes < 32 )
                    uTruthRes[0] |= (1 << iRes);
                else
                    uTruthRes[1] |= (1 << (iRes-32));
            }
        }
        else
        {
            if ( uTruth[1] & (1 << (i-32)) )
            {
                for ( iRes = 0, k = 0; k < 6; k++ )
                    if ( i & (1 << Perms[Phase][k]) )
                        iRes |= (1 << k);
                if ( iRes < 32 )
                    uTruthRes[0] |= (1 << iRes);
                else
                    uTruthRes[1] |= (1 << (iRes-32));
            }
        }
    }
}

unsigned Extra_TruthPermute	(	unsigned	Truth,
		char *	pPerms,
		int	nVars,
		int	fReverse
	)

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

Synopsis [Permutes the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 352 of file extraUtilMisc.c.

{
    unsigned Result;
    int * pMints;
    int * pMintsP;
    int nMints;
    int i, m;

    assert( nVars < 6 );
    nMints  = (1 << nVars);
    pMints  = ABC_ALLOC( int, nMints );
    pMintsP = ABC_ALLOC( int, nMints );
    for ( i = 0; i < nMints; i++ )
        pMints[i] = i;

    Extra_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP );

    Result = 0;
    if ( fReverse )
    {
        for ( m = 0; m < nMints; m++ )
            if ( Truth & (1 << pMintsP[m]) )
                Result |= (1 << m);
    }
    else
    {
        for ( m = 0; m < nMints; m++ )
            if ( Truth & (1 << m) )
                Result |= (1 << pMintsP[m]);
    }

    ABC_FREE( pMints );
    ABC_FREE( pMintsP );

    return Result;
}

unsigned Extra_TruthPolarize	(	unsigned	uTruth,
		int	Polarity,
		int	nVars
	)

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

Synopsis [Changes the phase of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 400 of file extraUtilMisc.c.

{
    // elementary truth tables
    static unsigned Signs[5] = {
        0xAAAAAAAA,    // 1010 1010 1010 1010 1010 1010 1010 1010
        0xCCCCCCCC,    // 1010 1010 1010 1010 1010 1010 1010 1010
        0xF0F0F0F0,    // 1111 0000 1111 0000 1111 0000 1111 0000
        0xFF00FF00,    // 1111 1111 0000 0000 1111 1111 0000 0000
        0xFFFF0000     // 1111 1111 1111 1111 0000 0000 0000 0000
    };
    unsigned uTruthRes, uCof0, uCof1;
    int nMints, Shift, v;
    assert( nVars < 6 );
    nMints = (1 << nVars);
    uTruthRes = uTruth;
    for ( v = 0; v < nVars; v++ )
        if ( Polarity & (1 << v) )
        {
            uCof0  = uTruth & ~Signs[v];
            uCof1  = uTruth &  Signs[v];
            Shift  = (1 << v);
            uCof0 <<= Shift;
            uCof1 >>= Shift;
            uTruth = uCof0 | uCof1;
        }
    return uTruth;
}

unsigned Extra_TruthSemiCanonicize	(	unsigned *	pInOut,
		unsigned *	pAux,
		int	nVars,
		char *	pCanonPerm,
		short *	pStore
	)

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 999 of file extraUtilTruth.c.

{
    unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
    int nWords = Extra_TruthWordNum( nVars );
    int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
    unsigned uCanonPhase;

    // canonicize output
    uCanonPhase = 0;
    nOnes = Extra_TruthCountOnes(pIn, nVars);
    if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
    {
        uCanonPhase |= (1 << nVars);
        Extra_TruthNot( pIn, pIn, nVars );
    }

    // collect the minterm counts
    Extra_TruthCountOnesInCofs( pIn, nVars, pStore );

    // canonicize phase
    for ( i = 0; i < nVars; i++ )
    {
        if ( pStore[2*i+0] <= pStore[2*i+1] )
            continue;
        uCanonPhase |= (1 << i);
        Temp = pStore[2*i+0];
        pStore[2*i+0] = pStore[2*i+1];
        pStore[2*i+1] = Temp;
        Extra_TruthChangePhase( pIn, nVars, i );
    }

//    Extra_PrintHexadecimal( stdout, pIn, nVars );
//    printf( "\n" );

    // permute
    Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
            if ( pStore[2*i] <= pStore[2*(i+1)] )
                continue;
            Counter++;
            fChange = 1;

            Temp = pCanonPerm[i];
            pCanonPerm[i] = pCanonPerm[i+1];
            pCanonPerm[i+1] = Temp;

            Temp = pStore[2*i];
            pStore[2*i] = pStore[2*(i+1)];
            pStore[2*(i+1)] = Temp;

            Temp = pStore[2*i+1];
            pStore[2*i+1] = pStore[2*(i+1)+1];
            pStore[2*(i+1)+1] = Temp;

            Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );

/*
    Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
    for ( i = 0; i < nVars; i++ )
        printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
    printf( "  C = %d\n", Counter );
    Extra_PrintHexadecimal( stdout, pIn, nVars );
    printf( "\n" );
*/

/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        if ( pStore[2*i] != pStore[2*i+1] )
            continue;
        if ( Extra_TruthVarsSymm( pIn, nVars, i, i+1 ) )
            continue;
        if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
            Extra_TruthChangePhase( pIn, nVars, i+1 );
    }
*/

/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        // i and i+1 can be symmetric
        // find the end of this group
        for ( k = i+1; k < nVars; k++ )
            if ( pStore[2*i] != pStore[2*k] ) 
                break;
        Limit = k;
        assert( i < Limit-1 );
        // go through the variables in this group
        for ( j = i + 1; j < Limit; j++ )
        {
            // check symmetry
            if ( Extra_TruthVarsSymm( pIn, nVars, i, j ) )
            {
                uSymms |= (1 << j);
                continue;
            }
            // they are phase-unknown
            if ( pStore[2*i] == pStore[2*i+1] ) 
            {
                if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, j ) )
                {
                    Extra_TruthChangePhase( pIn, nVars, j );
                    uCanonPhase ^= (1 << j);
                    uSymms |= (1 << j);
                    continue;
                }
            }

            // they are not symmetric - move j as far as it goes in the group
            for ( k = j; k < Limit-1; k++ )
            {
                Counter++;

                Temp = pCanonPerm[k];
                pCanonPerm[k] = pCanonPerm[k+1];
                pCanonPerm[k+1] = Temp;

                assert( pStore[2*k] == pStore[2*(k+1)] );
                Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
            }
            Limit--;
            j--;
        }
        i = Limit - 1;
    }
*/

    // swap if it was moved an even number of times
    if ( Counter & 1 )
        Extra_TruthCopy( pOut, pIn, nVars );
    return uCanonPhase;
}

static void Extra_TruthSetBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 251 of file extra.h.

{ p[Bit>>5] |= (1<<(Bit & 31));               }

static void Extra_TruthSharp ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 338 of file extra.h.

{
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] & ~pIn1[w];
}

void Extra_TruthShrink	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	nVarsAll,
		unsigned	Phase
	)

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

Synopsis [Shrinks the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows what variables should remain.]

SideEffects []

SeeAlso []

Definition at line 268 of file extraUtilTruth.c.

{
    unsigned * pTemp;
    int i, k, Var = 0, Counter = 0;
    for ( i = 0; i < nVarsAll; i++ )
        if ( Phase & (1 << i) )
        {
            for ( k = i-1; k >= Var; k-- )
            {
                Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
                Counter++;
            }
            Var++;
        }
    assert( Var == nVars );
    // swap if it was moved an even number of times
    if ( !(Counter & 1) )
        Extra_TruthCopy( pOut, pIn, nVarsAll );
}

void Extra_TruthStretch	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	nVarsAll,
		unsigned	Phase
	)

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

Synopsis [Expands the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows where the variables should go.]

SideEffects []

SeeAlso []

Definition at line 234 of file extraUtilTruth.c.

{
    unsigned * pTemp;
    int i, k, Var = nVars - 1, Counter = 0;
    for ( i = nVarsAll - 1; i >= 0; i-- )
        if ( Phase & (1 << i) )
        {
            for ( k = Var; k < i; k++ )
            {
                Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
                Counter++;
            }
            Var--;
        }
    assert( Var == -1 );
    // swap if it was moved an even number of times
    if ( !(Counter & 1) )
        Extra_TruthCopy( pOut, pIn, nVarsAll );
}

int Extra_TruthSupport	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 377 of file extraUtilTruth.c.

{
    int i, Support = 0;
    for ( i = 0; i < nVars; i++ )
        if ( Extra_TruthVarInSupport( pTruth, nVars, i ) )
            Support |= (1 << i);
    return Support;
}

int Extra_TruthSupportSize	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file extraUtilTruth.c.

{
    int i, Counter = 0;
    for ( i = 0; i < nVars; i++ )
        Counter += Extra_TruthVarInSupport( pTruth, nVars, i );
    return Counter;
}

void Extra_TruthSwapAdjacentVars	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	iVar
	)

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

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 114 of file extraUtilTruth.c.

{
    static unsigned PMasks[4][3] = {
        { 0x99999999, 0x22222222, 0x44444444 },
        { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
        { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
        { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
    };
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step, Shift;

    assert( iVar < nVars - 1 );
    if ( iVar < 4 )
    {
        Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
    }
    else if ( iVar > 4 )
    {
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 4*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pIn[i];
            for ( i = 0; i < Step; i++ )
                pOut[Step+i] = pIn[2*Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[2*Step+i] = pIn[Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[3*Step+i] = pIn[3*Step+i];
            pIn  += 4*Step;
            pOut += 4*Step;
        }
    }
    else // if ( iVar == 4 )
    {
        for ( i = 0; i < nWords; i += 2 )
        {
            pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
            pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
        }
    }
}

int Extra_TruthVarInSupport	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Returns 1 if TT depends on the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file extraUtilTruth.c.

{
    int nWords = Extra_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
                return 1;
        return 0;
    case 1:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
                return 1;
        return 0;
    case 2:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
                return 1;
        return 0;
    case 3:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
                return 1;
        return 0;
    case 4:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
                return 1;
        return 0;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                if ( pTruth[i] != pTruth[Step+i] )
                    return 1;
            pTruth += 2*Step;
        }
        return 0;
    }
}

static int Extra_TruthWordNum ( int  nVars )

inlinestatic

Definition at line 249 of file extra.h.

{ return nVars <= 5 ? 1 : (1 << (nVars - 5)); }

static void Extra_TruthXorBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 252 of file extra.h.

{ p[Bit>>5] ^= (1<<(Bit & 31));               }

char* Extra_UtilFileSearch	(	char *	file,
		char *	path,
		char *	mode
	)

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

Synopsis [util_file_search()]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file extraUtilUtil.c.

{
    int quit;
    char *buffer, *filename, *save_path, *cp;

    if (path == 0 || strcmp(path, "") == 0) {
    path = ".";     /* just look in the current directory */
    }

    save_path = path = Extra_UtilStrsav(path);
    quit = 0;
    do {
    cp = strchr(path, ':');
    if (cp != 0) {
        *cp = '\0';
    } else {
        quit = 1;
    }

    /* cons up the filename out of the path and file name */
    if (strcmp(path, ".") == 0) {
        buffer = Extra_UtilStrsav(file);
    } else {
        buffer = ABC_ALLOC(char, strlen(path) + strlen(file) + 4);
        (void) sprintf(buffer, "%s/%s", path, file);
    }
    filename = Extra_UtilTildeExpand(buffer);
    ABC_FREE(buffer);

    /* see if we can access it */
    if (Extra_UtilCheckFile(filename, mode)) {
        ABC_FREE(save_path);
        return filename;
    }
    ABC_FREE(filename);
    path = ++cp;
    } while (! quit); 

    ABC_FREE(save_path);
    return 0;
}

int Extra_UtilGetopt	(	int	argc,
		char *	argv[],
		const char *	optstring
	)

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

Synopsis [util_getopt()]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file extraUtilUtil.c.

{
    register int c;
    register const char *place;

    globalUtilOptarg = NULL;

    if (pScanStr == NULL || *pScanStr == '\0') {
    if (globalUtilOptind == 0) globalUtilOptind++;
    if (globalUtilOptind >= argc) return EOF;
    place = argv[globalUtilOptind];
    if (place[0] != '-' || place[1] == '\0') return EOF;
    globalUtilOptind++;
    if (place[1] == '-' && place[2] == '\0') return EOF;
    pScanStr = place+1;
    }

    c = *pScanStr++;
    place = strchr(optstring, c);
    if (place == NULL || c == ':') {
    (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
    return '?';
    }
    if (*++place == ':') {
    if (*pScanStr != '\0') {
        globalUtilOptarg = pScanStr;
        pScanStr = NULL;
    } else {
        if (globalUtilOptind >= argc) {
        (void) fprintf(stderr, "%s: %c requires an argument\n", 
            argv[0], c);
        return '?';
        }
        globalUtilOptarg = argv[globalUtilOptind];
        globalUtilOptind++;
    }
    }
    return c;
}

ABC_DLL void Extra_UtilGetoptReset

(

)

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

Synopsis [util_getopt_reset()]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file extraUtilUtil.c.

{
    globalUtilOptarg = 0;
    globalUtilOptind = 0;
    pScanStr = 0;
}

char* Extra_UtilPrintTime

(

long

t

)

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

Synopsis [util_print_time()]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file extraUtilUtil.c.

{
    static char s[40];

    (void) sprintf(s, "%ld.%02ld sec", t/1000, (t%1000)/10);
    return s;
}

char* Extra_UtilStrsav

(

const char *

s

)

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

Synopsis [Extra_UtilStrsav()]

Description []

SideEffects []

SeeAlso []

Definition at line 169 of file extraUtilUtil.c.

{
    if(s == NULL) {  /* added 7/95, for robustness */
       return NULL;
    }
    else {
       return strcpy(ABC_ALLOC(char, strlen(s)+1), s);
    }
}

char* Extra_UtilTildeExpand

(

char *

fname

)

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

Synopsis [util_tilde_expand()]

Description [The code contributed by Niklas Sorensson.]

SideEffects []

SeeAlso []

Definition at line 190 of file extraUtilUtil.c.

{
    return Extra_UtilStrsav( fname );
/*
    int         n_tildes = 0;
    const char* home;
    char*       expanded;
    int         length;
    int         i, j, k;

    for (i = 0; i < (int)strlen(fname); i++)
        if (fname[i] == '~') n_tildes++;

    home     = getenv("HOME");
    length   = n_tildes * strlen(home) + strlen(fname);
    expanded = ABC_ALLOC(char, length + 1);

    j = 0;
    for (i = 0; i < (int)strlen(fname); i++){
        if (fname[i] == '~'){
            for (k = 0; k < (int)strlen(home); k++)
                expanded[j++] = home[k];
        }else
            expanded[j++] = fname[i];
    }

    expanded[j] = '\0';
    return expanded; 
*/
}

static int Extra_WordCountOnes ( unsigned  uWord )

inlinestatic

Definition at line 255 of file extra.h.

{
    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
    return  (uWord & 0x0000FFFF) + (uWord>>16);
}

int Sdm_ManCanRead

(

)

Definition at line 1080 of file extraUtilDsd.c.

{
    char * pFileName = "dsdfuncs6.dat";
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
        return 0;
    fclose( pFile );
    return 1;
}

int Sdm_ManComputeFunc	(	Sdm_Man_t *	p,
		int	iDsdLit0,
		int	iDsdLit1,
		int *	pCut,
		int	uMask,
		int	fXor
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 920 of file extraUtilDsd.c.

{
//    int fVerbose = 0;
    int i, Config, iClass, fCompl, Res;
    int PermMask = uMask & 0x3FFFF;
    int ComplMask = uMask >> 18;
    word Truth0, Truth1p, t0, t1, t;
    p->nAllDsd++;

    assert( uMask > 1 );
    assert( iDsdLit0 < DSD_CLASS_NUM * 2 );
    assert( iDsdLit1 < DSD_CLASS_NUM * 2 );
    Truth0  = p->pDsd6[Abc_Lit2Var(iDsdLit0)].uTruth;
    Truth1p = Vec_WrdEntry( p->vPerm6, Abc_Lit2Var(iDsdLit1) * 720 + Vec_IntEntry(p->vMap2Perm, PermMask ) );
    if ( ComplMask )
        for ( i = 0; i < 6; i++ )
            if ( (ComplMask >> i) & 1 )
                Truth1p = Abc_Tt6Flip( Truth1p, i );            
    t0 = Abc_LitIsCompl(iDsdLit0) ? ~Truth0  : Truth0;
    t1 = Abc_LitIsCompl(iDsdLit1) ? ~Truth1p : Truth1p;
    t = fXor ? t0 ^ t1 : t0 & t1;
/*
if ( fVerbose )
{
Sdm_ManPrintPerm( PermMask );                      printf( "\n" );
Extra_PrintBinary( stdout, &ComplMask, 6 );        printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&Truth0, 6 );   printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&Truth1p, 6 );  printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );        printf( "\n" );
}
*/
    // find configuration
    Config = Sdm_ManCheckDsd6( p, t );
    if ( Config == -1 )
    {
        p->nNonDsd++;
        return -1;
    }

    // get the class
    iClass = Config >> 17;
    fCompl = (Config >> 16) & 1;
    Config &= 0xFFFF;

    // set the function
    Res = Abc_Var2Lit( iClass, fCompl );

    // update cut
    assert( (Config >> 6) < 720 );
    if ( pCut )
    {
        int pLeavesNew[6] = { -1, -1, -1, -1, -1, -1 };
        assert( pCut[0] <= 6 );
        for ( i = 0; i < pCut[0]; i++ )
            pLeavesNew[(int)(p->Perm6[Config >> 6][i])] = Abc_LitNotCond( pCut[i+1], (Config >> i) & 1 );
        pCut[0] = p->pDsd6[iClass].nVars;
        for ( i = 0; i < pCut[0]; i++ )
            assert( pLeavesNew[i] != -1 );
        for ( i = 0; i < pCut[0]; i++ )
            pCut[i+1] = pLeavesNew[i];
    }
    assert( iClass < DSD_CLASS_NUM );
    p->nCountDsd[iClass]++;
    return Res;
}

void Sdm_ManPrintDsdStats	(	Sdm_Man_t *	p,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 676 of file extraUtilDsd.c.

{
    int i, Absent = 0;
    for ( i = 0; i < DSD_CLASS_NUM; i++ )
    {
        if ( p->nCountDsd[i] == 0 )
        {
            Absent++;
            continue;
        }
        if ( fVerbose )
        {
            printf( "%5d  :  ", i );
            printf( "%-20s   ", p->pDsd6[i].pStr );
            printf( "%8d ",     p->nCountDsd[i] );
            printf( "\n" );
        }
    }
    printf( "Unused classes = %d (%.2f %%).  ", Absent, 100.0 * Absent / DSD_CLASS_NUM );
    printf( "Non-DSD cuts = %d (%.2f %%).  ",   p->nNonDsd, 100.0 * p->nNonDsd / Abc_MaxInt(1, p->nAllDsd) );
    printf( "\n" );
}

void Sdm_ManQuit

(

)

Definition at line 1074 of file extraUtilDsd.c.

{
    if ( s_SdmMan != NULL )
        Sdm_ManFree( s_SdmMan );
    s_SdmMan = NULL;
}

Sdm_Man_t* Sdm_ManRead

(

)

Definition at line 1067 of file extraUtilDsd.c.

{
    if ( s_SdmMan == NULL )
        s_SdmMan = Sdm_ManAlloc();
    memset( s_SdmMan->nCountDsd, 0, sizeof(int) * DSD_CLASS_NUM );
    return s_SdmMan;
}

void Sdm_ManReadCnfCosts	(	Sdm_Man_t *	p,
		int *	pCosts,
		int	nCosts
	)

Definition at line 1017 of file extraUtilDsd.c.

{
    int i;
    assert( nCosts == DSD_CLASS_NUM );
    pCosts[0] = pCosts[1] = 0;
    for ( i = 2; i < DSD_CLASS_NUM; i++ )
        pCosts[i] = Sdm_ManReadDsdClauseNum( p, i );
}

int Sdm_ManReadDsdAndNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1001 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nAnds;
}

int Sdm_ManReadDsdClauseNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1005 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nClauses;
}

char* Sdm_ManReadDsdStr	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1013 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].pStr;
}

word Sdm_ManReadDsdTruth	(	Sdm_Man_t *	p,
		int	iDsd
	)

Definition at line 1009 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].uTruth;
}

int Sdm_ManReadDsdVarNum	(	Sdm_Man_t *	p,
		int	iDsd
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 997 of file extraUtilDsd.c.

{
    return p->pDsd6[iDsd].nVars;
}

Variable Documentation

void(* Extra_UtilMMoutOfMemory)(long size)

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

Synopsis [MMoutOfMemory()]

Description []

SideEffects []

SeeAlso []

Definition at line 336 of file extraUtilUtil.c.

const char* globalUtilOptarg

Definition at line 44 of file extraUtilUtil.c.

int globalUtilOptind

Definition at line 45 of file extraUtilUtil.c.

ABC_NAMESPACE_HEADER_START typedef unsigned char uint8

CFile****************************************************************

FileName [extra.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [Various reusable software utilities.]

Description [This library contains a number of operators and traversal routines developed to extend the functionality of CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/) To compile your code with the library, #include "extra.h" in your source files and link your project to CUDD and this library. Use the library at your own risk and with caution. Note that debugging of some operators still continues.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

extra.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 71 of file extra.h.