bmcCexMin1.c 19.5 KB
Newer Older
1 2
/**CFile****************************************************************

3
  FileName    [bmcCexMin1.c]
4 5 6

  SystemName  [ABC: Logic synthesis and verification system.]

7
  PackageName [SAT-based bounded model checking.]
8 9 10 11 12 13 14 15 16

  Synopsis    [CEX minimization.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

17
  Revision    [$Id: bmcCexMin1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 19 20

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

21
#include "aig/ioa/ioa.h"
22
#include "bmc.h"
23 24 25 26 27 28 29 30 31 32 33 34 35 36

ABC_NAMESPACE_IMPL_START


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

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

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

37
  Synopsis    [Find the roots to begin traversal.]
38 39 40 41 42 43 44 45

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
46
void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Int_t * vLeaves, Vec_Int_t * vRoots )
47
{
48 49 50 51
    Aig_Obj_t * pObj;
    int i;
    Vec_IntClear( vRoots );
    if ( vLeaves == NULL )
52
    {
53
        pObj = Aig_ManCo( pAig, pCex->iPo );
54
        Vec_IntPush( vRoots, Aig_ObjId(pObj) );
55 56
        return;
    }
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
    Aig_ManForEachObjVec( vLeaves, pAig, pObj, i )
        if ( Saig_ObjIsLo(pAig, pObj) )
            Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
}

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

  Synopsis    [Collects CI of the given timeframe.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCexMinCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFrameCisOne )
{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
76
        return;
77
    Aig_ObjSetTravIdCurrent(pAig, pObj);
78
    if ( Aig_ObjIsCo(pObj) )
79 80
        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
    else if ( Aig_ObjIsNode(pObj) )
81
    {
82 83
        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFrameCisOne );
84
    }
85
    else if ( Aig_ObjIsCi(pObj) )
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
        Vec_IntPush( vFrameCisOne, Aig_ObjId(pObj) );
}

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

  Synopsis    [Collects CIs of all timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Vec_t * Saig_ManCexMinCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
    Vec_Vec_t * vFrameCis;
    Vec_Int_t * vRoots, * vLeaves;
    Aig_Obj_t * pObj;
    int i, f;
    // create terminals
    vRoots = Vec_IntAlloc( 1000 );
    vFrameCis = Vec_VecStart( pCex->iFrame+1 );
    for ( f = pCex->iFrame; f >= 0; f-- )
110
    {
111 112 113 114 115 116 117
        // create roots
        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
        // collect nodes starting from the roots
        Aig_ManIncrementTravId( pAig );
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
            Saig_ManCexMinCollectFrameTerms_rec( pAig, pObj, Vec_VecEntryInt(vFrameCis, f) );
118
    }
119 120
    Vec_IntFree( vRoots );
    return vFrameCis;
121 122
}

123 124


125 126 127 128 129 130 131 132 133 134 135
/**Function*************************************************************

  Synopsis    [Recursively sets phase and priority.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
136
void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj )
137 138 139 140
{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
141
    if ( Aig_ObjIsCo(pObj) )
142
    {
143 144 145
        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
        pObj->iData = Aig_ObjFanin0(pObj)->iData ^ Aig_ObjFaninC0(pObj);
146 147 148 149
    }
    else if ( Aig_ObjIsNode(pObj) )
    {
        int fPhase0, fPhase1, iPrio0, iPrio1;
150 151 152 153
        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) );
        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
        assert( Aig_ObjFanin1(pObj)->iData >= 0 );
154 155 156 157
        fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
        fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
        iPrio0  = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
        iPrio1  = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
158
        if ( fPhase0 && fPhase1 ) // both are one
159
            pObj->iData = Abc_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
160
        else if ( !fPhase0 && fPhase1 ) 
161
            pObj->iData = Abc_Var2Lit( iPrio0, 0 );
162
        else if ( fPhase0 && !fPhase1 )
163
            pObj->iData = Abc_Var2Lit( iPrio1, 0 );
164
        else // both are zero
165
            pObj->iData = Abc_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
166 167 168 169 170
    }
}

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

171
  Synopsis    [Verify phase.]
172 173 174 175 176 177 178 179

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
180
void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f )
181
{
182 183 184 185
    Aig_Obj_t * pObj;
    int i;
    Aig_ManConst1(pAig)->fPhase = 1;
    Saig_ManForEachPi( pAig, pObj, i )
186
        pObj->fPhase = Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
187
    if ( f == 0 )
188
    {
189 190
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->fPhase = 0;
191
    }
192 193 194 195 196 197 198 199
    else
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->fPhase = Saig_ObjLoToLi(pAig, pObj)->fPhase;
    }
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase) & 
                       (Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase);
200
    Aig_ManForEachCo( pAig, pObj, i )
201
        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase);
202 203 204 205
}

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

206
  Synopsis    [Collects phase and priority of all timeframes.]
207 208 209 210 211 212 213 214

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
215
void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int f, Vec_Int_t * vRoots )
216
{
217
    Vec_Int_t * vFramePPsOne, * vFrameCisOne, * vLeaves;
218
    Aig_Obj_t * pObj;
219 220 221 222 223
    int i;
    // set PP for the CIs
    vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
    vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
    Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
224
    {
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
        pObj->iData = Vec_IntEntry( vFramePPsOne, i );
        assert( pObj->iData >= 0 );
    }
//    if ( f == 0 )
//        Saig_ManCexMinVerifyPhase( pAig, pCex, f );

    // create roots
    vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
    Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
    // derive for the nodes starting from the roots
    Aig_ManIncrementTravId( pAig );
    Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
    {
        Saig_ManCexMinDerivePhasePriority_rec( pAig, pObj );
//        if ( f == 0 )
//            assert( (pObj->iData & 1) == pObj->fPhase );
241 242 243 244 245
    }
}

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

246
  Synopsis    [Collects phase and priority of all timeframes.]
247 248 249 250 251 252

  Description []
               
  SideEffects []

  SeeAlso     []
253
 
254
***********************************************************************/
255
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
256
{
257 258
    Vec_Vec_t * vFramePPs;
    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
259
    Aig_Obj_t * pObj;
260 261 262 263 264 265 266 267 268
    int i, f, nPrioOffset;

    // initialize phase and priority
    Aig_ManForEachObj( pAig, pObj, i )
        pObj->iData = -1;

    // set the constant node to higher priority than the flops
    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
    nPrioOffset = (pCex->iFrame + 1) * pCex->nPis;
269
    Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
270 271 272 273 274 275 276 277 278 279
    vRoots = Vec_IntAlloc( 1000 );
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        int nPiCount = 0;
        // fill in PP for the CIs
        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
        assert( Vec_IntSize(vFramePPsOne) == 0 );
        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
        {
280
            assert( Aig_ObjIsCi(pObj) );
281
            if ( Saig_ObjIsPi(pAig, pObj) )
282
                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
283
            else if ( f == 0 )
284
                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
285 286 287 288 289
            else
                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
        }
        // compute the PP info
        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
290 291 292
    }
    Vec_IntFree( vRoots );
    // check the output
293
    pObj = Aig_ManCo( pAig, pCex->iPo );
294
    assert( Abc_LitIsCompl(pObj->iData) );
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
    return vFramePPs;
}

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

  Synopsis    [Collects phase and priority of all timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
{
    Vec_Vec_t * vFramePPs;
    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
    Aig_Obj_t * pObj;
    int i, f, nPrioOffset;

    // initialize phase and priority
    Aig_ManForEachObj( pAig, pObj, i )
        pObj->iData = -1;

    // set the constant node to higher priority than the flops
    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
    nPrioOffset = pCex->nRegs;
323
    Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
324 325 326 327 328 329 330 331 332 333
    vRoots = Vec_IntAlloc( 1000 );
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        int nPiCount = 0;
        // fill in PP for the CIs
        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
        assert( Vec_IntSize(vFramePPsOne) == 0 );
        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
        {
334
            assert( Aig_ObjIsCi(pObj) );
335
            if ( Saig_ObjIsPi(pAig, pObj) )
336
                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
337
            else if ( f == 0 )
338
                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
339 340 341 342 343
            else
                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
        }
        // compute the PP info
        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
344 345 346
    }
    Vec_IntFree( vRoots );
    // check the output
347
    pObj = Aig_ManCo( pAig, pCex->iPo );
348
    assert( Abc_LitIsCompl(pObj->iData) );
349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368
    return vFramePPs;
}


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

  Synopsis    [Returns reasons for the property to fail.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vReason, int fPiReason )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
369
    if ( Aig_ObjIsCi(pObj) )
370
    {
371
        if ( fPiReason && Saig_ObjIsPi(p, pObj) )
372
            Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjCioId(pObj), !Abc_LitIsCompl(pObj->iData) ) );
373
        else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
374
            Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) );
375
        return;
376
    }
377
    if ( Aig_ObjIsCo(pObj) )
378
    {
379 380 381 382 383 384
        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
        return;
    }
    if ( Aig_ObjIsConst1(pObj) )
        return;
    assert( Aig_ObjIsNode(pObj) );
385
    if ( Abc_LitIsCompl(pObj->iData) ) // value 1
386
    {
387 388
        int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
        int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
389 390 391
        assert( fPhase0 && fPhase1 );
        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
392 393 394
    }
    else
    {
395 396
        int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
        int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
397 398 399 400 401 402
        assert( !fPhase0 || !fPhase1 );
        if ( !fPhase0 && fPhase1 )
            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
        else if ( fPhase0 && !fPhase1 )
            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
        else 
403
        {
404 405
            int iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
            int iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
406 407 408 409
            if ( iPrio0 >= iPrio1 )
                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
            else
                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
410 411 412 413 414 415 416
        }
    }
}


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

417
  Synopsis    [Collects phase and priority of all timeframes.]
418 419 420 421 422 423 424 425

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
426
Vec_Vec_t * Saig_ManCexMinCollectReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int fPiReason )
427
{
428 429
    Vec_Vec_t * vFrameReas;
    Vec_Int_t * vRoots, * vLeaves;
430
    Aig_Obj_t * pObj;
431
    int i, f;
432
    // select reason for the property to fail
433 434
    vFrameReas = Vec_VecStart( pCex->iFrame+1 );
    vRoots = Vec_IntAlloc( 1000 );
435 436 437
    for ( f = pCex->iFrame; f >= 0; f-- )
    {
        // set phase and polarity
438 439 440 441 442
        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
        // create roots
        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
        // collect nodes starting from the roots
443
        Aig_ManIncrementTravId( pAig );
444 445 446
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
            Saig_ManCexMinCollectReason_rec( pAig, pObj, Vec_VecEntryInt(vFrameReas, f), fPiReason );
//printf( "%d(%d) ", Vec_VecLevelSize(vFrameCis, f), Vec_VecLevelSize(vFrameReas, f) ); 
447
    }
448 449 450
//printf( "\n" );
    Vec_IntFree( vRoots );
    return vFrameReas;
451 452
}

453 454 455 456 457 458 459 460 461 462 463
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
464
Vec_Vec_t * Saig_ManCexMinComputeReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, int fPiReason )
465
{
466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
    Vec_Vec_t * vFrameCis, * vFramePPs, * vFrameReas;
    // sanity checks
    assert( pCex->nPis == Saig_ManPiNum(pAig) );
    assert( pCex->nRegs == Saig_ManRegNum(pAig) );
    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
    // derive frame terms
    vFrameCis = Saig_ManCexMinCollectFrameTerms( pAig, pCex );
    // derive phase and priority
    vFramePPs = Saig_ManCexMinCollectPhasePriority( pAig, pCex, vFrameCis );
    // derive reasons for property failure
    vFrameReas = Saig_ManCexMinCollectReason( pAig, pCex, vFrameCis, vFramePPs, fPiReason );
    Vec_VecFree( vFramePPs );
    Vec_VecFree( vFrameCis );
    return vFrameReas;
}


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

  Synopsis    [Duplicate with literals.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
{
    Vec_Int_t * vLevel;
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pMiter;
    int i, k, Lit;
    assert( pAig->nConstrs == 0 );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) );
503
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
504 505 506
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
507 508
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
509 510 511 512 513
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs for cubes
    Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
514
    {
515 516 517 518 519 520
        if ( i == 0 )
            continue;
        pMiter = Aig_ManConst1( pAigNew );
        Vec_IntForEachEntry( vLevel, Lit, k )
        {
            assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) );
521 522
            pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
            pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
523
        }
524
        Aig_ObjCreateCo( pAigNew, pMiter );
525
    }
526 527
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
528
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
529 530 531 532
    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
533 534 535
}


536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
    int fReasonPi = 0;

    Abc_Cex_t * pCexMin = NULL;
    Aig_Man_t * pManNew = NULL;
    Vec_Vec_t * vFrameReas;
    vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
    printf( "Reason size = %d.  Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );

    // try reducing the frames
    if ( !fReasonPi )
    {
        char * pFileName = "aigcube.aig";
        pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
        Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
        Aig_ManStop( pManNew );
        printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
    }

    // find reduced counter-example
    Vec_VecFree( vFrameReas );
    return pCexMin;
}

572 573 574 575 576 577 578
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END