fraigFeed.c File Reference

#include "fraigInt.h"

Include dependency graph for fraigFeed.c:

Go to the source code of this file.

Functions
void	Fraig_FeedBackInit (Fraig_Man_t *p)
	FUNCTION DEFINITIONS ///.
void	Fraig_FeedBack (Fraig_Man_t *p, int *pModel, Msat_IntVec_t *vVars, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int	Fraig_FeedBackCompress (Fraig_Man_t *p)
int *	Fraig_ManAllocCounterExample (Fraig_Man_t *p)
int	Fraig_ManSimulateBitNode_rec (Fraig_Man_t *p, Fraig_Node_t *pNode)
int	Fraig_ManSimulateBitNode (Fraig_Man_t *p, Fraig_Node_t *pNode, int *pModel)
int *	Fraig_ManSaveCounterExample (Fraig_Man_t *p, Fraig_Node_t *pNode)

Function Documentation

Fraig_FeedBack()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_FeedBackCompress()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_FeedBackInit()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManAllocCounterExample()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManSaveCounterExample()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManSimulateBitNode()

int Fraig_ManSimulateBitNode	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode,
		int *	pModel )

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

Synopsis [Simulates one bit.]

Description []

SideEffects []

SeeAlso []

Definition at line 832 of file fraigFeed.c.

{
    int fCompl, RetValue, i;
    // set the PI values
    Fraig_ManIncrementTravId( p );
    for ( i = 0; i < p->vInputs->nSize; i++ )
    {
        Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] );
        p->vInputs->pArray[i]->fMark3 = pModel[i];
    }
    // perform the traversal
    fCompl = Fraig_IsComplement(pNode);
    RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) );
    return fCompl ^ RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManSimulateBitNode_rec()

int Fraig_ManSimulateBitNode_rec	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode )

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

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 807 of file fraigFeed.c.

{
    int Value0, Value1;
    if ( Fraig_NodeIsTravIdCurrent( p, pNode ) )
        return pNode->fMark3;
    Fraig_NodeSetTravIdCurrent( p, pNode );
    Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) );
    Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) );
    Value0 ^= Fraig_IsComplement(pNode->p1);
    Value1 ^= Fraig_IsComplement(pNode->p2);
    pNode->fMark3 = Value0 & Value1;
    return pNode->fMark3;
}

Here is the call graph for this function:

Here is the caller graph for this function: