giaEra2.c File Reference

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

Go to the source code of this file.

Data Structures
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 ///. More...
#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)   for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) )
#define	Gia_ManAreForEachCubeList2(p, iList, pCube, iCube)
#define	Gia_ManAreForEachCubeStore(p, pCube, i)   for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ )
#define	Gia_ManAreForEachCubeVec(vVec, p, pCube, i)   for ( i = 0; i < Vec_IntSize(vVec) && (pCube = Gia_ManAreStaInt(p, Vec_IntEntry(vVec,i))); 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
static Gia_PtrAre_t	Gia_Int2Ptr (unsigned n)
static unsigned	Gia_Ptr2Int (Gia_PtrAre_t n)
static int	Gia_ObjHasBranch0 (Gia_ObjAre_t *q)
static int	Gia_ObjHasBranch1 (Gia_ObjAre_t *q)
static int	Gia_ObjHasBranch2 (Gia_ObjAre_t *q)
static Gia_ObjAre_t *	Gia_ManAreObj (Gia_ManAre_t *p, Gia_PtrAre_t n)
static Gia_StaAre_t *	Gia_ManAreSta (Gia_ManAre_t *p, Gia_PtrAre_t n)
static Gia_ObjAre_t *	Gia_ManAreObjInt (Gia_ManAre_t *p, int n)
static Gia_StaAre_t *	Gia_ManAreStaInt (Gia_ManAre_t *p, int n)
static Gia_ObjAre_t *	Gia_ManAreObjLast (Gia_ManAre_t *p)
static Gia_StaAre_t *	Gia_ManAreStaLast (Gia_ManAre_t *p)
static Gia_ObjAre_t *	Gia_ObjNextObj0 (Gia_ManAre_t *p, Gia_ObjAre_t *q)
static Gia_ObjAre_t *	Gia_ObjNextObj1 (Gia_ManAre_t *p, Gia_ObjAre_t *q)
static Gia_ObjAre_t *	Gia_ObjNextObj2 (Gia_ManAre_t *p, Gia_ObjAre_t *q)
static int	Gia_StaHasValue0 (Gia_StaAre_t *p, int iReg)
static int	Gia_StaHasValue1 (Gia_StaAre_t *p, int iReg)
static void	Gia_StaSetValue0 (Gia_StaAre_t *p, int iReg)
static void	Gia_StaSetValue1 (Gia_StaAre_t *p, int iReg)
static Gia_StaAre_t *	Gia_StaPrev (Gia_ManAre_t *p, Gia_StaAre_t *pS)
static Gia_StaAre_t *	Gia_StaNext (Gia_ManAre_t *p, Gia_StaAre_t *pS)
static int	Gia_StaIsGood (Gia_ManAre_t *p, Gia_StaAre_t *pS)
static void	Gia_StaSetUnused (Gia_StaAre_t *pS)
static int	Gia_StaIsUnused (Gia_StaAre_t *pS)
static int	Gia_StaIsUsed (Gia_StaAre_t *pS)
void	Gia_ManCountMintermsInCube (Gia_StaAre_t *pCube, int nVars, unsigned *pStore)
	FUNCTION DEFINITIONS ///. More...
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)
static int	Gia_StaAreEqual (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
static int	Gia_StaAreDisjoint (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
static int	Gia_StaAreContain (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
static int	Gia_StaAreDashNum (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
static int	Gia_StaAreSharpVar (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
static int	Gia_StaAreDisjointVar (Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Gia_ManAre_t *	Gia_ManAreCreate (Gia_Man_t *pAig)
void	Gia_ManAreFree (Gia_ManAre_t *p)
static Gia_ObjAre_t *	Gia_ManAreCreateObj (Gia_ManAre_t *p)
static Gia_StaAre_t *	Gia_ManAreCreateSta (Gia_ManAre_t *p)
static void	Gia_ManAreRycycleSta (Gia_ManAre_t *p, Gia_StaAre_t *pSta)
static Gia_StaAre_t *	Gia_ManAreCreateStaNew (Gia_ManAre_t *p)
static Gia_StaAre_t *	Gia_ManAreCreateStaInit (Gia_ManAre_t *p)
void	Gia_ManArePrintCube (Gia_ManAre_t *p, Gia_StaAre_t *pSta)
int	Gia_ManAreDepth (Gia_ManAre_t *p, int iState)
static int	Gia_ManAreListCountListUsed (Gia_ManAre_t *p, Gia_PtrAre_t Root)
int	Gia_ManAreListCountUsed_rec (Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)
static int	Gia_ManAreListCountUsed (Gia_ManAre_t *p)
static int	Gia_ManArePrintListUsed (Gia_ManAre_t *p, Gia_PtrAre_t Root)
int	Gia_ManArePrintUsed_rec (Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)
static int	Gia_ManArePrintUsed (Gia_ManAre_t *p)
int	Gia_ManAreFindBestVar (Gia_ManAre_t *p, Gia_PtrAre_t List)
static void	Gia_ManAreRebalance (Gia_ManAre_t *p, Gia_PtrAre_t *pRoot)
static void	Gia_ManAreCompress (Gia_ManAre_t *p, Gia_PtrAre_t *pRoot)
static int	Gia_ManAreCubeCheckList (Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, Gia_StaAre_t *pSta)
static void	Gia_ManAreCubeAddToList (Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, Gia_StaAre_t *pSta)
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)
static int	Gia_ManAreCubeCollectList (Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, 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)
static int	Gia_ManAreCubeProcess (Gia_ManAre_t *p, Gia_StaAre_t *pSta)
void	Gia_ManAreMostUsedPi_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
static Gia_Obj_t *	Gia_ManAreMostUsedPi (Gia_ManAre_t *p)
int	Gia_ManCheckPOs_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
static int	Gia_ManCheckPOs (Gia_ManAre_t *p)
static int	Gia_ManCheckPOstatus (Gia_ManAre_t *p)
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

#define Gia_ManAreForEachCubeList	(		p,
			pList,
			pCube
	)		for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) )

Definition at line 160 of file giaEra2.c.

#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_ManAreForEachCubeStore	(		p,
			pCube,
			i
	)		for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ )

Definition at line 166 of file giaEra2.c.

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

Definition at line 168 of file giaEra2.c.

#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.

#define MAX_CUBE_NUM   63

Definition at line 42 of file giaEra2.c.

#define MAX_ITEM_NUM   (1<<20)

Definition at line 39 of file giaEra2.c.

#define MAX_PAGE_NUM   (1<<11)

Definition at line 40 of file giaEra2.c.

#define MAX_VARS_NUM   (1<<14)

Definition at line 41 of file giaEra2.c.

Typedef Documentation

typedef struct Gia_ManAre_t_ Gia_ManAre_t

Definition at line 81 of file giaEra2.c.

typedef struct Gia_ObjAre_t_ Gia_ObjAre_t

Definition at line 61 of file giaEra2.c.

typedef struct Gia_PtrAre_t_ Gia_PtrAre_t

Definition at line 45 of file giaEra2.c.

typedef union Gia_PtrAreInt_t_ Gia_PtrAreInt_t

Definition at line 53 of file giaEra2.c.

typedef struct Gia_StaAre_t_ Gia_StaAre_t

Definition at line 72 of file giaEra2.c.

Function Documentation

static Gia_PtrAre_t Gia_Int2Ptr ( unsigned  n )

inlinestatic

Definition at line 128 of file giaEra2.c.

{ Gia_PtrAreInt_t g; g.iInt = n; return g.iGia;            }

static void Gia_ManAreCompress ( Gia_ManAre_t *  p, Gia_PtrAre_t *  pRoot  )

inlinestatic

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

Synopsis [Compresses the list by removing unused cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 940 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    Gia_PtrAre_t iList = *pRoot;
    Gia_PtrAre_t iCube, iNext;
    assert( pRoot->nItem || pRoot->nPage );
    pRoot->nItem = 0; 
    pRoot->nPage = 0;
    for ( iCube = iList, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext; 
          Gia_StaIsGood(p, pCube); 
          iCube = iNext, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext )
    {
        if ( Gia_StaIsUnused(pCube) )
            continue;
        pCube->iNext = *pRoot;
        *pRoot = iCube;
    }
}

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

static Gia_ObjAre_t* Gia_ManAreCreateObj ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Returns new object.]

Description []

SideEffects []

SeeAlso []

Definition at line 541 of file giaEra2.c.

{
    if ( p->nObjs == p->nObjPages * MAX_ITEM_NUM )
    {
        if ( p->nObjPages == MAX_PAGE_NUM )
        {
            printf( "ERA manager has run out of memory after allocating 2B internal nodes.\n" );
            return NULL;
        }
        p->ppObjs[p->nObjPages++] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * 4 );
        if ( p->nObjs == 0 )
            p->nObjs = 1;
    }
    return Gia_ManAreObjInt( p, p->nObjs++ );
}

static Gia_StaAre_t* Gia_ManAreCreateSta ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Returns new state.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file giaEra2.c.

{
    if ( p->nStas == p->nStaPages * MAX_ITEM_NUM )
    {
        if ( p->nStaPages == MAX_PAGE_NUM )
        {
            printf( "ERA manager has run out of memory after allocating 2B state cubes.\n" );
            return NULL;
        }
        if ( p->ppStas[p->nStaPages] == NULL )
            p->ppStas[p->nStaPages] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * p->nSize );
        p->nStaPages++;
        if ( p->nStas == 0 )
        {
            p->nStas = 1;
//            p->nUselessAlloc = (1 << 18);
//            p->pfUseless = ABC_CALLOC( unsigned, p->nUselessAlloc );
        }
//        if ( p->nStas == p->nUselessAlloc * 32 )
//        {
//            p->nUselessAlloc *= 2;
//            p->pfUseless = ABC_REALLOC( unsigned, p->pfUseless, p->nUselessAlloc );
//            memset( p->pfUseless + p->nUselessAlloc/2, 0, sizeof(unsigned) * p->nUselessAlloc/2 );
//        }
    }
    return Gia_ManAreStaInt( p, p->nStas++ );
}

static Gia_StaAre_t* Gia_ManAreCreateStaInit ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Creates new state state with latch init values.]

Description []

SideEffects []

SeeAlso []

Definition at line 660 of file giaEra2.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachRi( p->pAig, pObj, i )
        pObj->Value = 0;
    return Gia_ManAreCreateStaNew( p );
}

static Gia_StaAre_t* Gia_ManAreCreateStaNew ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Creates new state state from the latch values.]

Description []

SideEffects []

SeeAlso []

Definition at line 633 of file giaEra2.c.

{
    Gia_StaAre_t * pSta;
    Gia_Obj_t * pObj;
    int i;
    pSta = Gia_ManAreCreateSta( p );
    Gia_ManForEachRi( p->pAig, pObj, i )
    {
        if ( pObj->Value == 0 )
            Gia_StaSetValue0( pSta, i );
        else if ( pObj->Value == 1 )
            Gia_StaSetValue1( pSta, i );
    }
    return pSta;
}

static void Gia_ManAreCubeAddToList ( Gia_ManAre_t *  p, Gia_PtrAre_t *  pRoot, Gia_StaAre_t *  pSta  )

inlinestatic

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

Synopsis [Adds new state to the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 1040 of file giaEra2.c.

{
    int fVerbose = 0;
    pSta->iNext = *pRoot;
    *pRoot = Gia_Int2Ptr( p->nStas - 1 );
    assert( pSta == Gia_ManAreSta(p, *pRoot) );
if ( fVerbose )
{
printf( "Adding cube: " );
Gia_ManArePrintCube( p, pSta );
//printf( "\n" );
}
}

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

static int Gia_ManAreCubeCheckList ( Gia_ManAre_t *  p, Gia_PtrAre_t *  pRoot, Gia_StaAre_t *  pSta  )

inlinestatic

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

Synopsis [Checks if the state exists in the list.]

Description [The state may be sharped.]

SideEffects []

SeeAlso []

Definition at line 971 of file giaEra2.c.

{
    int fVerbose = 0;
    Gia_StaAre_t * pCube;
    int iVar;
if ( fVerbose )
{
printf( "Trying cube: " );
Gia_ManArePrintCube( p, pSta );
}
    Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, *pRoot), pCube )
    {
        p->nChecks++;
        if ( Gia_StaIsUnused( pCube ) )
            continue;
        if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
            continue;
        if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
        {
if ( fVerbose )
{
printf( "Contained in " );
Gia_ManArePrintCube( p, pCube );
}
            Gia_ManAreRycycleSta( p, pSta );
            return 0;
        }
        if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
        {
if ( fVerbose )
{
printf( "Contains     " );
Gia_ManArePrintCube( p, pCube );
}
            Gia_StaSetUnused( pCube );
            continue;
        }
        iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
        if ( iVar == -1 )
            continue;
if ( fVerbose )
{
printf( "Sharped by   " );
Gia_ManArePrintCube( p, pCube );
Gia_ManArePrintCube( p, pSta );
}
//        printf( "%d  %d\n", Gia_StaAreDashNum( pSta, pCube, p->nWords ), Gia_StaAreSharpVar( pSta, pCube, p->nWords ) );
        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_ManAreCubeCheckList( p, pRoot, pSta );
    }
    return 1;
}

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

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

static int Gia_ManAreCubeCollectList ( Gia_ManAre_t *  p, Gia_PtrAre_t *  pRoot, Gia_StaAre_t *  pSta  )

inlinestatic

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

Synopsis [Collects overlapping cubes in the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 1179 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    int iCube;
    Gia_ManAreForEachCubeList2( p, *pRoot, pCube, iCube )
    {
        if ( Gia_StaIsUnused( pCube ) )
            continue;
        if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
        {
/*
            int iVar;
            p->nDisjs++;
            iVar = Gia_StaAreDisjointVar( pSta, pCube, p->nWords );
            if ( iVar >= 0 )
            {
                p->nDisjs2++;
                if ( iCube > p->iStaCur )
                    p->nDisjs3++;
            }
*/
            continue;
        }
//        p->nCompares++;
//        p->nEquals += Gia_StaAreEqual( pSta, pCube, p->nWords );
        if ( iCube <= p->iStaCur )
            Vec_IntPush( p->vCubesA, iCube );
        else
            Vec_IntPush( p->vCubesB, iCube );
    }
    return 1;
}

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

static int Gia_ManAreCubeProcess ( Gia_ManAre_t *  p, Gia_StaAre_t *  pSta  )

inlinestatic

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

Synopsis [Processes the new cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 1357 of file giaEra2.c.

{
    int RetValue;
    p->nChecks = 0;
    if ( !p->fTree && p->nStas == MAX_CUBE_NUM )
        Gia_ManAreRebalance( p, &p->Root );
    if ( p->fTree )
    {
//        RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
        RetValue = Gia_ManAreCubeCheckTree( p, pSta );
        if ( RetValue )
            Gia_ManAreCubeAddToTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
    }
    else
    {
        RetValue = Gia_ManAreCubeCheckList( p, &p->Root, pSta );
        if ( RetValue )
            Gia_ManAreCubeAddToList( p, &p->Root, pSta );
    }
//    printf( "%d ", p->nChecks );
    return RetValue;
}

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

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

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

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

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

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

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

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

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

static int Gia_ManAreListCountListUsed ( Gia_ManAre_t *  p, Gia_PtrAre_t  Root  )

inlinestatic

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

Synopsis [Counts the number of cubes in the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 734 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    int Counter = 0;
    Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
        Counter += Gia_StaIsUsed(pCube);
    return Counter;
}

static int Gia_ManAreListCountUsed ( Gia_ManAre_t *  p )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 776 of file giaEra2.c.

{
    return Gia_ManAreListCountUsed_rec( p, p->Root, p->fTree );
}

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

static Gia_Obj_t* Gia_ManAreMostUsedPi ( Gia_ManAre_t *  p )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1418 of file giaEra2.c.

{
    Gia_Obj_t * pObj, * pObjMax = NULL;
    int i;
    // clean CI counters
    Gia_ManForEachCi( p->pNew, pObj, i )
        pObj->Value = 0;
    // traverse from each register output
    Gia_ManForEachRi( p->pAig, pObj, i )
    {
        if ( pObj->Value <= 1 )
            continue;
        Gia_ManIncrementTravId( p->pNew );
        Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Abc_Lit2Var(pObj->Value)) );
    }
    // check the CI counters
    Gia_ManForEachCi( p->pNew, pObj, i )
        if ( pObjMax == NULL || pObjMax->Value < pObj->Value )
            pObjMax = pObj;
    // return the result
    return pObjMax->Value > 1 ? pObjMax : NULL;
}

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

static Gia_ObjAre_t* Gia_ManAreObj ( Gia_ManAre_t *  p, Gia_PtrAre_t  n  )

inlinestatic

Definition at line 135 of file giaEra2.c.

{ return (Gia_ObjAre_t *)(p->ppObjs[n.nPage] + (n.nItem << 2));      }

static Gia_ObjAre_t* Gia_ManAreObjInt ( Gia_ManAre_t *  p, int  n  )

inlinestatic

Definition at line 137 of file giaEra2.c.

{ return Gia_ManAreObj( p, Gia_Int2Ptr(n) );               }

static Gia_ObjAre_t* Gia_ManAreObjLast ( Gia_ManAre_t *  p )

inlinestatic

Definition at line 139 of file giaEra2.c.

{ return Gia_ManAreObjInt( p, p->nObjs-1 );                }

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

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

static int Gia_ManArePrintListUsed ( Gia_ManAre_t *  p, Gia_PtrAre_t  Root  )

inlinestatic

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

Synopsis [Prints used cubes in the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file giaEra2.c.

{
    Gia_StaAre_t * pCube;
    Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
        if ( Gia_StaIsUsed(pCube) )
            Gia_ManArePrintCube( p, pCube );
    return 1;
}

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

static int Gia_ManArePrintUsed ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Prints used cubes in the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 835 of file giaEra2.c.

{
    return Gia_ManArePrintUsed_rec( p, p->Root, p->fTree );
}

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

static void Gia_ManAreRebalance ( Gia_ManAre_t *  p, Gia_PtrAre_t *  pRoot  )

inlinestatic

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

Synopsis [Rebalances the tree when cubes exceed the limit.]

Description []

SideEffects []

SeeAlso []

Definition at line 903 of file giaEra2.c.

{
    Gia_ObjAre_t * pNode;
    Gia_StaAre_t * pCube;
    Gia_PtrAre_t iCube, iNext;
    assert( pRoot->nItem || pRoot->nPage );
    pNode = Gia_ManAreCreateObj( p );
    pNode->iVar = Gia_ManAreFindBestVar( p, *pRoot );
    for ( iCube = *pRoot, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext; 
          Gia_StaIsGood(p, pCube); 
          iCube = iNext,  pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext )
    {
        if ( Gia_StaIsUnused(pCube) )
            continue;
        if ( Gia_StaHasValue0(pCube, pNode->iVar) )
            pCube->iNext = pNode->F[0], pNode->F[0] = iCube, pNode->nStas0++;
        else if ( Gia_StaHasValue1(pCube, pNode->iVar) )
            pCube->iNext = pNode->F[1], pNode->F[1] = iCube, pNode->nStas1++;
        else
            pCube->iNext = pNode->F[2], pNode->F[2] = iCube, pNode->nStas2++;
    }
    *pRoot = Gia_Int2Ptr(p->nObjs - 1);
    assert( pNode == Gia_ManAreObj(p, *pRoot) );
    p->fTree = 1;
}

static void Gia_ManAreRycycleSta ( Gia_ManAre_t *  p, Gia_StaAre_t *  pSta  )

inlinestatic

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

Synopsis [Recycles new state.]

Description []

SideEffects []

SeeAlso []

Definition at line 607 of file giaEra2.c.

{
    memset( pSta, 0, p->nSize << 2 );
    if ( pSta == Gia_ManAreStaLast(p) )
    {
        p->nStas--;
        if ( p->nStas == (p->nStaPages-1) * MAX_ITEM_NUM )
            p->nStaPages--;
    }
    else
    {
//        Gia_StaSetUnused( pSta );
    }
}

static Gia_StaAre_t* Gia_ManAreSta ( Gia_ManAre_t *  p, Gia_PtrAre_t  n  )

inlinestatic

Definition at line 136 of file giaEra2.c.

{ return (Gia_StaAre_t *)(p->ppStas[n.nPage] +  n.nItem * p->nSize); }

static Gia_StaAre_t* Gia_ManAreStaInt ( Gia_ManAre_t *  p, int  n  )

inlinestatic

Definition at line 138 of file giaEra2.c.

{ return Gia_ManAreSta( p, Gia_Int2Ptr(n) );               }

static Gia_StaAre_t* Gia_ManAreStaLast ( Gia_ManAre_t *  p )

inlinestatic

Definition at line 140 of file giaEra2.c.

{ return Gia_ManAreStaInt( p, p->nStas-1 );                }

static int Gia_ManCheckPOs ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Counts maximum support of primary outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1475 of file giaEra2.c.

{
    Gia_Obj_t * pObj, * pObjNew;
    int i, CountCur, CountMax = 0;
    Gia_ManForEachPo( p->pAig, pObj, i )
    {
        pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
        if ( Gia_ObjIsConst0(pObjNew) )
            CountCur = 0;
        else 
        {
            Gia_ManIncrementTravId( p->pNew );
            CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew );
        }
        CountMax = Abc_MaxInt( CountMax, CountCur );
    }
    return CountMax;
}

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

static int Gia_ManCheckPOstatus ( Gia_ManAre_t *  p )

inlinestatic

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

Synopsis [Returns the status of the primary outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1505 of file giaEra2.c.

{
    Gia_Obj_t * pObj, * pObjNew;
    int i;
    Gia_ManForEachPo( p->pAig, pObj, i )
    {
        pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
        if ( Gia_ObjIsConst0(pObjNew) )
        {
            if ( Abc_LitIsCompl(pObj->Value) )
            {
                p->iOutFail = i;
                return 1;
            }
        }
        else 
        {
            p->iOutFail = i;
//            printf( "To fix later:  PO may be assertable.\n" );
            return 1;
        }
    }
    return 0;
}

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

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

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

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

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

static int Gia_ObjHasBranch0 ( Gia_ObjAre_t *  q )

inlinestatic

Definition at line 131 of file giaEra2.c.

{ return !q->nStas0 && (q->F[0].nPage || q->F[0].nItem);   }

static int Gia_ObjHasBranch1 ( Gia_ObjAre_t *  q )

inlinestatic

Definition at line 132 of file giaEra2.c.

{ return !q->nStas1 && (q->F[1].nPage || q->F[1].nItem);   }

static int Gia_ObjHasBranch2 ( Gia_ObjAre_t *  q )

inlinestatic

Definition at line 133 of file giaEra2.c.

{ return !q->nStas2 && (q->F[2].nPage || q->F[2].nItem);   }

static Gia_ObjAre_t* Gia_ObjNextObj0 ( Gia_ManAre_t *  p, Gia_ObjAre_t *  q  )

inlinestatic

Definition at line 142 of file giaEra2.c.

{ return Gia_ManAreObj( p, q->F[0] );                      }

static Gia_ObjAre_t* Gia_ObjNextObj1 ( Gia_ManAre_t *  p, Gia_ObjAre_t *  q  )

inlinestatic

Definition at line 143 of file giaEra2.c.

{ return Gia_ManAreObj( p, q->F[1] );                      }

static Gia_ObjAre_t* Gia_ObjNextObj2 ( Gia_ManAre_t *  p, Gia_ObjAre_t *  q  )

inlinestatic

Definition at line 144 of file giaEra2.c.

{ return Gia_ManAreObj( p, q->F[2] );                      }

static unsigned Gia_Ptr2Int ( Gia_PtrAre_t  n )

inlinestatic

Definition at line 129 of file giaEra2.c.

{ Gia_PtrAreInt_t g; g.iGia = n; return g.iInt & 0x7fffffff; }

static int Gia_StaAreContain ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns 1 if cube p1 contains cube p2.]

Description []

SideEffects []

SeeAlso []

Definition at line 377 of file giaEra2.c.

{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( (p1->pData[w] | p2->pData[w]) != p2->pData[w] )
            return 0;
    return 1;
}

static int Gia_StaAreDashNum ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns the number of dashes in p1 that are non-dashes in p2.]

Description []

SideEffects []

SeeAlso []

Definition at line 397 of file giaEra2.c.

{
    int w, Counter = 0;
    for ( w = 0; w < nWords; w++ )
        Counter += Gia_WordCountOnes( (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555 );
    return Counter;
}

static int Gia_StaAreDisjoint ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns 1 if states are disjoint.]

Description []

SideEffects []

SeeAlso []

Definition at line 357 of file giaEra2.c.

{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( ((p1->pData[w] ^ p2->pData[w]) >> 1) & (p1->pData[w] ^ p2->pData[w]) & 0x55555555 )
            return 1;
    return 0;
}

static int Gia_StaAreDisjointVar ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns the number of a variable for merging the cubes.]

Description [If there is exactly one such variable, returns its index. Otherwise returns -1.]

SideEffects []

SeeAlso []

Definition at line 450 of file giaEra2.c.

{
    unsigned Word;
    int w, iVar = -1;
    for ( w = 0; w < nWords; w++ )
    {
        Word = (p1->pData[w] ^ p2->pData[w]) & ((p1->pData[w] ^ p2->pData[w]) >> 1) & 0x55555555;
        if ( Word == 0 )
            continue;
        if ( !Gia_WordHasOneBit(Word) )
            return -1;
        // has exactly one bit
        if ( iVar >= 0 )
            return -1;
        // the first variable of this type
        iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2;
    }
    return iVar;
}

static int Gia_StaAreEqual ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns 1 if states are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file giaEra2.c.

{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( p1->pData[w] != p2->pData[w] )
            return 0;
    return 1;
}

static int Gia_StaAreSharpVar ( Gia_StaAre_t *  p1, Gia_StaAre_t *  p2, int  nWords  )

inlinestatic

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

Synopsis [Returns the number of a variable for sharping the cube.]

Description [Counts the number of variables that have dash in p1 and non-dash in p2. If there is exactly one such variable, returns its index. Otherwise returns -1.]

SideEffects []

SeeAlso []

Definition at line 418 of file giaEra2.c.

{
    unsigned Word;
    int w, iVar = -1;
    for ( w = 0; w < nWords; w++ )
    {
        Word = (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555;
        if ( Word == 0 )
            continue;
        if ( !Gia_WordHasOneBit(Word) )
            return -1;
        // has exactly one bit
        if ( iVar >= 0 )
            return -1;
        // the first variable of this type
        iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2;
    }
    return iVar;
}

static int Gia_StaHasValue0 ( Gia_StaAre_t *  p, int  iReg  )

inlinestatic

Definition at line 146 of file giaEra2.c.

{ return Abc_InfoHasBit( p->pData,  iReg << 1 );           }

static int Gia_StaHasValue1 ( Gia_StaAre_t *  p, int  iReg  )

inlinestatic

Definition at line 147 of file giaEra2.c.

{ return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 );      }

static int Gia_StaIsGood ( Gia_ManAre_t *  p, Gia_StaAre_t *  pS  )

inlinestatic

Definition at line 154 of file giaEra2.c.

{ return ((unsigned *)pS) != p->ppStas[0];                         }

static int Gia_StaIsUnused ( Gia_StaAre_t *  pS )

inlinestatic

Definition at line 157 of file giaEra2.c.

{ return  pS->iPrev.fMark;                                 }

static int Gia_StaIsUsed ( Gia_StaAre_t *  pS )

inlinestatic

Definition at line 158 of file giaEra2.c.

{ return !pS->iPrev.fMark;                                 }

static Gia_StaAre_t* Gia_StaNext ( Gia_ManAre_t *  p, Gia_StaAre_t *  pS  )

inlinestatic

Definition at line 153 of file giaEra2.c.

{ return Gia_ManAreSta(p, pS->iNext);                      }

static Gia_StaAre_t* Gia_StaPrev ( Gia_ManAre_t *  p, Gia_StaAre_t *  pS  )

inlinestatic

Definition at line 152 of file giaEra2.c.

{ return Gia_ManAreSta(p, pS->iPrev);                      }

static void Gia_StaSetUnused ( Gia_StaAre_t *  pS )

inlinestatic

Definition at line 156 of file giaEra2.c.

{ pS->iPrev.fMark = 1;                                     }

static void Gia_StaSetValue0 ( Gia_StaAre_t *  p, int  iReg  )

inlinestatic

Definition at line 149 of file giaEra2.c.

{ Abc_InfoSetBit( p->pData,  iReg << 1 );                  }

static void Gia_StaSetValue1 ( Gia_StaAre_t *  p, int  iReg  )

inlinestatic

Definition at line 150 of file giaEra2.c.

{ Abc_InfoSetBit( p->pData, (iReg << 1) + 1 );             }