#include "gia.h"
#include "giaAig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"

Include dependency graph for giaEra2.c:

Classes
struct	Gia_PtrAre_t_

union	Gia_PtrAreInt_t_

struct	Gia_ObjAre_t_

struct	Gia_StaAre_t_

struct	Gia_ManAre_t_

Macros
#define	MAX_CALL_NUM (1000000)
	DECLARATIONS ///.

#define	MAX_ITEM_NUM (1<<20)

#define	MAX_PAGE_NUM (1<<11)

#define	MAX_VARS_NUM (1<<14)

#define	MAX_CUBE_NUM 63

#define	Gia_ManAreForEachCubeList(p, pList, pCube)

#define	Gia_ManAreForEachCubeList2(p, iList, pCube, iCube)

#define	Gia_ManAreForEachCubeStore(p, pCube, i)

#define	Gia_ManAreForEachCubeVec(vVec, p, pCube, i)

Typedefs
typedef struct Gia_PtrAre_t_	Gia_PtrAre_t

typedef union Gia_PtrAreInt_t_	Gia_PtrAreInt_t

typedef struct Gia_ObjAre_t_	Gia_ObjAre_t

typedef struct Gia_StaAre_t_	Gia_StaAre_t

typedef struct Gia_ManAre_t_	Gia_ManAre_t

Functions
void	Gia_ManCountMintermsInCube (Gia_StaAre_t pCube, int nVars, unsigned pStore)
	FUNCTION DEFINITIONS ///.

int	Gia_ManCountMinterms (Gia_ManAre_t *p)

int	Gia_ManDeriveCiTfo_rec (Gia_Man_t p, Gia_Obj_t pObj, Vec_Int_t *vRes)

Vec_Int_t *	Gia_ManDeriveCiTfoOne (Gia_Man_t p, Gia_Obj_t pPivot)

Vec_Vec_t *	Gia_ManDeriveCiTfo (Gia_Man_t *p)

Gia_ManAre_t *	Gia_ManAreCreate (Gia_Man_t *pAig)

void	Gia_ManAreFree (Gia_ManAre_t *p)

void	Gia_ManArePrintCube (Gia_ManAre_t p, Gia_StaAre_t pSta)

int	Gia_ManAreDepth (Gia_ManAre_t *p, int iState)

int	Gia_ManAreListCountUsed_rec (Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)

int	Gia_ManArePrintUsed_rec (Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)

int	Gia_ManAreFindBestVar (Gia_ManAre_t *p, Gia_PtrAre_t List)

int	Gia_ManAreCubeCheckTree_rec (Gia_ManAre_t p, Gia_ObjAre_t pObj, Gia_StaAre_t *pSta)

void	Gia_ManAreCubeAddToTree_rec (Gia_ManAre_t p, Gia_ObjAre_t pObj, Gia_StaAre_t *pSta)

int	Gia_ManAreCubeCollectTree_rec (Gia_ManAre_t p, Gia_ObjAre_t pObj, Gia_StaAre_t *pSta)

int	Gia_ManAreCubeCheckTree (Gia_ManAre_t p, Gia_StaAre_t pSta)

void	Gia_ManAreMostUsedPi_rec (Gia_Man_t p, Gia_Obj_t pObj)

int	Gia_ManCheckPOs_rec (Gia_Man_t p, Gia_Obj_t pObj)

int	Gia_ManAreDeriveNexts_rec (Gia_ManAre_t *p, Gia_PtrAre_t Sta)

int	Gia_ManAreDeriveNexts (Gia_ManAre_t *p, Gia_PtrAre_t Sta)

void	Gia_ManArePrintReport (Gia_ManAre_t *p, abctime Time, int fFinal)

int	Gia_ManArePerform (Gia_Man_t *pAig, int nStatesMax, int fMiter, int fVerbose)

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void	Gia_ManAreDeriveCexSatStart (Gia_ManAre_t *p)

void	Gia_ManAreDeriveCexSatStop (Gia_ManAre_t *p)

void	Gia_ManAreDeriveCexSat (Gia_ManAre_t p, Gia_StaAre_t pCur, Gia_StaAre_t *pNext, int iOutFailed)

Abc_Cex_t *	Gia_ManAreDeriveCex (Gia_ManAre_t p, Gia_StaAre_t pLast)

Macro Definition Documentation

◆ Gia_ManAreForEachCubeList

#define Gia_ManAreForEachCubeList	(	p,
		pList,
		pCube )

Value:

for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) )

p

Cube * p

Definition exorList.c:222

Definition at line 160 of file giaEra2.c.

160#define Gia_ManAreForEachCubeList( p, pList, pCube ) \

161 for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) )

◆ Gia_ManAreForEachCubeList2

#define Gia_ManAreForEachCubeList2	(	p,
		iList,
		pCube,
		iCube )

Value:

    for ( iCube = Gia_Ptr2Int(iList), pCube = Gia_ManAreSta(p, iList);       \
          Gia_StaIsGood(p, pCube);                                           \
          iCube = Gia_Ptr2Int(pCube->iNext), pCube = Gia_StaNext(p, pCube) )

Definition at line 162 of file giaEra2.c.

#define Gia_ManAreForEachCubeList2( p, iList, pCube, iCube )                 \
    for ( iCube = Gia_Ptr2Int(iList), pCube = Gia_ManAreSta(p, iList);       \
          Gia_StaIsGood(p, pCube);                                           \
          iCube = Gia_Ptr2Int(pCube->iNext), pCube = Gia_StaNext(p, pCube) )

◆ Gia_ManAreForEachCubeStore

#define Gia_ManAreForEachCubeStore	(	p,
		pCube,
		i )

Value:

for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ )

Definition at line 166 of file giaEra2.c.

166#define Gia_ManAreForEachCubeStore( p, pCube, i ) \

167 for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ )

◆ Gia_ManAreForEachCubeVec

#define Gia_ManAreForEachCubeVec	(	vVec,
		p,
		pCube,
		i )

Value:

for ( i = 0; i < Vec_IntSize(vVec) && (pCube = Gia_ManAreStaInt(p, Vec_IntEntry(vVec,i))); i++ )

Definition at line 168 of file giaEra2.c.

168#define Gia_ManAreForEachCubeVec( vVec, p, pCube, i ) \

169 for ( i = 0; i < Vec_IntSize(vVec) && (pCube = Gia_ManAreStaInt(p, Vec_IntEntry(vVec,i))); i++ )

◆ MAX_CALL_NUM

#define MAX_CALL_NUM (1000000)

DECLARATIONS ///.

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

FileName [gia.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 38 of file giaEra2.c.

◆ MAX_CUBE_NUM

#define MAX_CUBE_NUM 63

Definition at line 42 of file giaEra2.c.

◆ MAX_ITEM_NUM

#define MAX_ITEM_NUM (1<<20)

Definition at line 39 of file giaEra2.c.

◆ MAX_PAGE_NUM

#define MAX_PAGE_NUM (1<<11)

Definition at line 40 of file giaEra2.c.

◆ MAX_VARS_NUM

#define MAX_VARS_NUM (1<<14)

Definition at line 41 of file giaEra2.c.

Typedef Documentation

◆ Gia_ManAre_t

typedef struct Gia_ManAre_t_ Gia_ManAre_t

Definition at line 81 of file giaEra2.c.

◆ Gia_ObjAre_t

typedef struct Gia_ObjAre_t_ Gia_ObjAre_t

Definition at line 61 of file giaEra2.c.

◆ Gia_PtrAre_t

typedef struct Gia_PtrAre_t_ Gia_PtrAre_t

Definition at line 45 of file giaEra2.c.

◆ Gia_PtrAreInt_t

typedef union Gia_PtrAreInt_t_ Gia_PtrAreInt_t

Definition at line 53 of file giaEra2.c.

◆ Gia_StaAre_t

typedef struct Gia_StaAre_t_ Gia_StaAre_t

Definition at line 72 of file giaEra2.c.

Function Documentation

◆ Gia_ManAreCreate()

Gia_ManAre_t * Gia_ManAreCreate ( Gia_Man_t * pAig )

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

Synopsis [Creates reachability manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file giaEra2.c.

{
    Gia_ManAre_t * p;
    assert( sizeof(Gia_ObjAre_t) == 16 );
    p = ABC_CALLOC( Gia_ManAre_t, 1 );
    p->pAig       = pAig;
    p->nWords     = Abc_BitWordNum( 2 * Gia_ManRegNum(pAig) );
    p->nSize      = sizeof(Gia_StaAre_t)/4 + p->nWords;
    p->ppObjs     = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
    p->ppStas     = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
    p->vCiTfos    = Gia_ManDeriveCiTfo( pAig );
    p->vCiLits    = Vec_VecDupInt( p->vCiTfos );
    p->vCubesA    = Vec_IntAlloc( 100 );
    p->vCubesB    = Vec_IntAlloc( 100 );
    p->iOutFail   = -1;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreCubeAddToTree_rec()

void Gia_ManAreCubeAddToTree_rec	(	Gia_ManAre_t *	p,
		Gia_ObjAre_t *	pObj,
		Gia_StaAre_t *	pSta )

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

Synopsis [Adds new cube to the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 1102 of file giaEra2.c.

{
    if ( Gia_StaHasValue0(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch0(pObj) )
            Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
        else
        {
            Gia_ManAreCubeAddToList( p, pObj->F, pSta );
            if ( ++pObj->nStas0 == MAX_CUBE_NUM )
            {
                pObj->nStas0 = Gia_ManAreListCountListUsed( p, pObj->F[0] );
                if ( pObj->nStas0 < MAX_CUBE_NUM/2 )
                    Gia_ManAreCompress( p, pObj->F );
                else
                {
                    Gia_ManAreRebalance( p, pObj->F );
                    pObj->nStas0 = 0;
                }
            }
        }
    }
    else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch1(pObj) )
            Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
        else
        {
            Gia_ManAreCubeAddToList( p, pObj->F+1, pSta );
            if ( ++pObj->nStas1 == MAX_CUBE_NUM )
            {
                pObj->nStas1 = Gia_ManAreListCountListUsed( p, pObj->F[1] );
                if ( pObj->nStas1 < MAX_CUBE_NUM/2 )
                    Gia_ManAreCompress( p, pObj->F+1 );
                else
                {
                    Gia_ManAreRebalance( p, pObj->F+1 );
                    pObj->nStas1 = 0;
                }
            }
        }
    }
    else
    {
        if ( Gia_ObjHasBranch2(pObj) )
            Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
        else
        {
            Gia_ManAreCubeAddToList( p, pObj->F+2, pSta );
            if ( ++pObj->nStas2 == MAX_CUBE_NUM )
            {
                pObj->nStas2 = Gia_ManAreListCountListUsed( p, pObj->F[2] );
                if ( pObj->nStas2 < MAX_CUBE_NUM/2 )
                    Gia_ManAreCompress( p, pObj->F+2 );
                else
                {
                    Gia_ManAreRebalance( p, pObj->F+2 );
                    pObj->nStas2 = 0;
                }
            }
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreCubeCheckTree()

int Gia_ManAreCubeCheckTree	(	Gia_ManAre_t *	p,
		Gia_StaAre_t *	pSta )

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

Synopsis [Checks if the cube like this exists in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 1260 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    int i, iVar;
    assert( p->fTree );
    Vec_IntClear( p->vCubesA );
    Vec_IntClear( p->vCubesB );
    Gia_ManAreCubeCollectTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
//    if ( p->nStas > 3000 )
//        printf( "%d %d  \n", Vec_IntSize(p->vCubesA), Vec_IntSize(p->vCubesB) );
//    Vec_IntSort( p->vCubesA, 0 );
//    Vec_IntSort( p->vCubesB, 0 );
    Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i )
    {
        if ( Gia_StaIsUnused( pCube ) )
            continue;
        if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
            continue;
        if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
        {
            Gia_ManAreRycycleSta( p, pSta );
            return 0;
        }
        if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
        {
            Gia_StaSetUnused( pCube );
            continue;
        }
        iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
        if ( iVar == -1 )
            continue;
        assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) );
        assert(  Gia_StaHasValue0(pCube, iVar) ^  Gia_StaHasValue1(pCube, iVar) );
        if ( Gia_StaHasValue0(pCube, iVar) )
            Gia_StaSetValue1( pSta, iVar );
        else
            Gia_StaSetValue0( pSta, iVar );
        return Gia_ManAreCubeCheckTree( p, pSta );
    }
    Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i )
    {
        if ( Gia_StaIsUnused( pCube ) )
            continue;
        if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
            continue;
        if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
        {
            Gia_ManAreRycycleSta( p, pSta );
            return 0;
        }
        if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
        {
            Gia_StaSetUnused( pCube );
            continue;
        }
        iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
        if ( iVar == -1 )
            continue;
        assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) );
        assert(  Gia_StaHasValue0(pCube, iVar) ^  Gia_StaHasValue1(pCube, iVar) );
        if ( Gia_StaHasValue0(pCube, iVar) )
            Gia_StaSetValue1( pSta, iVar );
        else
            Gia_StaSetValue0( pSta, iVar );
        return Gia_ManAreCubeCheckTree( p, pSta );
    }
/*
    if ( p->nStas > 3000 )
    {
printf( "Trying cube:       " );
Gia_ManArePrintCube( p, pSta );
    Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i )
    {
printf( "aaaaaaaaaaaa %5d ", Vec_IntEntry(p->vCubesA,i) );
Gia_ManArePrintCube( p, pCube );
    }
    Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i )
    {
printf( "bbbbbbbbbbbb %5d ", Vec_IntEntry(p->vCubesB,i) );
Gia_ManArePrintCube( p, pCube );
    }
    }
*/
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreCubeCheckTree_rec()

int Gia_ManAreCubeCheckTree_rec	(	Gia_ManAre_t *	p,
		Gia_ObjAre_t *	pObj,
		Gia_StaAre_t *	pSta )

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

Synopsis [Checks if the cube like this exists in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 1065 of file giaEra2.c.

{
    int RetValue;
    if ( Gia_StaHasValue0(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch0(pObj) )
            RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
        else
            RetValue = Gia_ManAreCubeCheckList( p, pObj->F, pSta );
        if ( RetValue == 0 )
            return 0;
    }
    else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch1(pObj) )
            RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
        else
            RetValue = Gia_ManAreCubeCheckList( p, pObj->F + 1, pSta );
        if ( RetValue == 0 )
            return 0;
    }
    if ( Gia_ObjHasBranch2(pObj) )
        return Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
    return Gia_ManAreCubeCheckList( p, pObj->F + 2, pSta );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreCubeCollectTree_rec()

int Gia_ManAreCubeCollectTree_rec	(	Gia_ManAre_t *	p,
		Gia_ObjAre_t *	pObj,
		Gia_StaAre_t *	pSta )

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

Synopsis [Collects overlapping cubes in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 1223 of file giaEra2.c.

{
    int RetValue;
    if ( Gia_StaHasValue0(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch0(pObj) )
            RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
        else
            RetValue = Gia_ManAreCubeCollectList( p, pObj->F, pSta );
        if ( RetValue == 0 )
            return 0;
    }
    else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
    {
        if ( Gia_ObjHasBranch1(pObj) )
            RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
        else
            RetValue = Gia_ManAreCubeCollectList( p, pObj->F + 1, pSta );
        if ( RetValue == 0 )
            return 0;
    }
    if ( Gia_ObjHasBranch2(pObj) )
        return Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
    return Gia_ManAreCubeCollectList( p, pObj->F + 2, pSta );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreDepth()

int Gia_ManAreDepth	(	Gia_ManAre_t *	p,
		int	iState )

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

Synopsis [Counts the depth of state transitions leading ot this state.]

Description []

SideEffects []

SeeAlso []

Definition at line 714 of file giaEra2.c.

{
    Gia_StaAre_t * pSta;
    int Counter = 0;
    for ( pSta = Gia_ManAreStaInt(p, iState); Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) )
        Counter++;
    return Counter;
} 

Here is the caller graph for this function:

◆ Gia_ManAreDeriveCex()

Abc_Cex_t * Gia_ManAreDeriveCex	(	Gia_ManAre_t *	p,
		Gia_StaAre_t *	pLast )

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

Synopsis [Returns the status of the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 1919 of file giaEra2.c.

{
    Abc_Cex_t * pCex;
    Vec_Ptr_t * vStates;
    Gia_StaAre_t * pSta, * pPrev;
    int Var, i, v;
    assert( p->iOutFail >= 0 );
    Gia_ManAreDeriveCexSatStart( p );
    // compute the trace
    vStates = Vec_PtrAlloc( 1000 );
    for ( pSta = pLast; Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) )
        if ( pSta != pLast )
            Vec_PtrPush( vStates, pSta );
    assert( Vec_PtrSize(vStates) >= 1 );
    // start the counter-example
    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
    pCex->iFrame = Vec_PtrSize(vStates)-1;
    pCex->iPo = p->iOutFail;
    // compute states
    pPrev = NULL;
    Vec_PtrForEachEntry( Gia_StaAre_t *, vStates, pSta, i )
    {
        Gia_ManAreDeriveCexSat( p, pSta, pPrev, (i == 0) ? p->iOutFail : -1 ); 
        pPrev = pSta;
        // create the counter-example
        Vec_IntForEachEntry( p->vCofVars, Var, v )
        {
            assert( Var < Gia_ManPiNum(p->pAig) );
            Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
        }
    }
    // free temporary things
    Vec_PtrFree( vStates );
    Gia_ManAreDeriveCexSatStop( p );
    return pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreDeriveCexSat()

void Gia_ManAreDeriveCexSat	(	Gia_ManAre_t *	p,
		Gia_StaAre_t *	pCur,
		Gia_StaAre_t *	pNext,
		int	iOutFailed )

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

Synopsis [Computes satisfying assignment in one timeframe.]

Description [Returns the vector of integers represeting PIO ids of the primary inputs that should be 1 in the counter-example.]

SideEffects []

SeeAlso []

Definition at line 1852 of file giaEra2.c.

{
    int i, status;
    // make assuptions
    Vec_IntClear( p->vAssumps );
    for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
    {
        if ( Gia_StaHasValue0(pCur, i) )
            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
        else if ( Gia_StaHasValue1(pCur, i) )
            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
    }
    if ( pNext )
    for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
    {
        if ( Gia_StaHasValue0(pNext, i) )
            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
        else if ( Gia_StaHasValue1(pNext, i) )
            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
    }
    if ( iOutFailed >= 0 )
    {
        assert( iOutFailed < Gia_ManPoNum(p->pAig) );
        Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
    }
    // solve SAT
    status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps), 
        (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status != l_True )
    {
        printf( "SAT problem is not satisfiable. Failure...\n" );
        return;
    }
    assert( status == l_True );
    // check the model
    Vec_IntClear( p->vCofVars );
    for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
    {
        if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, i) ) )
            Vec_IntPush( p->vCofVars, i );
    }
    // write the current state
    for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
    {
        if ( Gia_StaHasValue0(pCur, i) )
            assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 );
        else if ( Gia_StaHasValue1(pCur, i) )
            assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 1 );
        // set don't-care value
        if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 )
            Gia_StaSetValue0( pCur, i );
        else
            Gia_StaSetValue1( pCur, i );
    }
}

Here is the caller graph for this function:

◆ Gia_ManAreDeriveCexSatStart()

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Gia_ManAreDeriveCexSatStart ( Gia_ManAre_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1799 of file giaEra2.c.

{
    Aig_Man_t * pAig2;
    Cnf_Dat_t * pCnf;
    assert( p->pSat == NULL );
    pAig2 = Gia_ManToAig( p->pAig, 0 );
    Aig_ManSetRegNum( pAig2, 0 );
    pCnf = Cnf_Derive( pAig2, Gia_ManCoNum(p->pAig) );
    p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    p->vSatNumCis = Cnf_DataCollectCiSatNums( pCnf, pAig2 );
    p->vSatNumCos = Cnf_DataCollectCoSatNums( pCnf, pAig2 );
    Cnf_DataFree( pCnf );
    Aig_ManStop( pAig2 );
    p->vAssumps = Vec_IntAlloc( 100 );
    p->vCofVars = Vec_IntAlloc( 100 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreDeriveCexSatStop()

void Gia_ManAreDeriveCexSatStop ( Gia_ManAre_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1827 of file giaEra2.c.

{
    assert( p->pSat != NULL );
    assert( p->pTarget != NULL );
    sat_solver_delete( (sat_solver *)p->pSat );
    Vec_IntFree( p->vSatNumCis );
    Vec_IntFree( p->vSatNumCos );
    Vec_IntFree( p->vAssumps );
    Vec_IntFree( p->vCofVars );
    p->pTarget = NULL;
    p->pSat = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreDeriveNexts()

int Gia_ManAreDeriveNexts	(	Gia_ManAre_t *	p,
		Gia_PtrAre_t	Sta )

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

Synopsis [Derives next state cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1618 of file giaEra2.c.

{
    Gia_StaAre_t * pSta;
    Gia_Obj_t * pObj;
    int i, RetValue;
    abctime clk = Abc_Clock();
    pSta = Gia_ManAreSta( p, Sta );
    if ( Gia_StaIsUnused(pSta) )
        return 0;
    // recycle the manager
    if ( p->pNew && Gia_ManObjNum(p->pNew) > 1000000 )
    {
        Gia_ManStop( p->pNew );
        p->pNew = NULL;
    }
    // allocate the manager
    if ( p->pNew == NULL )
    {
        p->pNew = Gia_ManStart( 10 * Gia_ManObjNum(p->pAig) );
        Gia_ManIncrementTravId( p->pNew );
        Gia_ManHashAlloc( p->pNew );
        Gia_ManConst0(p->pAig)->Value = 0;
        Gia_ManForEachCi( p->pAig, pObj, i )
            pObj->Value = Gia_ManAppendCi(p->pNew);
    }
    Gia_ManForEachRo( p->pAig, pObj, i )
    {
        if ( Gia_StaHasValue0( pSta, i ) )
            pObj->Value = 0;
        else if ( Gia_StaHasValue1( pSta, i ) )
            pObj->Value = 1;
        else // don't-care literal
            pObj->Value = Abc_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
    }
    Gia_ManForEachAnd( p->pAig, pObj, i )
        pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Gia_ManForEachCo( p->pAig, pObj, i )
        pObj->Value = Gia_ObjFanin0Copy(pObj);
 
    // perform case-splitting
    p->nRecCalls = 0;
    RetValue = Gia_ManAreDeriveNexts_rec( p, Sta );
    if ( p->nRecCalls >= MAX_CALL_NUM )
    {
        printf( "Exceeded the limit on the number of transitions from a state cube (%d).\n", MAX_CALL_NUM );
        p->fStopped = 1;
    }
//    printf( "%d ", p->nRecCalls );
//printf( "%d ", Gia_ManObjNum(p->pNew) );
    p->timeAig += Abc_Clock() - clk;
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreDeriveNexts_rec()

int Gia_ManAreDeriveNexts_rec	(	Gia_ManAre_t *	p,
		Gia_PtrAre_t	Sta )

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

Synopsis [Derives next state cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1541 of file giaEra2.c.

{
    Gia_Obj_t * pPivot;
    Vec_Int_t * vLits, * vTfos;
    Gia_Obj_t * pObj;
    int i;
    abctime clk;
    if ( ++p->nRecCalls == MAX_CALL_NUM )
        return 0;
    if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL )
    {
        Gia_StaAre_t * pNew;
        clk = Abc_Clock();
        pNew = Gia_ManAreCreateStaNew( p );
        pNew->iPrev = Sta;
        p->fStopped = (p->fMiter && (Gia_ManCheckPOstatus(p) & 1));
        if ( p->fStopped )
        {
            assert( p->pTarget == NULL );
            p->pTarget = pNew;
            return 1;
        }
        Gia_ManAreCubeProcess( p, pNew );
        p->timeCube += Abc_Clock() - clk;
        return p->fStopped;
    }
    // remember values in the cone and perform update
    vTfos = Vec_VecEntryInt( p->vCiTfos, Gia_ObjCioId(pPivot) );
    vLits = Vec_VecEntryInt( p->vCiLits, Gia_ObjCioId(pPivot) );
    assert( Vec_IntSize(vTfos) == Vec_IntSize(vLits) );
    Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
    {
        Vec_IntWriteEntry( vLits, i, pObj->Value );
        if ( Gia_ObjIsAnd(pObj) )
            pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        else if ( Gia_ObjIsCo(pObj) )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        else 
        {
            assert( Gia_ObjIsCi(pObj) );
            pObj->Value = 0;
        }
    }
    if ( Gia_ManAreDeriveNexts_rec( p, Sta ) )
        return 1;
    // compute different values
    Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        else if ( Gia_ObjIsCo(pObj) )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        else 
        {
            assert( Gia_ObjIsCi(pObj) );
            pObj->Value = 1;
        }
    }
    if ( Gia_ManAreDeriveNexts_rec( p, Sta ) )
        return 1;
    // reset the original values
    Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
        pObj->Value = Vec_IntEntry( vLits, i );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreFindBestVar()

int Gia_ManAreFindBestVar	(	Gia_ManAre_t *	p,
		Gia_PtrAre_t	List )

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

Synopsis [Best var has max weight.]

Description [Weight is defined as the number of 0/1-lits minus the absolute value of the diff between the number of 0-lits and 1-lits.]

SideEffects []

SeeAlso []

Definition at line 853 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    int Count0, Count1, Count2;
    int iVarThis, iVarBest = -1, WeightThis, WeightBest = -1;
    for ( iVarThis = 0; iVarThis < Gia_ManRegNum(p->pAig); iVarThis++ )
    {
        Count0 = Count1 = Count2 = 0;
        Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, List), pCube )
        {
            if ( Gia_StaIsUnused(pCube) )
                continue;
            if ( Gia_StaHasValue0(pCube, iVarThis) )
                Count0++;
            else if ( Gia_StaHasValue1(pCube, iVarThis) )
                Count1++;
            else
                Count2++;
        }
//        printf( "%4d : %5d  %5d  %5d   Weight = %5d\n", iVarThis, Count0, Count1, Count2, 
//            Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0) );
        if ( (!Count0 && !Count1) || (!Count0 && !Count2) || (!Count1 && !Count2) )
            continue;
        WeightThis = Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0);
        if ( WeightBest < WeightThis ) 
        {
            WeightBest = WeightThis;
            iVarBest = iVarThis;
        }
    }
    if ( iVarBest == -1 )
    {
        Gia_ManArePrintListUsed( p, List );
        printf( "Error: Best variable not found!!!\n" );
    }
    assert( iVarBest != -1 );
    return iVarBest;
}

◆ Gia_ManAreFree()

void Gia_ManAreFree ( Gia_ManAre_t * p )

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

Synopsis [Deletes reachability manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 510 of file giaEra2.c.

{
    int i;
    Gia_ManStop( p->pAig );
    if ( p->pNew )
        Gia_ManStop( p->pNew );
    Vec_IntFree( p->vCubesA );
    Vec_IntFree( p->vCubesB );
    Vec_VecFree( p->vCiTfos );
    Vec_VecFree( p->vCiLits );
    for ( i = 0; i < p->nObjPages; i++ )
        ABC_FREE( p->ppObjs[i] );
    ABC_FREE( p->ppObjs );
    for ( i = 0; i < p->nStaPages; i++ )
        ABC_FREE( p->ppStas[i] );
    ABC_FREE( p->ppStas );
//    ABC_FREE( p->pfUseless );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreListCountUsed_rec()

int Gia_ManAreListCountUsed_rec	(	Gia_ManAre_t *	p,
		Gia_PtrAre_t	Root,
		int	fTree )

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

Synopsis [Counts the number of used cubes in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 754 of file giaEra2.c.

{
    Gia_ObjAre_t * pObj;
    if ( !fTree )
        return Gia_ManAreListCountListUsed( p, Root );
    pObj = Gia_ManAreObj(p, Root);
    return Gia_ManAreListCountUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) +
           Gia_ManAreListCountUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) +
           Gia_ManAreListCountUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManAreMostUsedPi_rec()

void Gia_ManAreMostUsedPi_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj )

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

Synopsis [Returns the most used CI, or NULL if condition is met.]

Description []

SideEffects []

SeeAlso []

Definition at line 1392 of file giaEra2.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        pObj->Value++;
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin0(pObj) );
    Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin1(pObj) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManArePerform()

int Gia_ManArePerform	(	Gia_Man_t *	pAig,
		int	nStatesMax,
		int	fMiter,
		int	fVerbose )

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

Synopsis [Performs explicit reachability.]

Description []

SideEffects []

SeeAlso []

Definition at line 1710 of file giaEra2.c.

{
//    extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose );
    extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast );
    Gia_ManAre_t * p;
    abctime clk = Abc_Clock();
    int RetValue = 1;
    if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM )
    {
        printf( "Currently can only handle circuit with up to %d registers.\n", MAX_VARS_NUM );
        return -1;
    }
    ABC_FREE( pAig->pCexSeq );
//    p = Gia_ManAreCreate( Gia_ManCompress2(pAig, 0, 0) );
    p = Gia_ManAreCreate( Gia_ManDup(pAig) );
    p->fMiter = fMiter;
    Gia_ManAreCubeProcess( p, Gia_ManAreCreateStaInit(p) );
    for ( p->iStaCur = 1; p->iStaCur < p->nStas; p->iStaCur++ )
    {
//        printf( "Explored state %d. Total cubes %d.\n", p->iStaCur, p->nStas-1 );
        if ( Gia_ManAreDeriveNexts( p, Gia_Int2Ptr(p->iStaCur) ) || p->nStas > nStatesMax )
            pAig->pCexSeq = Gia_ManAreDeriveCex( p, p->pTarget );
        if ( p->fStopped )
        {
            RetValue = -1;
            break;
        }
        if ( fVerbose )//&& p->iStaCur % 5000 == 0 )
            Gia_ManArePrintReport( p, clk, 0 );
    }
    Gia_ManArePrintReport( p, clk, 1 );
    printf( "%s after finding %d state cubes (%d not contained) with depth %d.  ", 
        p->fStopped ? "Stopped" : "Completed", 
        p->nStas, Gia_ManAreListCountUsed(p), 
        Gia_ManAreDepth(p, p->iStaCur-1) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    if ( pAig->pCexSeq != NULL )
        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", 
            p->iStaCur, pAig->pName, Gia_ManAreDepth(p, p->iStaCur)-1 );
    if ( fVerbose )
    {
        ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube,    Abc_Clock() - clk );
        ABC_PRTP( "Containment", p->timeCube,                 Abc_Clock() - clk );
        ABC_PRTP( "Other      ", Abc_Clock() - clk - p->timeAig,  Abc_Clock() - clk );
        ABC_PRTP( "TOTAL      ", Abc_Clock() - clk,               Abc_Clock() - clk );
    }
    if ( Gia_ManRegNum(pAig) <= 30 )
    {
        clk = Abc_Clock();
        printf( "The number of unique state minterms in computed state cubes is %d.   ", Gia_ManCountMinterms(p) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
//    printf( "Compares = %d.  Equals = %d.  Disj = %d.  Disj2 = %d.  Disj3 = %d.\n", 
//        p->nCompares, p->nEquals, p->nDisjs, p->nDisjs2, p->nDisjs3 );
//    Gia_ManAreFindBestVar( p, Gia_ManAreSta(p, p->Root) );
//    Gia_ManArePrintUsed( p );
    Gia_ManAreFree( p );
    // verify
    if ( pAig->pCexSeq )
    {
        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            printf( "Generated counter-example is INVALID.                       \n" );
        else
            printf( "Generated counter-example verified correctly.               \n" );
        return 0;
    }
    return RetValue;
}

Here is the call graph for this function:

◆ Gia_ManArePrintCube()

void Gia_ManArePrintCube	(	Gia_ManAre_t *	p,
		Gia_StaAre_t *	pSta )

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

Synopsis [Prints the state cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 681 of file giaEra2.c.

{
    Gia_Obj_t * pObj;
    int i, Count0 = 0, Count1 = 0, Count2 = 0;
    printf( "%4d %4d :  ", p->iStaCur, p->nStas-1 );
    printf( "Prev %4d   ", Gia_Ptr2Int(pSta->iPrev) );
    printf( "%p   ", pSta );
    Gia_ManForEachRi( p->pAig, pObj, i )
    {
        if ( Gia_StaHasValue0(pSta, i) )
            printf( "0" ), Count0++;
        else if ( Gia_StaHasValue1(pSta, i) )
            printf( "1" ), Count1++;
        else
            printf( "-" ), Count2++;
    }
    printf( "  0 =%3d", Count0 );
    printf( "  1 =%3d", Count1 );
    printf( "  - =%3d", Count2 );
    printf( "\n" );
}

◆ Gia_ManArePrintReport()

void Gia_ManArePrintReport	(	Gia_ManAre_t *	p,
		abctime	Time,
		int	fFinal )

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

Synopsis [Prints the report]

Description []

SideEffects []

SeeAlso []

Definition at line 1683 of file giaEra2.c.

{
    printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f MB.  ", 
        p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur), 
        (sizeof(Gia_ManAre_t) + 4.0*Gia_ManRegNum(p->pAig) + 8.0*MAX_PAGE_NUM + 
         4.0*p->nStaPages*p->nSize*MAX_ITEM_NUM + 16.0*p->nObjPages*MAX_ITEM_NUM)/(1<<20) );
    if ( fFinal )
    {
        ABC_PRT( "Time", Abc_Clock() - Time );
    }
    else
    {
        ABC_PRTr( "Time", Abc_Clock() - Time );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManArePrintUsed_rec()

int Gia_ManArePrintUsed_rec	(	Gia_ManAre_t *	p,
		Gia_PtrAre_t	Root,
		int	fTree )

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

Synopsis [Prints used cubes in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file giaEra2.c.

{
    Gia_ObjAre_t * pObj;
    if ( !fTree )
        return Gia_ManArePrintListUsed( p, Root );
    pObj = Gia_ManAreObj(p, Root);
    return Gia_ManArePrintUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) +
           Gia_ManArePrintUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) +
           Gia_ManArePrintUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManCheckPOs_rec()

int Gia_ManCheckPOs_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj )

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

Synopsis [Counts maximum support of primary outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1452 of file giaEra2.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return 0;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
        return 1;
    assert( Gia_ObjIsAnd(pObj) );
    return Gia_ManCheckPOs_rec( p, Gia_ObjFanin0(pObj) ) +
           Gia_ManCheckPOs_rec( p, Gia_ObjFanin1(pObj) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManCountMinterms()

int Gia_ManCountMinterms ( Gia_ManAre_t * p )

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

Synopsis [Count state minterms contains in the used cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    unsigned * pMemory;
    int i, nMemSize, Counter = 0;
    if ( Gia_ManRegNum(p->pAig) > 30 )
        return -1;
    nMemSize = Abc_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
    pMemory  = ABC_CALLOC( unsigned, nMemSize );
    Gia_ManAreForEachCubeStore( p, pCube, i )
        if ( Gia_StaIsUsed(pCube) )
            Gia_ManCountMintermsInCube( pCube, Gia_ManRegNum(p->pAig), pMemory );
    for ( i = 0; i < nMemSize; i++ )
        Counter += Gia_WordCountOnes( pMemory[i] );
    ABC_FREE( pMemory );
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManCountMintermsInCube()

void Gia_ManCountMintermsInCube	(	Gia_StaAre_t *	pCube,
		int	nVars,
		unsigned *	pStore )

FUNCTION DEFINITIONS ///.

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

Synopsis [Count state minterms contained in a cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file giaEra2.c.

{
    unsigned Mint, Mask = 0;
    int i, m, nMints, nDashes = 0, Dashes[32];
    // count the number of dashes
    for ( i = 0; i < nVars; i++ )
    {
        if ( Gia_StaHasValue0( pCube, i ) )
            continue;
        if ( Gia_StaHasValue1( pCube, i ) )
            Mask |= (1 << i);
        else
            Dashes[nDashes++] = i;
    }
    // fill in the miterms
    nMints = (1 << nDashes);
    for ( m = 0; m < nMints; m++ )
    {
        Mint = Mask;
        for ( i = 0; i < nVars; i++ )
            if ( m & (1 << i) )
                Mint |= (1 << Dashes[i]);
        Abc_InfoSetBit( pStore, Mint );
    }
}

Here is the caller graph for this function:

◆ Gia_ManDeriveCiTfo()

Vec_Vec_t * Gia_ManDeriveCiTfo ( Gia_Man_t * p )

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

Synopsis [Derives the TFO of each CI.]

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file giaEra2.c.

{
    Vec_Ptr_t * vRes;
    Gia_Obj_t * pPivot;
    int i;
    Gia_ManCleanMark0( p );
    Gia_ManIncrementTravId( p );
    vRes = Vec_PtrAlloc( Gia_ManCiNum(p) );
    Gia_ManForEachCi( p, pPivot, i )
        Vec_PtrPush( vRes, Gia_ManDeriveCiTfoOne(p, pPivot) );
    Gia_ManCleanMark0( p );
    return (Vec_Vec_t *)vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManDeriveCiTfo_rec()

int Gia_ManDeriveCiTfo_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vRes )

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

Synopsis [Derives the TFO of one CI.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file giaEra2.c.

{
    if ( Gia_ObjIsCi(pObj) )
        return pObj->fMark0;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return pObj->fMark0;
    Gia_ObjSetTravIdCurrent(p, pObj);
    assert( Gia_ObjIsAnd(pObj) );
    Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes );
    Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin1(pObj), vRes );
    pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 | Gia_ObjFanin1(pObj)->fMark0;
    if ( pObj->fMark0 )
        Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
    return pObj->fMark0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gia_ManDeriveCiTfoOne()

Vec_Int_t * Gia_ManDeriveCiTfoOne	(	Gia_Man_t *	p,
		Gia_Obj_t *	pPivot )

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

Synopsis [Derives the TFO of one CI.]

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file giaEra2.c.

{
    Vec_Int_t * vRes;
    Gia_Obj_t * pObj;
    int i;
    assert( pPivot->fMark0 == 0 );
    pPivot->fMark0 = 1;
    vRes = Vec_IntAlloc( 100 );
    Vec_IntPush( vRes, Gia_ObjId(p, pPivot) );
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
    Gia_ManForEachCo( p, pObj, i )
    {
        Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes );
        if ( Gia_ObjFanin0(pObj)->fMark0 )
            Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
    }
    pPivot->fMark0 = 0;
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ Gia_ManAreForEachCubeList

◆ Gia_ManAreForEachCubeList2

◆ Gia_ManAreForEachCubeStore

◆ Gia_ManAreForEachCubeVec

◆ MAX_CALL_NUM

◆ MAX_CUBE_NUM

◆ MAX_ITEM_NUM

◆ MAX_PAGE_NUM

◆ MAX_VARS_NUM

Typedef Documentation

◆ Gia_ManAre_t

◆ Gia_ObjAre_t

◆ Gia_PtrAre_t

◆ Gia_PtrAreInt_t

◆ Gia_StaAre_t

Function Documentation

◆ Gia_ManAreCreate()

◆ Gia_ManAreCubeAddToTree_rec()

◆ Gia_ManAreCubeCheckTree()

◆ Gia_ManAreCubeCheckTree_rec()

◆ Gia_ManAreCubeCollectTree_rec()

◆ Gia_ManAreDepth()

◆ Gia_ManAreDeriveCex()

◆ Gia_ManAreDeriveCexSat()

◆ Gia_ManAreDeriveCexSatStart()

◆ Gia_ManAreDeriveCexSatStop()

◆ Gia_ManAreDeriveNexts()

◆ Gia_ManAreDeriveNexts_rec()

◆ Gia_ManAreFindBestVar()

◆ Gia_ManAreFree()

◆ Gia_ManAreListCountUsed_rec()

◆ Gia_ManAreMostUsedPi_rec()

◆ Gia_ManArePerform()

◆ Gia_ManArePrintCube()

◆ Gia_ManArePrintReport()

◆ Gia_ManArePrintUsed_rec()

◆ Gia_ManCheckPOs_rec()

◆ Gia_ManCountMinterms()

◆ Gia_ManCountMintermsInCube()

◆ Gia_ManDeriveCiTfo()

◆ Gia_ManDeriveCiTfo_rec()

◆ Gia_ManDeriveCiTfoOne()