pdrCore.c 35.6 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
                Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
623 624
                    nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
625 626 627
                if ( p->pPars->fUseBridge )
                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
628 629
                if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                {
630
                    if ( p->pPars->fVerbose )
631
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
632 633 634 635 636
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Quitting due to callback on fail.\n" );
                    p->pPars->iFrame = k;
                    return -1;
                }
637 638
                if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
                    return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
639
                p->pPars->timeLastSolved = Abc_Clock();
640
                continue;
641
            }
642
            // try to solve this output
643 644 645
            if ( p->pTime4Outs )
            {
                assert( p->pTime4Outs[p->iOutCur] > 0 );
646 647
                clkOne = Abc_Clock();
                p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
648
            }
649
            while ( 1 )
650
            {
651
                if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
652
                {
653
                    if ( p->pPars->fVerbose )
654
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
655 656 657
                    if ( !p->pPars->fSilent )
                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
                    p->pPars->iFrame = k;
658
                    return -1;
659
                }
660 661 662 663
                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
                if ( RetValue == 1 )
                    break;
                if ( RetValue == -1 )
664
                {
665
                    if ( p->pPars->fVerbose )
666
                        Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
667 668 669 670 671 672 673 674 675 676 677
                    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 )
678
                        Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
679
                    else if ( p->pPars->fVerbose )
680
                        Abc_Print( 1, "Computation cancelled by the callback.\n" );
681
                    p->pPars->iFrame = k;
682
                    return -1;
683
                }
684 685 686 687 688
                if ( RetValue == 0 )
                {
                    RetValue = Pdr_ManBlockCube( p, pCube );
                    if ( RetValue == -1 )
                    {
689
                        if ( p->pPars->fVerbose )
690
                            Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
691
                        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
692
                            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
693
                        else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
694
                            Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
695
                        else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
696 697 698 699 700
                        {
                            Pdr_QueueClean( p );
                            pCube = NULL;
                            break; // keep solving
                        }
701 702
                        else if ( p->pPars->nConfLimit )
                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
703
                        else if ( p->pPars->fVerbose )
704 705
                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
                        p->pPars->iFrame = k;
706
                        return -1;
707 708 709 710 711 712 713 714
                    }
                    if ( RetValue == 0 )
                    {
                        if ( fPrintClauses )
                        {
                            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
                            Pdr_ManPrintClauses( p, 0 );
                        }
715
                        if ( p->pPars->fVerbose )
716
                            Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
717 718 719
                        p->pPars->iFrame = k;
                        if ( !p->pPars->fSolveAll )
                        {
720
                            p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
721 722 723
                            return 0; // SAT
                        }
                        p->pPars->nFailOuts++;
724
                        pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
725
                        if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
726
                        assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
727 728 729
                        if ( p->pPars->fUseBridge )
                            Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
730 731
                        if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                        {
732
                            if ( p->pPars->fVerbose )
733
                                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
734 735 736 737 738
                            if ( !p->pPars->fSilent )
                                Abc_Print( 1, "Quitting due to callback on fail.\n" );
                            p->pPars->iFrame = k;
                            return -1;
                        }
739
                        if ( !p->pPars->fNotVerbose )
740
                            Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
741
                                nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
742 743
                        if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                            return 0; // all SAT
744 745 746
                        Pdr_QueueClean( p );
                        pCube = NULL;
                        break; // keep solving
747
                    }
748
                    if ( p->pPars->fVerbose )
749
                        Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
750
                }
751
            }
752 753
            if ( p->pTime4Outs )
            {
754
                abctime timeSince = Abc_Clock() - clkOne;
755 756
                assert( p->pTime4Outs[p->iOutCur] > 0 );
                p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
757
                if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
758 759
                {
                    p->pPars->nDropOuts++;
760 761
                    if ( p->pPars->vOutMap ) 
                        Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
762 763
                    if ( !p->pPars->fNotVerbose ) 
                        Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
764
                }
765
                p->timeToStopOne = 0;
766
            }
767
        }
768

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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

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

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


ABC_NAMESPACE_IMPL_END