fraigInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/util/abc_global.h"
#include "fraig.h"
#include "sat/msat/msat.h"

Go to the source code of this file.

Data Structures
struct	Fraig_ManStruct_t_
struct	Fraig_NodeStruct_t_
struct	Fraig_NodeVecStruct_t_
struct	Fraig_HashTableStruct_t_

Macros
#define	FRAIG_ENABLE_FANOUTS
	INCLUDES ///. More...
#define	FRAIG_PATTERNS_RANDOM   2048
#define	FRAIG_PATTERNS_DYNAMIC   2048
#define	FRAIG_MAX_PRIMES   1024
#define	FRAIG_WORDS_STORE   5
#define	FRAIG_MASK(n)   ((~((unsigned)0)) >> (32-(n)))
#define	FRAIG_FULL   (~((unsigned)0))
#define	FRAIG_NUM_WORDS(n)   (((n)>>5) + (((n)&31) > 0))
#define	FRAIG_RANDOM_UNSIGNED   Aig_ManRandom(0)
#define	Fraig_BitStringSetBit(p, i)   ((p)[(i)>>5] |= (1<<((i) & 31)))
#define	Fraig_BitStringXorBit(p, i)   ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define	Fraig_BitStringHasBit(p, i)   (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
#define	Fraig_NodeSetVarStr(p, i)   Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)
#define	Fraig_NodeHasVarStr(p, i)   Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)
#define	Fraig_PrintTime(a, t)   printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
#define	Fraig_HashKey2(a, b, TSIZE)   (((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * 12582917) % TSIZE)
#define	Fraig_NodeReadNextFanout(pNode, pFanout)
#define	Fraig_NodeReadNextFanoutPlace(pNode, pFanout)
#define	Fraig_NodeForEachFanout(pNode, pFanout)
#define	Fraig_NodeForEachFanoutSafe(pNode, pFanout, pFanout2)
#define	Fraig_TableBinForEachEntryS(pBin, pEnt)
#define	Fraig_TableBinForEachEntrySafeS(pBin, pEnt, pEnt2)
#define	Fraig_TableBinForEachEntryF(pBin, pEnt)
#define	Fraig_TableBinForEachEntrySafeF(pBin, pEnt, pEnt2)
#define	Fraig_TableBinForEachEntryD(pBin, pEnt)
#define	Fraig_TableBinForEachEntrySafeD(pBin, pEnt, pEnt2)
#define	Fraig_TableBinForEachEntryE(pBin, pEnt)
#define	Fraig_TableBinForEachEntrySafeE(pBin, pEnt, pEnt2)

Typedefs
typedef struct Fraig_MemFixed_t_	Fraig_MemFixed_t
	STRUCTURE DEFINITIONS ///. More...

Functions
unsigned	Aig_ManRandom (int fReset)
	GLOBAL VARIABLES ///. More...
Fraig_Node_t *	Fraig_NodeAndCanon (Fraig_Man_t *pMan, Fraig_Node_t *p1, Fraig_Node_t *p2)
	FUNCTION DEFINITIONS ///. More...
void	Fraig_NodeAddFaninFanout (Fraig_Node_t *pFanin, Fraig_Node_t *pFanout)
	DECLARATIONS ///. More...
void	Fraig_NodeRemoveFaninFanout (Fraig_Node_t *pFanin, Fraig_Node_t *pFanoutToRemove)
int	Fraig_NodeGetFanoutNum (Fraig_Node_t *pNode)
void	Fraig_FeedBackInit (Fraig_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
void	Fraig_FeedBack (Fraig_Man_t *p, int *pModel, Msat_IntVec_t *vVars, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
void	Fraig_FeedBackTest (Fraig_Man_t *p)
int	Fraig_FeedBackCompress (Fraig_Man_t *p)
int *	Fraig_ManAllocCounterExample (Fraig_Man_t *p)
int *	Fraig_ManSaveCounterExample (Fraig_Man_t *p, Fraig_Node_t *pNode)
void	Fraig_ManCreateSolver (Fraig_Man_t *p)
Fraig_MemFixed_t *	Fraig_MemFixedStart (int nEntrySize)
	FUNCTION DEFINITIONS ///. More...
void	Fraig_MemFixedStop (Fraig_MemFixed_t *p, int fVerbose)
char *	Fraig_MemFixedEntryFetch (Fraig_MemFixed_t *p)
void	Fraig_MemFixedEntryRecycle (Fraig_MemFixed_t *p, char *pEntry)
void	Fraig_MemFixedRestart (Fraig_MemFixed_t *p)
int	Fraig_MemFixedReadMemUsage (Fraig_MemFixed_t *p)
Fraig_Node_t *	Fraig_NodeCreateConst (Fraig_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
Fraig_Node_t *	Fraig_NodeCreatePi (Fraig_Man_t *p)
Fraig_Node_t *	Fraig_NodeCreate (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
void	Fraig_NodeSimulate (Fraig_Node_t *pNode, int iWordStart, int iWordStop, int fUseRand)
int	Fraig_NodeIsImplication (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
Fraig_HashTable_t *	Fraig_HashTableCreate (int nSize)
	FUNCTION DEFINITIONS ///. More...
void	Fraig_HashTableFree (Fraig_HashTable_t *p)
int	Fraig_HashTableLookupS (Fraig_Man_t *pMan, Fraig_Node_t *p1, Fraig_Node_t *p2, Fraig_Node_t **ppNodeRes)
Fraig_Node_t *	Fraig_HashTableLookupF (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Fraig_Node_t *	Fraig_HashTableLookupF0 (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
void	Fraig_HashTableInsertF0 (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int	Fraig_CompareSimInfo (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand)
int	Fraig_CompareSimInfoUnderMask (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand, unsigned *puMask)
int	Fraig_FindFirstDiff (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int fCompl, int iWordLast, int fUseRand)
void	Fraig_CollectXors (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand, unsigned *puMask)
void	Fraig_TablePrintStatsS (Fraig_Man_t *pMan)
void	Fraig_TablePrintStatsF (Fraig_Man_t *pMan)
void	Fraig_TablePrintStatsF0 (Fraig_Man_t *pMan)
int	Fraig_TableRehashF0 (Fraig_Man_t *pMan, int fLinkEquiv)
int	Fraig_NodeCountPis (Msat_IntVec_t *vVars, int nVarsPi)
int	Fraig_NodeCountSuppVars (Fraig_Man_t *p, Fraig_Node_t *pNode, int fSuppStr)
int	Fraig_NodesCompareSupps (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int	Fraig_NodeAndSimpleCase_rec (Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int	Fraig_NodeIsExorType (Fraig_Node_t *pNode)
void	Fraig_ManSelectBestChoice (Fraig_Man_t *p)
int	Fraig_BitStringCountOnes (unsigned *pString, int nWords)
void	Fraig_PrintBinary (FILE *pFile, unsigned *pSign, int nBits)
int	Fraig_NodeIsExor (Fraig_Node_t *pNode)
int	Fraig_NodeIsMuxType (Fraig_Node_t *pNode)
Fraig_Node_t *	Fraig_NodeRecognizeMux (Fraig_Node_t *pNode, Fraig_Node_t **ppNodeT, Fraig_Node_t **ppNodeE)
int	Fraig_ManCountExors (Fraig_Man_t *pMan)
int	Fraig_ManCountMuxes (Fraig_Man_t *pMan)
int	Fraig_NodeSimsContained (Fraig_Man_t *pMan, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2)
int	Fraig_NodeIsInSupergate (Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Fraig_NodeVec_t *	Fraig_CollectSupergate (Fraig_Node_t *pNode, int fStopAtMux)
int	Fraig_CountPis (Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
void	Fraig_ManIncrementTravId (Fraig_Man_t *pMan)
void	Fraig_NodeSetTravIdCurrent (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int	Fraig_NodeIsTravIdCurrent (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int	Fraig_NodeIsTravIdPrevious (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
void	Fraig_NodeVecSortByRefCount (Fraig_NodeVec_t *p)

Variables
int	s_FraigPrimes [FRAIG_MAX_PRIMES]
	DECLARATIONS ///. More...

Macro Definition Documentation

#define Fraig_BitStringHasBit	(		p,
			i
	)		(((p)[(i)>>5] & (1<<((i) & 31))) > 0)

Definition at line 81 of file fraigInt.h.

#define Fraig_BitStringSetBit	(		p,
			i
	)		((p)[(i)>>5] |= (1<<((i) & 31)))

Definition at line 79 of file fraigInt.h.

#define Fraig_BitStringXorBit	(		p,
			i
	)		((p)[(i)>>5] ^= (1<<((i) & 31)))

Definition at line 80 of file fraigInt.h.

#define FRAIG_ENABLE_FANOUTS

INCLUDES ///.

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

FileName [fraigInt.h]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Internal declarations of the FRAIG package.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigInt.h,v 1.15 2005/07/08 01:01:31 alanmi Exp

]PARAMETERS ///MACRO DEFINITIONS ///

Definition at line 57 of file fraigInt.h.

#define FRAIG_FULL   (~((unsigned)0))

Definition at line 71 of file fraigInt.h.

#define Fraig_HashKey2	(		a,
			b,
			TSIZE
	)		(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * 12582917) % TSIZE)

Definition at line 92 of file fraigInt.h.

#define FRAIG_MASK

(

n

)

((~((unsigned)0)) >> (32-(n)))

Definition at line 70 of file fraigInt.h.

#define FRAIG_MAX_PRIMES   1024

Definition at line 60 of file fraigInt.h.

#define Fraig_NodeForEachFanout	(		pNode,
			pFanout
	)

Value:

for ( pFanout = (pNode)->pFanPivot; pFanout;                  \
          pFanout = Fraig_NodeReadNextFanout(pNode, pFanout) )

Definition at line 288 of file fraigInt.h.

#define Fraig_NodeForEachFanoutSafe	(		pNode,
			pFanout,
			pFanout2
	)

Value:

for ( pFanout  = (pNode)->pFanPivot,                          \
          pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout);    \
          pFanout;                                                \
          pFanout  = pFanout2,                                    \
          pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout) )

Definition at line 292 of file fraigInt.h.

#define Fraig_NodeHasVarStr	(		p,
			i
	)		Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)

Definition at line 87 of file fraigInt.h.

#define Fraig_NodeReadNextFanout	(		pNode,
			pFanout
	)

Value:

( ( pFanout == NULL )? NULL :                                 \
        ((Fraig_Regular((pFanout)->p1) == (pNode))?               \
             (pFanout)->pFanFanin1 : (pFanout)->pFanFanin2) )

Definition at line 279 of file fraigInt.h.

#define Fraig_NodeReadNextFanoutPlace	(		pNode,
			pFanout
	)

Value:

( (Fraig_Regular((pFanout)->p1) == (pNode))?                  \
         &(pFanout)->pFanFanin1 : &(pFanout)->pFanFanin2 )

Definition at line 284 of file fraigInt.h.

#define Fraig_NodeSetVarStr	(		p,
			i
	)		Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)

Definition at line 86 of file fraigInt.h.

#define FRAIG_NUM_WORDS

(

n

)

(((n)>>5) + (((n)&31) > 0))

Definition at line 72 of file fraigInt.h.

#define FRAIG_PATTERNS_DYNAMIC   2048

Definition at line 59 of file fraigInt.h.

#define FRAIG_PATTERNS_RANDOM   2048

Definition at line 58 of file fraigInt.h.

#define Fraig_PrintTime	(		a,
			t
	)		printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )

Definition at line 90 of file fraigInt.h.

#define FRAIG_RANDOM_UNSIGNED   Aig_ManRandom(0)

Definition at line 76 of file fraigInt.h.

#define Fraig_TableBinForEachEntryD	(		pBin,
			pEnt
	)

Value:

for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextD )

Definition at line 323 of file fraigInt.h.

#define Fraig_TableBinForEachEntryE	(		pBin,
			pEnt
	)

Value:

for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextE )

Definition at line 334 of file fraigInt.h.

#define Fraig_TableBinForEachEntryF	(		pBin,
			pEnt
	)

Value:

for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextF )

Definition at line 312 of file fraigInt.h.

#define Fraig_TableBinForEachEntryS	(		pBin,
			pEnt
	)

Value:

for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextS )

Definition at line 301 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeD	(		pBin,
			pEnt,
			pEnt2
	)

Value:

for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextD: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextD: NULL )

Definition at line 327 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeE	(		pBin,
			pEnt,
			pEnt2
	)

Value:

for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextE: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextE: NULL )

Definition at line 338 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeF	(		pBin,
			pEnt,
			pEnt2
	)

Value:

for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextF: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextF: NULL )

Definition at line 316 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeS	(		pBin,
			pEnt,
			pEnt2
	)

Value:

for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextS: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextS: NULL )

Definition at line 305 of file fraigInt.h.

#define FRAIG_WORDS_STORE   5

Definition at line 67 of file fraigInt.h.

Typedef Documentation

typedef struct Fraig_MemFixed_t_ Fraig_MemFixed_t

STRUCTURE DEFINITIONS ///.

Definition at line 101 of file fraigInt.h.

Function Documentation

unsigned Aig_ManRandom

(

int

fReset

)

GLOBAL VARIABLES ///.

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

Synopsis [Creates a sequence of random numbers.]

Description []

SideEffects []

SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]

Definition at line 1157 of file aigUtil.c.

{
    static unsigned int m_z = NUMBER1;
    static unsigned int m_w = NUMBER2;
    if ( fReset )
    {
        m_z = NUMBER1;
        m_w = NUMBER2;
    }
    m_z = 36969 * (m_z & 65535) + (m_z >> 16);
    m_w = 18000 * (m_w & 65535) + (m_w >> 16);
    return (m_z << 16) + m_w;
}

int Fraig_BitStringCountOnes	(	unsigned *	pString,
		int	nWords
	)

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

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file fraigUtil.c.

{
    unsigned char * pSuppBytes = (unsigned char *)pString;
    int i, nOnes, nBytes = sizeof(unsigned) * nWords;
    // count the number of ones in the simulation vector
    for ( i = nOnes = 0; i < nBytes; i++ )
        nOnes += bit_count[pSuppBytes[i]];
    return nOnes;
}

Fraig_NodeVec_t* Fraig_CollectSupergate	(	Fraig_Node_t *	pNode,
		int	fStopAtMux
	)

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 960 of file fraigUtil.c.

{
    Fraig_NodeVec_t * vSuper;
    vSuper = Fraig_NodeVecAlloc( 8 );
    Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
    return vSuper;
}

void Fraig_CollectXors	(	Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	iWordLast,
		int	fUseRand,
		unsigned *	puMask
	)

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

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 478 of file fraigTable.c.

{
    unsigned * pSims1, * pSims2;
    int i;
    assert( !Fraig_IsComplement(pNode1) );
    assert( !Fraig_IsComplement(pNode2) );
    // get hold of simulation info
    pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
    pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
    // check the simulation info
    for ( i = 0; i < iWordLast; i++ )
        puMask[i] = ( pSims1[i] ^ pSims2[i] );
}

int Fraig_CompareSimInfo	(	Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	iWordLast,
		int	fUseRand
	)

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

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 351 of file fraigTable.c.

{
    int i;
    assert( !Fraig_IsComplement(pNode1) );
    assert( !Fraig_IsComplement(pNode2) );
    if ( fUseRand )
    {
        // if their signatures differ, skip
        if ( pNode1->uHashR != pNode2->uHashR )
            return 0;
        // check the simulation info
        for ( i = 0; i < iWordLast; i++ )
            if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
                return 0;
    }
    else
    {
        // if their signatures differ, skip
        if ( pNode1->uHashD != pNode2->uHashD )
            return 0;
        // check the simulation info
        for ( i = 0; i < iWordLast; i++ )
            if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
                return 0;
    }
    return 1;
}

int Fraig_CompareSimInfoUnderMask	(	Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	iWordLast,
		int	fUseRand,
		unsigned *	puMask
	)

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

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 451 of file fraigTable.c.

{
    unsigned * pSims1, * pSims2;
    int i;
    assert( !Fraig_IsComplement(pNode1) );
    assert( !Fraig_IsComplement(pNode2) );
    // get hold of simulation info
    pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
    pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
    // check the simulation info
    for ( i = 0; i < iWordLast; i++ )
        if ( (pSims1[i] & puMask[i]) != (pSims2[i] & puMask[i]) )
            return 0;
    return 1;
}

int Fraig_CountPis	(	Fraig_Man_t *	p,
		Msat_IntVec_t *	vVarNums
	)

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

Synopsis [Count the number of PI variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 817 of file fraigUtil.c.

{
    int * pVars, nVars, i, Counter;

    nVars = Msat_IntVecReadSize(vVarNums);
    pVars = Msat_IntVecReadArray(vVarNums);
    Counter = 0;
    for ( i = 0; i < nVars; i++ )
        Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] );
    return Counter;
}

void Fraig_FeedBack	(	Fraig_Man_t *	p,
		int *	pModel,
		Msat_IntVec_t *	vVars,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew
	)

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

Synopsis [Processes the feedback from teh solver.]

Description [Array pModel gives the value of each variable in the SAT solver. Array vVars is the array of integer numbers of variables involves in this conflict.]

SideEffects []

SeeAlso []

Definition at line 80 of file fraigFeed.c.

{
    int nVarsPi, nWords;
    int i;
    abctime clk = Abc_Clock();

    // get the number of PI vars in the feedback (also sets the PI values)
    nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars );

    // set the PI values
    nWords = Fraig_FeedBackInsert( p, nVarsPi );
    assert( p->iWordStart + nWords <= p->nWordsDyna );

    // resimulates the words from p->iWordStart to iWordStop
    for ( i = 1; i < p->vNodes->nSize; i++ )
        if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) )
            Fraig_NodeSimulate( p->vNodes->pArray[i], p->iWordStart, p->iWordStart + nWords, 0 );

    if ( p->fDoSparse )
        Fraig_TableRehashF0( p, 0 );

    if ( !p->fChoicing )
    Fraig_FeedBackVerify( p, pOld, pNew );

    // if there is no room left, compress the patterns
    if ( p->iWordStart + nWords == p->nWordsDyna )
        p->iWordStart = Fraig_FeedBackCompress( p );
    else  // otherwise, update the starting word
        p->iWordStart += nWords;

p->timeFeed += Abc_Clock() - clk;
}

int Fraig_FeedBackCompress

(

Fraig_Man_t *

p

)

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

Synopsis [Compress the simulation patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file fraigFeed.c.

{
    unsigned * pSims;
    unsigned uHash;
    int i, w, t, nPats, * pPats;
    int fPerformChecks = (p->nBTLimit == -1);

    // solve the covering problem
    if ( fPerformChecks )
    {
        Fraig_FeedBackCheckTable( p );
        if ( p->fDoSparse ) 
            Fraig_FeedBackCheckTableF0( p );
    }

    // solve the covering problem
    Fraig_FeedBackCovering( p, p->vPatsReal );


    // get the number of additional patterns
    nPats = Msat_IntVecReadSize( p->vPatsReal );
    pPats = Msat_IntVecReadArray( p->vPatsReal );
    // get the new starting word
    p->iWordStart = FRAIG_NUM_WORDS( p->iPatsPerm + nPats );

    // set the simulation info for the PIs
    for ( i = 0; i < p->vInputs->nSize; i++ )
    {
        // get hold of the simulation info for this PI
        pSims = p->vInputs->pArray[i]->puSimD;
        // clean the storage for the new patterns
        for ( w = p->iWordPerm; w < p->iWordStart; w++ )
            p->pSimsTemp[w] = 0;
        // set the patterns
        for ( t = 0; t < nPats; t++ )
            if ( Fraig_BitStringHasBit( pSims, pPats[t] ) )
            {
                // check if this pattern falls into temporary storage
                if ( p->iPatsPerm + t < p->iWordPerm * 32 )
                    Fraig_BitStringSetBit( pSims, p->iPatsPerm + t );
                else
                    Fraig_BitStringSetBit( p->pSimsTemp, p->iPatsPerm + t );
            }
        // copy the pattern 
        for ( w = p->iWordPerm; w < p->iWordStart; w++ )
            pSims[w] = p->pSimsTemp[w];
        // recompute the hashing info
        uHash = 0;
        for ( w = 0; w < p->iWordStart; w++ )
            uHash ^= pSims[w] * s_FraigPrimes[w];
        p->vInputs->pArray[i]->uHashD = uHash;
    }

    // update info about the permanently stored patterns
    p->iWordPerm = p->iWordStart;
    p->iPatsPerm += nPats;
    assert( p->iWordPerm == FRAIG_NUM_WORDS( p->iPatsPerm ) );

    // resimulate and recompute the hash values
    for ( i = 1; i < p->vNodes->nSize; i++ )
        if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) )
        {
            p->vNodes->pArray[i]->uHashD = 0;
            Fraig_NodeSimulate( p->vNodes->pArray[i], 0, p->iWordPerm, 0 );
        }

    // double-check that the nodes are still distinguished
    if ( fPerformChecks )
        Fraig_FeedBackCheckTable( p );

    // rehash the values in the F0 table
    if ( p->fDoSparse ) 
    {
        Fraig_TableRehashF0( p, 0 );
        if ( fPerformChecks )
            Fraig_FeedBackCheckTableF0( p );
    }

    // check if we need to resize the simulation info
    // if less than FRAIG_WORDS_STORE words are left, reallocate simulation info
    if ( p->iWordPerm + FRAIG_WORDS_STORE > p->nWordsDyna )
        Fraig_ReallocateSimulationInfo( p );

    // set the real patterns
    Msat_IntVecClear( p->vPatsReal );
    memset( p->pSimsReal, 0, sizeof(unsigned)*p->nWordsDyna );
    for ( w = 0; w < p->iWordPerm; w++ )
        p->pSimsReal[w] = FRAIG_FULL;
    if ( p->iPatsPerm % 32 > 0 )
        p->pSimsReal[p->iWordPerm-1] = FRAIG_MASK( p->iPatsPerm % 32 );
//    printf( "The number of permanent words = %d.\n", p->iWordPerm );
    return p->iWordStart;
}

void Fraig_FeedBackInit

(

Fraig_Man_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Initializes the feedback information.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file fraigFeed.c.

{
    p->vCones    = Fraig_NodeVecAlloc( 500 );
    p->vPatsReal = Msat_IntVecAlloc( 1000 ); 
    p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
    memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna );
    p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
    p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
}

void Fraig_FeedBackTest

(

Fraig_Man_t *

p

)

int Fraig_FindFirstDiff	(	Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	fCompl,
		int	iWordLast,
		int	fUseRand
	)

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

Synopsis [Find the number of the different pattern.]

Description [Returns -1 if there is no such pattern]

SideEffects []

SeeAlso []

Definition at line 390 of file fraigTable.c.

{
    int i, v;
    assert( !Fraig_IsComplement(pNode1) );
    assert( !Fraig_IsComplement(pNode2) );
    // take into account possible internal complementation
    fCompl ^= pNode1->fInv;
    fCompl ^= pNode2->fInv;
    // find the pattern
    if ( fCompl )
    {
        if ( fUseRand )
        {
            for ( i = 0; i < iWordLast; i++ )
                if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] )
                    for ( v = 0; v < 32; v++ )
                        if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) )
                            return i * 32 + v;
        }
        else
        {
            for ( i = 0; i < iWordLast; i++ )
                if ( pNode1->puSimD[i] !=  ~pNode2->puSimD[i] )
                    for ( v = 0; v < 32; v++ )
                        if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) )
                            return i * 32 + v;
        }
    }
    else
    {
        if ( fUseRand )
        {
            for ( i = 0; i < iWordLast; i++ )
                if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
                    for ( v = 0; v < 32; v++ )
                        if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
                            return i * 32 + v;
        }
        else
        {
            for ( i = 0; i < iWordLast; i++ )
                if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
                    for ( v = 0; v < 32; v++ )
                        if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
                            return i * 32 + v;
        }
    }
    return -1;
}

Fraig_HashTable_t* Fraig_HashTableCreate

(

int

nSize

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraigTable.c.

{
    Fraig_HashTable_t * p;
    // allocate the table
    p = ABC_ALLOC( Fraig_HashTable_t, 1 );
    memset( p, 0, sizeof(Fraig_HashTable_t) );
    // allocate and clean the bins
    p->nBins = Abc_PrimeCudd(nSize);
    p->pBins = ABC_ALLOC( Fraig_Node_t *, p->nBins );
    memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins );
    return p;
}

void Fraig_HashTableFree

(

Fraig_HashTable_t *

p

)

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

Synopsis [Deallocates the supergate hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file fraigTable.c.

{
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}

void Fraig_HashTableInsertF0	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis [Insert the entry in the functional hash table.]

Description [Unconditionally add the node to the corresponding linked list in the table.]

SideEffects []

SeeAlso []

Definition at line 237 of file fraigTable.c.

{
    Fraig_HashTable_t * p = pMan->pTableF0;
    unsigned Key = pNode->uHashD % p->nBins;

    pNode->pNextF = p->pBins[Key];
    p->pBins[Key] = pNode;
    p->nEntries++;
}

Fraig_Node_t* Fraig_HashTableLookupF	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis [Insert the entry in the functional hash table.]

Description [If the entry with the same key exists, return it right away. If the entry with the same key does not exists, inserts it and returns NULL. ]

SideEffects []

SeeAlso []

Definition at line 136 of file fraigTable.c.

{
    Fraig_HashTable_t * p = pMan->pTableF;
    Fraig_Node_t * pEnt, * pEntD;
    unsigned Key;

    // go through the hash table entries
    Key = pNode->uHashR % p->nBins;
    Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
    {
        // if their simulation info differs, skip
        if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->nWordsRand, 1 ) )
            continue;
        // equivalent up to the complement
        Fraig_TableBinForEachEntryD( pEnt, pEntD )
        {
            // if their simulation info differs, skip
            if ( !Fraig_CompareSimInfo( pNode, pEntD, pMan->iWordStart, 0 ) )
                continue;
            // found a simulation-equivalent node
            return pEntD; 
        }
        // did not find a simulation equivalent node
        // add the node to the corresponding linked list
        pNode->pNextD = pEnt->pNextD;
        pEnt->pNextD  = pNode;
        // return NULL, because there is no functional equivalence in this case
        return NULL;
    }

    // check if it is a good time for table resizing
    if ( p->nEntries >= 2 * p->nBins )
    {
        Fraig_TableResizeF( p, 1 );
        Key = pNode->uHashR % p->nBins;
    }

    // add the node to the corresponding linked list in the table
    pNode->pNextF = p->pBins[Key];
    p->pBins[Key] = pNode;
    p->nEntries++;
    // return NULL, because there is no functional equivalence in this case
    return NULL;
}

Fraig_Node_t* Fraig_HashTableLookupF0	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis [Insert the entry in the functional hash table.]

Description [If the entry with the same key exists, return it right away. If the entry with the same key does not exists, inserts it and returns NULL. ]

SideEffects []

SeeAlso []

Definition at line 193 of file fraigTable.c.

{
    Fraig_HashTable_t * p = pMan->pTableF0;
    Fraig_Node_t * pEnt;
    unsigned Key;

    // go through the hash table entries
    Key = pNode->uHashD % p->nBins;
    Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
    {
        // if their simulation info differs, skip
        if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->iWordStart, 0 ) )
            continue;
        // found a simulation-equivalent node
        return pEnt; 
    }

    // check if it is a good time for table resizing
    if ( p->nEntries >= 2 * p->nBins )
    {
        Fraig_TableResizeF( p, 0 );
        Key = pNode->uHashD % p->nBins;
    }

    // add the node to the corresponding linked list in the table
    pNode->pNextF = p->pBins[Key];
    p->pBins[Key] = pNode;
    p->nEntries++;
    // return NULL, because there is no functional equivalence in this case
    return NULL;
}

int Fraig_HashTableLookupS	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2,
		Fraig_Node_t **	ppNodeRes
	)

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

Synopsis [Looks up an entry in the structural hash table.]

Description [If the entry with the same children does not exists, creates it, inserts it into the table, and returns 0. If the entry with the same children exists, finds it, and return 1. In both cases, the new/old entry is returned in ppNodeRes.]

SideEffects []

SeeAlso []

Definition at line 90 of file fraigTable.c.

{
    Fraig_HashTable_t * p = pMan->pTableS;
    Fraig_Node_t * pEnt;
    unsigned Key;

    // order the arguments
    if ( Fraig_Regular(p1)->Num > Fraig_Regular(p2)->Num )
        pEnt = p1, p1 = p2, p2 = pEnt;

    Key = Fraig_HashKey2( p1, p2, p->nBins );
    Fraig_TableBinForEachEntryS( p->pBins[Key], pEnt )
        if ( pEnt->p1 == p1 && pEnt->p2 == p2 )
        {
            *ppNodeRes = pEnt;
            return 1;
        }
    // check if it is a good time for table resizing
    if ( p->nEntries >= 2 * p->nBins )
    {
        Fraig_TableResizeS( p );
        Key = Fraig_HashKey2( p1, p2, p->nBins );
    }
    // create the new node
    pEnt = Fraig_NodeCreate( pMan, p1, p2 );
    // add the node to the corresponding linked list in the table
    pEnt->pNextS = p->pBins[Key];
    p->pBins[Key] = pEnt;
    *ppNodeRes = pEnt;
    p->nEntries++;
    return 0;
}

int* Fraig_ManAllocCounterExample

(

Fraig_Man_t *

p

)

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

Synopsis [Generated trivial counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 787 of file fraigFeed.c.

{
    int * pModel;
    pModel = ABC_ALLOC( int, p->vInputs->nSize );
    memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
    return pModel;
}

int Fraig_ManCountExors

(

Fraig_Man_t *

pMan

)

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

Synopsis [Counts the number of EXOR type nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 742 of file fraigUtil.c.

{
    int i, nExors;
    nExors = 0;
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
        nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] );
    return nExors;

}

int Fraig_ManCountMuxes

(

Fraig_Man_t *

pMan

)

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

Synopsis [Counts the number of EXOR type nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 763 of file fraigUtil.c.

{
    int i, nMuxes;
    nMuxes = 0;
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
        nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] );
    return nMuxes;

}

void Fraig_ManCreateSolver

(

Fraig_Man_t *

p

)

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

Synopsis [Prepares the SAT solver to run on the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file fraigMan.c.

{
    extern abctime timeSelect;
    extern abctime timeAssign;
    assert( p->pSat == NULL );
    // allocate data for SAT solving
    p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
    p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
    p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
    p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
    timeSelect = 0;
    timeAssign = 0;
}

void Fraig_ManIncrementTravId

(

Fraig_Man_t *

pMan

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 980 of file fraigUtil.c.

{
    pMan->nTravIds2++;
}

int* Fraig_ManSaveCounterExample	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode
	)

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

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 860 of file fraigFeed.c.

{
    int * pModel;
    int iPattern;
    int i, fCompl;

    // the node can be complemented
    fCompl = Fraig_IsComplement(pNode);
    // because we compare with constant 0, p->pConst1 should also be complemented
    fCompl = !fCompl;

    // derive the model
    pModel = Fraig_ManAllocCounterExample( p );
    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 );
    if ( iPattern >= 0 )
    {
        for ( i = 0; i < p->vInputs->nSize; i++ )
            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
                pModel[i] = 1;
/*
printf( "SAT solver's pattern:\n" );
for ( i = 0; i < p->vInputs->nSize; i++ )
    printf( "%d", pModel[i] );
printf( "\n" );
*/
        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
        return pModel;
    }
    iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 );
    if ( iPattern >= 0 )
    {
        for ( i = 0; i < p->vInputs->nSize; i++ )
            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
                pModel[i] = 1;
/*
printf( "SAT solver's pattern:\n" );
for ( i = 0; i < p->vInputs->nSize; i++ )
    printf( "%d", pModel[i] );
printf( "\n" );
*/
        assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
        return pModel;
    }
    ABC_FREE( pModel );
    return NULL;
}

void Fraig_ManSelectBestChoice

(

Fraig_Man_t *

p

)

char* Fraig_MemFixedEntryFetch

(

Fraig_MemFixed_t *

p

)

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

Synopsis [Extracts one entry from the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file fraigMem.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 Fraig_MemFixedEntryRecycle	(	Fraig_MemFixed_t *	p,
		char *	pEntry
	)

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

Synopsis [Returns one entry into the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file fraigMem.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 Fraig_MemFixedReadMemUsage

(

Fraig_MemFixed_t *

p

)

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

Synopsis [Reports the memory usage.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file fraigMem.c.

{
    return p->nMemoryAlloc;
}

void Fraig_MemFixedRestart

(

Fraig_MemFixed_t *

p

)

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

Synopsis [Frees all associated memory and resets the manager.]

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

SideEffects []

SeeAlso []

Definition at line 202 of file fraigMem.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;
}

Fraig_MemFixed_t* Fraig_MemFixedStart

(

int

nEntrySize

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts the internal memory manager.]

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

SideEffects []

SeeAlso []

Definition at line 63 of file fraigMem.c.

{
    Fraig_MemFixed_t * p;

    p = ABC_ALLOC( Fraig_MemFixed_t, 1 );
    memset( p, 0, sizeof(Fraig_MemFixed_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 Fraig_MemFixedStop	(	Fraig_MemFixed_t *	p,
		int	fVerbose
	)

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

Synopsis [Stops the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file fraigMem.c.

{
    int i;
    if ( p == NULL )
        return;
    if ( fVerbose )
    {
        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
            p->nEntrySize, p->nChunkSize, p->nChunks );
        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
    }
    for ( i = 0; i < p->nChunks; i++ )
        ABC_FREE( p->pChunks[i] );
    ABC_FREE( p->pChunks );
    ABC_FREE( p );
}

void Fraig_NodeAddFaninFanout	(	Fraig_Node_t *	pFanin,
		Fraig_Node_t *	pFanout
	)

DECLARATIONS ///.

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

FileName [fraigFanout.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Procedures to manipulate fanouts of the FRAIG nodes.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigFanout.c,v 1.5 2005/07/08 01:01:31 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Add the fanout to the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fraigFanout.c.

{
    Fraig_Node_t * pPivot;

    // pFanins is a fanin of pFanout
    assert( !Fraig_IsComplement(pFanin) );
    assert( !Fraig_IsComplement(pFanout) );
    assert( Fraig_Regular(pFanout->p1) == pFanin || Fraig_Regular(pFanout->p2) == pFanin );

    pPivot = pFanin->pFanPivot;
    if ( pPivot == NULL )
    {
        pFanin->pFanPivot = pFanout;
        return;
    }

    if ( Fraig_Regular(pPivot->p1) == pFanin )
    {
        if ( Fraig_Regular(pFanout->p1) == pFanin )
        {
            pFanout->pFanFanin1 = pPivot->pFanFanin1;
            pPivot->pFanFanin1  = pFanout;
        }
        else // if ( Fraig_Regular(pFanout->p2) == pFanin )
        {
            pFanout->pFanFanin2 = pPivot->pFanFanin1;
            pPivot->pFanFanin1  = pFanout;
        }
    }
    else // if ( Fraig_Regular(pPivot->p2) == pFanin )
    {
        assert( Fraig_Regular(pPivot->p2) == pFanin );
        if ( Fraig_Regular(pFanout->p1) == pFanin )
        {
            pFanout->pFanFanin1 = pPivot->pFanFanin2;
            pPivot->pFanFanin2  = pFanout;
        }
        else // if ( Fraig_Regular(pFanout->p2) == pFanin )
        {
            pFanout->pFanFanin2 = pPivot->pFanFanin2;
            pPivot->pFanFanin2  = pFanout;
        }
    }
}

Fraig_Node_t* Fraig_NodeAndCanon	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

FUNCTION DEFINITIONS ///.

FUNCTION DEFINITIONS ///.

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

FileName [fraigCanon.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [AND-node creation and elementary AND-operation.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigCanon.c,v 1.4 2005/07/08 01:01:31 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [The internal AND operation for the two FRAIG nodes.]

Description [This procedure is the core of the FRAIG package, because it performs the two-step canonicization of FRAIG nodes. The first step involves the lookup in the structural hash table (which hashes two ANDs into a node that has them as fanins, if such a node exists). If the node is not found in the structural hash table, an attempt is made to find a functionally equivalent node in another hash table (which hashes the simulation info into the nodes, which has this simulation info). Some tricks used on the way are described in the comments to the code and in the paper "FRAIGs: Functionally reduced AND-INV graphs".]

SideEffects []

SeeAlso []

Definition at line 52 of file fraigCanon.c.

{
    Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
    int fUseSatCheck;
//    int RetValue;

    // check for trivial cases
    if ( p1 == p2 )
        return p1;
    if ( p1 == Fraig_Not(p2) )
        return Fraig_Not(pMan->pConst1);
    if ( Fraig_NodeIsConst(p1) )
    {
        if ( p1 == pMan->pConst1 )
            return p2;
        return Fraig_Not(pMan->pConst1);
    }
    if ( Fraig_NodeIsConst(p2) )
    {
        if ( p2 == pMan->pConst1 )
            return p1;
        return Fraig_Not(pMan->pConst1);
    }
/*
    // check for less trivial cases
    if ( Fraig_IsComplement(p1) )
    {
        if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p1), p2 ) )
        {
            if ( RetValue == -1 )
                pMan->nImplies0++;
            else
                pMan->nImplies1++;

            if ( RetValue == -1 )
                return p2;
        }
    }
    else
    {
        if ( RetValue = Fraig_NodeIsInSupergate( p1, p2 ) )
        {
            if ( RetValue == 1 )
                pMan->nSimplifies1++;
            else
                pMan->nSimplifies0++;

            if ( RetValue == 1 )
                return p1;
            return Fraig_Not(pMan->pConst1);
        }
    }
 
    if ( Fraig_IsComplement(p2) )
    {
        if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p2), p1 ) )
        {
            if ( RetValue == -1 )
                pMan->nImplies0++;
            else
                pMan->nImplies1++;

            if ( RetValue == -1 )
                return p1;
        }
    }
    else
    {
        if ( RetValue = Fraig_NodeIsInSupergate( p2, p1 ) )
        {
            if ( RetValue == 1 )
                pMan->nSimplifies1++;
            else
                pMan->nSimplifies0++;

            if ( RetValue == 1 )
                return p2;
            return Fraig_Not(pMan->pConst1);
        }
    }
*/
    // perform level-one structural hashing
    if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
    {
        // if the existent node is part of the cone of unused logic
        // (that is logic feeding the node which is equivalent to the given node)
        // return the canonical representative of this node
        // determine the phase of the given node, with respect to its canonical form
        pNodeRepr = Fraig_Regular(pNodeNew)->pRepr;
        if ( pMan->fFuncRed && pNodeRepr )
            return Fraig_NotCond( pNodeRepr, Fraig_IsComplement(pNodeNew) ^ Fraig_NodeComparePhase(Fraig_Regular(pNodeNew), pNodeRepr) );
        // otherwise, the node is itself a canonical representative, return it
        return pNodeNew;
    }
    // the same node is not found, but the new one is created

    // if one level hashing is requested (without functionality hashing), return
    if ( !pMan->fFuncRed )
        return pNodeNew;

    // check if the new node is unique using the simulation info
    if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 )
    {
        pMan->nSatZeros++;
        if ( !pMan->fDoSparse ) // if we do not do sparse functions, skip
            return pNodeNew;
        // check the sparse function simulation hash table
        pNodeOld = Fraig_HashTableLookupF0( pMan, pNodeNew );
        if ( pNodeOld == NULL ) // the node is unique (it is added to the table)
            return pNodeNew;
    }
    else
    {
        // check the simulation hash table
        pNodeOld = Fraig_HashTableLookupF( pMan, pNodeNew );
        if ( pNodeOld == NULL ) // the node is unique
            return pNodeNew;
    }
    assert( pNodeOld->pRepr == 0 );
    // there is another node which looks the same according to simulation

    // use SAT to resolve the ambiguity
    fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); 
    if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
    {
        // set the node to be equivalent with this node
        // to prevent loops, only set if the old node is not in the TFI of the new node
        // the loop may happen in the following case: suppose 
        // NodeC = AND(NodeA, NodeB) and at the same time NodeA => NodeB
        // in this case, NodeA and NodeC are functionally equivalent
        // however, NodeA is a fanin of node NodeC (this leads to the loop)
        // add the node to the list of equivalent nodes or dereference it
        if ( pMan->fChoicing && !Fraig_CheckTfi( pMan, pNodeOld, pNodeNew ) )
        { 
            // if the old node is not in the TFI of the new node and choicing 
            // is enabled, add the new node to the list of equivalent ones
            pNodeNew->pNextE = pNodeOld->pNextE;
            pNodeOld->pNextE = pNodeNew;
        }
        // set the canonical representative of this node
        pNodeNew->pRepr = pNodeOld;
        // return the equivalent node
        return Fraig_NotCond( pNodeOld, Fraig_NodeComparePhase(pNodeOld, pNodeNew) );
    }

    // now we add another member to this simulation class
    if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 )
    {
        Fraig_Node_t * pNodeTemp;
        assert( pMan->fDoSparse );
        pNodeTemp = Fraig_HashTableLookupF0( pMan, pNodeNew );
//        assert( pNodeTemp == NULL );
//        Fraig_HashTableInsertF0( pMan, pNodeNew );
    }
    else
    {
        pNodeNew->pNextD = pNodeOld->pNextD;
        pNodeOld->pNextD = pNodeNew;
    }
    // return the new node
    assert( pNodeNew->pRepr == 0 );
    return pNodeNew;
}

int Fraig_NodeAndSimpleCase_rec	(	Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew
	)

int Fraig_NodeCountPis	(	Msat_IntVec_t *	vVars,
		int	nVarsPi
	)

int Fraig_NodeCountSuppVars	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode,
		int	fSuppStr
	)

Fraig_Node_t* Fraig_NodeCreate	(	Fraig_Man_t *	p,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

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

Synopsis [Creates a new node.]

Description [This procedure should be called to create the constant node and the PI nodes first.]

SideEffects []

SeeAlso []

Definition at line 160 of file fraigNode.c.

{
    Fraig_Node_t * pNode;
    abctime clk;

    // create the node
    pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
    memset( pNode, 0, sizeof(Fraig_Node_t) );

    // assign the children
    pNode->p1  = p1;  Fraig_Ref(p1);  Fraig_Regular(p1)->nRefs++;
    pNode->p2  = p2;  Fraig_Ref(p2);  Fraig_Regular(p2)->nRefs++;

    // assign the number and add to the array of nodes
    pNode->Num = p->vNodes->nSize;
    Fraig_NodeVecPush( p->vNodes,  pNode );

    // assign the PI number
    pNode->NumPi = -1;

    // compute the level of this node
    pNode->Level = 1 + Abc_MaxInt(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
    pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
    pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;

    // derive the simulation info 
clk = Abc_Clock();
    // allocate memory for the simulation info
    pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
    pNode->puSimD = pNode->puSimR + p->nWordsRand;
    // derive random simulation info
    pNode->uHashR = 0;
    Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 );
    // derive dynamic simulation info
    pNode->uHashD = 0;
    Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 );
    // count the number of ones in the random simulation info
    pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
    if ( pNode->fInv )
        pNode->nOnes = p->nWordsRand * 32 - pNode->nOnes;
    // add to the runtime of simulation
p->timeSims += Abc_Clock() - clk;

#ifdef FRAIG_ENABLE_FANOUTS
    // create the fanout info
    Fraig_NodeAddFaninFanout( Fraig_Regular(p1), pNode );
    Fraig_NodeAddFaninFanout( Fraig_Regular(p2), pNode );
#endif
    return pNode;
}

Fraig_Node_t* Fraig_NodeCreateConst

(

Fraig_Man_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraigNode.c.

{
    Fraig_Node_t * pNode;

    // create the node
    pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
    memset( pNode, 0, sizeof(Fraig_Node_t) );

    // assign the number and add to the array of nodes
    pNode->Num   = p->vNodes->nSize;
    Fraig_NodeVecPush( p->vNodes,  pNode );
    pNode->NumPi = -1;  // this is not a PI, so its number is -1
    pNode->Level =  0;  // just like a PI, it has 0 level
    pNode->nRefs =  1;  // it is a persistent node, which comes referenced
    pNode->fInv  =  1;  // the simulation info is complemented

    // create the simulation info
    pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
    pNode->puSimD = pNode->puSimR + p->nWordsRand;
    memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand );
    memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );

    // count the number of ones in the simulation vector
    pNode->nOnes = p->nWordsRand * sizeof(unsigned) * 8;

    // insert it into the hash table
    Fraig_HashTableLookupF0( p, pNode );
    return pNode;
}

Fraig_Node_t* Fraig_NodeCreatePi

(

Fraig_Man_t *

p

)

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

Synopsis [Creates a primary input node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file fraigNode.c.

{
    Fraig_Node_t * pNode, * pNodeRes;
    int i;
    abctime clk;

    // create the node
    pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
    memset( pNode, 0, sizeof(Fraig_Node_t) );
    pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
    pNode->puSimD = pNode->puSimR + p->nWordsRand;
    memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );

    // assign the number and add to the array of nodes
    pNode->Num   = p->vNodes->nSize;
    Fraig_NodeVecPush( p->vNodes,  pNode );

    // assign the PI number and add to the array of primary inputs
    pNode->NumPi = p->vInputs->nSize;   
    Fraig_NodeVecPush( p->vInputs, pNode );

    pNode->Level =  0;  // PI has 0 level
    pNode->nRefs =  1;  // it is a persistent node, which comes referenced
    pNode->fInv  =  0;  // the simulation info of the PI is not complemented

    // derive the simulation info for the new node
clk = Abc_Clock();
    // set the random simulation info for the primary input
    pNode->uHashR = 0;
    for ( i = 0; i < p->nWordsRand; i++ )
    {
        // generate the simulation info
        pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
        // for reasons that take very long to explain, it makes sense to have (0000000...) 
        // pattern in the set (this helps if we need to return the counter-examples)
        if ( i == 0 )
            pNode->puSimR[i] <<= 1;
        // compute the hash key
        pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
    }
    // count the number of ones in the simulation vector
    pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );

    // set the systematic simulation info for the primary input
    pNode->uHashD = 0;
    for ( i = 0; i < p->iWordStart; i++ )
    {
        // generate the simulation info
        pNode->puSimD[i] = FRAIG_RANDOM_UNSIGNED;
        // compute the hash key
        pNode->uHashD ^= pNode->puSimD[i] * s_FraigPrimes[i];
    }
p->timeSims += Abc_Clock() - clk;

    // insert it into the hash table
    pNodeRes = Fraig_HashTableLookupF( p, pNode );
    assert( pNodeRes == NULL );
    // add to the runtime of simulation
    return pNode;
}

int Fraig_NodeGetFanoutNum

(

Fraig_Node_t *

pNode

)

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

Synopsis [Returns the number of fanouts of a node.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file fraigFanout.c.

{
    Fraig_Node_t * pFanout;
    int Counter = 0;
    Fraig_NodeForEachFanout( pNode, pFanout )
        Counter++;
    return Counter;
}

int Fraig_NodeIsExor

(

Fraig_Node_t *

pNode

)

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

Synopsis [Returns 1 if the node is EXOR, 0 if it is NEXOR.]

Description [The node should be EXOR type and not complemented.]

SideEffects []

SeeAlso []

Definition at line 633 of file fraigUtil.c.

{
    Fraig_Node_t * pNode1;
    assert( !Fraig_IsComplement(pNode) );
    assert( Fraig_NodeIsExorType(pNode) );
    assert( Fraig_IsComplement(pNode->p1) );
    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2);
}

int Fraig_NodeIsExorType

(

Fraig_Node_t *

pNode

)

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

Synopsis [Returns 1 if the node is the root of EXOR/NEXOR gate.]

Description [The node can be complemented.]

SideEffects []

SeeAlso []

Definition at line 558 of file fraigUtil.c.

{
    Fraig_Node_t * pNode1, * pNode2;
    // make the node regular (it does not matter for EXOR/NEXOR)
    pNode = Fraig_Regular(pNode);
    // if the node or its children are not ANDs or not compl, this cannot be EXOR type
    if ( !Fraig_NodeIsAnd(pNode) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
        return 0;

    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    assert( pNode1->Num < pNode2->Num );

    // compare grandchildren
    return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2);
}

int Fraig_NodeIsImplication	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew,
		int	nBTLimit
	)

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

Synopsis [Checks whether pOld => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 551 of file fraigSat.c.

{
    int RetValue, RetValue1, i, fComp;
    abctime clk;
    int fVerbose = 0;

    // make sure the nodes are not complemented
    assert( !Fraig_IsComplement(pNew) );
    assert( !Fraig_IsComplement(pOld) );
    assert( pNew != pOld );

    p->nSatCallsImp++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    // make sure the SAT solver has enough variables
    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );

   // get the logic cone
clk = Abc_Clock();
    Fraig_OrderVariables( p, pOld, pNew );
//    Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += Abc_Clock() - clk;

if ( fVerbose )
    printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );


    // get the complemented attribute
    fComp = Fraig_NodeComparePhase( pOld, pNew );
//Msat_SolverPrintClauses( p->pSat );

    ////////////////////////////////////////////
    // prepare the solver to run incrementally on these variables
//clk = Abc_Clock();
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += Abc_Clock() - clk;

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
    // run the solver
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
p->timeSat += Abc_Clock() - clk;

    if ( RetValue1 == MSAT_FALSE )
    {
//p->time1 += Abc_Clock() - clk;

if ( fVerbose )
{
//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}

        // add the clause
        Msat_IntVecClear( p->vProj );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
        assert( RetValue );
//        p->nSatProofImp++;
        return 1;
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
//p->time2 += Abc_Clock() - clk;

if ( fVerbose )
{
//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
        // record the counter example
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
        p->nSatCounterImp++;
        return 0;
    }
    else // if ( RetValue1 == MSAT_UNKNOWN )
    {
p->time3 += Abc_Clock() - clk;
        p->nSatFailsImp++;
        return 0;
    }
}

int Fraig_NodeIsInSupergate	(	Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew
	)

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

Synopsis [Checks if pNew exists among the implication fanins of pOld.]

Description [If pNew is an implication fanin of pOld, returns 1. If Fraig_Not(pNew) is an implication fanin of pOld, return -1. Otherwise returns 0.]

SideEffects []

SeeAlso []

Definition at line 905 of file fraigUtil.c.

{
    int RetValue1, RetValue2;
    if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) )
        return (pOld == pNew)? 1 : -1;
    if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) )
        return 0;
    RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew );
    RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew );
    if ( RetValue1 == -1 || RetValue2 == -1 )
        return -1;
    if ( RetValue1 ==  1 || RetValue2 ==  1 )
        return 1;
    return 0;
}

int Fraig_NodeIsMuxType

(

Fraig_Node_t *

pNode

)

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

Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

Description [The node can be complemented.]

SideEffects []

SeeAlso []

Definition at line 591 of file fraigUtil.c.

{
    Fraig_Node_t * pNode1, * pNode2;

    // make the node regular (it does not matter for EXOR/NEXOR)
    pNode = Fraig_Regular(pNode);
    // if the node or its children are not ANDs or not compl, this cannot be EXOR type
    if ( !Fraig_NodeIsAnd(pNode) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
        return 0;

    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    assert( pNode1->Num < pNode2->Num );

    // compare grandchildren
    // node is an EXOR/NEXOR
    if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) )
        return 1; 

    // otherwise the node is MUX iff it has a pair of equal grandchildren
    return pNode1->p1 == Fraig_Not(pNode2->p1) || 
           pNode1->p1 == Fraig_Not(pNode2->p2) ||
           pNode1->p2 == Fraig_Not(pNode2->p1) ||
           pNode1->p2 == Fraig_Not(pNode2->p2);
}

int Fraig_NodeIsTravIdCurrent	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1012 of file fraigUtil.c.

{
    return pNode->TravId2 == pMan->nTravIds2;
}

int Fraig_NodeIsTravIdPrevious	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1028 of file fraigUtil.c.

{
    return pNode->TravId2 == pMan->nTravIds2 - 1;
}

Fraig_Node_t* Fraig_NodeRecognizeMux	(	Fraig_Node_t *	pNode,
		Fraig_Node_t **	ppNodeT,
		Fraig_Node_t **	ppNodeE
	)

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

Synopsis [Recognizes what nodes are control and data inputs of a MUX.]

Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]

SideEffects []

SeeAlso []

Definition at line 658 of file fraigUtil.c.

{
    Fraig_Node_t * pNode1, * pNode2;
    assert( !Fraig_IsComplement(pNode) );
    assert( Fraig_NodeIsMuxType(pNode) );
    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    // find the control variable
    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p1;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p2;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p1;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p2;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p2;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p2;
        }
    }
    assert( 0 ); // this is not MUX
    return NULL;
}

void Fraig_NodeRemoveFaninFanout	(	Fraig_Node_t *	pFanin,
		Fraig_Node_t *	pFanoutToRemove
	)

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

Synopsis [Add the fanout to the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file fraigFanout.c.

{
    Fraig_Node_t * pFanout, * pFanout2, ** ppFanList;
    // start the linked list of fanouts
    ppFanList = &pFanin->pFanPivot; 
    // go through the fanouts
    Fraig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 )
    {
        // skip the fanout-to-remove
        if ( pFanout == pFanoutToRemove )
            continue;
        // add useful fanouts to the list
        *ppFanList = pFanout;
        ppFanList = Fraig_NodeReadNextFanoutPlace( pFanin, pFanout );
    }
    *ppFanList = NULL;
}

int Fraig_NodesCompareSupps	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew
	)

void Fraig_NodeSetTravIdCurrent	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 996 of file fraigUtil.c.

{
    pNode->TravId2 = pMan->nTravIds2;
}

int Fraig_NodeSimsContained	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2
	)

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

Synopsis [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.]

Description []

SideEffects []

SeeAlso []

Definition at line 784 of file fraigUtil.c.

{
    unsigned * pUnsigned1, * pUnsigned2;
    int i;

    // compare random siminfo
    pUnsigned1 = pNode1->puSimR;
    pUnsigned2 = pNode2->puSimR;
    for ( i = 0; i < pMan->nWordsRand; i++ )
        if ( pUnsigned1[i] & ~pUnsigned2[i] )
            return 0;

    // compare systematic siminfo
    pUnsigned1 = pNode1->puSimD;
    pUnsigned2 = pNode2->puSimD;
    for ( i = 0; i < pMan->iWordStart; i++ )
        if ( pUnsigned1[i] & ~pUnsigned2[i] )
            return 0;

    return 1;
}

void Fraig_NodeSimulate	(	Fraig_Node_t *	pNode,
		int	iWordStart,
		int	iWordStop,
		int	fUseRand
	)

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

Synopsis [Simulates the node.]

Description [Simulates the random or dynamic simulation info through the node. Uses phases of the children to determine their real simulation info. Uses phase of the node to determine the way its simulation info is stored. The resulting info is guaranteed to be 0 for the first pattern.]

SideEffects [This procedure modified the hash value of the simulation info.]

SeeAlso []

Definition at line 226 of file fraigNode.c.

{
    unsigned * pSims, * pSims1, * pSims2;
    unsigned uHash;
    int fCompl, fCompl1, fCompl2, i;

    assert( !Fraig_IsComplement(pNode) );

    // get hold of the simulation information
    pSims  = fUseRand? pNode->puSimR                    : pNode->puSimD;
    pSims1 = fUseRand? Fraig_Regular(pNode->p1)->puSimR : Fraig_Regular(pNode->p1)->puSimD;
    pSims2 = fUseRand? Fraig_Regular(pNode->p2)->puSimR : Fraig_Regular(pNode->p2)->puSimD;

    // get complemented attributes of the children using their random info
    fCompl  = pNode->fInv;
    fCompl1 = Fraig_NodeIsSimComplement(pNode->p1);
    fCompl2 = Fraig_NodeIsSimComplement(pNode->p2);

    // simulate
    uHash = 0;
    if ( fCompl1 && fCompl2 )
    {
        if ( fCompl )
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (pSims1[i] | pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
        else
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = ~(pSims1[i] | pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
    }
    else if ( fCompl1 && !fCompl2 )
    {
        if ( fCompl )
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (pSims1[i] | ~pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
        else
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (~pSims1[i] & pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
    }
    else if ( !fCompl1 && fCompl2 )
    {
        if ( fCompl )
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (~pSims1[i] | pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
        else
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (pSims1[i] & ~pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
    }
    else // if ( !fCompl1 && !fCompl2 )
    {
        if ( fCompl )
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = ~(pSims1[i] & pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
        else
            for ( i = iWordStart; i < iWordStop; i++ )
            {
                pSims[i] = (pSims1[i] & pSims2[i]);
                uHash ^= pSims[i] * s_FraigPrimes[i];
            }
    }

    if ( fUseRand )
        pNode->uHashR ^= uHash;
    else
        pNode->uHashD ^= uHash;
}

void Fraig_NodeVecSortByRefCount

(

Fraig_NodeVec_t *

p

)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file fraigVec.c.

{
    qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
            (int (*)(const void *, const void *)) Fraig_NodeVecCompareRefCounts );
}

void Fraig_PrintBinary	(	FILE *	pFile,
		unsigned *	pSign,
		int	nBits
	)

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

Synopsis [Prints the bit string.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file fraigUtil.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)((pSign[w] & (1<<i)) > 0) );

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

void Fraig_TablePrintStatsF

(

Fraig_Man_t *

pMan

)

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

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 537 of file fraigTable.c.

{
    Fraig_HashTable_t * pT = pMan->pTableF;
    Fraig_Node_t * pNode;
    int i, Counter;

    printf( "Functional table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
    for ( i = 0; i < pT->nBins; i++ )
    {
        Counter = 0;
        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
            Counter++;
        if ( Counter > 1 )
            printf( "{%d} ", Counter );
    }
    printf( "\n" );
}

void Fraig_TablePrintStatsF0

(

Fraig_Man_t *

pMan

)

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

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 566 of file fraigTable.c.

{
    Fraig_HashTable_t * pT = pMan->pTableF0;
    Fraig_Node_t * pNode;
    int i, Counter;

    printf( "Zero-node table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
    for ( i = 0; i < pT->nBins; i++ )
    {
        Counter = 0;
        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
            Counter++;
        if ( Counter == 0 )
            continue;
/*
        printf( "\nBin = %4d :  Number of entries = %4d\n", i, Counter );
        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
            printf( "Node %5d. Hash = %10d.\n", pNode->Num, pNode->uHashD );
*/
    }
    printf( "\n" );
}

void Fraig_TablePrintStatsS

(

Fraig_Man_t *

pMan

)

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

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file fraigTable.c.

{
    Fraig_HashTable_t * pT = pMan->pTableS;
    Fraig_Node_t * pNode;
    int i, Counter;

    printf( "Structural table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
    for ( i = 0; i < pT->nBins; i++ )
    {
        Counter = 0;
        Fraig_TableBinForEachEntryS( pT->pBins[i], pNode )
            Counter++;
        if ( Counter > 1 )
        {
            printf( "%d ", Counter );
            if ( Counter > 50 )
                printf( "{%d} ", i );
        }
    }
    printf( "\n" );
}

int Fraig_TableRehashF0	(	Fraig_Man_t *	pMan,
		int	fLinkEquiv
	)

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

Synopsis [Rehashes the table after the simulation info has changed.]

Description [Assumes that the hash values have been updated after performing additional simulation. Rehashes the table using the new hash values. Uses pNextF to link the entries in the bins. Uses pNextD to link the entries with identical hash values. Returns 1 if the identical entries have been found. Note that identical hash values may mean that the simulation data is different.]

SideEffects []

SeeAlso []

Definition at line 604 of file fraigTable.c.

{
    Fraig_HashTable_t * pT = pMan->pTableF0;
    Fraig_Node_t ** pBinsNew;
    Fraig_Node_t * pEntF, * pEntF2, * pEnt, * pEntD2, * pEntN;
    int ReturnValue, Counter, i;
    unsigned Key;

    // allocate a new array of bins
    pBinsNew = ABC_ALLOC( Fraig_Node_t *, pT->nBins );
    memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins );

    // rehash the entries in the table
    // go through all the nodes in the F-lists (and possible in D-lists, if used)
    Counter = 0;
    ReturnValue = 0;
    for ( i = 0; i < pT->nBins; i++ )
        Fraig_TableBinForEachEntrySafeF( pT->pBins[i], pEntF, pEntF2 )
        Fraig_TableBinForEachEntrySafeD( pEntF, pEnt, pEntD2 )
        {
            // decide where to put entry pEnt
            Key = pEnt->uHashD % pT->nBins;
            if ( fLinkEquiv )
            {
                // go through the entries in the new bin
                Fraig_TableBinForEachEntryF( pBinsNew[Key], pEntN )
                {
                    // if they have different values skip
                    if ( pEnt->uHashD != pEntN->uHashD )
                        continue;
                    // they have the same hash value, add pEnt to the D-list pEnt3
                    pEnt->pNextD  = pEntN->pNextD;
                    pEntN->pNextD = pEnt;
                    ReturnValue = 1;
                    Counter++;
                    break;
                }
                if ( pEntN != NULL ) // already linked
                    continue;
                // we did not find equal entry
            }
            // link the new entry
            pEnt->pNextF  = pBinsNew[Key];
            pBinsNew[Key] = pEnt;
            pEnt->pNextD  = NULL;
            Counter++;
        }
    assert( Counter == pT->nEntries );
    // replace the table and the parameters
    ABC_FREE( pT->pBins );
    pT->pBins = pBinsNew;
    return ReturnValue;
}

Variable Documentation

int s_FraigPrimes[FRAIG_MAX_PRIMES]

DECLARATIONS ///.

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

FileName [fraigPrime.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [The table of the first 1000 primes.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigPrime.c,v 1.4 2005/07/08 01:01:32 alanmi Exp

]

Definition at line 30 of file fraigPrime.c.