giaSat.c File Reference

#include "gia.h"

Go to the source code of this file.

Data Structures
struct	Gia_ManSat_t_
struct	Gia_ObjSat1_t_
struct	Gia_ObjSat2_t_
struct	Gia_ObjSat_t_

Macros
#define	GIA_LIMIT   10
	DECLARATIONS ///. More...

Typedefs
typedef struct Gia_ManSat_t_	Gia_ManSat_t
typedef struct Gia_ObjSat1_t_	Gia_ObjSat1_t
typedef struct Gia_ObjSat2_t_	Gia_ObjSat2_t
typedef struct Gia_ObjSat_t_	Gia_ObjSat_t

Functions
Gia_ManSat_t *	Gia_ManSatStart ()
	FUNCTION DEFINITIONS ///. More...
void	Gia_ManSatStop (Gia_ManSat_t *p)
void	Gia_ManSatPartCollectSuper (Gia_Man_t *p, Gia_Obj_t *pObj, int *pLits, int *pnLits)
int	Gia_ManSatPartCreate_rec (Gia_Man_t *p, Gia_Obj_t *pObj, int *pObjPlace, int *pStore)
int	Gia_ManSatPartCreate (Gia_Man_t *p, Gia_Obj_t *pObj, int *pStore)
void	Gia_ManSatPartCountClauses (Gia_Man_t *p, Gia_Obj_t *pObj, int *pnOnset, int *pnOffset)
int	Gia_ManSatPartCount (Gia_Man_t *p, Gia_Obj_t *pObj, int *pnLeaves, int *pnNodes)
int	Gia_ManSatPartCountNodes (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManSatPartPrint (Gia_Man_t *p, Gia_Obj_t *pObj, int Step)
void	Gia_ManSatExperiment (Gia_Man_t *p)

Macro Definition Documentation

#define GIA_LIMIT   10

DECLARATIONS ///.

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

FileName [giaSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [New constraint-propagation procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 30 of file giaSat.c.

Typedef Documentation

typedef struct Gia_ManSat_t_ Gia_ManSat_t

Definition at line 33 of file giaSat.c.

typedef struct Gia_ObjSat1_t_ Gia_ObjSat1_t

Definition at line 39 of file giaSat.c.

typedef struct Gia_ObjSat2_t_ Gia_ObjSat2_t

Definition at line 48 of file giaSat.c.

typedef struct Gia_ObjSat_t_ Gia_ObjSat_t

Definition at line 55 of file giaSat.c.

Function Documentation

void Gia_ManSatExperiment

(

Gia_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file giaSat.c.

{
    int nStored, Storage[1000], * pStart; 
    Gia_ManSat_t * pMan;
    Gia_Obj_t * pObj;
    int i, nLevels, nLeaves, nNodes, nCount[2*GIA_LIMIT+2] = {0}, nCountAll = 0;
    int Num0 = 0, Num1 = 0;
    clock_t clk = clock();
    int nWords = 0, nWords2 = 0;
    pMan = Gia_ManSatStart();
    // mark the nodes to become roots of leaf-DAGs
    Gia_ManCreateValueRefs( p );
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
        else if ( Gia_ObjIsCi(pObj) )
            pObj->fMark0 = 1;
        else if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pObj->Value > 1 || Gia_ManSatPartCountNodes(p,pObj) >= GIA_LIMIT )
                pObj->fMark0 = 1;
        }
        pObj->Value = 0;
    }
    // compute the sizes of leaf-DAGs
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( pObj->fMark0 == 0 )
            continue;
        pObj->fMark0 = 0;

        nCountAll++;
        nStored = Gia_ManSatPartCreate( p, pObj, Storage );
        nWords2 += nStored;
        assert( nStored < 500 );
        pStart = (int *)Aig_MmFlexEntryFetch( pMan->pMem, sizeof(int) * nStored );
        memcpy( pStart, Storage, sizeof(int) * nStored );

        nLeaves = nNodes = 0;
        nLevels = 1+Gia_ManSatPartCount( p, pObj, &nLeaves, &nNodes );
        nWords += nLeaves + nNodes;
        if ( nNodes <= 2*GIA_LIMIT )
            nCount[nNodes]++;
        else
            nCount[2*GIA_LIMIT+1]++;
//        if ( nNodes > 10 && i % 100 == 0 )
//        if ( nNodes > 5 )
        if ( 0 )
        {
            Gia_ManSatPartCountClauses( p, pObj, &Num0, &Num1 );
            printf( "%8d :  And = %3d.  Lev = %2d. Clauses = %3d. (%3d + %3d).\n", i, nNodes, nLevels, Num0+Num1, Num0, Num1 );
            Gia_ManSatPartPrint( p, pObj, 0 );
            printf( "\n" );
        }

        pObj->fMark0 = 1;
    }
    printf( "\n" );
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = 0;
    Gia_ManSatStop( pMan );
    for ( i = 0; i < 2*GIA_LIMIT+2; i++ )
        printf( "%2d=%6d  %7.2f %%  %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) );
    ABC_PRMn( "MemoryEst", 4*nWords );
    ABC_PRMn( "MemoryReal", 4*nWords2 );
    printf( "%5.2f bpn  ", 4.0*nWords2/Gia_ManObjNum(p) );
    ABC_PRT( "Time", clock() - clk );
}

void Gia_ManSatPartCollectSuper	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pLits,
		int *	pnLits
	)

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

Synopsis [Collects the supergate rooted at this ]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 || Gia_ObjFaninC0(pObj) )
        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC0(pObj));
    else
        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 || Gia_ObjFaninC1(pObj) )
        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC1(pObj));
    else
        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
}

int Gia_ManSatPartCount	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pnLeaves,
		int *	pnNodes
	)

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

Synopsis [Count the number of internal nodes in the leaf-DAG.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    int Level0 = 0, Level1 = 0;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    (*pnNodes)++;
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        (*pnLeaves)++;
    else
        Level0 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC0(pObj);
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        (*pnLeaves)++;
    else
        Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
    return Abc_MaxInt( Level0, Level1 );
}

void Gia_ManSatPartCountClauses	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pnOnset,
		int *	pnOffset
	)

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

Synopsis [Count the number of internal nodes in the leaf-DAG.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    int nOnset0, nOnset1, nOffset0, nOffset1;
    assert( Gia_ObjIsAnd(pObj) );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        nOnset0 = 1, nOffset0 = 1;
    else
    {
        Gia_ManSatPartCountClauses(p, pFanin, &nOnset0, &nOffset0);
        if ( Gia_ObjFaninC0(pObj) )
        {
            int Temp = nOnset0;
            nOnset0 = nOffset0;
            nOffset0 = Temp;
        }
    }
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        nOnset1 = 1, nOffset1 = 1;
    else
    {
        Gia_ManSatPartCountClauses(p, pFanin, &nOnset1, &nOffset1);
        if ( Gia_ObjFaninC1(pObj) )
        {
            int Temp = nOnset1;
            nOnset1 = nOffset1;
            nOffset1 = Temp;
        }
    }
    *pnOnset  = nOnset0  * nOnset1;
    *pnOffset = nOffset0 + nOffset1;
}

int Gia_ManSatPartCountNodes	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Count the number of internal nodes in the leaf-DAG.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    int nNodes0 = 0, nNodes1 = 0;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( !(pFanin->fMark0) )
        nNodes0 = Gia_ManSatPartCountNodes(p, pFanin);
    pFanin = Gia_ObjFanin1(pObj);
    if ( !(pFanin->fMark0) )
        nNodes1 = Gia_ManSatPartCountNodes(p, pFanin);
    return nNodes0 + nNodes1 + 1;
}

int Gia_ManSatPartCreate	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pStore
	)

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

Synopsis [Creates part and returns the number of words used.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file giaSat.c.

{
    return 1 + Gia_ManSatPartCreate_rec( p, pObj, pStore, pStore + 1 );
}

int Gia_ManSatPartCreate_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pObjPlace,
		int *	pStore
	)

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

Synopsis [Returns the number of words used.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    int i, nWordsUsed, nSuperSize = 0, Super[2*GIA_LIMIT];
    // make sure this is a valid node
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    // collect inputs to the supergate
    Gia_ManSatPartCollectSuper( p, pObj, Super, &nSuperSize );
    assert( nSuperSize <= 2*GIA_LIMIT );
    // create the root entry
    *pObjPlace = 0;
    ((Gia_ObjSat1_t *)pObjPlace)->nFans   = Gia_Var2Lit( nSuperSize, 0 );
    ((Gia_ObjSat1_t *)pObjPlace)->nOffset = pStore - pObjPlace;
    nWordsUsed = nSuperSize;
    for ( i = 0; i < nSuperSize; i++ )
    {
        pFanin = Gia_ManObj( p, Gia_Lit2Var(Super[i]) );
        if ( pFanin->fMark0 )
        {
            ((Gia_ObjSat2_t *)(pStore + i))->fTerm = 1;
            ((Gia_ObjSat2_t *)(pStore + i))->iLit  = Super[i];
        }
        else
        {
            assert( Gia_LitIsCompl(Super[i]) );
            nWordsUsed += Gia_ManSatPartCreate_rec( p, pFanin, pStore + i, pStore + nWordsUsed );
        }
    }
    return nWordsUsed;
}

void Gia_ManSatPartPrint	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int	Step
	)

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

Synopsis [Count the number of internal nodes in the leaf-DAG.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file giaSat.c.

{
    Gia_Obj_t * pFanin;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        printf( "%s%d", Gia_ObjFaninC0(pObj)?"!":"", Gia_ObjId(p,pFanin) );
    else
    {
        if ( Gia_ObjFaninC0(pObj) )
            printf( "(" );
        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC0(pObj));
        if ( Gia_ObjFaninC0(pObj) )
            printf( ")" );
    }
    printf( "%s", (Step & 1)? " + " : "*" );
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        printf( "%s%d", Gia_ObjFaninC1(pObj)?"!":"", Gia_ObjId(p,pFanin) );
    else
    {
        if ( Gia_ObjFaninC1(pObj) )
            printf( "(" );
        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC1(pObj));
        if ( Gia_ObjFaninC1(pObj) )
            printf( ")" );
    }
}

Gia_ManSat_t* Gia_ManSatStart

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file giaSat.c.

{
    Gia_ManSat_t * p;
    p = ABC_CALLOC( Gia_ManSat_t, 1 );
    p->pMem = Aig_MmFlexStart();
    return p;
}

void Gia_ManSatStop

(

Gia_ManSat_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file giaSat.c.

{
    Aig_MmFlexStop( p->pMem, 0 );
    ABC_FREE( p );
}