path: root/src/aig/gia/giaAbsGla2.c

/**CFile****************************************************************

  FileName    [gia.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Scalable gate-level abstraction.]

  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"

ABC_NAMESPACE_IMPL_START


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

typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
struct Ga2_Man_t_
{
    // user data
    Gia_Man_t *    pGia;            // working AIG manager
    Gia_ParVta_t * pPars;           // parameters
    // internal data
    int            nObjs;           // the number of objects (abstracted and PPIs)
    int            nObjsAlloc;      // the number of allocated objects
    Vec_Int_t *    vAbs;            // array of abstracted objects
    int            nAbs;            // starting abstraction
//    Vec_Int_t *    vExtra;          // additional objects 
    // object structure
    Vec_Int_t *    pvLeaves;        // leaves for each object
    Vec_Int_t *    pvCnf0;          // positive CNF 
    Vec_Int_t *    pvCnf1;          // negative CNF
    Vec_Int_t *    pvMap;           // mapping into SAT vars for each frame  
    // temporaries
    Vec_Int_t *    vCnf;
    Vec_Int_t *    vLits;
    Vec_Int_t *    vIsopMem;
    // other data
    sat_solver2 *  pSat;            // incremental SAT solver
    int            nSatVars;        // the number of SAT variables
    // statistics  
    clock_t        timeStart;
    clock_t        timeInit;
    clock_t        timeSat;
    clock_t        timeUnsat;
    clock_t        timeCex;
    clock_t        timeOther;
};

// returns literal of this object, or -1 if the literal is not assigned
static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )  
{ 
    Vec_Int_t * vMap;
    assert( pObj->fPhase );
    if ( pObj->Value == 0 )
        return -1;
    vMap = &p->pvMap[pObj->Value];
    if ( f < Vec_IntSize(vMap) )
        return -1;
    return Vec_IntEntry( vMap, f );
}
// inserts the literal for this object
static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )  
{ 
    Vec_Int_t * vMap;
    assert( Lit > 1 );
    assert( pObj->fPhase ); 
    assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
    if ( pObj->Value == 0 )
        pObj->Value = p->nObjs++;
    vMap = &p->pvMap[pObj->Value];
    Vec_IntSetEntry( vMap, f, Lit );
}
// returns 
static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )  
{ 
    int Lit = Ga2_ObjFindLit( p, pObj, f );
    if ( Lit == -1 )
    {
        Lit = toLitCond( p->nSatVars++, 0 );
        Ga2_ObjAddLit( p, pObj, f, Lit );
    }
    assert( Lit > 1 );
    return Lit;
}

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

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

  Synopsis    [Returns AIG marked for CNF generation.]

  Description [The marking satisfies the following requirements:
  Each marked node has the number of marked fanins no more than N.]
               
  SideEffects [Uses pObj->fPhase to store the markings.]

  SeeAlso     []

***********************************************************************/
int Ga2_ManBreakTree_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst, int N )
{   // breaks a tree rooted at the node into N-feasible subtrees
    int Val0, Val1;
    if ( pObj->fPhase && !fFirst )
        return 1;
    Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N );
    Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N );
    if ( Val0 + Val1 < N )
        return Val0 + Val1;
    if ( Val0 + Val1 == N )
    {
        pObj->fPhase = 1;
        return 1;
    }
    assert( Val0 + Val1 > N );
    assert( Val0 < N && Val1 < N );
    if ( Val0 >= Val1 )
    {
        Gia_ObjFanin0(pObj)->fPhase = 1;
        Val0 = 1;
    }
    else 
    {
        Gia_ObjFanin1(pObj)->fPhase = 1;
        Val1 = 1;
    }
    if ( Val0 + Val1 < N )
        return Val0 + Val1;
    if ( Val0 + Val1 == N )
    {
        pObj->fPhase = 1;
        return 1;
    }
    assert( 0 );
    return -1;
}
int Ga2_ManCheckNodesAnd( Gia_Man_t * p, Vec_Int_t * vNodes )
{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) || 
             (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) )
            return 0;
    return 1;
}
void Ga2_ManCollectNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, int fFirst )
{
    if ( pObj->fPhase && !fFirst )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 );
    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );

}
void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, int fFirst )
{
    if ( pObj->fPhase && !fFirst )
    {
        Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
}
int Ga2_ManMarkup( Gia_Man_t * p, int N )
{
    clock_t clk = clock();
    Vec_Int_t * vLeaves;
    Gia_Obj_t * pObj;
    int i, CountMarks;
    // label nodes with multiple fanouts and inputs MUXes
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->Value = 0;
        if ( !Gia_ObjIsAnd(pObj) )
            continue;
        Gia_ObjFanin0(pObj)->Value++;
        Gia_ObjFanin1(pObj)->Value++;
        if ( !Gia_ObjIsMuxType(pObj) )
            continue;
        Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++;
        Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++;
        Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++;
        Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++;
    }
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fPhase = 0;
        if ( Gia_ObjIsAnd(pObj) )
            pObj->fPhase = (pObj->Value > 1);
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fPhase = 1;
        else 
            pObj->fPhase = 1;
        pObj->Value = 0;
    } 
    // add marks when needed
    vLeaves = Vec_IntAlloc( 100 );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !pObj->fPhase )
            continue;
        Vec_IntClear( vLeaves );
        Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
        if ( Vec_IntSize(vLeaves) > N )
            Ga2_ManBreakTree_rec( p, pObj, 1, N );
    }
    // verify that the tree is split correctly
    CountMarks = 0;
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !pObj->fPhase )
            continue;
        Vec_IntClear( vLeaves );
        Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
        assert( Vec_IntSize(vLeaves) <= N );
//        printf( "%d ", Vec_IntSize(vLeaves) );
        CountMarks++;
    }
//    printf( "Internal nodes = %d.   ", CountMarks );
    Abc_PrintTime( 1, "Time", clock() - clk );
    Vec_IntFree( vLeaves );
    return CountMarks;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gla_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{
    Gla_Man_t * p;
    int Lit;
    p = ABC_CALLOC( Gla_Man_t, 1 );
    p->pGia  = pGia;
    p->pPars = pPars;
    // internal data
    p->vAbs   = Vec_IntAlloc( 100 );
//    p->vExtra = Vec_IntAlloc( 100 );
    // object structure
    p->nObjsAlloc = 256;
    p->pvLeaves = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
    p->pvCnf0   = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
    p->pvCnf1   = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
    p->pvMap    = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
    // temporaries
    p->vCnf     = Vec_IntAlloc( 100 );
    p->vLits    = Vec_IntAlloc( 100 );
    p->vIsopMem = Vec_IntAlloc( 100 );
    // prepare AIG
    p->timeStart = clock();
    Ga2_ManMarkup( pGia, 5 );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManStop( Gla_Man_t * p )
{
    int i;
//    if ( p->pPars->fVerbose )
        Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Reduce = %d  Cex = %d  ObjsAdded = %d\n", 
            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
    for ( i = 0; i < p->nObjsAlloc; i++ )
    {
        ABC_FREE( p->pvLeaves->pArray );
        ABC_FREE( p->pvCnf0->pArray );
        ABC_FREE( p->pvCnf1->pArray );
        ABC_FREE( p->pvMap->pArray );
    }
    ABC_FREE( p->pvLeaves );
    ABC_FREE( p->pvCnf0 );
    ABC_FREE( p->pvCnf1 );
    ABC_FREE( p->pvMap );
    Vec_IntFree( p->vCnf );
    Vec_IntFree( p->vLits );
    Vec_IntFree( p->vIsopMem );
    Vec_IntFree( p->vAbs );
//    Vec_IntFree( p->vExtra );
    sat_solver2_delete( p->pSat );
    ABC_FREE( p );
}


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

  Synopsis    [Computes truth table for the marked node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
{
    unsigned Val0, Val1;
    if ( pObj->fPhase && !fFirst )
        return pObj->Value;
    assert( Gia_ObjIsAnd(pObj) );
    Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
    Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
    return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
}
unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
{
    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned Res, Values[5];
    Gia_Obj_t * pObj;
    int i;
    // compute leaves
    Vec_IntClear( vLeaves );
    Ga2_ManCollectLeaves_rec( p, pRoot, vLeaves, 1 );
    // assign elementary truth tables
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
    {
        assert( pObj->fPhase );
        Values[i] = pObj->Value;
        pObj->Value = uTruth5[i];
    }
    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
    // return values
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        pObj->Value = Values[i];
    return Res;
}
void Ga2_ManComputeTest( Gia_Man_t * p )
{
    clock_t clk;
    Vec_Int_t * vLeaves;
    Gia_Obj_t * pObj;
    int i;
    Ga2_ManMarkup( p, 5 );
    clk = clock();
    vLeaves = Vec_IntAlloc( 100 );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !pObj->fPhase )
            continue;
        Ga2_ManComputeTruth( p, pObj, vLeaves );
    }
    Vec_IntFree( vLeaves );
    Abc_PrintTime( 1, "Time", clock() - clk );
}

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

  Synopsis    [Computes and minimizes the truth table.]

  Description [Array of input literals may contain 0 (const0), 1 (const1)
  or 2 (literal).  Upon exit, it contains the variables in the support.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v )
{
    assert( v >= 0 && v <= 4 );
    if ( v == 0 )
        return ((t ^ (t >> 1)) & 0x55555555);
    if ( v == 1 )
        return ((t ^ (t >> 2)) & 0x33333333);
    if ( v == 2 )
        return ((t ^ (t >> 4)) & 0x0F0F0F0F);
    if ( v == 3 )
        return ((t ^ (t >> 8)) & 0x00FF00FF);
    if ( v == 4 )
        return ((t ^ (t >>16)) & 0x0000FFFF);
    return -1;
}
unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits )
{
    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned Res, Values[5];
    Gia_Obj_t * pObj;
    int i, k, Entry;
    // assign elementary truth tables
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
    {
        assert( pObj->fPhase );
        Values[i] = pObj->Value;
        Entry = Vec_IntEntry( vLits, i );
        assert( Entry >= 0 && Entry <= 2 );
        if ( Entry == 0 )
            pObj->Value = 0;
        else if ( Entry == 1 )
            pObj->Value = ~0;
        else // if ( Entry == 2 )
            pObj->Value = uTruth5[i];
    }
    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
    Vec_IntClear( vLits );
    if ( Res != 0 && Res != ~0 )
    {
        // check if truth table depends on them
        k = 0;
        Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        {
            if ( Ga2_ObjTruthDepends( Res, i ) )
            {
                pObj->Value = uTruth5[k++];
                Vec_IntPush( vLits, i );
            }
        }
        // recompute the truth table
        Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
        // verify that the true table depends on them
        for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
            assert( (i < Vec_IntSize(vLits)) == (Ga2_ObjTruthDepends(Res, i) > 0) );
    }
    // return values
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        pObj->Value = Values[i];
    return Res;
}

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

  Synopsis    [Returns CNF of the function.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCnf, Vec_Int_t * vCover )
{
    extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
    int i, k, Cube, Literal, NewCube, RetValue;
    assert( n == 5 );
    // transform truth table into the SOP
    RetValue = Kit_TruthIsop( &uTruth, 5, vCover, 0 );
    assert( RetValue == 0 );
    // check the case of constant cover
    Vec_IntClear( vCnf );
    Vec_IntForEachEntry( vCover, Cube, i )
    {
        for ( k = 0; k < nVars; k++ )
        {
            Literal = 3 & (Cube >> (k << 1));
            if ( Literal == 1 )
//                pCube[k] = '0';
                NewCube = NewCube * 3 + 0;
            else if ( Literal == 2 )
//                pCube[k] = '1';
                NewCube = NewCube * 3 + 1;
            else if ( Literal == 0 )
                NewCube = NewCube * 3 + 2;
            else
                assert( 0 );
        }
        Vec_IntPush( vCnf, NewCube );
    }
}


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

  Synopsis    [Derives CNF for one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManCnfAddClause( Vec_Int_t * vCnf, int Lits[], int iLitOut, int ProofId )
{
    int k, b, Clause, nClaLits, ClaLits[6];
//    for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
    Vec_IntForEacEntry( vCnf, Clause, k )
    {
        nClaLits = 0;
        ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
//        Clause = p->pSops[uTruth][k];
        for ( b = 3; b >= 0; b-- )
        {
            if ( Clause % 3 == 0 ) // value 0 --> write positive literal
            {
                assert( Lits[b] > 1 );
                ClaLits[nClaLits++] = Lits[b];
            }
            else if ( Clause % 3 == 1 ) // value 1 --> write negative literal
            {
                assert( Lits[b] > 1 );
                ClaLits[nClaLits++] = lit_neg(Lits[b]);
            }
            Clause = Clause / 3;
        }
        sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ) );
    }
}
void Ga2_ManCnfAddPrecomputed( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut )
{
    int i, k;
    assert( uTruth > 0 && uTruth < 0xffff );
    // write positive/negative polarity
    for ( i = 0; i < 2; i++ )
    {
        if ( i )
            uTruth = 0xffff & ~uTruth;
//        Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
        Vec_IntClear( p->vCnf );
        for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
            Vec_IntPush( p->vCnf, p->pSops[uTruth][k] );
        Ga2_ManCnfAddClause( p->vCnf, Lits, (i ? lit_neg(iLitOut) : iLitOut), ProofId );
    }
}
void Ga2_ManCnfAddDerived( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut )
{
    Ga2_ManCnfAddClause( vCnf0, Lits, iLitOut,          ProofId );
    Ga2_ManCnfAddClause( vCnf1, Lits, lit_neg(iLitOut), ProofId );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
    int Id = p->nObjs++;
    Vec_Int_t * vLeaves  = &p->pvLeaves[Id];
    Vec_Int_t * vCnf0    = &p->pvCnfs0[Id];
    Vec_Int_t * vCnf1    = &p->pvCnfs1[Id];
    Vec_Int_t * vMap     = &p->pvMaps[Id];
    unsigned uTruth;
    assert( pObj->Value == 0 );
    assert( p->nObjs > 1 );
    // prepare leaves
    if ( Vec_IntSize(vLeaves) == 0 )
    {
        Vec_IntGrow( vLeaves, 5 );
        Ga2_ManCollectLeaves_rec( p->pGia, pObj, vLeaves, 1 );
        assert( Vec_IntSize(vLeaves) < 6 );
        // compute truth table
        uTruth = Ga2_ManComputeTruth( p->pGia, pObj, vLeaves );
        // prepare CNF
        Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf0, p->vCover );
        uTruth = (~uTruth) & ~((~0) << (1 << Vec_IntSize(vLeaves)));
        Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf1, p->vCover );
        // prepare mapping
        Vec_IntGrow( vLeaves, 100 );
    }
    else
        Vec_IntClear( vMap );
    // remember the number
    pObj->Value = Id;
    // realloc
    if ( p->nObjs == p->nObjsAlloc )
    {
        p->pvLeaves = ABC_REALLOC( Vec_Int_t, p->pvLeaves, 2 * p->nObjsAlloc );
        p->pvCnfs0  = ABC_REALLOC( Vec_Int_t, p->pvCnfs0,  2 * p->nObjsAlloc );
        p->pvCnfs1  = ABC_REALLOC( Vec_Int_t, p->pvCnfs1,  2 * p->nObjsAlloc );
        p->pvMaps   = ABC_REALLOC( Vec_Int_t, p->pvMaps,   2 * p->nObjsAlloc );
        memset( p->pvLeaves + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
        memset( p->pvCnfs0  + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
        memset( p->pvCnfs1  + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
        memset( p->pvMaps   + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
        p->nObjsAlloc *= 2;
    }
}
void Ga2_ManSetdownNode( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
    assert( pObj->Value > 0 );
    pObj->Value = 0;
}
void Ga2_ManAddNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
    assert( pObj->Value > 0 );

}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManRestart( Ga2_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    assert( p->pGia != NULL );
    assert( p->pGia->vGateClasses != NULL );
    assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
    // clear mappings from objects
    for ( i = 1; i < p->nObjs; i++ )
    {
        Vec_IntShrink( &p->pvLeaves[i], 0 );
        Vec_IntShrink( &p->pvCnfs0[i], 0 );
        Vec_IntShrink( &p->pvCnfs1[i], 0 );
        Vec_IntShrink( &p->pvMaps[i], 0 );
    }
    // clear SAT variable numbers (begin with 1)
    if ( p->pSat ) sat_solver2_delete( p->pSat );
    p->pSat      = sat_solver2_new();
    p->nSatVars  = 1;
    // create constant literal
    Lit = toLitCond( 1, 1 );
    sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 );
    // collect abstraction
    p->nObjs = 1;
    Gia_ManCleanValue( p->pGia );
    Vec_IntClear( p->vAbs );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( pObj->fPhase && Vec_IntEntry(p->pGia->vGateClasses, i) )
        {
            Vec_IntPush( p->vAbs, i );
            Ga2_ManSetupNode( p, pObj );
        }
    }
    p->nAbs = Vec_IntSize( p->vAbs );
    // set runtime limit
    if ( p->pPars->nTimeOut )
        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
{
    if ( pObj->fPhase && !fFirst )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
    Ga2_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
    Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
}
Vec_Int_t * Ga2_ManTranslate( Ga2_Man_t * p )
{
    Vec_Int_t * vGateClasses;
    Gia_Obj_t * pObj;
    int i;
    vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
    Gia_ManForEachObjVec( p->vAbs, p, pObj, i )
        Ga2_ManTranslate_rec( p, pObj, vGateClasses, 1 );
    return vGateClasses;
}

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

  Synopsis    [Unrolls one timeframe.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_ManUnroll( Ga2_Man_t * p, int f )
{
    Gia_Obj_t * pObj, * pObjRi, * pLeaf;
    unsigned uTruth;
    int i, k, Lit, fFullTable;
    // construct CNF for internal nodes
    Gia_ManForEachObjVec( p->vAbs, p, pObj, i )
    {
        // assign RO literal values (no need to add clauses)
        assert( pObj->fPhase && pObj->Value );
        if ( Gia_ObjIsConst0(pObj) )
        {
            Ga2_ObjAddLit( p, pObj, f, 3 ); // const 0 
            continue;
        }
        if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            pObjRi = Gia_ObjRoToRi(p->pGia, pObj);
            Lit = f ? Ga2_ObjFindOrAddLit( p, pObjRi, f-1 ) : 3;  // const 0
            Ga2_ObjAddLit( p, pObj, f, Lit ); 
            continue;
        }
        assert( Gia_ObjIsAnd(pObj) );
        vLeaves = Ga2_ManReadLeaves( p, pObj );
        // for nodes recently added to abstration, add CNF without const propagation
        fFullTable = 1;
        if ( i < p->nAbs )
        {
            Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
            {
                Lit = Ga2_ObjReadLit( p, pLeaf, f );
                if ( Lit == 2 || Lit == 3 )
                {
                    fFullTable = 0;
                    break;
                }
            }
        }
        if ( fFullTable )
        {
            Vec_IntClear( p->vLits );
            Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
                Vec_IntWriteEntry( p->vLits, Ga2_ObjFindOrAddLit(p, pLeaf, f) );        
            iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f);
            Ga2_ManCnfAddClause( vCnf0, Vec_IntArray(p->vLits), iLitOut,          i < p->nAbs ? 0 : Gia_ObjId(p->pGia, pObj) );
            Ga2_ManCnfAddClause( vCnf1, Vec_IntArray(p->vLits), lit_neg(iLitOut), i < p->nAbs ? 0 : Gia_ObjId(p->pGia, pObj) );
            continue;
        }
        assert( i < p->nAbs );
        // collect literal types
        Vec_IntClear( p->vLits );
        Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
        {
            Lit = Ga2_ObjReadLit( p, pLeaf, f );
            if ( Lit == 3 ) // const 0
                Vec_IntPush( p->vLits, 0 );
            else if ( Lit == 2 ) // const 1
                Vec_IntPush( p->vLits, 1 );
            else 
                Vec_IntPush( p->vLits, 2 );
        }
        uTruth = Ga2_ObjComputeTruthSpecial( p, pObj, vLeaves, p->vLits );
        if ( uTruth == 0 || uTruth == ~0 )
            Ga2_ObjAddLit( p, pObj, f, uTruth == 0 ? 3 : 2 );     // const 0 / 1
        else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 )  // buffer / inverter
        {
            Lit = Vec_IntEntry( p->vLits, 0 );
            pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) );
            Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
            Ga2_ObjAddLit( p, pObj, f, Abc_LitNotCond(Lit, uTruth == 0x55555555) );
        }
        else
        {
            // replace numbers of literals by actual literals
            Vec_IntForEachEntry( p->vLits, Lit, i )
            {
                pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) );
                Lit = Ga2_ObjFindOrAddLit(p, pLeaf, f);
                Vec_IntWriteEntry( p->vLits, Lit );        
            }
            // add CNF
            iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f);
            Ga2_ManCnfAddPrecomputed( p, uTruth, Vec_IntArray(p->vLits), iLitOut );
        }

    }
    // propagate literals to the PO and flop outputs
    pObjRi = Gia_ManPo( p->pGia, 0 );
    Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f );
    assert( Lit > 1 );
    Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) );
    Ga2_ObjAddLit( p, pObj, f, Lit ); 
    Gia_ManForEachObjVec( p->vAbs, p, pObj, i )
    {
        if ( !Gia_ObjIsRo(p->pGia, pObj) )
            continue;
        pObjRi = Gia_ObjRoToRi(p->pGia, pObj);
        Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f );
        assert( Lit > 1 );
        Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) );
        Ga2_ObjAddLit( p, pObjRi, f, Lit ); 
    }
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Vec_IntCheckUnique( Vec_Int_t * p )
{
    int RetValue;
    Vec_Int_t * pDup = Vec_IntDup( p );
    Vec_IntUniqify( pDup );
    RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
    Vec_IntFree( pDup );
    return RetValue;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ga2_ManRefine( Gla_Man_t * p )
{
    return NULL;
}

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

  Synopsis    [Performs gate-level abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
    Gla_Man_t * p;
    Vec_Int_t * vCore, * vPPis;
    clock_t clk = clock();
    int i, c, f, Lit, Status, RetValue = -1;;
    // start the manager
    p = Ga2_ManStart( pAig, pPars );
    // check trivial case 
    assert( Gia_ManPoNum(pAig) == 1 );
    ABC_FREE( pAig->pCexSeq );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            printf( "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        printf( "Sequential miter is trivially SAT.\n" );
        return 0;
    }
    // create gate classes if not given
    if ( pAig->vGateClasses == NULL )
    {
        pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
        Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
        Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
    }
    // start the manager
    p = Gla_ManStart( pAig, pPars );
    p->timeInit = clock() - clk;
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%.\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
        Abc_Print( 1, "LearnStart = %d  LearnDelta = %d  LearnRatio = %d %%.\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time      Mem\n" );
    }
    // iterate unrolling
    for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
    {
        // create new SAT solver
        Ga2_ManRestart( p );
        // unroll the circuit
        for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
        {
            // add one more time-frame
            Ga2_ManUnroll( p, f );
            // check for counter-examples
            for ( c = 0; ; c++ )
            {
                // perform SAT solving
                Lit = Ga2_ObjFindOrAddLit( p, Gia_ManPo(p->pGia, 0), f );
                Status = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( Status == l_True ) // perform refinement
                {
                    vPPis = Ga2_ManRefine( p );
                    if ( vPPis == NULL )
                        goto finish;
                    Vec_IntAppend( p->vAbs, vPPis );
                    Vec_IntFree( vPPis );
                    if ( Vec_IntCheckUnique(p->vAbs) )
                        printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
                    continue;
                }
                if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout
                    goto finish;
                if ( Status == l_Undef ) // ran out of resources
                    goto finish;
                assert( RetValue == l_False );
                // derive UNSAT core
                vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
                Vec_IntAppend( p->vAbs, vCore );
                Vec_IntSort( p->vAbs, 0 ); // check unique!!!
                Vec_IntFree( vCore );
                if ( Vec_IntCheckUnique(p->vAbs) )
                    printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
                break;
            }
            if ( c > 0 )
            {
                Vec_IntFreeP( &pAig->vGateClasses );
                pAig->vGateClasses = Ga2_ManTranslate( p );
                break;
            }
        }
        // check if the number of objects is below limit
        if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
        {
            Status = l_Undef;
            break;
        }
    }
finish:
    // analize the results
    if ( pAig->pCexSeq == NULL )
    {
        if ( pAig->vGateClasses != NULL )
            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Ga2_ManTranslate( p );
        if ( Status == l_Undef )
        {
            if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
                Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
            else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
            else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
                Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
            else
                Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
        }
        else
        {
            p->pPars->iFrame++;
            Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction.  ", f );
        }
    }
    else
    {
        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            Abc_Print( 1, "    Gia_GlaPerform(): CEX verification has failed!\n" );
        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = pCex->iFrame - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
    }
    Abc_PrintTime( 1, "Time", clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
        Gla_ManReportMemory( p );
    }
    Gla_ManStop( p );
    fflush( stdout );
    return RetValue;


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


ABC_NAMESPACE_IMPL_END