acecCore.c

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

  FileName    [acecCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [CEC for arithmetic circuits.]

  Synopsis    [Core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: acecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "acecInt.h"
#include "proof/cec/cec.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"

ABC_NAMESPACE_IMPL_START


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

#define TRUTH_UNUSED 0x1234567812345678

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

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

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
{
    memset( p, 0, sizeof(Acec_ParCec_t) );
    p->nBTLimit       =    1000;    // conflict limit at a node
    p->TimeLimit      =       0;    // the runtime limit in seconds
    p->fMiter         =       0;    // input circuit is a miter
    p->fDualOutput    =       0;    // dual-output miter
    p->fTwoOutput     =       0;    // two-output miter
    p->fSilent        =       0;    // print no messages
    p->fVeryVerbose   =       0;    // verbose stats
    p->fVerbose       =       0;    // verbose stats
    p->iOutFail       =      -1;    // the number of failed output
}  

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs )
{
    Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) );
    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
    Vec_Int_t * vLevel;
    int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0;
    Vec_WecForEachLevel( vLits, vLevel, i )
    {
        Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) );
        Vec_IntForEachEntry( vLevel, Entry, k )
        {
            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
            if ( Vec_IntSize(vSupp) > 6  )
            {
                nOvers++;
                Vec_WrdPush( vTruths, TRUTH_UNUSED );
                continue;
            }
            vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
            if ( Vec_IntSize(vSupp) > 5  )
            {
                nOvers++;
                Vec_WrdPush( vTruths, TRUTH_UNUSED );
                continue;
            }
            Vec_WrdPush( vTruths, Truth );
        }
        Vec_PtrPush( vFunc, vTruths );
    }
    if ( nOvers )
        printf( "Detected %d oversize support nodes.\n", nOvers );
    Vec_IntFree( vSupp );
    Vec_WrdFree( vTemp );
    // verify the classes
    Vec_WecForEachLevel( vReprs, vLevel, i )
    {
        Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i );
        Vec_IntForEachEntry( vLevel, Entry, k )
        Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 )
        {
            word Truth = Vec_WrdEntry( vTruths, k );
            word Truth2 = Vec_WrdEntry( vTruths, j );
            if ( Entry == Entry2 )
            {
                nErrors++;
                if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
            }
            if ( Entry == Abc_LitNot(Entry2) )
            {
                nErrors++;
                if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
            }
        }
    }
    if ( nErrors )
        printf( "Total errors in equivalence classes = %d.\n", nErrors );
    Vec_VecFree( (Vec_Vec_t *)vFunc );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManFillValue( pAdd );
    Gia_ManConst0(pAdd)->Value = 0;
    if ( pBase == NULL )
    {
        pBase = Gia_ManStart( Gia_ManObjNum(pAdd) );
        pBase->pName = Abc_UtilStrsav( pAdd->pName );
        pBase->pSpec = Abc_UtilStrsav( pAdd->pSpec );
        Gia_ManForEachCi( pAdd, pObj, i )
            pObj->Value = Gia_ManAppendCi(pBase);
        Gia_ManHashAlloc( pBase );
    }
    else
    {
        assert( Gia_ManCiNum(pBase) == Gia_ManCiNum(pAdd) );
        Gia_ManForEachCi( pAdd, pObj, i )
            pObj->Value = Gia_Obj2Lit( pBase, Gia_ManCi(pBase, i) );
    }
    Gia_ManForEachAnd( pAdd, pObj, i )
        pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    return pBase;
}
void Acec_CommonFinish( Gia_Man_t * pBase )
{
    int Id;
    Gia_ManCreateRefs( pBase );
    Gia_ManForEachAndId( pBase, Id )
        if ( Gia_ObjRefNumId(pBase, Id) == 0 )
            Gia_ManAppendCo( pBase, Abc_Var2Lit(Id,0) );
}
Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
{
    Gia_Obj_t * pObj; int i;
    Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
    Gia_ManSetPhase( pAdd );
    Vec_IntWriteEntry( vMapNew, 0, 0 );
    Gia_ManForEachCand( pAdd, pObj, i )
    {
        int iObjBase = Abc_Lit2Var(pObj->Value);
        Gia_Obj_t * pObjBase = Gia_ManObj( pBase, iObjBase );
        int iObjRepr = Abc_Lit2Var(pObjBase->Value);
        Vec_IntWriteEntry( vMapNew, i, Abc_Var2Lit(iObjRepr, Gia_ObjPhase(pObj)) );
    }
    return vMapNew;
}
void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
{
    abctime clk = Abc_Clock();
    Gia_Man_t * pBase, * pRepr;
    pBase = Acec_CommonStart( NULL, pOne );
    pBase = Acec_CommonStart( pBase, pTwo );
    Acec_CommonFinish( pBase );
    //Gia_ManShow( pBase, NULL, 0, 0, 0 );
    pRepr = Gia_ManComputeGiaEquivs( pBase, 100, 0 );
    *pvMap1 = Acec_CountRemap( pOne, pBase );
    *pvMap2 = Acec_CountRemap( pTwo, pBase );
    Gia_ManStop( pBase );
    Gia_ManStop( pRepr );
    printf( "Finished computing equivalent nodes.  " );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
{
    int i, j, best_i;
    for ( i = 0; i < nSize-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nSize; j++ )
            if ( Abc_Lit2LitL(pCostLits, pArray[j]) > Abc_Lit2LitL(pCostLits, pArray[best_i]) )
                best_i = j;
        ABC_SWAP( int, pArray[i], pArray[best_i] );
    }
}
void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
{
    Vec_Int_t * vSupp;
    Vec_Wrd_t * vTemp;
    Vec_Int_t * vLevel;
    int i, k, Entry;
    printf( "Leaf literals and their classes:\n" );
    Vec_WecForEachLevel( vLits, vLevel, i )
    {
        if ( Vec_IntSize(vLevel) == 0 )
            continue;
        printf( "Rank %2d : %2d  ", i, Vec_IntSize(vLevel) );
        Vec_IntForEachEntry( vLevel, Entry, k )
            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
        printf( "\n" );
    }
    if ( !fVerbose )
        return;
    vSupp = Vec_IntAlloc( 100 );
    vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
    Vec_WecForEachLevel( vLits, vLevel, i )
    {
        //if ( i != 20 )
        //    continue;
        if ( Vec_IntSize(vLevel) == 0 )
            continue;
        Vec_IntForEachEntry( vLevel, Entry, k )
        {
            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
/*
            {
                int iObj = Abc_Lit2Var(Entry);
                Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
                Gia_ManShow( pGia0, NULL, 0, 0, 0 );
                Gia_ManStop( pGia0 );
            }
*/
            printf( "Rank = %4d : ", i );
            printf( "Obj = %4d  ", Abc_Lit2Var(Entry) );
            if ( Vec_IntSize(vSupp) > 6  )
            {
                printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
                continue;
            }
            vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
            if ( Vec_IntSize(vSupp) > 5  )
            {
                printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
                continue;
            }
            Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
            if ( Vec_IntSize(vSupp) == 4 ) printf( "    " );
            if ( Vec_IntSize(vSupp) == 3 ) printf( "      " );
            if ( Vec_IntSize(vSupp) <= 2 ) printf( "       " );
            printf( "  " );
            Vec_IntPrint( vSupp );
        }
        printf( "\n" );
    }
    Vec_IntFree( vSupp );
    Vec_WrdFree( vTemp );
}
Vec_Wec_t * Acec_MatchCopy( Vec_Wec_t * vLits, Vec_Int_t * vMap )
{
    Vec_Wec_t * vRes = Vec_WecStart( Vec_WecSize(vLits) );
    Vec_Int_t * vLevel; int i, k, iLit;
    Vec_WecForEachLevel( vLits, vLevel, i )
        Vec_IntForEachEntry( vLevel, iLit, k )
            Vec_WecPush( vRes, i, Abc_Lit2LitL(Vec_IntArray(vMap), iLit) );
    return vRes;
}
int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
{
    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
    Vec_Int_t * vLevel1, * vLevel2; 
    int i, nCommon = 0;
    Vec_WecForEachLevel( vLits1, vLevel1, i )
    {
        if ( i+Shift < 0 || i+Shift >= Vec_WecSize(vLits2) )
            continue;
        vLevel2 = Vec_WecEntry( vLits2, i+Shift );
        nCommon += Vec_IntTwoFindCommonReverse( vLevel1, vLevel2, vRes );
    }
    Vec_IntFree( vRes );
    return nCommon;
}
void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int Class )
{
    int i;
    for ( i = Vec_IntSize(vClasses)-1; i >= 0; i-- )
        if ( Vec_IntEntry(vClasses,i) >= Class )
            break;
    Vec_IntInsert( vLits, i+1, Lit );
    Vec_IntInsert( vClasses, i+1, Class );
}
void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
{
    Vec_Int_t * vLevel1, * vLevel2; 
    int i, k, Prev, This, Entry, Counter = 0;
    Vec_WecForEachLevel( vLits, vLevel1, i )
    {
        if ( i == Vec_WecSize(vLits) - 1 )
            break;
        vLevel2 = Vec_WecEntry(vClasses, i);
        assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
        Prev = -1;
        Vec_IntForEachEntry( vLevel2, This, k )
        {
            if ( Prev != This )
            {
                Prev = This;
                continue;
            }
            Prev = -1;
            Entry = Vec_IntEntry( vLevel1, k );

            Vec_IntDrop( vLevel1, k );
            Vec_IntDrop( vLevel2, k-- );

            Vec_IntDrop( vLevel1, k );
            Vec_IntDrop( vLevel2, k-- );

            Vec_IntInsertOrder( Vec_WecEntry(vLits, i+1), Vec_WecEntry(vClasses, i+1), Entry, This );

            assert( Vec_IntSize(vLevel1)                  == Vec_IntSize(vLevel2) );
            assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
            Counter++;
        }
    }
    printf( "Moved %d pairs of PPs to normalize the matrix.\n", Counter );
}

void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
{
    Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
    Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
    int nCommon      = Acec_MatchCountCommon( vRes0, vRes1,  0 );
    int nCommonPlus  = Acec_MatchCountCommon( vRes0, vRes1,  1 );
    int nCommonMinus = Acec_MatchCountCommon( vRes0, vRes1, -1 );
    if ( nCommonPlus >= nCommonMinus && nCommonPlus > nCommon )
    {
        Vec_WecInsertLevel( vLits0, 0 );
        Vec_WecInsertLevel( vRoots0, 0 );
        Vec_WecInsertLevel( vRes0, 0 );
        printf( "Shifted one level up.\n" );
    }
    else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
    {
        Vec_WecInsertLevel( vLits1, 0 );
        Vec_WecInsertLevel( vRoots1, 0 );
        Vec_WecInsertLevel( vRes1, 0 );
        printf( "Shifted one level down.\n" );
    }
    Acec_MoveDuplicates( vLits0, vRes0 );
    Acec_MoveDuplicates( vLits1, vRes1 );

    //Vec_WecPrintLits( vLits1 );
    //printf( "Input literals:\n" );
    //Vec_WecPrintLits( vLits0 );
    //printf( "Equiv classes:\n" );
    //Vec_WecPrintLits( vRes0 );
    //printf( "Input literals:\n" );
    //Vec_WecPrintLits( vLits1 );
    //printf( "Equiv classes:\n" );
    //Vec_WecPrintLits( vRes1 );
    //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
    //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
    Vec_WecFree( vRes0 );
    Vec_WecFree( vRes1 );
}
int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
{
    Vec_Int_t * vMap0, * vMap1, * vLevel; 
    int i, nSize, nTotal;
    Acec_ComputeEquivClasses( pBox0->pGia, pBox1->pGia, &vMap0, &vMap1 );
    // sort nodes in the classes by their equivalences
    Vec_WecForEachLevel( pBox0->vLeafLits, vLevel, i )
        Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
    Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
        Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
    Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
    
    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
    //printf( "Outputs:\n" );
    //Vec_WecPrintLits( pBox0->vRootLits );
    //printf( "Outputs:\n" );
    //Vec_WecPrintLits( pBox1->vRootLits );

    // reorder nodes to have the same order
    assert( pBox0->vShared == NULL );
    assert( pBox1->vShared == NULL );
    pBox0->vShared = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
    pBox1->vShared = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
    pBox0->vUnique = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
    pBox1->vUnique = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
    nSize = Abc_MinInt( Vec_WecSize(pBox0->vLeafLits), Vec_WecSize(pBox1->vLeafLits) );
    Vec_WecForEachLevelStart( pBox0->vLeafLits, vLevel, i, nSize )
        Vec_IntAppend( Vec_WecEntry(pBox0->vUnique, i), vLevel );
    Vec_WecForEachLevelStart( pBox1->vLeafLits, vLevel, i, nSize )
        Vec_IntAppend( Vec_WecEntry(pBox1->vUnique, i), vLevel );
    for ( i = 0; i < nSize; i++ )
    {
        Vec_Int_t * vShared0 = Vec_WecEntry( pBox0->vShared, i );
        Vec_Int_t * vShared1 = Vec_WecEntry( pBox1->vShared, i );
        Vec_Int_t * vUnique0 = Vec_WecEntry( pBox0->vUnique, i );
        Vec_Int_t * vUnique1 = Vec_WecEntry( pBox1->vUnique, i );

        Vec_Int_t * vLevel0 = Vec_WecEntry( pBox0->vLeafLits, i );
        Vec_Int_t * vLevel1 = Vec_WecEntry( pBox1->vLeafLits, i );
        int * pBeg0 = Vec_IntArray(vLevel0);
        int * pBeg1 = Vec_IntArray(vLevel1);
        int * pEnd0 = Vec_IntLimit(vLevel0);
        int * pEnd1 = Vec_IntLimit(vLevel1);
        while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
        {
            int Entry0 = Abc_Lit2LitL( Vec_IntArray(vMap0), *pBeg0 );
            int Entry1 = Abc_Lit2LitL( Vec_IntArray(vMap1), *pBeg1 );
            assert( *pBeg0 && *pBeg1 );
            if ( Entry0 == Entry1 )
            {
                Vec_IntPush( vShared0, *pBeg0++ );
                Vec_IntPush( vShared1, *pBeg1++ );
            }
            else if ( Entry0 > Entry1 )
                Vec_IntPush( vUnique0, *pBeg0++ );
            else 
                Vec_IntPush( vUnique1, *pBeg1++ );
        }
        while ( pBeg0 < pEnd0 )
            Vec_IntPush( vUnique0, *pBeg0++ );
        while ( pBeg1 < pEnd1 )
            Vec_IntPush( vUnique1, *pBeg1++ );
        assert( Vec_IntSize(vShared0) == Vec_IntSize(vShared1) );
        assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
        assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
    }
    nTotal = Vec_WecSizeSize(pBox0->vShared);
    printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
    printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );

    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vShared, Vec_IntArray(vMap0), 0 );
    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vShared, Vec_IntArray(vMap1), 0 );
    //printf( "\n" );

    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );

    Vec_IntFree( vMap0 );
    Vec_IntFree( vMap1 );
    return nTotal;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
{
    int status = -1;
    abctime clk = Abc_Clock();
    Gia_Man_t * pMiter;
    Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
    Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
//    Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
//    Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
//    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
//    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
//    Vec_BitFreeP( &vIgnore0 );
//    Vec_BitFreeP( &vIgnore1 );
    Acec_Box_t * pBox0 = Acec_ProduceBox( pGia0, pPars->fVerbose );
    Acec_Box_t * pBox1 = Acec_ProduceBox( pGia1, pPars->fVerbose );
    if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
        printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
    else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
        printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
    else 
    {
        pGia0n = Acec_InsertBox( pBox0, 0 );
        pGia1n = Acec_InsertBox( pBox1, 0 );
        printf( "Matching of adder trees in LHS and RHS succeeded.  " );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        // remove the last output
        Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
        Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );

        Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
        Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
    }
    // solve regular CEC problem 
    Cec_ManCecSetDefaultParams( pCecPars );
    pCecPars->nBTLimit = pPars->nBTLimit;
    pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
    if ( pMiter )
    {
        int fDumpMiter = 0;
        if ( fDumpMiter )
        {
            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
            Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
        }
        status = Cec_ManVerify( pMiter, pCecPars );
        ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
        Gia_ManStop( pMiter );
    }
    else
        printf( "Miter computation has failed.\n" );
    if ( pGia0n != pGia0 )
        Gia_ManStop( pGia0n );
    if ( pGia1n != pGia1 )
        Gia_ManStop( pGia1n );
    Acec_BoxFreeP( &pBox0 );
    Acec_BoxFreeP( &pBox1 );
    return status;
}

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


ABC_NAMESPACE_IMPL_END