sbdSim.c File Reference

#include "sbdInt.h"

Include dependency graph for sbdSim.c:

Go to the source code of this file.

Functions
void	Sbd_GiaSimRoundBack2 (Gia_Man_t *p)
	FUNCTION DEFINITIONS ///.
int	Sbd_GiaSatOne_rec (Gia_Man_t *p, Gia_Obj_t *pObj, int Value, int fFirst, int iPat)
int	Sbd_GiaSatOne (Gia_Man_t *p, Vec_Int_t *vPairs)
void	Sbd_GiaSimRoundBack (Gia_Man_t *p)
void	Sbd_GiaSimRound (Gia_Man_t *p, int fTry, Vec_Int_t **pvMap)
void	Sbd_GiaSimTest (Gia_Man_t *pGia)

Function Documentation

Sbd_GiaSatOne()

int Sbd_GiaSatOne	(	Gia_Man_t *	p,
		Vec_Int_t *	vPairs )

Definition at line 116 of file sbdSim.c.

{
    int k, n, Var1, Var2, iPat = 0;
    //Gia_ManSetPhase( p );
    Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k )
    {
        Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 );
        Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 );
        assert( Var2 > 0 );
        if ( Var1 == 0 )
        {
            for ( n = 0; n < 2; n++ )
            {
                Gia_ManIncrementTravId( p );
                if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
                {
                    iPat++;
                    break;
                }
            }
            printf( "%c", n == 2 ? '.' : 'c' );
        }
        else
        {
            for ( n = 0; n < 2; n++ )
            {
                Gia_ManIncrementTravId( p );
                if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) )
                {
                    iPat++;
                    break;
                }
                Gia_ManIncrementTravId( p );
                if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
                {
                    iPat++;
                    break;
                }
            }
            printf( "%c", n == 2 ? '.' : 'e' );
        }
        if ( iPat == 64 * p->iPatsPi - 1 )
            break;
    }
    printf( "\n" );
    return iPat;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_GiaSatOne_rec()

int Sbd_GiaSatOne_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int	Value,
		int	fFirst,
		int	iPat )

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

Synopsis [Tries to falsify a sequence of two-literal SAT problems.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file sbdSim.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return (int)pObj->fMark0 == Value;
    Gia_ObjSetTravIdCurrent(p, pObj);
    pObj->fMark0 = Value;
    if ( Gia_ObjIsCi(pObj) )
    {
        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
        if ( Abc_TtGetBit( pSims, iPat ) != Value )
            Abc_TtXorBit( pSims, iPat );
        return 1;
    }
    assert( Gia_ObjIsAnd(pObj) );
    assert( !Gia_ObjIsXor(pObj) );
    if ( Value )
        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) &&
               Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat );
    if ( fFirst )
        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat );
    else
        return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_GiaSimRound()

void Sbd_GiaSimRound	(	Gia_Man_t *	p,
		int	fTry,
		Vec_Int_t **	pvMap )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file sbdSim.c.

{
    int nWords = p->iPatsPi;
    Vec_Mem_t * vStore;
    Gia_Obj_t * pObj;
    Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) );
    int w, i, Id, fCompl, RetValue;
    // init primary inputs
    if ( fTry )
    {
        Sbd_GiaSimRoundBack( p );
        Gia_ManForEachCiId( p, Id, i )
            Sbd_ObjSims(p, Id)[0] <<= 1;
    }
    else
    {
        Gia_ManForEachCiId( p, Id, i )
            for ( w = 0; w < nWords; w++ )
                Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w;
    }
    // simulate internal nodes
    vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page
    Vec_MemHashAlloc( vStore, 1 << 16 );
    RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero
    assert( RetValue == 0 );
    Gia_ManForEachAnd( p, pObj, i )
    {
        word * pSims = Sbd_ObjSims(p, i);
        if ( Gia_ObjIsXor(pObj) )
            Abc_TtXor( pSims, 
                Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), 
                Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), 
                nWords, 
                Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
        else
            Abc_TtAndCompl( pSims, 
                Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj), 
                Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj), 
                nWords );
        // hash sim info
        fCompl = (int)(pSims[0] & 1);
        if ( fCompl ) Abc_TtNot( pSims, nWords );
        Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) );
        if ( fCompl ) Abc_TtNot( pSims, nWords );
    }
    Gia_ManForEachCo( p, pObj, i )
    {
        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
        Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) );
//        printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) );
        assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) );
    }
//    printf( "\n" );
    Vec_MemHashFree( vStore );
    Vec_MemFree( vStore );
    printf( "Objects = %6d.  Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) );
    if ( pvMap )
        *pvMap = vMap;
    else
        Vec_IntFree( vMap );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_GiaSimRoundBack()

void Sbd_GiaSimRoundBack

(

Gia_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file sbdSim.c.

{
    extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap );
    Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) );
    Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
    Vec_Int_t * vMap; // maps each node into its class
    int i, nConsts = 0, nClasses = 0, nPats;
    Sbd_GiaSimRound( p, 0, &vMap );
    Gia_ManForEachAndId( p, i )
    {
        if ( Vec_IntEntry(vMap, i) == 0 )
            Vec_IntPushTwo( vPairs, 0, i ), nConsts++;
        else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 )
            Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i );
        else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 )
        {
            Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i );
            Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 );
            nClasses++;
        }
    }
    Vec_IntFree( vMap );
    Vec_IntFree( vReprs );
    printf( "Constants = %d.   Classes = %d.\n", nConsts, nClasses );
 
    nPats = Sbd_GiaSatOne( p, vPairs );
    Vec_IntFree( vPairs );
 
    printf( "Generated %d patterns.\n", nPats );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_GiaSimRoundBack2()

void Sbd_GiaSimRoundBack2

(

Gia_Man_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [This does not work.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file sbdSim.c.

{
    int nWords = p->iPatsPi;
    Gia_Obj_t * pObj;
    int w, i, Id;
    // init primary outputs
    Gia_ManForEachCoId( p, Id, i )
        for ( w = 0; w < nWords; w++ )
            Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0);
    // transfer to nodes
    Gia_ManForEachCo( p, pObj, i )
    {
        word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
        Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) );
    }
    // simulate nodes
    Gia_ManForEachAndReverse( p, pObj, i )
    {
        word * pSims  = Sbd_ObjSims(p, i);
        word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i));
        word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i));
        word Rand = Gia_ManRandomW(0);
        for ( w = 0; w < nWords; w++ )
        {
            pSims0[w] = pSims[w] | Rand;
            pSims1[w] = pSims[w] | ~Rand;
        }
        if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords );
        if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords );
    }
    // primary inputs are initialized
}

Here is the call graph for this function:

Sbd_GiaSimTest()

void Sbd_GiaSimTest

(

Gia_Man_t *

pGia

)

Definition at line 278 of file sbdSim.c.

{
    Gia_ManSetPhase( pGia );
 
    // allocate simulation info
    pGia->iPatsPi = 32;
    pGia->vSims   = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
    pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
 
    Gia_ManRandom( 1 );
 
    Sbd_GiaSimRound( pGia, 0, NULL );
    Sbd_GiaSimRound( pGia, 0, NULL );
    Sbd_GiaSimRound( pGia, 0, NULL );
 
    printf( "\n" );
    Sbd_GiaSimRound( pGia, 1, NULL );
    printf( "\n" );
    Sbd_GiaSimRound( pGia, 1, NULL );
    printf( "\n" );
    Sbd_GiaSimRound( pGia, 1, NULL );
 
    Vec_WrdFreeP( &pGia->vSims );
    Vec_WrdFreeP( &pGia->vSimsPi );
}

Here is the call graph for this function: