absVta.c 59.4 KB
Newer Older
1 2
/**CFile****************************************************************

3
  FileName    [absVta.c]
4 5 6

  SystemName  [ABC: Logic synthesis and verification system.]

7
  PackageName [Abstraction package.]
8 9 10 11 12 13 14 15 16

  Synopsis    [Variable time-frame abstraction.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

21 22
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
23
#include "abs.h"
24 25 26

ABC_NAMESPACE_IMPL_START

27
#define VTA_LARGE  0xFFFFFFF
28 29 30 31 32

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

33 34 35 36 37 38
typedef struct Vta_Obj_t_ Vta_Obj_t; // object
struct Vta_Obj_t_
{
    int           iObj;
    int           iFrame;
    int           iNext;
39
    unsigned      Prio   : 28;  // related to VTA_LARGE
40 41
    unsigned      Value  :  2;
    unsigned      fAdded :  1;
42
    unsigned      fVisit :  1;
43 44
};

45 46 47 48
typedef struct Vta_Man_t_ Vta_Man_t; // manager
struct Vta_Man_t_
{
    // user data
49
    Gia_Man_t *   pGia;         // AIG manager
50
    Abs_Par_t *   pPars;        // parameters
51
    // internal data
52
    int           nObjs;        // the number of objects
53
    int           nObjsAlloc;   // the number of objects allocated
54 55
    int           nBins;        // number of hash table entries
    int *         pBins;        // hash table bins
56
    Vta_Obj_t *   pObjs;        // storage for objects
57
    Vec_Int_t *   vOrder;       // objects in DPS order
58
    // abstraction
59 60 61 62
    int           nObjBits;     // the number of bits to represent objects
    unsigned      nObjMask;     // object mask
    Vec_Ptr_t *   vFrames;      // start abstraction for each frame
    int           nWords;       // the number of words in the record
63
    int           nCexes;       // the number of CEXes
64
    int           nObjAdded;    // objects added to the abstraction
65
    Vec_Int_t *   vSeens;       // seen objects
66 67
    Vec_Bit_t *   vSeenGla;     // seen objects in all frames
    int           nSeenGla;     // seen objects in all frames
68
    int           nSeenAll;     // seen objects in all frames
69
    // other data
70
    Vec_Ptr_t *   vCores;       // unsat core for each frame
71
    sat_solver2 * pSat;         // incremental SAT solver
72 73
    Vec_Int_t *   vAddedNew;    // the IDs of variables added to the solver
    // statistics 
74 75 76 77
    abctime       timeSat;
    abctime       timeUnsat;
    abctime       timeCex;
    abctime       timeOther;
78 79
};

80 81 82

// ternary simulation

83 84 85 86 87 88
#define VTA_VAR0   1
#define VTA_VAR1   2
#define VTA_VARX   3

static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
{
89 90 91 92 93
    if ( pThis->Value == VTA_VAR1 && fCompl )
        return 1;
    if ( pThis->Value == VTA_VAR0 && !fCompl )
        return 1;
    return 0;
94 95 96
}
static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
{
97 98 99 100 101
    if ( pThis->Value == VTA_VAR0 && fCompl )
        return 1;
    if ( pThis->Value == VTA_VAR1 && !fCompl )
        return 1;
    return 0;
102 103
}

104 105 106
static inline Vta_Obj_t *  Vta_ManObj( Vta_Man_t * p, int i )           { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                     }
static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;      }

107 108
#define Vta_ManForEachObj( p, pObj, i )                                 \
    for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
109 110 111 112 113
#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i )                  \
    for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i )           \
    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

114 115
#define Vta_ManForEachObjVec( vVec, p, pObj, i )                        \
    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
116
#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i )                 \
117
    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
118

119 120 121
#define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i )              \
    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
#define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i )       \
122
    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
123 124


125 126 127 128
// abstraction is given as an array of integers:
// - the first entry is the number of timeframes (F)
// - the next (F+1) entries give the beginning position of each timeframe
// - the following entries give the object IDs
129
// invariant:  assert( vec[vec[0]+1] == size(vec) );
130

131
extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
132

133 134 135 136 137 138
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

139 140 141 142 143 144 145 146 147
  Synopsis    [Converting from one array to per-frame arrays.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
148
Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs )
149 150 151
{
    Vec_Ptr_t * vFrames;
    Vec_Int_t * vFrame;
152
    int i, k, Entry, iStart, iStop = -1;
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
    int nFrames = Vec_IntEntry( vAbs, 0 );
    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
    vFrames = Vec_PtrAlloc( nFrames );
    for ( i = 0; i < nFrames; i++ )
    {
        iStart = Vec_IntEntry( vAbs, i+1 );
        iStop  = Vec_IntEntry( vAbs, i+2 );
        vFrame = Vec_IntAlloc( iStop - iStart );
        Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
            Vec_IntPush( vFrame, Entry );
        Vec_PtrPush( vFrames, vFrame );
    }
    assert( iStop == Vec_IntSize(vAbs) );
    return vFrames;
}

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

  Synopsis    [Converting from per-frame arrays to one integer array.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
180
Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
{
    Vec_Int_t * vOne, * vAbs;
    int i, k, Entry, nSize;
    vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) );
    Vec_IntPush( vAbs, Vec_VecSize(vFrames) );
    nSize = Vec_VecSize(vFrames) + 2;
    Vec_VecForEachLevelInt( vFrames, vOne, i )
    {
        Vec_IntPush( vAbs, nSize );
        nSize += Vec_IntSize( vOne );
    }
    Vec_IntPush( vAbs, nSize );
    assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 );
    Vec_VecForEachLevelInt( vFrames, vOne, i )
        Vec_IntForEachEntry( vOne, Entry, k )
            Vec_IntPush( vAbs, Entry );
    assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) );
    return vAbs;
}

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

203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
  Synopsis    [Detects how many frames are completed.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Vec_Int_t * Vta_ManDeriveAbsAll( Vec_Int_t * p, int nWords )
{
    Vec_Int_t * vRes;
    unsigned * pThis;
    int i, w, nObjs = Vec_IntSize(p) / nWords;
    assert( Vec_IntSize(p) % nWords == 0 );
    vRes = Vec_IntAlloc( nObjs );
    for ( i = 0; i < nObjs; i++ )
    {
        pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
        for ( w = 0; w < nWords; w++ )
            if ( pThis[w] )
                break;
        Vec_IntPush( vRes, (int)(w < nWords) );
    }
    return vRes;
}

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

232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
  Synopsis    [Collect nodes/flops involved in different timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
{
    int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 );
    int i, w, nObjs = Vec_IntSize(p) / nWords;
    assert( Vec_IntSize(p) % nWords == 0 );
    for ( i = 0; i < nObjs; i++ )
        for ( w = 0; w < nWords; w++ )
            pArray[2 * nWords * i + w] = p->pArray[nWords * i + w];
    ABC_FREE( p->pArray );
    p->pArray = pArray;
    p->nSize *= 2;
    p->nCap = p->nSize;
    return 2 * nWords;
}

256 257 258 259


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

260
  Synopsis    []
261 262 263 264 265 266 267 268

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
269
static inline int Vga_ManHash( int iObj, int iFrame, int nBins )
270
{
271
    return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
272
}
273 274 275 276
static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame )
{
    Vta_Obj_t * pThis;
    int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins );
277
    for ( pThis = Vta_ManObj(p, *pPlace); 
278
          pThis;  pPlace = &pThis->iNext, 
279
          pThis = Vta_ManObj(p, *pPlace) )
280 281 282 283 284 285 286
        if ( pThis->iObj == iObj && pThis->iFrame == iFrame )
            break;
    return pPlace;
}
static inline Vta_Obj_t * Vga_ManFind( Vta_Man_t * p, int iObj, int iFrame )
{
    int * pPlace = Vga_ManLookup( p, iObj, iFrame );
287
    return Vta_ManObj(p, *pPlace);
288 289
}
static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame )
290
{
291
    Vta_Obj_t * pThis;
292
    int i, * pPlace;
293
    assert( iObj >= 0 && iFrame >= -1 );
294 295
    if ( p->nObjs == p->nObjsAlloc )
    {
296
        // resize objects
297 298 299 300
        p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
        memset( p->pObjs + p->nObjsAlloc, 0, p->nObjsAlloc * sizeof(Vta_Obj_t) );
        p->nObjsAlloc *= 2;
        // rehash entries in the table
301 302 303 304 305 306 307 308 309 310
        ABC_FREE( p->pBins );
        p->nBins = Abc_PrimeCudd( 2 * p->nBins );
        p->pBins = ABC_CALLOC( int, p->nBins );
        Vta_ManForEachObj( p, pThis, i )
        {
            pThis->iNext = 0;
            pPlace = Vga_ManLookup( p, pThis->iObj, pThis->iFrame );
            assert( *pPlace == 0 );
            *pPlace = i;
        }
311 312 313 314
    }
    pPlace = Vga_ManLookup( p, iObj, iFrame );
    if ( *pPlace )
        return Vta_ManObj(p, *pPlace);
315
    *pPlace = p->nObjs++;
316
    pThis = Vta_ManObj(p, *pPlace);
317 318 319 320 321 322 323
    pThis->iObj   = iObj;
    pThis->iFrame = iFrame;
    return pThis;
}
static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
{
    int * pPlace = Vga_ManLookup( p, iObj, iFrame );
324
    Vta_Obj_t * pThis = Vta_ManObj(p, *pPlace);
325 326 327
    assert( pThis != NULL );
    *pPlace = pThis->iNext;
    pThis->iNext = -1;
328 329
}

330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356

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

  Synopsis    [Derives counter-example using current assignments.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Vga_ManDeriveCex( Vta_Man_t * p )
{
    Abc_Cex_t * pCex;
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    int i;
    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
    pCex->iPo = 0;
    pCex->iFrame = p->pPars->iFrame;
    Vta_ManForEachObjObj( p, pThis, pObj, i )
        if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
    return pCex;
}

357 358
/**Function*************************************************************

359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
  Synopsis    [Remaps core into frame/node pairs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore )
{
    Vta_Obj_t * pThis;
    int i, Entry;
    Vec_IntForEachEntry( vCore, Entry, i )
    {
        pThis = Vta_ManObj( p, Entry );
        Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
        Vec_IntWriteEntry( vCore, i, Entry );
    }
}
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405

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

  Synopsis    [Compares two objects by their distance.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 )
{
    int Diff = (*pp1)->Prio - (*pp2)->Prio;
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    Diff = (*pp1) - (*pp2);
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    return 0; 
}

406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425
/**Function*************************************************************

  Synopsis    [Returns 1 if the object is already used.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
{
    int i;
    unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
    for ( i = 0; i < p->nWords; i++ )
        if ( pInfo[i] )
            return 1;
    return 0;
}
426 427 428

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

429 430 431 432 433 434 435 436 437 438 439 440 441
  Synopsis    [Finds predecessors of the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * pObj, Vta_Obj_t ** ppThis0, Vta_Obj_t ** ppThis1 )
{
    *ppThis0 = NULL;
    *ppThis1 = NULL;
442 443
//    if ( !pThis->fAdded )
//        return;
444 445 446 447 448 449 450
    assert( !Gia_ObjIsPi(p->pGia, pObj) );
    if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
        return;
    if ( Gia_ObjIsAnd(pObj) )
    {
        *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
        *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
451
//        assert( *ppThis0 && *ppThis1 );
452 453 454 455 456
        return;
    }
    assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
    pObj = Gia_ObjRoToRi( p->pGia, pObj );
    *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
457
//    assert( *ppThis0 );
458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
}

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

  Synopsis    [Collect const/PI/RO/AND in a topological order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrder )
{
    Gia_Obj_t * pObj;
    Vta_Obj_t * pThis0, * pThis1;
475
    if ( pThis->fVisit )
476 477 478
        return;
    pThis->fVisit = 1;
    pObj = Gia_ManObj( p->pGia, pThis->iObj );
479 480 481 482 483 484
    if ( pThis->fAdded )
    {
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
        if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
    }
485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
    Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
}
Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
{
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    Vec_IntClear( p->vOrder );
    pObj = Gia_ManPo( p->pGia, 0 );
    pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
    assert( pThis != NULL );
    assert( !pThis->fVisit );
    Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
    assert( pThis->fVisit );
    return p->vOrder;
}

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

503 504 505 506 507 508 509 510 511
  Synopsis    [Refines abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556
void Vta_ManSatVerify( Vta_Man_t * p )
{
    Vta_Obj_t * pThis, * pThis0, * pThis1;
    Gia_Obj_t * pObj;
    int i;
    Vta_ManForEachObj( p, pThis, i )
        pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
    Vta_ManForEachObjObj( p, pThis, pObj, i )
    {
        if ( !pThis->fAdded )
            continue;
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
            if ( pThis->iFrame == 0 )
                assert( pThis->Value == VTA_VAR0 );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
            else if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
            else assert( 0 );
        }
    }
}

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

  Synopsis    [Refines abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
557 558 559 560 561 562 563 564 565
void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd )
{
    Vta_Obj_t * pThis;
    Gia_Obj_t * pObj;
    // profile the added ones
    int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
    Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
        pCounters[pThis->iFrame]++;
    for ( i = 0; i <= p->pPars->iFrame; i++ )
566 567
        Abc_Print( 1, "%2d", pCounters[i] );
    Abc_Print( 1, "***\n" );
568 569 570 571 572 573 574 575 576 577 578 579 580
}

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

  Synopsis    [Refines abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
581
Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
582
{
583
    int fVerify = 0;
584
    Abc_Cex_t * pCex = NULL;
585
    Vec_Int_t * vOrder, * vTermsToAdd;
586 587 588 589
    Vec_Ptr_t * vTermsUsed, * vTermsUnused;
    Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
    Gia_Obj_t * pObj;
    int i, Counter;
590

591
    if ( fVerify )
592
    Vta_ManSatVerify( p );
593

594 595 596
    // collect nodes in a topological order
    vOrder = Vta_ManCollectNodes( p, f );
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
597 598
    {
        pThis->Prio = VTA_LARGE;
599
        pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
600
        pThis->fVisit = 0;
601
    }
602

603
    // verify
604
    if ( fVerify )
605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
    {
        if ( !pThis->fAdded )
            continue;
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
            if ( pThis->iFrame == 0 )
                assert( pThis->Value == VTA_VAR0 );
            else if ( pThis->Value == VTA_VAR0 )
                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
            else if ( pThis->Value == VTA_VAR1 )
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
            else assert( 0 );
        }
    }
630

631
    // compute distance in reverse order
632
    pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
633 634
    pThis->Prio  = 1;
    // collect used and unused terms
635 636
    vTermsUsed   = Vec_PtrAlloc( 1015 );
    vTermsUnused = Vec_PtrAlloc( 1016 );
637
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
638
    {
639 640 641
        // there is no unreachable states
        assert( pThis->Prio < VTA_LARGE );
        // skip constants and PIs
642 643
        if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
        {
644
            pThis->Prio = 0; // set highest priority
645 646
            continue;
        }
647
        // collect terminals
648 649 650
        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
        if ( !pThis->fAdded )
        {
651
            assert( pThis->Prio > 0 );
652
            if ( Vta_ManObjIsUsed(p, pThis->iObj) )
653 654 655 656 657 658
                Vec_PtrPush( vTermsUsed, pThis );
            else
                Vec_PtrPush( vTermsUnused, pThis );
            continue;
        }
        // propagate
659 660
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        if ( pThis0 ) 
661
            pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
662
        if ( pThis1 ) 
663 664
            pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
    }
665 666

/*
667 668 669 670 671 672
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
        if ( pThis->Prio > 0 )
            pThis->Prio = 10;
*/
/*
    // update priorities according to reconvergence counters
673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
    {
        Vta_Obj_t * pThis0, * pThis1;
        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        pThis->Prio += 10000000;
        if ( pThis0 )
            pThis->Prio -= 1000000 * pThis0->fAdded;
        if ( pThis1 )
            pThis->Prio -= 1000000 * pThis1->fAdded;
    }
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
    {
        Vta_Obj_t * pThis0, * pThis1;
        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
        pThis->Prio += 10000000;
        if ( pThis0 )
            pThis->Prio -= 1000000 * pThis0->fAdded;
        if ( pThis1 )
            pThis->Prio -= 1000000 * pThis1->fAdded;
    }
*/

697 698

    // update priorities according to reconvergence counters
699 700 701 702
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        pThis->Prio = pThis->iObj;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
        pThis->Prio = pThis->iObj;
703

704

705 706 707 708 709
    // objects with equal distance should receive priority based on number
    // those objects whose prototypes have been added in other timeframes
    // should have higher priority than the current object
    Vec_PtrSort( vTermsUsed,   (int (*)(void))Vta_ManComputeDepthIncrease );
    Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
710 711 712 713 714 715
    if ( Vec_PtrSize(vTermsUsed) > 1 )
    {
        pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
        pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
        assert( pThis0->Prio <= pThis1->Prio );
    }
716 717 718 719 720 721
    // assign the priority based on these orders
    Counter = 1;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        pThis->Prio = Counter++;
    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
        pThis->Prio = Counter++;
722
//    Abc_Print( 1, "Used %d  Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
723

724 725

    // propagate in the direct order
726
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
727
    {
728 729
        assert( pThis->fVisit == 0 );
        assert( pThis->Prio < VTA_LARGE );
730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748
        // skip terminal objects
        if ( !pThis->fAdded )
            continue;
        // assumes that values are assigned!!!
        assert( pThis->Value != 0 );
        // propagate
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( pThis->Value == VTA_VAR1 )
            {
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
                pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
            }
            else if ( pThis->Value == VTA_VAR0 )
            {
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
749
                    pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766
                else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Prio = pThis0->Prio;
                else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                    pThis->Prio = pThis1->Prio;
                else assert( 0 );
            }
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
                pThis->Prio = pThis0->Prio;
            }
767 768
            else
                pThis->Prio = 0;
769
        }
770 771 772 773
        else if ( Gia_ObjIsConst0(pObj) )
            pThis->Prio = 0;
        else
            assert( 0 );
774 775 776
    }

    // select important values
777
    pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
778 779 780
    pTop->fVisit = 1;
    vTermsToAdd = Vec_IntAlloc( 100 );
    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
781
    {
782
        if ( !pThis->fVisit )
783
            continue;
784
        pThis->fVisit = 0;
785 786 787 788
        assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
        // skip terminal objects
        if ( !pThis->fAdded )
        {
789
            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
790
            Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
791 792 793 794 795 796 797 798 799 800 801 802 803
            continue;
        }
        // assumes that values are assigned!!!
        assert( pThis->Value != 0 );
        // propagate
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( pThis->Value == VTA_VAR1 )
            {
                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
804 805 806 807
                assert( pThis0->Prio <= pThis->Prio );
                assert( pThis1->Prio <= pThis->Prio );
                pThis0->fVisit = 1;
                pThis1->fVisit = 1;
808 809 810 811 812
            }
            else if ( pThis->Value == VTA_VAR0 )
            {
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                {
813 814 815 816 817 818 819
                    if ( pThis0->fVisit )
                    {
                    }
                    else if ( pThis1->fVisit )
                    {
                    }
                    else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
820 821 822 823
                    {
                        pThis0->fVisit = 1;
                        assert( pThis0->Prio == pThis->Prio );
                    }
824
                    else
825 826 827 828
                    {
                        pThis1->fVisit = 1;
                        assert( pThis1->Prio == pThis->Prio );
                    }
829 830
                }
                else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
831 832 833 834
                {
                    pThis0->fVisit = 1;
                    assert( pThis0->Prio == pThis->Prio );
                }
835
                else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
836 837 838 839
                {
                    pThis1->fVisit = 1;
                    assert( pThis1->Prio == pThis->Prio );
                }
840 841 842 843 844 845 846 847 848 849 850
                else assert( 0 );
            }
            else assert( 0 );
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
851 852
                pThis0->fVisit = 1;
                assert( pThis0->Prio == pThis->Prio );
853 854
            }
        }
855 856
        else if ( !Gia_ObjIsConst0(pObj) )
            assert( 0 );
857 858
    }

859
    if ( p->pPars->fAddLayer )
860
    {
861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879
        // mark those currently included
        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
        {
            assert( pThis->fVisit == 0 );
            pThis->fVisit = 1;
        }
        // add used terms, which have close relationship
        Counter = Vec_IntSize(vTermsToAdd);
        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
        {
            if ( pThis->fVisit )
                continue;
    //        Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
    //        if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
                Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
        }
        // remove those currenty included
        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
            pThis->fVisit = 0;
880 881 882 883 884
    }
//    printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
//Vec_IntReverseOrder( vTermsToAdd );
//Vec_IntSort( vTermsToAdd, 1 );

885

886 887 888 889
    // cleanup
    Vec_PtrFree( vTermsUsed );
    Vec_PtrFree( vTermsUnused );

890

891 892
    if ( fVerify )
    {
893
    // verify
894 895
    Vta_ManForEachObjVec( vOrder, p, pThis, i )
        pThis->Value = VTA_VARX;
896
    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
897 898
    {
        assert( !pThis->fAdded );
899
        pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
900
    }
901
    // simulate 
902
    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
903
    {
904
        assert( pThis->fVisit == 0 );
905 906
        if ( !pThis->fAdded )
            continue;
907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932
        if ( Gia_ObjIsAnd(pObj) )
        {
            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
            assert( pThis0 && pThis1 );
            if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
                pThis->Value = VTA_VAR1;
            else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                pThis->Value = VTA_VAR0;
            else
                pThis->Value = VTA_VARX;
        }
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( pThis->iFrame > 0 )
            {
                pObj = Gia_ObjRoToRi( p->pGia, pObj );
                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                assert( pThis0 );
                if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Value = VTA_VAR0;
                else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
                    pThis->Value = VTA_VAR1;
                else
                    pThis->Value = VTA_VARX;
            }
933
            else
934
            {
935
                pThis->Value = VTA_VAR0;
936 937 938 939 940
            }
        }
        else if ( Gia_ObjIsConst0(pObj) )
        {
            pThis->Value = VTA_VAR0;
941
        }
942
        else assert( 0 );
943
        // double check the solver
944
        assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
945 946 947
    }

    // check the output
948
    if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
949
        Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
950
//    else
951
//        Abc_Print( 1, "Verification OK.\n" );
952
    }
953

954 955 956

    // produce true counter-example
    if ( pTop->Prio == 0 )
957
        pCex = Vga_ManDeriveCex( p );
958 959
    else
    {
960 961
//       Vta_ManProfileAddition( p, vTermsToAdd );

962 963 964
        Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
            if ( !Gia_ObjIsPi(p->pGia, pObj) )
                Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
965
        sat_solver2_simplify( p->pSat );
966
    }
967
    p->nObjAdded += Vec_IntSize(vTermsToAdd);
968
    Vec_IntFree( vTermsToAdd );
969 970 971
    return pCex;
}

972 973 974 975 976 977 978 979 980 981 982
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
983
Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
984 985 986
{
    Vta_Man_t * p;
    p = ABC_CALLOC( Vta_Man_t, 1 );
987 988
    p->pGia        = pGia;
    p->pPars       = pPars;
989
    // internal data
990
    p->nObjsAlloc  = (1 << 18);
991 992
    p->pObjs       = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
    p->nObjs       = 1;
993
    p->nBins       = Abc_PrimeCudd( 2*p->nObjsAlloc );
994 995
    p->pBins       = ABC_CALLOC( int, p->nBins );
    p->vOrder      = Vec_IntAlloc( 1013 );
996
    // abstraction
997
    p->nObjBits    = Abc_Base2Log( Gia_ManObjNum(pGia) );
998
    p->nObjMask    = (1 << p->nObjBits) - 1;
999
    assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
1000 1001
    p->nWords      = 1;
    p->vSeens      = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
1002 1003
    p->vSeenGla    = Vec_BitStart( Gia_ManObjNum(pGia) );
    p->nSeenGla    = 1;
1004
    p->nSeenAll    = 1;
1005
    // other data
1006 1007
    p->vCores      = Vec_PtrAlloc( 100 );
    p->pSat        = sat_solver2_new();
1008
    p->pSat->pPrf1 = Vec_SetAlloc( 20 );
1009
//    p->pSat->fVerbose = p->pPars->fVerbose;
1010 1011 1012 1013 1014
//    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
    p->pSat->nLearntStart = p->pPars->nLearnedStart;
    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
    p->pSat->nLearntMax   = p->pSat->nLearntStart;
1015 1016 1017
    // start the abstraction
    assert( pGia->vObjClasses != NULL );
    p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
1018
    p->vAddedNew   = Vec_IntAlloc( 1000 );
1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034
    return p;
}

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

  Synopsis    [Delete manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Vga_ManStop( Vta_Man_t * p )
{
1035
    if ( p->pPars->fVerbose )
1036 1037 1038
        Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  Objs+ = %d\n", 
            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), 
            sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
1039 1040
    Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
    Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
1041
    Vec_BitFreeP( &p->vSeenGla );
1042 1043
    Vec_IntFreeP( &p->vSeens );
    Vec_IntFreeP( &p->vOrder );
1044
    Vec_IntFreeP( &p->vAddedNew );
1045 1046 1047 1048 1049
    sat_solver2_delete( p->pSat );
    ABC_FREE( p->pBins );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}
1050

1051 1052
/**Function*************************************************************

Alan Mishchenko committed
1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069
  Synopsis    [Returns the output literal.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
{
    Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
    Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
    assert( pThis != NULL && pThis->fAdded );
    if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
        return -Vta_ObjId(p, pThis);
    return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
1070
} 
Alan Mishchenko committed
1071 1072 1073

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

1074 1075 1076 1077 1078 1079 1080 1081 1082
  Synopsis    [Finds the set of clauses involved in the UNSAT core.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1083
Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
1084
{
1085
    abctime clk = Abc_Clock();
1086 1087
    Vec_Int_t * vCore;
    int RetValue, nConfPrev = pSat->stats.conflicts;
1088 1089
    if ( piRetValue )
        *piRetValue = 1;
Alan Mishchenko committed
1090 1091 1092 1093 1094 1095 1096 1097
    // consider special case when PO points to the flop
    // this leads to immediate conflict in the first timeframe
    if ( iLit < 0 )
    {
        vCore = Vec_IntAlloc( 1 );
        Vec_IntPush( vCore, -iLit );
        return vCore;
    }
1098 1099
    // solve the problem
    RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1100 1101
    if ( pnConfls )
        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115
    if ( RetValue == l_Undef )
    {
        if ( piRetValue )
            *piRetValue = -1;
        return NULL;
    }
    if ( RetValue == l_True )
    {
        if ( piRetValue )
            *piRetValue = 0;
        return NULL;
    }
    if ( fVerbose )
    {
1116 1117
//        Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
//        Abc_Print( 1, "UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
1118
//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1119 1120 1121
    }
    assert( RetValue == l_False );
    // derive the UNSAT core
1122
    clk = Abc_Clock();
1123 1124 1125
    vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
    if ( fVerbose )
    {
1126
//        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
1127
//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1128 1129 1130 1131 1132 1133
    }
    return vCore;
}

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

1134 1135 1136 1137 1138 1139 1140 1141 1142
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1143
int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose )
1144
{
1145
    unsigned * pInfo;
1146
    int * pCountAll = NULL, * pCountUni = NULL;
1147
    int i, iFrame, iObj, Entry, fChanges = 0;
1148
    // print info about frames
1149
    if ( vCore )
1150
    {
1151 1152 1153
        pCountAll = ABC_CALLOC( int, nFrames + 1 );
        pCountUni = ABC_CALLOC( int, nFrames + 1 );
        Vec_IntForEachEntry( vCore, Entry, i )
1154
        {
1155 1156 1157 1158 1159 1160 1161 1162 1163
            iObj   = (Entry &  p->nObjMask);
            iFrame = (Entry >> p->nObjBits);
            assert( iFrame < nFrames );
            pInfo  = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
            if ( !Abc_InfoHasBit(pInfo, iFrame) )
            {
                Abc_InfoSetBit( pInfo, iFrame );
                pCountUni[iFrame+1]++;
                pCountUni[0]++;
1164
                p->nSeenAll++;
1165 1166 1167 1168 1169 1170 1171
            }
            pCountAll[iFrame+1]++;
            pCountAll[0]++;
            if ( !Vec_BitEntry(p->vSeenGla, iObj) )
            {
                Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
                p->nSeenGla++;
1172
                fChanges = 1;
1173
            }
1174
        }
1175
    }
1176 1177 1178 1179 1180 1181 1182
    if ( !fVerbose )
    {
        ABC_FREE( pCountAll );
        ABC_FREE( pCountUni );
        return fChanges;
    }

1183 1184 1185
    if ( Abc_FrameIsBatchMode() && !vCore )
        return fChanges;

1186
//    Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] ); 
1187
    Abc_Print( 1, "%4d :", nFrames-1 );
1188
    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) ); 
1189 1190 1191
    Abc_Print( 1, "%6d", p->nSeenGla ); 
    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) ); 
    Abc_Print( 1, "%8d", nConfls );
1192
    if ( nCexes == 0 )
1193
        Abc_Print( 1, "%5c", '-' ); 
1194
    else
1195
        Abc_Print( 1, "%5d", nCexes ); 
1196 1197 1198 1199
//    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1200 1201
    if ( vCore == NULL )
    {
1202
        Abc_Print( 1, "    ..." ); 
1203 1204
//        for ( k = 0; k < 7; k++ )
//            Abc_Print( 1, "     " );
1205
        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1206
        Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1207
        Abc_Print( 1, "\r" );
1208 1209
    }
    else
1210
    {
1211
        Abc_PrintInt( pCountAll[0] );
1212
/*
1213
        if ( nFrames > 7 )
1214
        {
1215
            for ( k = 0; k < 3; k++ )
1216 1217
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
            Abc_Print( 1, "  ..." );
1218
            for ( k = nFrames-3; k < nFrames; k++ )
1219
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
1220 1221 1222 1223
        }
        else
        {
            for ( k = 0; k < nFrames; k++ )
1224
                Abc_Print( 1, "%5d", pCountAll[k+1] ); 
1225
            for ( k = nFrames; k < 7; k++ )
1226
                Abc_Print( 1, "     " );
1227
        }
1228
*/
1229
        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1230
        Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1231
        Abc_Print( 1, "\n" );
1232
    }
1233 1234 1235 1236 1237 1238 1239
    fflush( stdout );

    if ( vCore )
    {
        ABC_FREE( pCountAll );
        ABC_FREE( pCountUni );
    }
1240
    return fChanges;
1241 1242 1243 1244
}

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

1245 1246 1247 1248 1249 1250 1251 1252 1253
  Synopsis    [Adds clauses to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1254
void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
1255
{ 
1256
    Vta_Obj_t * pThis0, * pThis1;
1257 1258
    Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
    Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
1259
    int iThis0, iMainVar = Vta_ObjId(p, pThis);
1260
    assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
1261 1262
    if ( pThis->fAdded )
        return;
1263
    pThis->fAdded = 1;
1264
    Vec_IntPush( p->vAddedNew, iMainVar );
1265 1266
    if ( Gia_ObjIsAnd(pObj) )
    {
1267
        pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
1268
        iThis0 = Vta_ObjId(p, pThis0);
1269
        pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
1270
        sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), 
1271
            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
1272 1273 1274
    }
    else if ( Gia_ObjIsRo(p->pGia, pObj) )
    {
1275
        if ( iFrame == 0 )
1276
        {
1277 1278 1279
            if ( p->pPars->fUseTermVars )
            {
                pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
1280
                sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
1281 1282 1283
            }
            else
            {
1284
                sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1285
            }
1286 1287 1288 1289
        }
        else
        {
            pObj = Gia_ObjRoToRi( p->pGia, pObj );
1290
            pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
1291
            sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );  
1292 1293 1294 1295
        }
    }
    else if ( Gia_ObjIsConst0(pObj) )
    {
1296
        sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1297
    }
1298
    else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
1299 1300 1301 1302 1303
        assert( 0 );
}

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

1304 1305 1306 1307 1308 1309 1310 1311 1312
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1313
void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
1314
{
1315
    int i, Entry;
1316
    Vec_IntForEachEntry( vOne, Entry, i )
1317
        Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
1318
    sat_solver2_simplify( p->pSat );
1319 1320 1321 1322
}

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

1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
{
    int i, Entry, iObj, iFrame;
    Vec_IntForEachEntry( vCore, Entry, i )
    {
        iObj   = (Entry &  p->nObjMask);
        iFrame = (Entry >> p->nObjBits);
1339
        Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
1340
    }
1341
    Abc_Print( 1, "\n" );
1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
{
    Vta_Obj_t * pThis  = p->pObjs + nObjOld;
    Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
1359
    int i, Entry;
1360 1361 1362 1363
    for ( ; pThis < pLimit; pThis++ )
        Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
    memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
    p->nObjs = nObjOld;
1364 1365 1366 1367 1368 1369 1370
    Vec_IntForEachEntry( p->vAddedNew, Entry, i )
        if ( Entry < p->nObjs )
        {
            pThis = Vta_ManObj(p, Entry);
            assert( pThis->fAdded == 1 );
            pThis->fAdded = 0;
        }
1371
}
1372

1373 1374
/**Function*************************************************************

1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386
  Synopsis    [Send abstracted model or send cancel.]

  Description [Counter-example will be sent automatically when &vta terminates.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose )
{
    Gia_Man_t * pAbs;
1387
    assert( Abc_FrameIsBridgeMode() );
1388 1389
//    if ( fVerbose )
//        Abc_Print( 1, "Sending abstracted model...\n" );
1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400
    // create obj classes
    Vec_IntFreeP( &p->pGia->vObjClasses );
    p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
    // create gate classes
    Vec_IntFreeP( &p->pGia->vGateClasses );
    p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
    Vec_IntFreeP( &p->pGia->vObjClasses );
    // create abstrated model
    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
    Vec_IntFreeP( &p->pGia->vGateClasses );
    // send it out
1401
    Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1402 1403 1404 1405 1406
    Gia_ManStop( pAbs );
}
void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
{
    extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1407
    assert( Abc_FrameIsBridgeMode() );
1408 1409
//    if ( fVerbose )
//        Abc_Print( 1, "Cancelling previously sent model...\n" );
1410 1411 1412 1413 1414
    Gia_ManToBridgeBadAbs( stdout );
}

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

1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425
  Synopsis    [Send abstracted model or send cancel.]

  Description [Counter-example will be sent automatically when &vta terminates.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
{
1426 1427
    char * pFileNameDef = "vabs.aig";
    char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
1428 1429
    Gia_Man_t * pAbs;
    if ( fVerbose )
1430
        Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441
    // create obj classes
    Vec_IntFreeP( &p->pGia->vObjClasses );
    p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
    // create gate classes
    Vec_IntFreeP( &p->pGia->vGateClasses );
    p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
    Vec_IntFreeP( &p->pGia->vObjClasses );
    // create abstrated model
    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
    Vec_IntFreeP( &p->pGia->vGateClasses );
    // send it out
1442
    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
1443 1444 1445
    Gia_ManStop( pAbs );
}

Alan Mishchenko committed
1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461
    
/**Function*************************************************************

  Synopsis    [Print memory report.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_VtaPrintMemory( Vta_Man_t * p )
{
    double memTot = 0;
    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
1462
    double memSat = sat_solver2_memory( p->pSat, 1 );
Alan Mishchenko committed
1463 1464 1465 1466 1467 1468 1469 1470 1471
    double memPro = sat_solver2_memory_proof( p->pSat );
    double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
    double memOth = sizeof(Vta_Man_t);
    memOth += Vec_IntCap(p->vOrder) * sizeof(int);
    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
    memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
    memTot = memAig + memSat + memPro + memMap + memOth;
1472 1473 1474 1475 1476 1477
    ABC_PRMP( "Memory: AIG     ", memAig, memTot );
    ABC_PRMP( "Memory: SAT     ", memSat, memTot );
    ABC_PRMP( "Memory: Proof   ", memPro, memTot );
    ABC_PRMP( "Memory: Map     ", memMap, memTot );
    ABC_PRMP( "Memory: Other   ", memOth, memTot );
    ABC_PRMP( "Memory: TOTAL   ", memTot, memTot );
Alan Mishchenko committed
1478 1479 1480
}


1481 1482
/**Function*************************************************************

1483 1484 1485 1486 1487 1488 1489 1490 1491
  Synopsis    [Collect nodes/flops involved in different timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1492
int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
1493
{
1494
    Vta_Man_t * p;
1495
    Vec_Int_t * vCore;
1496
    Abc_Cex_t * pCex = NULL;
1497
    int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
1498
    abctime clk = Abc_Clock(), clk2;
1499
    // preconditions
1500
    assert( Gia_ManPoNum(pAig) == 1 );
1501
    assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
1502 1503 1504 1505 1506 1507
    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;
1508
        } 
1509 1510 1511 1512 1513 1514
        ABC_FREE( pAig->pCexSeq );
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        printf( "Sequential miter is trivially SAT.\n" );
        return 0;
    }

1515 1516 1517 1518 1519 1520 1521 1522 1523
    // compute intial abstraction
    if ( pAig->vObjClasses == NULL )
    {
        pAig->vObjClasses = Vec_IntAlloc( 5 );
        Vec_IntPush( pAig->vObjClasses, 1 );
        Vec_IntPush( pAig->vObjClasses, 3 );
        Vec_IntPush( pAig->vObjClasses, 4 );
        Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
    }
1524
    // start the manager
1525
    p = Vga_ManStart( pAig, pPars );
1526 1527
    // set runtime limit
    if ( p->pPars->nTimeOut )
1528
        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1529
    // perform initial abstraction
1530
    if ( p->pPars->fVerbose )
1531
    {
1532
        Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
1533 1534 1535 1536
        Abc_Print( 1, "FramePast = %d  FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%\n", 
            pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
        Abc_Print( 1, "LearnStart = %d  LearnDelta = %d  LearnRatio = %d %%.\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
1537
//        Abc_Print( 1, "Frame   %%   Abs   %%   Confl  Cex    SatVar   Core   F0   F1   F2  ...\n" );
1538
        Abc_Print( 1, " Frame   %%   Abs   %%   Confl  Cex   Vars   Clas   Lrns   Core     Time      Mem\n" );
1539
    }
1540
    assert( Vec_PtrSize(p->vFrames) > 0 );
1541
    for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
1542
    {
1543
        int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1544 1545
        p->pPars->iFrame = f;
        // realloc storage for abstraction marks
1546 1547
        if ( f == p->nWords * 32 )
            p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
1548 1549 1550 1551 1552 1553 1554 1555 1556

        // create bookmark to be used for rollback
        nObjOld = p->nObjs;
        sat_solver2_bookmark( p->pSat );
        Vec_IntClear( p->vAddedNew );

        // load new timeframe
        Vga_ManAddClausesOne( p, 0, f );
        if ( f < Vec_PtrSize(p->vFrames) )
1557
            Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
1558 1559
        else
        {
1560
            for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
1561
                Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
1562 1563 1564 1565 1566
        }

        // iterate as long as there are counter-examples
        for ( i = 0; ; i++ )
        { 
1567
            clk2 = Abc_Clock();
1568
            vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
1569 1570 1571 1572 1573 1574 1575
            assert( (vCore != NULL) == (Status == 1) );
            if ( Status == -1 ) // resource limit is reached
            {
                Vga_ManRollBack( p, nObjOld );
                goto finish;
            }
            // check timeout
1576
            if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit )
1577 1578 1579 1580 1581 1582
            {
                Vga_ManRollBack( p, nObjOld );
                goto finish;
            }
            if ( vCore != NULL )
            {
1583
                p->timeUnsat += Abc_Clock() - clk2;
1584 1585
                break;
            }
1586
            p->timeSat += Abc_Clock() - clk2;
1587 1588 1589
            assert( Status == 0 );
            p->nCexes++;
            // perform the refinement
1590
            clk2 = Abc_Clock();
1591
            pCex = Vta_ManRefineAbstraction( p, f );
1592
            p->timeCex += Abc_Clock() - clk2;
1593 1594 1595
            if ( pCex != NULL )
                goto finish;
            // print the result (do not count it towards change)
1596
            Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose );
1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609
        }
        assert( Status == 1 );
        // valid core is obtained
        Vta_ManUnsatCoreRemap( p, vCore );
        Vec_IntSort( vCore, 1 );
        // update the SAT solver
        sat_solver2_rollback( p->pSat );
        // update storage
        Vga_ManRollBack( p, nObjOld );
        // load this timeframe
        Vga_ManLoadSlice( p, vCore, 0 );
        Vec_IntFree( vCore );

1610
        // run SAT solver
1611
        clk2 = Abc_Clock();
1612
        vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
1613
        p->timeUnsat += Abc_Clock() - clk2;
1614 1615
        assert( (vCore != NULL) == (Status == 1) );
        if ( Status == -1 ) // resource limit is reached
1616
            break;
1617
        if ( Status == 0 )
1618
        {
1619
            Vta_ManSatVerify( p );
1620 1621 1622
            // make sure, there was no initial abstraction (otherwise, it was invalid)
            assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
            pCex = Vga_ManDeriveCex( p );
1623
            break;
1624
        }
1625
        // add the core
1626
        Vta_ManUnsatCoreRemap( p, vCore );
1627
        // add in direct topological order
1628
        Vec_IntSort( vCore, 1 );
1629 1630
        Vec_PtrPush( p->vCores, vCore );
        // print the result
1631
        if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) )
1632 1633 1634
        {
            // reset the counter of frames without change
            nCountNoChange = 1;
1635
            p->pPars->nFramesNoChange = 0;
1636 1637 1638
        }
        else if ( ++nCountNoChange == 2 ) // time to send
        {
1639
            p->pPars->nFramesNoChange++;
1640 1641 1642 1643 1644 1645 1646 1647 1648
            if ( Abc_FrameIsBridgeMode() )
            {
                // cancel old one if it was sent
                if ( fOneIsSent )
                    Gia_VtaSendCancel( p, pPars->fVerbose );
                // send new one 
                Gia_VtaSendAbsracted( p, pPars->fVerbose );
                fOneIsSent = 1;
            }
1649
        }
1650 1651
        // dump the model
        if ( p->pPars->fDumpVabs && (f & 1) )
1652
        {
1653
            char Command[1000];
1654
            Abc_FrameSetStatus( -1 );
1655 1656
            Abc_FrameSetCex( NULL );
            Abc_FrameSetNFrames( f+1 );
1657
            sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "vtabs.aig"), ".status") );
1658
            Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1659
            Gia_VtaDumpAbsracted( p, pPars->fVerbose );
1660
        }
1661
        // check if the number of objects is below limit
1662 1663 1664 1665 1666
        if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
        {
            Status = -1;
            break;
        }
1667
    }
1668
finish:
1669
    // analize the results
1670 1671
    if ( pCex == NULL )
    {
1672 1673
        if ( p->pPars->fVerbose && Status == -1 )
            printf( "\n" );
1674 1675 1676
        if ( Vec_PtrSize(p->vCores) == 0 )
            Abc_Print( 1, "Abstraction is not produced because first frame is not solved.  " );
        else
1677
        {
1678
            assert( Vec_PtrSize(p->vCores) > 0 );
1679 1680
//            if ( pAig->vObjClasses != NULL )
//                Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
1681 1682 1683 1684
            Vec_IntFreeP( &pAig->vObjClasses );
            pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
            if ( Status == -1 )
            {
1685
                if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
1686
                    Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
1687
                else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1688
                    Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
1689 1690 1691 1692 1693
                else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (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 );
            }
1694
            else
1695 1696
            {
                p->pPars->iFrame++;
1697
                Abc_Print( 1, "VTA completed %d frames with a %d-stable abstraction.  ", f, p->pPars->nFramesNoChange );
1698
            }
1699
        }
1700 1701 1702
    }
    else
    {
1703 1704
        if ( p->pPars->fVerbose )
            printf( "\n" );
1705 1706 1707
        ABC_FREE( p->pGia->pCexSeq );
        p->pGia->pCexSeq = pCex;
        if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
1708 1709
            Abc_Print( 1, "    Gia_VtaPerform(): CEX verification has failed!\n" );
        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
1710
        p->pPars->iFrame = pCex->iFrame - 1;
1711
        Vec_IntFreeP( &pAig->vObjClasses );
1712
        RetValue = 0;
1713
    }
1714
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1715

1716 1717
    if ( p->pPars->fVerbose )
    {
1718 1719 1720 1721 1722 1723
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
1724 1725
        Gia_VtaPrintMemory( p );
    }
1726

1727
    Vga_ManStop( p );
1728
    fflush( stdout );
1729
    return RetValue;
1730 1731
}

1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742
/**Function*************************************************************

  Synopsis    [Collect nodes/flops involved in different timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1743
int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars )
1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757
{
    int RetValue = -1;
    if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
    {
        int nFramesMaxOld = pPars->nFramesMax;
        pPars->nFramesMax = pPars->nFramesStart;
        RetValue = Gia_VtaPerformInt( pAig, pPars );
        pPars->nFramesMax = nFramesMaxOld;
    }
    if ( RetValue == 0 )
        return RetValue;
    return Gia_VtaPerformInt( pAig, pPars );
}

1758 1759 1760 1761 1762 1763 1764
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END