acecCore.c 20.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
/**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"
22
#include "proof/cec/cec.h"
23 24
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
25 26 27 28 29 30 31 32

ABC_NAMESPACE_IMPL_START


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

33 34
#define TRUTH_UNUSED 0x1234567812345678

35 36 37 38 39 40
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
  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*************************************************************

66 67 68 69 70 71 72 73 74
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
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     []

***********************************************************************/
148
Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
{
    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;
}
173 174 175 176 177 178 179 180 181
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 )
182 183 184
{
    Gia_Obj_t * pObj; int i;
    Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
185 186
    Gia_ManSetPhase( pAdd );
    Vec_IntWriteEntry( vMapNew, 0, 0 );
187
    Gia_ManForEachCand( pAdd, pObj, i )
188 189 190 191 192 193
    {
        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)) );
    }
194 195 196 197
    return vMapNew;
}
void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
{
198
    abctime clk = Abc_Clock();
199 200 201 202 203 204 205 206
    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 );
207
    Gia_ManStop( pBase );
208
    Gia_ManStop( pRepr );
209 210
    printf( "Finished computing equivalent nodes.  " );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
211
}
212
void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
213 214 215 216 217 218
{
    int i, j, best_i;
    for ( i = 0; i < nSize-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nSize; j++ )
219
            if ( Abc_Lit2LitL(pCostLits, pArray[j]) > Abc_Lit2LitL(pCostLits, pArray[best_i]) )
220 221 222 223
                best_i = j;
        ABC_SWAP( int, pArray[i], pArray[best_i] );
    }
}
224
void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
225
{
226 227
    Vec_Int_t * vSupp;
    Vec_Wrd_t * vTemp;
228 229 230 231 232
    Vec_Int_t * vLevel;
    int i, k, Entry;
    printf( "Leaf literals and their classes:\n" );
    Vec_WecForEachLevel( vLits, vLevel, i )
    {
233 234
        if ( Vec_IntSize(vLevel) == 0 )
            continue;
235 236 237 238 239
        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" );
    }
240 241
    if ( !fVerbose )
        return;
242 243
    vSupp = Vec_IntAlloc( 100 );
    vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
244 245
    Vec_WecForEachLevel( vLits, vLevel, i )
    {
246 247 248
        //if ( i != 20 )
        //    continue;
        if ( Vec_IntSize(vLevel) == 0 )
249 250 251 252
            continue;
        Vec_IntForEachEntry( vLevel, Entry, k )
        {
            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
253 254 255 256 257 258 259 260
/*
            {
                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 );
            }
*/
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
            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;
}
310 311 312 313 314 315 316 317 318 319 320 321
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; 
322
    int i, k, Prev, This, Entry, Counter = 0;
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
    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)) );
350
            Counter++;
351 352
        }
    }
353
    printf( "Moved %d pairs of PPs to normalize the matrix.\n", Counter );
354 355
}

356
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 )
357 358 359 360 361 362 363 364 365 366
{
    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 );
367
        Vec_WecInsertLevel( vRes0, 0 );
368
        printf( "Shifted one level up.\n" );
369 370 371 372 373
    }
    else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
    {
        Vec_WecInsertLevel( vLits1, 0 );
        Vec_WecInsertLevel( vRoots1, 0 );
374
        Vec_WecInsertLevel( vRes1, 0 );
375
        printf( "Shifted one level down.\n" );
376
    }
377 378 379 380
    Acec_MoveDuplicates( vLits0, vRes0 );
    Acec_MoveDuplicates( vLits1, vRes1 );

    //Vec_WecPrintLits( vLits1 );
381 382
    //printf( "Input literals:\n" );
    //Vec_WecPrintLits( vLits0 );
383 384
    //printf( "Equiv classes:\n" );
    //Vec_WecPrintLits( vRes0 );
385 386
    //printf( "Input literals:\n" );
    //Vec_WecPrintLits( vLits1 );
387 388
    //printf( "Equiv classes:\n" );
    //Vec_WecPrintLits( vRes1 );
389 390
    //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
    //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
391 392
    Vec_WecFree( vRes0 );
    Vec_WecFree( vRes1 );
393
}
394 395 396 397 398 399 400 401 402 403
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) );
404
    Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
405 406 407
    
    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
408 409 410 411
    //printf( "Outputs:\n" );
    //Vec_WecPrintLits( pBox0->vRootLits );
    //printf( "Outputs:\n" );
    //Vec_WecPrintLits( pBox1->vRootLits );
412

413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
    // 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 )
        {
440 441 442
            int Entry0 = Abc_Lit2LitL( Vec_IntArray(vMap0), *pBeg0 );
            int Entry1 = Abc_Lit2LitL( Vec_IntArray(vMap1), *pBeg1 );
            assert( *pBeg0 && *pBeg1 );
443
            if ( Entry0 == Entry1 )
444 445 446 447
            {
                Vec_IntPush( vShared0, *pBeg0++ );
                Vec_IntPush( vShared1, *pBeg1++ );
            }
448
            else if ( Entry0 > Entry1 )
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
                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) );
464

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

469 470 471 472 473
    //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 );
474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490
    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;
491
    abctime clk = Abc_Clock();
492 493 494
    Gia_Man_t * pMiter;
    Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
    Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
495 496 497 498 499 500 501 502
//    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 );
503 504 505 506 507 508
    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 
    {
509 510
        pGia0n = Acec_InsertBox( pBox0, 0 );
        pGia1n = Acec_InsertBox( pBox1, 0 );
511 512
        printf( "Matching of adder trees in LHS and RHS succeeded.  " );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
513
        // remove the last output
514 515 516 517 518
        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 );
519 520 521 522 523 524 525
    }
    // solve regular CEC problem 
    Cec_ManCecSetDefaultParams( pCecPars );
    pCecPars->nBTLimit = pPars->nBTLimit;
    pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
    if ( pMiter )
    {
526
        int fDumpMiter = 0;
527 528 529
        if ( fDumpMiter )
        {
            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
530
            Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
531 532 533 534 535 536 537 538 539 540 541 542 543 544
        }
        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;
545 546 547 548 549 550 551 552 553
}

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


ABC_NAMESPACE_IMPL_END