aigJust.c File Reference

#include "aig.h"

Go to the source code of this file.

Macros
#define	AIG_VAL0   1
	DECLARATIONS ///. More...
#define	AIG_VAL1   2
#define	AIG_VALX   3

Typedefs
typedef struct Aig_ManPack_t_	Aig_ManPack_t

Functions
static int	Aig_ObjSetTerValue (Aig_Obj_t *pNode, int Value)
static int	Aig_ObjGetTerValue (Aig_Obj_t *pNode)
static int	Aig_ObjNotTerValue (int Value)
static int	Aig_ObjAndTerValue (int Value0, int Value1)
static int	Aig_ObjNotCondTerValue (int Value, int Cond)
static int	Aig_ObjSatValue (Aig_Man_t *pAig, Aig_Obj_t *pNode, int fCompl)
	FUNCTION DEFINITIONS ///. More...
int	Aig_NtkFindSatAssign_rec (Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits, int Heur)
int	Aig_ObjFindSatAssign (Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits)
int	Aig_ObjTerSimulate_rec (Aig_Man_t *pAig, Aig_Obj_t *pNode)
int	Aig_ObjTerSimulate (Aig_Man_t *pAig, Aig_Obj_t *pNode, Vec_Int_t *vSuppLits)
Aig_ManPack_t *	Aig_ManPackStart (Aig_Man_t *pAig)
void	Aig_ManPackStop (Aig_ManPack_t *p)
void	Aig_ManPackAddPattern (Aig_ManPack_t *p, Vec_Int_t *vLits)
Vec_Int_t *	Aig_ManPackConstNodes (Aig_ManPack_t *p)
void	Aig_ManJustExperiment (Aig_Man_t *pAig)

Macro Definition Documentation

#define AIG_VAL0   1

DECLARATIONS ///.

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

FileName [aigJust.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Justification of node values.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

aigJust.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 30 of file aigJust.c.

#define AIG_VAL1   2

Definition at line 31 of file aigJust.c.

#define AIG_VALX   3

Definition at line 32 of file aigJust.c.

Typedef Documentation

typedef struct Aig_ManPack_t_ Aig_ManPack_t

Definition at line 234 of file aigJust.c.

Function Documentation

void Aig_ManJustExperiment

(

Aig_Man_t *

pAig

)

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

Synopsis [Testing of the framework.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file aigJust.c.

{
    Aig_ManPack_t * pPack;
    Vec_Int_t * vSuppLits, * vNodes;
    Aig_Obj_t * pObj;
    int i;
    abctime clk = Abc_Clock();
    int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
    int nTotalLits = 0;
    vSuppLits = Vec_IntAlloc( 100 );
    pPack = Aig_ManPackStart( pAig );
    vNodes = Aig_ManPackConstNodes( pPack );
//    Aig_ManForEachCo( pAig, pObj, i )
    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
    {
        if ( pObj->fPhase ) // const 1
        {
            if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) )
            {
//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 );
//                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
//                    printf( "Justification error!\n" );
                Count0++;
                nTotalLits += Vec_IntSize(vSuppLits);
                Aig_ManPackAddPattern( pPack, vSuppLits );
            }
            else
                Count0f++;
        }
        else
        {
            if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) )
            {
//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 );
//                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
//                    printf( "Justification error!\n" );
                Count1++;
                nTotalLits += Vec_IntSize(vSuppLits);
                Aig_ManPackAddPattern( pPack, vSuppLits );
            }
            else
                Count1f++;
        }
    }
    Vec_IntFree( vSuppLits );
    printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ", 
        Aig_ManCoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManCoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
    Abc_PrintTime( 1, "T", Abc_Clock() - clk );
    Aig_ManCleanMarkAB( pAig );
    Aig_ManPackStop( pPack );
    Vec_IntFree( vNodes );
}

void Aig_ManPackAddPattern	(	Aig_ManPack_t *	p,
		Vec_Int_t *	vLits
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file aigPack.c.

{
    int k;
    for ( k = 1; k < 64; k++ )
        if ( Aig_ManPackAddPatternTry( p, k, vLits ) )
            break;
    if ( k == 64 )
    {
/*
        word * pInfo, * pPres;
        int i, Lit;
        Vec_IntForEachEntry( vLits, Lit, i )
            printf( "%d", Abc_LitIsCompl(Lit) );
        printf( "\n\n" );
        for ( k = 1; k < 64; k++ )
        {
            Vec_IntForEachEntry( vLits, Lit, i )
            {
                pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
                pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
                if ( Abc_InfoHasBit( (unsigned *)pPres, k ) )
                    printf( "%d", Abc_InfoHasBit( (unsigned *)pInfo, k ) );
                else
                    printf( "-" );
            }
            printf( "\n" );
        }
*/
        p->nPatSkip++;
    }
    p->nPatTotal++;
}

Vec_Int_t* Aig_ManPackConstNodes

(

Aig_ManPack_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file aigPack.c.

{
    Vec_Int_t * vNodes;
    Aig_Obj_t * pObj;
    word Sign;
    int i;
    vNodes = Vec_IntAlloc( 1000 );
    Aig_ManForEachNode( p->pAig, pObj, i )
    {
        Sign  = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) );
        if ( Sign == 0 || ~Sign == 0 || Aig_Word6HasOneBit(Sign) || Aig_Word6HasOneBit(~Sign) )
            Vec_IntPush( vNodes, Aig_ObjId(pObj) );
    }
    return vNodes;
}

Aig_ManPack_t* Aig_ManPackStart

(

Aig_Man_t *

pAig

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file aigPack.c.

{
    Aig_ManPack_t * p;
    p = Aig_ManPackAlloc( pAig );
    Aig_ManPackSetRandom( p );
    Aig_ManPackSimulate( p );
    Aig_ManPackPrintStats( p );
    return p;
}

void Aig_ManPackStop

(

Aig_ManPack_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file aigPack.c.

{
    Aig_ManPackSimulate( p );
    Aig_ManPackPrintStats( p );
    Aig_ManPackFree( p );
}

int Aig_NtkFindSatAssign_rec	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pNode,
		int	Value,
		Vec_Int_t *	vSuppLits,
		int	Heur
	)

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

Synopsis [Recursively searched for a satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file aigJust.c.

{
    int Value0, Value1;
//    ++Heur;
    if ( Aig_ObjIsConst1(pNode) )
        return 1;
    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
        return ((int)pNode->fMarkA == Value);
    Aig_ObjSetTravIdCurrent(pAig, pNode);
    pNode->fMarkA = Value;
    if ( Aig_ObjIsCi(pNode) )
    {
//        if ( Aig_ObjId(pNode) % 1000 == 0 )
//            Value ^= 1;
        if ( vSuppLits )
            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
        return 1;
    }
    assert( Aig_ObjIsNode(pNode) );
    // propagation
    if ( Value ) 
    {
        if ( !Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), vSuppLits, Heur) )
            return 0;
        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), vSuppLits, Heur);
    }
    // justification
    Value0 = Aig_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
    if ( Value0 == AIG_VAL0 )
        return 1;
    Value1 = Aig_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
    if ( Value1 == AIG_VAL0 )
        return 1;
    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
        return 0;
    if ( Value0 == AIG_VAL1 )
        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
    if ( Value1 == AIG_VAL1 )
        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
    assert( Value0 == AIG_VALX && Value1 == AIG_VALX );
    // decision making
//    if ( rand() % 10 == Heur )
//    if ( Aig_ObjId(pNode) % 8 == Heur )
    if ( ++Heur % 8 == 0 )
        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
    else
        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
}

static int Aig_ObjAndTerValue ( int  Value0, int  Value1  )

inlinestatic

Definition at line 56 of file aigJust.c.

{
    if ( Value0 == AIG_VAL0 || Value1 == AIG_VAL0 )
        return AIG_VAL0;
    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
        return AIG_VAL1;
    return AIG_VALX;
}

int Aig_ObjFindSatAssign	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pNode,
		int	Value,
		Vec_Int_t *	vSuppLits
	)

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

Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file aigJust.c.

{
    int i;
    if ( Aig_ObjIsCo(pNode) )
        return Aig_ObjFindSatAssign( pAig, Aig_ObjFanin0(pNode), Value ^ Aig_ObjFaninC0(pNode), vSuppLits );
    for ( i = 0; i < 8; i++ )
    {
        Vec_IntClear( vSuppLits );
        Aig_ManIncrementTravId( pAig );
        if ( Aig_NtkFindSatAssign_rec( pAig, pNode, Value, vSuppLits, i ) )
            return 1;
    }
    return 0;
}

static int Aig_ObjGetTerValue ( Aig_Obj_t *  pNode )

inlinestatic

Definition at line 42 of file aigJust.c.

{
    return (pNode->fMarkB << 1) | pNode->fMarkA;
}

static int Aig_ObjNotCondTerValue ( int  Value, int  Cond  )

inlinestatic

Definition at line 64 of file aigJust.c.

{
    return Cond ? Aig_ObjNotTerValue( Value ) : Value;
}

static int Aig_ObjNotTerValue ( int  Value )

inlinestatic

Definition at line 48 of file aigJust.c.

{
    if ( Value == AIG_VAL1 )
        return AIG_VAL0;
    if ( Value == AIG_VAL0 )
        return AIG_VAL1;
    return AIG_VALX;
}

static int Aig_ObjSatValue ( Aig_Man_t *  pAig, Aig_Obj_t *  pNode, int  fCompl  )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns value (0 or 1) or X if unassigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file aigJust.c.

{
    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
        return (pNode->fMarkA ^ fCompl) ? AIG_VAL1 : AIG_VAL0;
    return AIG_VALX;
}

static int Aig_ObjSetTerValue ( Aig_Obj_t *  pNode, int  Value  )

inlinestatic

Definition at line 35 of file aigJust.c.

{
    assert( Value );
    pNode->fMarkA = (Value & 1);
    pNode->fMarkB = ((Value >> 1) & 1);
    return Value;
}

int Aig_ObjTerSimulate	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pNode,
		Vec_Int_t *	vSuppLits
	)

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

Synopsis [Returns value of the object under input assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file aigJust.c.

{
    Aig_Obj_t * pObj;
    int i, Entry;
    Aig_ManIncrementTravId( pAig );
    Vec_IntForEachEntry( vSuppLits, Entry, i )
    {
        pObj = Aig_ManCi( pAig, Abc_Lit2Var(Entry) );
        Aig_ObjSetTerValue( pObj, Abc_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
        Aig_ObjSetTravIdCurrent( pAig, pObj );
//printf( "%d ", Entry );
    }
//printf( "\n" );
    return Aig_ObjTerSimulate_rec( pAig, pNode );
}

int Aig_ObjTerSimulate_rec	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pNode
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file aigJust.c.

{
    int Value0, Value1;
    if ( Aig_ObjIsConst1(pNode) )
        return AIG_VAL1;
    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
        return Aig_ObjGetTerValue( pNode );
    Aig_ObjSetTravIdCurrent( pAig, pNode );
    if ( Aig_ObjIsCi(pNode) )
        return Aig_ObjSetTerValue( pNode, AIG_VALX );
    Value0 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin0(pNode)), Aig_ObjFaninC0(pNode) );
    if ( Aig_ObjIsCo(pNode) || Value0 == AIG_VAL0 )
        return Aig_ObjSetTerValue( pNode, Value0 );
    assert( Aig_ObjIsNode(pNode) );
    Value1 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin1(pNode)), Aig_ObjFaninC1(pNode) );
    return Aig_ObjSetTerValue( pNode, Aig_ObjAndTerValue(Value0, Value1) );
}