/**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 $]

***********************************************************************/

#include "gia.h"
#include "giaAig.h"

ABC_NAMESPACE_IMPL_START

/*
    Limitations of this package:
    - no more than (1<<31)-1 state cubes and internal nodes
    - no more than MAX_VARS_NUM state variables
    - no more than MAX_CALL_NUM transitions from a state
    - cube list rebalancing happens when cube count reaches MAX_CUBE_NUM
*/

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

#define MAX_CALL_NUM    (1000000)  // the max number of recursive calls
#define MAX_ITEM_NUM      (1<<20)  // the number of items on a page
#define MAX_PAGE_NUM      (1<<11)  // the max number of memory pages
#define MAX_VARS_NUM      (1<<14)  // the max number of state vars allowed
#define MAX_CUBE_NUM          63   // the max number of cubes before rebalancing

// pointer to the tree node or state cube
typedef struct Gia_PtrAre_t_ Gia_PtrAre_t;
struct Gia_PtrAre_t_
{
    unsigned       nItem    : 20;  // item number (related to MAX_ITEM_NUM)
    unsigned       nPage    : 11;  // page number (related to MAX_PAGE_NUM)
    unsigned       fMark    :  1;  // user mark
};

typedef union Gia_PtrAreInt_t_ Gia_PtrAreInt_t;
union Gia_PtrAreInt_t_
{
    Gia_PtrAre_t   iGia;
    unsigned       iInt;
};

// tree nodes
typedef struct Gia_ObjAre_t_ Gia_ObjAre_t;
struct Gia_ObjAre_t_
{
    unsigned       iVar     : 14;  // variable     (related to MAX_VARS_NUM)
    unsigned       nStas0   :  6;  // cube counter (related to MAX_CUBE_NUM)
    unsigned       nStas1   :  6;  // cube counter (related to MAX_CUBE_NUM)
    unsigned       nStas2   :  6;  // cube counter (related to MAX_CUBE_NUM)
    Gia_PtrAre_t   F[3];           // branches
};

// state cube
typedef struct Gia_StaAre_t_ Gia_StaAre_t;
struct Gia_StaAre_t_
{
    Gia_PtrAre_t   iPrev;          // previous state
    Gia_PtrAre_t   iNext;          // next cube in the list
    unsigned       pData[0];       // state bits
};

// explicit state reachability manager
typedef struct Gia_ManAre_t_ Gia_ManAre_t;
struct Gia_ManAre_t_
{
    Gia_Man_t *    pAig;           // user's AIG manager
    Gia_Man_t *    pNew;           // temporary AIG manager
    unsigned **    ppObjs;         // storage for objects (MAX_PAGE_NUM pages)
    unsigned **    ppStas;         // storage for states  (MAX_PAGE_NUM pages)
//    unsigned *     pfUseless;      // to label useless cubes
//    int            nUselessAlloc;  // the number of useless alloced
    // internal flags
    int            fMiter;         // stops when a bug is discovered
    int            fStopped;       // set high when reachability is stopped
    int            fTree;          // working in the tree mode
    // internal parametesr
    int            nWords;         // the size of bit info in words
    int            nSize;          // the size of state structure in words
    int            nObjPages;      // the number of pages used for objects
    int            nStaPages;      // the number of pages used for states
    int            nObjs;          // the number of objects 
    int            nStas;          // the number of states  
    int            iStaCur;        // the next state to be explored
    Gia_PtrAre_t   Root;           // root of the tree
    Vec_Vec_t *    vCiTfos;        // storage for nodes in the CI TFOs
    Vec_Vec_t *    vCiLits;        // storage for literals of these nodes
    Vec_Int_t *    vCubesA;        // checked cubes
    Vec_Int_t *    vCubesB;        // unchecked cubes
    // deriving counter-example
    void *         pSat;           // SAT solver
    Vec_Int_t *    vSatNumCis;     // SAT variables for CIs
    Vec_Int_t *    vSatNumCos;     // SAT variables for COs 
    Vec_Int_t *    vCofVars;       // variables used to cofactor
    Vec_Int_t *    vAssumps;       // temporary storage for assumptions
    Gia_StaAre_t * pTarget;        // state that needs to be reached
    int            iOutFail;       // the number of the failed output
    // statistics
    int            nChecks;        // the number of timea cube was checked
    int            nEquals;        // total number of equal
    int            nCompares;      // the number of compares
    int            nRecCalls;      // the number of rec calls
    int            nDisjs;         // the number of disjoint cube pairs
    int            nDisjs2;        // the number of disjoint cube pairs
    int            nDisjs3;        // the number of disjoint cube pairs
    // time
    int            timeAig;        // AIG cofactoring time
    int            timeCube;       // cube checking time 
}; 

static inline Gia_PtrAre_t    Gia_Int2Ptr( unsigned n )                               { Gia_PtrAreInt_t g; g.iInt = n; return g.iGia;            }
static inline unsigned        Gia_Ptr2Int( Gia_PtrAre_t n )                           { Gia_PtrAreInt_t g; g.iGia = n; return g.iInt & 0x7fffffff; }

static inline int             Gia_ObjHasBranch0( Gia_ObjAre_t * q )                   { return !q->nStas0 && (q->F[0].nPage || q->F[0].nItem);   }
static inline int             Gia_ObjHasBranch1( Gia_ObjAre_t * q )                   { return !q->nStas1 && (q->F[1].nPage || q->F[1].nItem);   }
static inline int             Gia_ObjHasBranch2( Gia_ObjAre_t * q )                   { return !q->nStas2 && (q->F[2].nPage || q->F[2].nItem);   }

static inline Gia_ObjAre_t *  Gia_ManAreObj( Gia_ManAre_t * p, Gia_PtrAre_t n )       { return (Gia_ObjAre_t *)(p->ppObjs[n.nPage] + (n.nItem << 2));      }
static inline Gia_StaAre_t *  Gia_ManAreSta( Gia_ManAre_t * p, Gia_PtrAre_t n )       { return (Gia_StaAre_t *)(p->ppStas[n.nPage] +  n.nItem * p->nSize); }
static inline Gia_ObjAre_t *  Gia_ManAreObjInt( Gia_ManAre_t * p, int n )             { return Gia_ManAreObj( p, Gia_Int2Ptr(n) );               }
static inline Gia_StaAre_t *  Gia_ManAreStaInt( Gia_ManAre_t * p, int n )             { return Gia_ManAreSta( p, Gia_Int2Ptr(n) );               }
static inline Gia_ObjAre_t *  Gia_ManAreObjLast( Gia_ManAre_t * p )                   { return Gia_ManAreObjInt( p, p->nObjs-1 );                }
static inline Gia_StaAre_t *  Gia_ManAreStaLast( Gia_ManAre_t * p )                   { return Gia_ManAreStaInt( p, p->nStas-1 );                }

static inline Gia_ObjAre_t *  Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t * q )   { return Gia_ManAreObj( p, q->F[0] );                      }
static inline Gia_ObjAre_t *  Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q )   { return Gia_ManAreObj( p, q->F[1] );                      }
static inline Gia_ObjAre_t *  Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q )   { return Gia_ManAreObj( p, q->F[2] );                      }

static inline int             Gia_StaHasValue0( Gia_StaAre_t * p, int iReg )          { return Abc_InfoHasBit( p->pData,  iReg << 1 );           }
static inline int             Gia_StaHasValue1( Gia_StaAre_t * p, int iReg )          { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 );      }

static inline void            Gia_StaSetValue0( Gia_StaAre_t * p, int iReg )          { Abc_InfoSetBit( p->pData,  iReg << 1 );                  }
static inline void            Gia_StaSetValue1( Gia_StaAre_t * p, int iReg )          { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 );             }

static inline Gia_StaAre_t *  Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS )      { return Gia_ManAreSta(p, pS->iPrev);                      }
static inline Gia_StaAre_t *  Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS )      { return Gia_ManAreSta(p, pS->iNext);                      }
static inline int             Gia_StaIsGood( Gia_ManAre_t * p, Gia_StaAre_t * pS )    { return ((unsigned *)pS) != p->ppStas[0];                         }

static inline void            Gia_StaSetUnused( Gia_StaAre_t * pS )                   { pS->iPrev.fMark = 1;                                     }
static inline int             Gia_StaIsUnused( Gia_StaAre_t * pS )                    { return  pS->iPrev.fMark;                                 }
static inline int             Gia_StaIsUsed( Gia_StaAre_t * pS )                      { return !pS->iPrev.fMark;                                 }

#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 )                 \
    for ( iCube = Gia_Ptr2Int(iList), pCube = Gia_ManAreSta(p, iList);       \
          Gia_StaIsGood(p, pCube);                                           \
          iCube = Gia_Ptr2Int(pCube->iNext), pCube = Gia_StaNext(p, pCube) )
#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++ )

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Count state minterms contained in a cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pStore )
{
    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 );
    }
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCountMinterms( Gia_ManAre_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Derives the TFO of one CI.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManDeriveCiTfo_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRes )
{
    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;
}


/**Function*************************************************************

  Synopsis    [Derives the TFO of one CI.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_ManDeriveCiTfoOne( Gia_Man_t * p, Gia_Obj_t * pPivot )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Derives the TFO of each CI.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Vec_t * Gia_ManDeriveCiTfo( Gia_Man_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Returns 1 if states are equal.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_StaAreEqual( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( p1->pData[w] != p2->pData[w] )
            return 0;
    return 1;
}

/**Function*************************************************************

  Synopsis    [Returns 1 if states are disjoint.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_StaAreDisjoint( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    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;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_StaAreContain( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( (p1->pData[w] | p2->pData[w]) != p2->pData[w] )
            return 0;
    return 1;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_StaAreDashNum( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    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;
}

/**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     []

***********************************************************************/
static inline int Gia_StaAreSharpVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    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;
}

/**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     []

***********************************************************************/
static inline int Gia_StaAreDisjointVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Creates reachability manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Deletes reachability manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManAreFree( Gia_ManAre_t * p )
{
    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 );
}

/**Function*************************************************************

  Synopsis    [Returns new object.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Gia_ObjAre_t * Gia_ManAreCreateObj( Gia_ManAre_t * p )
{
    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++ );
}

/**Function*************************************************************

  Synopsis    [Returns new state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Gia_StaAre_t * Gia_ManAreCreateSta( Gia_ManAre_t * p )
{
    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++ );
}

/**Function*************************************************************

  Synopsis    [Recycles new state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManAreRycycleSta( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
{
    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 );
    }
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Gia_StaAre_t * Gia_ManAreCreateStaNew( Gia_ManAre_t * p )
{
    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;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Gia_StaAre_t * Gia_ManAreCreateStaInit( Gia_ManAre_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachRi( p->pAig, pObj, i )
        pObj->Value = 0;
    return Gia_ManAreCreateStaNew( p );
}


/**Function*************************************************************

  Synopsis    [Prints the state cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManArePrintCube( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
{
    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" );
}
 
/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreDepth( Gia_ManAre_t * p, int iState )
{
    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;
} 

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManAreListCountListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root )
{
    Gia_StaAre_t * pCube;
    int Counter = 0;
    Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
        Counter += Gia_StaIsUsed(pCube);
    return Counter;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreListCountUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree )
{
    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) );
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManAreListCountUsed( Gia_ManAre_t * p )
{
    return Gia_ManAreListCountUsed_rec( p, p->Root, p->fTree );
}


/**Function*************************************************************

  Synopsis    [Prints used cubes in the list.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManArePrintListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root )
{
    Gia_StaAre_t * pCube;
    Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
        if ( Gia_StaIsUsed(pCube) )
            Gia_ManArePrintCube( p, pCube );
    return 1;
}

/**Function*************************************************************

  Synopsis    [Prints used cubes in the tree.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManArePrintUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree )
{
    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) );
}

/**Function*************************************************************

  Synopsis    [Prints used cubes in the tree.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManArePrintUsed( Gia_ManAre_t * p )
{
    return Gia_ManArePrintUsed_rec( p, p->Root, p->fTree );
}


/**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     []

***********************************************************************/
int Gia_ManAreFindBestVar( Gia_ManAre_t * p, Gia_PtrAre_t List )
{
    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;
}
 
/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManAreRebalance( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot )
{
    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;
}
 
/**Function*************************************************************

  Synopsis    [Compresses the list by removing unused cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManAreCompress( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot )
{
    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;
    }
}


/**Function*************************************************************

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

  Description [The state may be sharped.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManAreCubeCheckList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Adds new state to the list.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManAreCubeAddToList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
{
    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" );
}
}
 
/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreCubeCheckTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
{
    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 );
}

/**Function*************************************************************

  Synopsis    [Adds new cube to the tree.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManAreCubeAddToTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
{
    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;
                }
            }
        }
    }
}


/**Function*************************************************************

  Synopsis    [Collects overlapping cubes in the list.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManAreCubeCollectList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Collects overlapping cubes in the tree.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreCubeCollectTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
{
    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 );
}
 
/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreCubeCheckTree( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Processes the new cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManAreCubeProcess( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
{
    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;
}


/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManAreMostUsedPi_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
    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) );
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Counts maximum support of primary outputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCheckPOs_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
    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) );
}

/**Function*************************************************************

  Synopsis    [Counts maximum support of primary outputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Returns the status of the primary outputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Derives next state cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Derives next state cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
{
    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;
}

 
/**Function*************************************************************

  Synopsis    [Prints the report]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManArePrintReport( Gia_ManAre_t * p, abctime Time, int fFinal )
{
    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 );
    }
}
 
/**Function*************************************************************

  Synopsis    [Performs explicit reachability.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose )
{
//    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;
}

ABC_NAMESPACE_IMPL_END

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

ABC_NAMESPACE_IMPL_START


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManAreDeriveCexSatStart( Gia_ManAre_t * p )
{
    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 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManAreDeriveCexSatStop( Gia_ManAre_t * p )
{
    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;
}

/**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     []

***********************************************************************/
void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t * pNext, int iOutFailed )
{
    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 );
    }
}

/**Function*************************************************************

  Synopsis    [Returns the status of the cone.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
{
    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;
}


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END