pdrCore.c 35.7 KB
Newer Older
1 2 3 4 5 6
/**CFile****************************************************************

  FileName    [pdrCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

7
  PackageName [Property driven reachability.]
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

  Synopsis    [Core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - November 20, 2010.]

  Revision    [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]

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

#include "pdrInt.h"

ABC_NAMESPACE_IMPL_START


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

30
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
Alan Mishchenko committed
31
extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
32

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Returns 1 if the state could be blocked.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
{
    memset( pPars, 0, sizeof(Pdr_Par_t) );
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
//    pPars->iOutput        =      -1;  // zero-based output number
    pPars->nRecycle       =     300;  // limit on vars for recycling
    pPars->nFrameMax      =   10000;  // limit on number of timeframes
    pPars->nTimeOut       =       0;  // timeout in seconds
    pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
    pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
    pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
    pPars->fTwoRounds     =       0;  // use two rounds for generalization
    pPars->fMonoCnf       =       0;  // monolythic CNF
    pPars->fDumpInv       =       0;  // dump inductive invariant
    pPars->fShortest      =       0;  // forces bug traces to be shortest
    pPars->fVerbose       =       0;  // verbose output
    pPars->fVeryVerbose   =       0;  // very verbose output
    pPars->fNotVerbose    =       0;  // not printing line-by-line progress
    pPars->iFrame         =      -1;  // explored up to this frame
66 67
    pPars->nFailOuts      =       0;  // the number of disproved outputs
    pPars->nDropOuts      =       0;  // the number of timed out outputs
68
    pPars->timeLastSolved =       0;  // last one solved
69 70 71 72 73 74 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
}

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

  Synopsis    [Reduces clause using analyzeFinal.]

  Description [Assumes that the SAT solver just terminated an UNSAT call.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
{
    Pdr_Set_t * pCubeMin;
    Vec_Int_t * vLits;
    int i, Entry, nCoreLits, * pCoreLits;
    // get relevant SAT literals
    nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
    // translate them into register literals and remove auxiliary
    vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
    // skip if there is no improvement
    if ( Vec_IntSize(vLits) == pCube->nLits )
        return NULL;
    assert( Vec_IntSize(vLits) < pCube->nLits );
    // if the cube overlaps with init, add any literal
    Vec_IntForEachEntry( vLits, Entry, i )
        if ( lit_sign(Entry) == 0 ) // positive literal
            break;
    if ( i == Vec_IntSize(vLits) ) // only negative literals
    {
        // add the first positive literal
        for ( i = 0; i < pCube->nLits; i++ )
            if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
            {
                Vec_IntPush( vLits, pCube->Lits[i] );
                break;
            }
        assert( i < pCube->nLits );
    }
    // generate a starting cube
    pCubeMin  = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
    assert( !Pdr_SetIsInit(pCubeMin, -1) );
/*
    // make sure the cube works
    {
    int RetValue;
    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
    assert( RetValue );
    }
*/
    return pCubeMin;
}

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

  Synopsis    [Returns 1 if the state could be blocked.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManPushClauses( Pdr_Man_t * p )
{
    Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
    Vec_Ptr_t * vArrayK, * vArrayK1;
139
    int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
140
    int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
141
    int Counter = 0;
142
    abctime clk = Abc_Clock();
143
    assert( p->iUseFrame > 0 );
144
    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
145 146
    {
        Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
147
        vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
        {
            Counter++;

            // remove cubes in the same frame that are contained by pCubeK
            Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
            {
                if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
                    continue;
                Pdr_SetDeref( pTemp );
                Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
                Vec_PtrPop(vArrayK);
                m--;
            }

            // check if the clause can be moved to the next frame
164 165 166 167
            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
            if ( RetValue2 == -1 )
                return -1;
            if ( !RetValue2 )
168 169 170 171 172 173 174
                continue;

            {
                Pdr_Set_t * pCubeMin;
                pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
                if ( pCubeMin != NULL )
                {
175
//                Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
                    Pdr_SetDeref( pCubeK );
                    pCubeK = pCubeMin;
                }
            }

            // if it can be moved, add it to the next frame
            Pdr_ManSolverAddClause( p, k+1, pCubeK );
            // check if the clause subsumes others
            Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
            {
                if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
                    continue;
                Pdr_SetDeref( pCubeK1 );
                Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
                Vec_PtrPop(vArrayK1);
                i--;
            }
            // add the last clause
            Vec_PtrPush( vArrayK1, pCubeK );
            Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
            Vec_PtrPop(vArrayK);
            j--;
        }
        if ( Vec_PtrSize(vArrayK) == 0 )
            RetValue = 1;
    }

    // clean up the last one
204
    vArrayK = Vec_VecEntry( p->vClauses, kMax );
205 206 207 208 209 210 211 212 213
    Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
    Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
    {
        // remove cubes in the same frame that are contained by pCubeK
        Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
        {
            if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
                continue;
/*
214
            Abc_Print( 1, "===\n" );
215
            Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
216
            Abc_Print( 1, "\n" );
217
            Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
218
            Abc_Print( 1, "\n" );
219 220 221 222 223 224 225
*/
            Pdr_SetDeref( pTemp );
            Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
            Vec_PtrPop(vArrayK);
            m--;
        }
    }
226
    p->tPush += Abc_Clock() - clk;
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
    return RetValue;
}

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

  Synopsis    [Returns 1 if the clause is contained in higher clauses.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
{
    Pdr_Set_t * pThis;
    Vec_Ptr_t * vArrayK;
    int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
246
    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
            if ( Pdr_SetContains( pSet, pThis ) )
                return 1;
    return 0;
}


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

  Synopsis    [Sorts literals by priority.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
{
    int * pPrios = Vec_IntArray(p->vPrio);
    int * pArray = p->pOrder;
    int temp, i, j, best_i, nSize = pCube->nLits;
    // initialize variable order
    for ( i = 0; i < nSize; i++ )
        pArray[i] = i;
    for ( i = 0; i < nSize-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nSize; j++ )
//            if ( pArray[j] < pArray[best_i] )
            if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
                best_i = j;
280 281
        temp = pArray[i];
        pArray[i] = pArray[best_i];
282 283 284 285
        pArray[best_i] = temp;
    }
/*
    for ( i = 0; i < pCube->nLits; i++ )
286 287
        Abc_Print( 1, "%2d : %5d    %5d  %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
    Abc_Print( 1, "\n" );
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
*/
    return pArray;
}


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

  Synopsis    [Returns 1 if the state could be blocked.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
{
    Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
307
    int i, j, n, Lit, RetValue;
308
    abctime clk = Abc_Clock();
309 310 311 312 313 314 315 316
    int * pOrder;
    // if there is no induction, return
    *ppCubeMin = NULL;
    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
    if ( RetValue == -1 )
        return -1;
    if ( RetValue == 0 )
    {
317
        p->tGeneral += Abc_Clock() - clk;
318 319
        return 0;
    }
320

321 322 323 324 325 326
    // reduce clause using assumptions
//    pCubeMin = Pdr_SetDup( pCube );
    pCubeMin = Pdr_ManReduceClause( p, k, pCube );
    if ( pCubeMin == NULL )
        pCubeMin = Pdr_SetDup( pCube );

327 328
    // perform generalization
    if ( !p->pPars->fSkipGeneral )
329
    {
330 331 332 333
        // sort literals by their occurences
        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
        // try removing literals
        for ( j = 0; j < pCubeMin->nLits; j++ )
334
        {
335 336 337 338 339 340 341 342 343
            // use ordering
    //        i = j;
            i = pOrder[j];

            // check init state
            assert( pCubeMin->Lits[i] != -1 );
            if ( Pdr_SetIsInit(pCubeMin, i) )
                continue;
            // try removing this literal
344
            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
            if ( RetValue == -1 )
            {
                Pdr_SetDeref( pCubeMin );
                return -1;
            }
            pCubeMin->Lits[i] = Lit;
            if ( RetValue == 0 )
                continue;

            // remove j-th entry
            for ( n = j; n < pCubeMin->nLits-1; n++ )
                pOrder[n] = pOrder[n+1];
            j--;

            // success - update the cube
            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
            Pdr_SetDeref( pCubeTmp );
            assert( pCubeMin->nLits > 0 );
            i--;

            // get the ordering by decreasing priorit
            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
368 369
        }

370 371
        if ( p->pPars->fTwoRounds )
        for ( j = 0; j < pCubeMin->nLits; j++ )
372
        {
373 374 375 376 377 378 379 380 381
            // use ordering
    //        i = j;
            i = pOrder[j];

            // check init state
            assert( pCubeMin->Lits[i] != -1 );
            if ( Pdr_SetIsInit(pCubeMin, i) )
                continue;
            // try removing this literal
382
            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
            if ( RetValue == -1 )
            {
                Pdr_SetDeref( pCubeMin );
                return -1;
            }
            pCubeMin->Lits[i] = Lit;
            if ( RetValue == 0 )
                continue;

            // remove j-th entry
            for ( n = j; n < pCubeMin->nLits-1; n++ )
                pOrder[n] = pOrder[n+1];
            j--;

            // success - update the cube
            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
            Pdr_SetDeref( pCubeTmp );
            assert( pCubeMin->nLits > 0 );
            i--;

            // get the ordering by decreasing priorit
            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
406 407 408 409 410
        }
    }

    assert( ppCubeMin != NULL );
    *ppCubeMin = pCubeMin;
411
    p->tGeneral += Abc_Clock() - clk;
412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430
    return 1;
}

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

  Synopsis    [Returns 1 if the state could be blocked.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
{
    Pdr_Obl_t * pThis;
    Pdr_Set_t * pPred, * pCubeMin;
    int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
431
    int kMax = Vec_PtrSize(p->vSolvers)-1;
432
    abctime clk;
433 434
    p->nBlocks++;
    // create first proof obligation
435
//    assert( p->pQueue == NULL );
436 437 438 439 440 441 442 443 444
    pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
    Pdr_QueuePush( p, pThis );
    // try to solve it recursively
    while ( !Pdr_QueueIsEmpty(p) )
    {
        Counter++;
        pThis = Pdr_QueueHead( p );
        if ( pThis->iFrame == 0 )
            return 0; // SAT
445 446
        if ( pThis->iFrame > kMax ) // finished this level
            return 1;
Alan Mishchenko committed
447 448
        if ( p->nQueLim && p->nQueCur >= p->nQueLim )
        {
Alan Mishchenko committed
449
            p->nQueLim = p->nQueLim * 3 / 2;
Alan Mishchenko committed
450 451 452
            Pdr_QueueStop( p );
            return 1; // restart
        }
453 454 455
        pThis = Pdr_QueuePop( p );
        assert( pThis->iFrame > 0 );
        assert( !Pdr_SetIsInit(pThis->pState, -1) );
456
        p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame );
457
        clk = Abc_Clock();
458 459
        if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
        {
460
            p->tContain += Abc_Clock() - clk;
461 462 463
            Pdr_OblDeref( pThis );
            continue;
        }
464
        p->tContain += Abc_Clock() - clk;
465 466

        // check if the cube is already contained
467
        RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
468
        if ( RetValue == -1 ) // resource limit is reached
469 470 471 472 473
        {
            Pdr_OblDeref( pThis );
            return -1;
        }
        if ( RetValue ) // cube is blocked by clauses in this frame
474 475 476 477 478 479 480 481
        {
            Pdr_OblDeref( pThis );
            continue;
        }

        // check if the cube holds with relative induction
        pCubeMin = NULL;
        RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
482
        if ( RetValue == -1 ) // resource limit is reached
483 484 485 486 487 488 489 490 491 492 493 494
        {
            Pdr_OblDeref( pThis );
            return -1;
        }
        if ( RetValue ) // cube is blocked inductively in this frame
        {
            assert( pCubeMin != NULL );
            // k is the last frame where pCubeMin holds
            k = pThis->iFrame;
            // check other frames
            assert( pPred == NULL );
            for ( k = pThis->iFrame; k < kMax; k++ )
495 496 497 498 499 500 501 502
            {
                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
                if ( RetValue == -1 )
                {
                    Pdr_OblDeref( pThis );
                    return -1;
                }
                if ( !RetValue )
503
                    break;
504
            }
505 506 507
            // add new clause
            if ( p->pPars->fVeryVerbose )
            {
Alan Mishchenko committed
508 509 510
                Abc_Print( 1, "Adding cube " );
                Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
                Abc_Print( 1, " to frame %d.\n", k );
511 512 513 514 515 516 517 518 519 520 521 522 523 524
            }
            // set priority flops
            for ( i = 0; i < pCubeMin->nLits; i++ )
            {
                assert( pCubeMin->Lits[i] >= 0 );
                assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
            }
            Vec_VecPush( p->vClauses, k, pCubeMin );   // consume ref
            p->nCubes++;
            // add clause
            for ( i = 1; i <= k; i++ )
                Pdr_ManSolverAddClause( p, i, pCubeMin );
            // schedule proof obligation
525
            if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
            {
                pThis->iFrame = k+1;
                pThis->prio   = Prio--;
                Pdr_QueuePush( p, pThis );
            }
            else
            {
                Pdr_OblDeref( pThis );
            }
        }
        else
        {
            assert( pCubeMin == NULL );
            assert( pPred != NULL );
            pThis->prio = Prio--;
            Pdr_QueuePush( p, pThis );
            pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
            Pdr_QueuePush( p, pThis );
        }

546 547 548
        // check termination
        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
            return -1;
549
        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
550
            return -1;
551
        if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
552
            return -1;
553
        if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
554
            return -1;
555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
    }
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManSolveInt( Pdr_Man_t * p )
{
    int fPrintClauses = 0;
573
    Pdr_Set_t * pCube = NULL;
574
    Aig_Obj_t * pObj;
575
    Abc_Cex_t * pCexNew;
576
    int k, RetValue = -1;
577
    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
578 579
    abctime clkStart = Abc_Clock(), clkOne = 0;
    p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
580
    assert( Vec_PtrSize(p->vSolvers) == 0 );
581 582 583 584 585 586 587 588 589 590
    // in the multi-output mode, mark trivial POs (those fed by const0) as solved 
    if ( p->pPars->fSolveAll )
        Saig_ManForEachPo( p->pAig, pObj, k )
            if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
            {
                Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
                p->pPars->nProveOuts++;
                if ( p->pPars->fUseBridge )
                    Gia_ManToBridgeResult( stdout, 1, NULL, k );
            }
591
    // create the first timeframe
592
    p->pPars->timeLastSolved = Abc_Clock();
593 594 595 596 597
    Pdr_ManCreateSolver( p, (k = 0) );
    while ( 1 )
    {
        p->nFrames = k;
        assert( k == Vec_PtrSize(p->vSolvers)-1 );
598
        p->iUseFrame = Abc_MaxInt(k, 1);
599
        Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
600
        {
601
            // skip disproved outputs
602 603
            if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
                continue;
604 605 606
            // skip output whose time has run out
            if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
                continue;
607 608 609 610 611
            // check if the output is trivially solved
            if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
                continue;
            // check if the output is trivially solved
            if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
612
            {
613 614
                if ( !p->pPars->fSolveAll )
                {
615 616
                    pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
                    p->pAig->pSeqModel = pCexNew;
617 618
                    return 0; // SAT
                }
619
                pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
620
                p->pPars->nFailOuts++;
621
                if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
622
                if ( !p->pPars->fNotVerbose )
623
                Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
624 625
                    nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
626 627 628
                if ( p->pPars->fUseBridge )
                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
629 630
                if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                {
631
                    if ( p->pPars->fVerbose )
632
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
633 634 635 636 637
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Quitting due to callback on fail.\n" );
                    p->pPars->iFrame = k;
                    return -1;
                }
638 639
                if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
                    return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
640
                p->pPars->timeLastSolved = Abc_Clock();
641
                continue;
642
            }
643
            // try to solve this output
644 645 646
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[p->iOutCur] > 0 );
647 648
                clkOne = Abc_Clock();
                p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
649
            }
650
            while ( 1 )
651
            {
652
                if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
653
                {
654
                    if ( p->pPars->fVerbose )
655
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
656 657 658
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
                    p->pPars->iFrame = k;
659
                    return -1;
660
                }
661 662 663 664
                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
                if ( RetValue == 1 )
                    break;
                if ( RetValue == -1 )
665
                {
666
                    if ( p->pPars->fVerbose )
667
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
668 669 670 671 672 673 674 675 676 677 678
                    if ( p->timeToStop && Abc_Clock() > p->timeToStop )
                        Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
                    else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
                    else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
                    {
                        Pdr_QueueClean( p );
                        pCube = NULL;
                        break; // keep solving
                    }
                    else if ( p->pPars->nConfLimit )
679
                        Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
680
                    else if ( p->pPars->fVerbose )
681
                        Abc_Print( 1, "Computation cancelled by the callback.\n" );
682
                    p->pPars->iFrame = k;
683
                    return -1;
684
                }
685 686 687 688 689
                if ( RetValue == 0 )
                {
                    RetValue = Pdr_ManBlockCube( p, pCube );
                    if ( RetValue == -1 )
                    {
690
                        if ( p->pPars->fVerbose )
691
                            Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
692
                        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
693
                            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
694
                        else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
695
                            Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
696
                        else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
697 698 699 700 701
                        {
                            Pdr_QueueClean( p );
                            pCube = NULL;
                            break; // keep solving
                        }
702 703
                        else if ( p->pPars->nConfLimit )
                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
704
                        else if ( p->pPars->fVerbose )
705 706
                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
                        p->pPars->iFrame = k;
707
                        return -1;
708 709 710 711 712 713 714 715
                    }
                    if ( RetValue == 0 )
                    {
                        if ( fPrintClauses )
                        {
                            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
                            Pdr_ManPrintClauses( p, 0 );
                        }
716
                        if ( p->pPars->fVerbose )
717
                            Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
718 719 720
                        p->pPars->iFrame = k;
                        if ( !p->pPars->fSolveAll )
                        {
721
                            p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
722 723 724
                            return 0; // SAT
                        }
                        p->pPars->nFailOuts++;
725
                        pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
726
                        if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
727
                        assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
728 729 730
                        if ( p->pPars->fUseBridge )
                            Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
731 732
                        if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                        {
733
                            if ( p->pPars->fVerbose )
734
                                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
735 736 737 738 739
                            if ( !p->pPars->fSilent )
                                Abc_Print( 1, "Quitting due to callback on fail.\n" );
                            p->pPars->iFrame = k;
                            return -1;
                        }
740
                        if ( !p->pPars->fNotVerbose )
741
                            Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
742
                                nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
743 744
                        if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                            return 0; // all SAT
745 746 747
                        Pdr_QueueClean( p );
                        pCube = NULL;
                        break; // keep solving
748
                    }
749
                    if ( p->pPars->fVerbose )
750
                        Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
751
                }
752
            }
753 754
            if ( p->pTime4Outs )
            {
755
                abctime timeSince = Abc_Clock() - clkOne;
756 757
                assert( p->pTime4Outs[p->iOutCur] > 0 );
                p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
758
                if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
759 760
                {
                    p->pPars->nDropOuts++;
761 762
                    if ( p->pPars->vOutMap ) 
                        Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
763 764
                    if ( !p->pPars->fNotVerbose ) 
                        Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
765
                }
766
                p->timeToStopOne = 0;
767
            }
768
        }
769

770
        if ( p->pPars->fVerbose )
771
            Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
772 773 774 775 776 777 778 779 780 781 782 783 784
        // open a new timeframe
        p->nQueLim = p->pPars->nRestLimit;
        assert( pCube == NULL );
        Pdr_ManSetPropertyOutput( p, k );
        Pdr_ManCreateSolver( p, ++k );
        if ( fPrintClauses )
        {
            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
            Pdr_ManPrintClauses( p, 0 );
        }
        // push clauses into this timeframe
        RetValue = Pdr_ManPushClauses( p );
        if ( RetValue == -1 )
785
        {
786
            if ( p->pPars->fVerbose )
787
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
788
            if ( !p->pPars->fSilent )
789
            {
790
                if ( p->timeToStop && Abc_Clock() > p->timeToStop )
791 792 793 794
                    Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
                else
                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
            }
795
            p->pPars->iFrame = k;
796
            return -1;
797 798 799
        }
        if ( RetValue )
        {
800
            if ( p->pPars->fVerbose )
801
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
802 803 804 805 806
            if ( !p->pPars->fSilent )
                Pdr_ManReportInvariant( p );
            if ( !p->pPars->fSilent )
                Pdr_ManVerifyInvariant( p );
            p->pPars->iFrame = k;
807 808 809
            // count the number of UNSAT outputs
            p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
            // convert previously 'unknown' into 'unsat'
810
            if ( p->pPars->vOutMap )
811
                for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
812
                    if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
813
                    {
814
                        Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
815 816 817
                        if ( p->pPars->fUseBridge )
                            Gia_ManToBridgeResult( stdout, 1, NULL, k );
                    }
818 819 820 821
            if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
                return 1; // UNSAT
            if ( p->pPars->nFailOuts > 0 )
                return 0; // SAT
822
            return -1;
823
        }
824
        if ( p->pPars->fVerbose )
825
            Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
826

827 828 829 830
        // check termination
        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
        {
            p->pPars->iFrame = k;
831
            return -1;
832
        }
833
        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
834 835 836
        {
            if ( fPrintClauses )
            {
837
                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
838 839
                Pdr_ManPrintClauses( p, 0 );
            }
840
            if ( p->pPars->fVerbose )
841
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
842 843
            if ( !p->pPars->fSilent )
                Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
844
            p->pPars->iFrame = k;
845
            return -1;
846
        }
847
        if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
848 849 850 851 852 853
        {
            if ( fPrintClauses )
            {
                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
                Pdr_ManPrintClauses( p, 0 );
            }
854
            if ( p->pPars->fVerbose )
855
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
856
            if ( !p->pPars->fSilent )
857
                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
858
            p->pPars->iFrame = k;
859
            return -1;
860
        }
861 862
        if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
        {
863
            if ( p->pPars->fVerbose )
864
                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
865 866
            if ( !p->pPars->fSilent )
                Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
867
            p->pPars->iFrame = k;
868
            return -1;
869
        }
870
    }
871 872
    assert( 0 );
    return -1;
873 874 875 876 877 878 879 880 881 882 883 884 885
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
886
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
887 888
{
    Pdr_Man_t * p;
889
    int k, RetValue;
890
    abctime clk = Abc_Clock();
891 892
    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
        pPars->nTimeOutOne = 0;
893
    if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
894
        pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
895 896 897
    if ( pPars->fVerbose )
    {
//    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
898 899 900 901
        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
            pPars->nRecycle,
            pPars->nFrameMax,
            pPars->nRestLimit,
902
            pPars->nTimeOut );
903 904 905
        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
            pPars->fMonoCnf ?     "yes" : "no",
            pPars->fSkipGeneral ? "yes" : "no",
906
            pPars->fSolveAll ?    "yes" : "no" );
907 908 909
    }
    ABC_FREE( pAig->pSeqModel );
    p = Pdr_ManStart( pAig, pPars, NULL );
910
    RetValue = Pdr_ManSolveInt( p );
911 912 913 914 915 916 917 918
    if ( RetValue == 0 )
        assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
    if ( p->vCexes )
    {
        assert( p->pAig->vSeqModelVec == NULL );
        p->pAig->vSeqModelVec = p->vCexes;
        p->vCexes = NULL;
    }
919 920
    if ( p->pPars->fDumpInv )
        Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
921
    p->tTotal += Abc_Clock() - clk;
922
    Pdr_ManStop( p );
923
    pPars->iFrame--;
924 925 926 927 928
    // convert all -2 (unknown) entries into -1 (undec)
    if ( pPars->vOutMap )
        for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
            if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
                Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
Alan Mishchenko committed
929 930
    if ( pPars->fUseBridge )
        Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
931 932 933 934 935 936 937 938 939
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END