1 /**CFile****************************************************************
2 
3   FileName    [pdrCore.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Property driven reachability.]
8 
9   Synopsis    [Core procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - November 20, 2010.]
16 
17   Revision    [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "pdrInt.h"
22 #include "base/main/main.h"
23 #include "misc/hash/hash.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 ///                        DECLARATIONS                              ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
33 extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
34 
35 ////////////////////////////////////////////////////////////////////////
36 ///                     FUNCTION DEFINITIONS                         ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 /**Function*************************************************************
40 
41   Synopsis    [Returns 1 if the state could be blocked.]
42 
43   Description []
44 
45   SideEffects []
46 
47   SeeAlso     []
48 
49 ***********************************************************************/
Pdr_ManSetDefaultParams(Pdr_Par_t * pPars)50 void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
51 {
52     memset( pPars, 0, sizeof(Pdr_Par_t) );
53 //    pPars->iOutput        =      -1;  // zero-based output number
54     pPars->nRecycle       =     300;  // limit on vars for recycling
55     pPars->nFrameMax      =   10000;  // limit on number of timeframes
56     pPars->nTimeOut       =       0;  // timeout in seconds
57     pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
58     pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
59     pPars->nConfGenLimit  =       0;  // limit on SAT solver conflicts during generalization
60     pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
61     pPars->nRandomSeed   = 91648253;  // value to seed the SAT solver with
62     pPars->fTwoRounds     =       0;  // use two rounds for generalization
63     pPars->fMonoCnf       =       0;  // monolythic CNF
64     pPars->fNewXSim       =       0;  // updated X-valued simulation
65     pPars->fFlopPrio      =       0;  // use structural flop priorities
66     pPars->fFlopOrder     =       0;  // order flops for 'analyze_final' during generalization
67     pPars->fDumpInv       =       0;  // dump inductive invariant
68     pPars->fUseSupp       =       1;  // using support variables in the invariant
69     pPars->fShortest      =       0;  // forces bug traces to be shortest
70     pPars->fUsePropOut    =       1;  // use property output
71     pPars->fSkipDown      =       1;  // apply down in generalization
72     pPars->fCtgs          =       0;  // handle CTGs in down
73     pPars->fUseAbs        =       0;  // use abstraction
74     pPars->fUseSimpleRef  =       0;  // simplified CEX refinement
75     pPars->fVerbose       =       0;  // verbose output
76     pPars->fVeryVerbose   =       0;  // very verbose output
77     pPars->fNotVerbose    =       0;  // not printing line-by-line progress
78     pPars->iFrame         =      -1;  // explored up to this frame
79     pPars->nFailOuts      =       0;  // the number of disproved outputs
80     pPars->nDropOuts      =       0;  // the number of timed out outputs
81     pPars->timeLastSolved =       0;  // last one solved
82     pPars->pInvFileName   =    NULL;  // invariant file name
83 }
84 
85 /**Function*************************************************************
86 
87   Synopsis    [Reduces clause using analyzeFinal.]
88 
89   Description [Assumes that the SAT solver just terminated an UNSAT call.]
90 
91   SideEffects []
92 
93   SeeAlso     []
94 
95 ***********************************************************************/
Pdr_ManReduceClause(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)96 Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
97 {
98     Pdr_Set_t * pCubeMin;
99     Vec_Int_t * vLits;
100     int i, Entry, nCoreLits, * pCoreLits;
101     // get relevant SAT literals
102     nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
103     // translate them into register literals and remove auxiliary
104     vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
105     // skip if there is no improvement
106     if ( Vec_IntSize(vLits) == pCube->nLits )
107         return NULL;
108     assert( Vec_IntSize(vLits) < pCube->nLits );
109     // if the cube overlaps with init, add any literal
110     Vec_IntForEachEntry( vLits, Entry, i )
111         if ( Abc_LitIsCompl(Entry) == 0 ) // positive literal
112             break;
113     if ( i == Vec_IntSize(vLits) ) // only negative literals
114     {
115         // add the first positive literal
116         for ( i = 0; i < pCube->nLits; i++ )
117             if ( Abc_LitIsCompl(pCube->Lits[i]) == 0 ) // positive literal
118             {
119                 Vec_IntPush( vLits, pCube->Lits[i] );
120                 break;
121             }
122         assert( i < pCube->nLits );
123     }
124     // generate a starting cube
125     pCubeMin  = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
126     assert( !Pdr_SetIsInit(pCubeMin, -1) );
127 /*
128     // make sure the cube works
129     {
130     int RetValue;
131     RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
132     assert( RetValue );
133     }
134 */
135     return pCubeMin;
136 }
137 
138 /**Function*************************************************************
139 
140   Synopsis    [Returns 1 if the state could be blocked.]
141 
142   Description []
143 
144   SideEffects []
145 
146   SeeAlso     []
147 
148 ***********************************************************************/
Pdr_ManPushClauses(Pdr_Man_t * p)149 int Pdr_ManPushClauses( Pdr_Man_t * p )
150 {
151     Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
152     Vec_Ptr_t * vArrayK, * vArrayK1;
153     int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
154     int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
155     int Counter = 0;
156     abctime clk = Abc_Clock();
157     assert( p->iUseFrame > 0 );
158     Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
159     {
160         Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
161         vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
162         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
163         {
164             Counter++;
165 
166             // remove cubes in the same frame that are contained by pCubeK
167             Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
168             {
169                 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
170                     continue;
171                 Pdr_SetDeref( pTemp );
172                 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
173                 Vec_PtrPop(vArrayK);
174                 m--;
175             }
176 
177             // check if the clause can be moved to the next frame
178             RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
179             if ( RetValue2 == -1 )
180                 return -1;
181             if ( !RetValue2 )
182                 continue;
183 
184             {
185                 Pdr_Set_t * pCubeMin;
186                 pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
187                 if ( pCubeMin != NULL )
188                 {
189 //                Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
190                     Pdr_SetDeref( pCubeK );
191                     pCubeK = pCubeMin;
192                 }
193             }
194 
195             // if it can be moved, add it to the next frame
196             Pdr_ManSolverAddClause( p, k+1, pCubeK );
197             // check if the clause subsumes others
198             Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
199             {
200                 if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
201                     continue;
202                 Pdr_SetDeref( pCubeK1 );
203                 Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
204                 Vec_PtrPop(vArrayK1);
205                 i--;
206             }
207             // add the last clause
208             Vec_PtrPush( vArrayK1, pCubeK );
209             Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
210             Vec_PtrPop(vArrayK);
211             j--;
212         }
213         if ( Vec_PtrSize(vArrayK) == 0 )
214             RetValue = 1;
215     }
216 
217     // clean up the last one
218     vArrayK = Vec_VecEntry( p->vClauses, kMax );
219     Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
220     Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
221     {
222         // remove cubes in the same frame that are contained by pCubeK
223         Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
224         {
225             if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
226                 continue;
227 /*
228             Abc_Print( 1, "===\n" );
229             Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
230             Abc_Print( 1, "\n" );
231             Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
232             Abc_Print( 1, "\n" );
233 */
234             Pdr_SetDeref( pTemp );
235             Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
236             Vec_PtrPop(vArrayK);
237             m--;
238         }
239     }
240     p->tPush += Abc_Clock() - clk;
241     return RetValue;
242 }
243 
244 /**Function*************************************************************
245 
246   Synopsis    [Returns 1 if the clause is contained in higher clauses.]
247 
248   Description []
249 
250   SideEffects []
251 
252   SeeAlso     []
253 
254 ***********************************************************************/
Pdr_ManCheckContainment(Pdr_Man_t * p,int k,Pdr_Set_t * pSet)255 int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
256 {
257     Pdr_Set_t * pThis;
258     Vec_Ptr_t * vArrayK;
259     int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
260     Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
261         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
262             if ( Pdr_SetContains( pSet, pThis ) )
263                 return 1;
264     return 0;
265 }
266 
267 
268 /**Function*************************************************************
269 
270   Synopsis    [Sorts literals by priority.]
271 
272   Description []
273 
274   SideEffects []
275 
276   SeeAlso     []
277 
278 ***********************************************************************/
Pdr_ManSortByPriority(Pdr_Man_t * p,Pdr_Set_t * pCube)279 int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
280 {
281     int * pPrios = Vec_IntArray(p->vPrio);
282     int * pArray = p->pOrder;
283     int temp, i, j, best_i, nSize = pCube->nLits;
284     // initialize variable order
285     for ( i = 0; i < nSize; i++ )
286         pArray[i] = i;
287     for ( i = 0; i < nSize-1; i++ )
288     {
289         best_i = i;
290         for ( j = i+1; j < nSize; j++ )
291 //            if ( pArray[j] < pArray[best_i] )
292             if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
293                 best_i = j;
294         temp = pArray[i];
295         pArray[i] = pArray[best_i];
296         pArray[best_i] = temp;
297     }
298 /*
299     for ( i = 0; i < pCube->nLits; i++ )
300         Abc_Print( 1, "%2d : %5d    %5d  %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
301     Abc_Print( 1, "\n" );
302 */
303     return pArray;
304 }
305 
306 
307 /**Function*************************************************************
308 
309   Synopsis    []
310 
311   Description []
312 
313   SideEffects []
314 
315   SeeAlso     []
316 
317 ***********************************************************************/
ZPdr_ManSimpleMic(Pdr_Man_t * p,int k,Pdr_Set_t ** ppCube)318 int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
319 {
320     int * pOrder;
321     int i, j, Lit, RetValue;
322     Pdr_Set_t * pCubeTmp;
323     // perform generalization
324     if ( p->pPars->fSkipGeneral )
325       return 0;
326 
327     // sort literals by their occurences
328     pOrder = Pdr_ManSortByPriority( p, *ppCube );
329     // try removing literals
330     for ( j = 0; j < (*ppCube)->nLits; j++ )
331     {
332         // use ordering
333     //        i = j;
334         i = pOrder[j];
335 
336         assert( (*ppCube)->Lits[i] != -1 );
337         // check init state
338         if ( Pdr_SetIsInit(*ppCube, i) )
339             continue;
340         // try removing this literal
341         Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1;
342         RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0, 1 );
343         if ( RetValue == -1 )
344             return -1;
345         (*ppCube)->Lits[i] = Lit;
346         if ( RetValue == 0 )
347             continue;
348 
349         // success - update the cube
350         *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i );
351         Pdr_SetDeref( pCubeTmp );
352         assert( (*ppCube)->nLits > 0 );
353 
354         // get the ordering by decreasing priority
355         pOrder = Pdr_ManSortByPriority( p, *ppCube );
356         j--;
357     }
358     return 0;
359 }
360 
361 
362 
363 /**Function*************************************************************
364 
365   Synopsis    []
366 
367   Description []
368 
369   SideEffects []
370 
371   SeeAlso     []
372 
373 ***********************************************************************/
ZPdr_ManDown(Pdr_Man_t * p,int k,Pdr_Set_t ** ppCube,Pdr_Set_t * pPred,Hash_Int_t * keep,Pdr_Set_t * pIndCube,int * added)374 int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added )
375 {
376     int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
377     int kMax = Vec_PtrSize(p->vSolvers)-1;
378     Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
379     while ( RetValue == 0 )
380     {
381         ctgAttempts = 0;
382         while ( p->pPars->fCtgs && RetValue == 0 && k > 1 && ctgAttempts < 3 )
383         {
384             pCtg = Pdr_SetDup( pPred );
385             //Check CTG for inductiveness
386             if ( Pdr_SetIsInit( pCtg, -1 ) )
387             {
388                 Pdr_SetDeref( pCtg );
389                 break;
390             }
391             if (*added == 0)
392             {
393                 for ( i = 1; i <= k; i++ )
394                     Pdr_ManSolverAddClause( p, i, pIndCube);
395                 *added = 1;
396             }
397             ctgAttempts++;
398             CtgRetValue = Pdr_ManCheckCube( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0, 1 );
399             if ( CtgRetValue != 1 )
400             {
401                 Pdr_SetDeref( pCtg );
402                 break;
403             }
404             pCubeMin = Pdr_ManReduceClause( p, k-1, pCtg );
405             if ( pCubeMin == NULL )
406                 pCubeMin = Pdr_SetDup ( pCtg );
407 
408             for ( l = k; l < kMax; l++ )
409                 if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0, 1 ) )
410                     break;
411             micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
412             assert ( micResult != -1 );
413 
414             // add new clause
415             if ( p->pPars->fVeryVerbose )
416             {
417                 Abc_Print( 1, "Adding cube " );
418                 Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
419                 Abc_Print( 1, " to frame %d.\n", l );
420             }
421             // set priority flops
422             for ( i = 0; i < pCubeMin->nLits; i++ )
423             {
424                 assert( pCubeMin->Lits[i] >= 0 );
425                 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
426                 if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
427                     p->nAbsFlops++;
428                 Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
429             }
430 
431             Vec_VecPush( p->vClauses, l, pCubeMin );   // consume ref
432             p->nCubes++;
433             // add clause
434             for ( i = 1; i <= l; i++ )
435                 Pdr_ManSolverAddClause( p, i, pCubeMin );
436             Pdr_SetDeref( pPred );
437             RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
438             assert( RetValue >= 0 );
439             Pdr_SetDeref( pCtg );
440             if ( RetValue == 1 )
441             {
442                 //printf ("IT'S A ONE\n");
443                 return 1;
444             }
445         }
446 
447         //join
448         if ( p->pPars->fVeryVerbose )
449         {
450             printf("Cube:\n");
451             ZPdr_SetPrint( *ppCube );
452             printf("\nPred:\n");
453             ZPdr_SetPrint( pPred );
454         }
455         *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
456         Pdr_SetDeref( pCubeTmp );
457         Pdr_SetDeref( pPred );
458         if ( *ppCube == NULL )
459             return 0;
460         if ( p->pPars->fVeryVerbose )
461         {
462             printf("Intersection:\n");
463             ZPdr_SetPrint( *ppCube );
464         }
465         if ( Pdr_SetIsInit( *ppCube, -1 ) )
466         {
467             if ( p->pPars->fVeryVerbose )
468                 printf ("Failed initiation\n");
469             return 0;
470         }
471         RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
472         if ( RetValue == -1 )
473             return -1;
474         if ( RetValue == 1 )
475         {
476             //printf ("*********IT'S A ONE\n");
477             break;
478         }
479         if ( RetValue == 0 && (*ppCube)->nLits == 1)
480         {
481             Pdr_SetDeref( pPred ); // fixed memory leak
482             // A workaround for the incomplete assignment returned by the SAT
483             // solver
484             return 0;
485         }
486     }
487     return 1;
488 }
489 
490 /**Function*************************************************************
491 
492   Synopsis    [Specialized sorting of flops based on priority.]
493 
494   Description []
495 
496   SideEffects []
497 
498   SeeAlso     []
499 
500 ***********************************************************************/
Vec_IntSelectSortPrioReverseLit(int * pArray,int nSize,Vec_Int_t * vPrios)501 static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
502 {
503     int i, j, best_i;
504     for ( i = 0; i < nSize-1; i++ )
505     {
506         best_i = i;
507         for ( j = i+1; j < nSize; j++ )
508             if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
509                 best_i = j;
510         ABC_SWAP( int, pArray[i], pArray[best_i] );
511     }
512     return 1;
513 }
514 
515 /**Function*************************************************************
516 
517   Synopsis    [Performs generalization using a different idea.]
518 
519   Description []
520 
521   SideEffects []
522 
523   SeeAlso     []
524 
525 ***********************************************************************/
Pdr_ManGeneralize2(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,Pdr_Set_t ** ppCubeMin)526 int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
527 {
528 #if 0
529     int fUseMinAss = 0;
530     sat_solver * pSat = Pdr_ManFetchSolver( p, k );
531     int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
532     Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
533     int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
534     // create free variables
535     int i, iUseVar, iAndVar;
536     iAndVar = Pdr_ManFreeVar(p, k);
537     for ( i = 1; i < nLits; i++ )
538         Pdr_ManFreeVar(p, k);
539     iUseVar = Pdr_ManFreeVar(p, k);
540     for ( i = 1; i < nLits; i++ )
541         Pdr_ManFreeVar(p, k);
542     assert( iUseVar == iAndVar + nLits );
543     // if there is only one positive literal, put it in front and always assume
544     if ( fUseMinAss )
545     {
546         for ( i = 0; i < pCube->nLits && Count < 2; i++ )
547             Count += !Abc_LitIsCompl(pCube->Lits[i]);
548         if ( Count == 1 )
549         {
550             for ( i = 0; i < pCube->nLits; i++ )
551                 if ( !Abc_LitIsCompl(pCube->Lits[i]) )
552                     break;
553             assert( i < pCube->nLits );
554             iLit = pCube->Lits[i];
555             for ( ; i > 0; i-- )
556                 pCube->Lits[i] = pCube->Lits[i-1];
557             pCube->Lits[0] = iLit;
558         }
559     }
560     // add clauses for the additional AND-gates
561     Vec_IntForEachEntry( vLits1, iLit, i )
562     {
563         sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
564         Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
565     }
566     // add clauses for the additional OR-gate
567     RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
568     assert( RetValue == 1 );
569     // add implications
570     vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
571     assert( Vec_IntSize(vLits1) == nLits );
572     Vec_IntForEachEntry( vLits1, iLit, i )
573     {
574         Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
575         Lits[1] = iLit;
576         RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
577         assert( RetValue == 1 );
578         Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
579     }
580     sat_solver_compress( pSat );
581     // perform minimization
582     if ( fUseMinAss )
583     {
584         if ( Count == 1 ) // always assume the only positive literal
585         {
586             if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
587                 nLits = 1;
588             else
589                 nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
590             sat_solver_pop(pSat); // unassume the first literal
591         }
592         else
593             nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
594         Vec_IntShrink( vLits1, nLits );
595     }
596     else
597     {
598         // try removing one literal at a time in the old-fashioned way
599         int k, Entry;
600         Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
601         for ( i = nLits - 1; i >= 0; i-- )
602         {
603             // if we are about to remove a positive lit, make sure at least one positive lit remains
604             if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
605             {
606                 Vec_IntForEachEntry( vLits1, iLit, k )
607                     if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
608                         break;
609                 if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
610                     continue;
611             }
612             // load remaining literals
613             Vec_IntClear( vTemp );
614             Vec_IntForEachEntry( vLits1, Entry, k )
615                 if ( Entry != -1 && k != i )
616                     Vec_IntPush( vTemp, Entry );
617                 else if ( Entry != -1 ) // assume opposite literal
618                     Vec_IntPush( vTemp, Abc_LitNot(Entry) );
619             // solve with assumptions
620             RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
621             // commit the literal
622             if ( RetValue == l_False )
623             {
624                 int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
625                 int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
626                 assert( RetValue );
627             }
628             // update the clause
629             if ( RetValue == l_False )
630                 Vec_IntWriteEntry( vLits1, i, -1 );
631         }
632         Vec_IntFree( vTemp );
633         // compact
634         k = 0;
635         Vec_IntForEachEntry( vLits1, Entry, i )
636             if ( Entry != -1 )
637                 Vec_IntWriteEntry( vLits1, k++, Entry );
638         Vec_IntShrink( vLits1, k );
639     }
640     // remap auxiliary literals into original literals
641     Vec_IntForEachEntry( vLits1, iLit, i )
642         Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
643     // make sure the cube has at least one positive literal
644     if ( fUseMinAss )
645     {
646         Vec_IntForEachEntry( vLits1, iLit, i )
647             if ( !Abc_LitIsCompl(iLit) )
648                 break;
649         if ( i == Vec_IntSize(vLits1) ) // has no positive literals
650         {
651             // find positive lit in the cube
652             for ( i = 0; i < pCube->nLits; i++ )
653                 if ( !Abc_LitIsCompl(pCube->Lits[i]) )
654                     break;
655             assert( i < pCube->nLits );
656             Vec_IntPush( vLits1, pCube->Lits[i] );
657 //            printf( "-" );
658         }
659 //        else
660 //            printf( "+" );
661     }
662     // create a subset cube
663     *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
664     assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
665     Order = 0;
666 #endif
667     return 0;
668 }
669 
670 /**Function*************************************************************
671 
672   Synopsis    [Returns 1 if the state could be blocked.]
673 
674   Description []
675 
676   SideEffects []
677 
678   SeeAlso     []
679 
680 ***********************************************************************/
Pdr_ManGeneralize(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,Pdr_Set_t ** ppPred,Pdr_Set_t ** ppCubeMin)681 int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
682 {
683     Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL;
684     int i, j, Lit, RetValue;
685     abctime clk = Abc_Clock();
686     int * pOrder;
687     int added = 0;
688     Hash_Int_t * keep = NULL;
689     // if there is no induction, return
690     *ppCubeMin = NULL;
691     if ( p->pPars->fFlopOrder )
692         Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
693     RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
694     if ( p->pPars->fFlopOrder )
695         Vec_IntSelectSort( pCube->Lits, pCube->nLits );
696     if ( RetValue == -1 )
697         return -1;
698     if ( RetValue == 0 )
699     {
700         p->tGeneral += clock() - clk;
701         return 0;
702     }
703 
704     // reduce clause using assumptions
705 //    pCubeMin = Pdr_SetDup( pCube );
706     pCubeMin = Pdr_ManReduceClause( p, k, pCube );
707     if ( pCubeMin == NULL )
708         pCubeMin = Pdr_SetDup( pCube );
709 
710     // perform simplified generalization
711     if ( p->pPars->fSimpleGeneral )
712     {
713         assert( pCubeMin->nLits > 0 );
714         if ( pCubeMin->nLits > 1 )
715         {
716             RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
717             Pdr_SetDeref( pCubeMin );
718             assert( ppCubeMin != NULL );
719             pCubeMin = *ppCubeMin;
720         }
721         *ppCubeMin = pCubeMin;
722         if ( p->pPars->fVeryVerbose )
723         {
724             printf("Cube:\n");
725             for ( i = 0; i < pCubeMin->nLits; i++)
726                 printf ("%d ", pCubeMin->Lits[i]);
727             printf("\n");
728         }
729         p->tGeneral += Abc_Clock() - clk;
730         return 1;
731     }
732 
733     keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
734 
735     // perform generalization
736     if ( !p->pPars->fSkipGeneral )
737     {
738         // assume the unminimized cube
739         if ( p->pPars->fSimpleGeneral )
740         {
741             sat_solver *  pSat = Pdr_ManFetchSolver( p, k );
742             Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
743             int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
744             assert( RetValue1 == 1 );
745             sat_solver_compress( pSat );
746         }
747 
748         // sort literals by their occurences
749         pOrder = Pdr_ManSortByPriority( p, pCubeMin );
750         // try removing literals
751         for ( j = 0; j < pCubeMin->nLits; j++ )
752         {
753             // use ordering
754     //        i = j;
755             i = pOrder[j];
756 
757             assert( pCubeMin->Lits[i] != -1 );
758             if ( keep && Hash_IntExists( keep, pCubeMin->Lits[i] ) )
759             {
760                 //printf("Undroppable\n");
761                 continue;
762             }
763 
764             // check init state
765             if ( Pdr_SetIsInit(pCubeMin, i) )
766                 continue;
767 
768             // try removing this literal
769             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
770             if ( p->pPars->fSkipDown )
771                 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
772             else
773                 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
774             if ( RetValue == -1 )
775             {
776                 Pdr_SetDeref( pCubeMin );
777                 return -1;
778             }
779             pCubeMin->Lits[i] = Lit;
780             if ( RetValue == 0 )
781             {
782                 if ( p->pPars->fSkipDown )
783                     continue;
784                 pCubeCpy = Pdr_SetCreateFrom( pCubeMin, i );
785                 RetValue = ZPdr_ManDown( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
786                 if ( p->pPars->fCtgs )
787                     //CTG handling code messes up with the internal order array
788                     pOrder = Pdr_ManSortByPriority( p, pCubeMin );
789                 if ( RetValue == -1 )
790                 {
791                     Pdr_SetDeref( pCubeMin );
792                     Pdr_SetDeref( pCubeCpy );
793                     Pdr_SetDeref( pPred );
794                     return -1;
795                 }
796                 if ( RetValue == 0 )
797                 {
798                     if ( keep )
799                         Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
800                     if ( pCubeCpy )
801                         Pdr_SetDeref( pCubeCpy );
802                     continue;
803                 }
804                 //Inductive subclause
805                 added = 0;
806                 Pdr_SetDeref( pCubeMin );
807                 pCubeMin = pCubeCpy;
808                 assert( pCubeMin->nLits > 0 );
809                 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
810                 j = -1;
811                 continue;
812             }
813             added = 0;
814 
815             // success - update the cube
816             pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
817             Pdr_SetDeref( pCubeTmp );
818             assert( pCubeMin->nLits > 0 );
819 
820             // assume the minimized cube
821             if ( p->pPars->fSimpleGeneral )
822             {
823                 sat_solver *  pSat = Pdr_ManFetchSolver( p, k );
824                 Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
825                 int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
826                 assert( RetValue1 == 1 );
827                 sat_solver_compress( pSat );
828             }
829 
830             // get the ordering by decreasing priority
831             pOrder = Pdr_ManSortByPriority( p, pCubeMin );
832             j--;
833         }
834 
835         if ( p->pPars->fTwoRounds )
836         for ( j = 0; j < pCubeMin->nLits; j++ )
837         {
838             // use ordering
839     //        i = j;
840             i = pOrder[j];
841 
842             // check init state
843             assert( pCubeMin->Lits[i] != -1 );
844             if ( Pdr_SetIsInit(pCubeMin, i) )
845                 continue;
846             // try removing this literal
847             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
848             RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 );
849             if ( RetValue == -1 )
850             {
851                 Pdr_SetDeref( pCubeMin );
852                 return -1;
853             }
854             pCubeMin->Lits[i] = Lit;
855             if ( RetValue == 0 )
856                 continue;
857 
858             // success - update the cube
859             pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
860             Pdr_SetDeref( pCubeTmp );
861             assert( pCubeMin->nLits > 0 );
862 
863             // get the ordering by decreasing priority
864             pOrder = Pdr_ManSortByPriority( p, pCubeMin );
865             j--;
866         }
867     }
868 
869     assert( ppCubeMin != NULL );
870     if ( p->pPars->fVeryVerbose )
871     {
872         printf("Cube:\n");
873         for ( i = 0; i < pCubeMin->nLits; i++)
874             printf ("%d ", pCubeMin->Lits[i]);
875         printf("\n");
876     }
877     *ppCubeMin = pCubeMin;
878     p->tGeneral += Abc_Clock() - clk;
879     if ( keep ) Hash_IntFree( keep );
880     return 1;
881 }
882 
883 /**Function*************************************************************
884 
885   Synopsis    [Returns 1 if the state could be blocked.]
886 
887   Description []
888 
889   SideEffects []
890 
891   SeeAlso     []
892 
893 ***********************************************************************/
Pdr_ManBlockCube(Pdr_Man_t * p,Pdr_Set_t * pCube)894 int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
895 {
896     Pdr_Obl_t * pThis;
897     Pdr_Set_t * pPred, * pCubeMin;
898     int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
899     int kMax = Vec_PtrSize(p->vSolvers)-1;
900     abctime clk;
901     p->nBlocks++;
902     // create first proof obligation
903 //    assert( p->pQueue == NULL );
904     pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
905     Pdr_QueuePush( p, pThis );
906     // try to solve it recursively
907     while ( !Pdr_QueueIsEmpty(p) )
908     {
909         Counter++;
910         pThis = Pdr_QueueHead( p );
911         if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
912             return 0; // SAT
913         if ( pThis->iFrame > kMax ) // finished this level
914             return 1;
915         if ( p->nQueLim && p->nQueCur >= p->nQueLim )
916         {
917             p->nQueLim = p->nQueLim * 3 / 2;
918             Pdr_QueueStop( p );
919             return 1; // restart
920         }
921         pThis = Pdr_QueuePop( p );
922         assert( pThis->iFrame > 0 );
923         assert( !Pdr_SetIsInit(pThis->pState, -1) );
924         p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame );
925         clk = Abc_Clock();
926         if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
927         {
928             p->tContain += Abc_Clock() - clk;
929             Pdr_OblDeref( pThis );
930             continue;
931         }
932         p->tContain += Abc_Clock() - clk;
933 
934         // check if the cube is already contained
935         RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
936         if ( RetValue == -1 ) // resource limit is reached
937         {
938             Pdr_OblDeref( pThis );
939             return -1;
940         }
941         if ( RetValue ) // cube is blocked by clauses in this frame
942         {
943             Pdr_OblDeref( pThis );
944             continue;
945         }
946 
947         // check if the cube holds with relative induction
948         pCubeMin = NULL;
949         RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
950         if ( RetValue == -1 ) // resource limit is reached
951         {
952             Pdr_OblDeref( pThis );
953             return -1;
954         }
955         if ( RetValue ) // cube is blocked inductively in this frame
956         {
957             assert( pCubeMin != NULL );
958             // k is the last frame where pCubeMin holds
959             k = pThis->iFrame;
960             // check other frames
961             assert( pPred == NULL );
962             for ( k = pThis->iFrame; k < kMax; k++ )
963             {
964                 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
965                 if ( RetValue == -1 )
966                 {
967                     Pdr_OblDeref( pThis );
968                     return -1;
969                 }
970                 if ( !RetValue )
971                     break;
972             }
973             // add new clause
974             if ( p->pPars->fVeryVerbose )
975             {
976                 Abc_Print( 1, "Adding cube " );
977                 Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
978                 Abc_Print( 1, " to frame %d.\n", k );
979             }
980             // set priority flops
981             for ( i = 0; i < pCubeMin->nLits; i++ )
982             {
983                 assert( pCubeMin->Lits[i] >= 0 );
984                 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
985                 if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
986                     p->nAbsFlops++;
987                 Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
988             }
989             Vec_VecPush( p->vClauses, k, pCubeMin );   // consume ref
990             p->nCubes++;
991             // add clause
992             for ( i = 1; i <= k; i++ )
993                 Pdr_ManSolverAddClause( p, i, pCubeMin );
994             // schedule proof obligation
995             if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
996             {
997                 pThis->iFrame = k+1;
998                 pThis->prio   = Prio--;
999                 Pdr_QueuePush( p, pThis );
1000             }
1001             else
1002             {
1003                 Pdr_OblDeref( pThis );
1004             }
1005         }
1006         else
1007         {
1008             assert( pCubeMin == NULL );
1009             assert( pPred != NULL );
1010             pThis->prio = Prio--;
1011             Pdr_QueuePush( p, pThis );
1012             pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
1013             Pdr_QueuePush( p, pThis );
1014         }
1015 
1016         // check termination
1017         if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
1018             return -1;
1019         if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1020             return -1;
1021         if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1022             return -1;
1023         if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1024             return -1;
1025     }
1026     return 1;
1027 }
1028 
1029 /**Function*************************************************************
1030 
1031   Synopsis    []
1032 
1033   Description []
1034 
1035   SideEffects []
1036 
1037   SeeAlso     []
1038 
1039 ***********************************************************************/
Pdr_ManSolveInt(Pdr_Man_t * p)1040 int Pdr_ManSolveInt( Pdr_Man_t * p )
1041 {
1042     int fPrintClauses = 0;
1043     Pdr_Set_t * pCube = NULL;
1044     Aig_Obj_t * pObj;
1045     Abc_Cex_t * pCexNew;
1046     int iFrame, RetValue = -1;
1047     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
1048     abctime clkStart = Abc_Clock(), clkOne = 0;
1049     p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1050     assert( Vec_PtrSize(p->vSolvers) == 0 );
1051     // in the multi-output mode, mark trivial POs (those fed by const0) as solved
1052     if ( p->pPars->fSolveAll )
1053         Saig_ManForEachPo( p->pAig, pObj, iFrame )
1054             if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
1055             {
1056                 Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
1057                 p->pPars->nProveOuts++;
1058                 if ( p->pPars->fUseBridge )
1059                     Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
1060             }
1061     // create the first timeframe
1062     p->pPars->timeLastSolved = Abc_Clock();
1063     Pdr_ManCreateSolver( p, (iFrame = 0) );
1064     while ( 1 )
1065     {
1066         int fRefined = 0;
1067         if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
1068         {
1069 //            int i, Prio;
1070             assert( p->vAbsFlops == NULL );
1071             p->vAbsFlops  = Vec_IntStart( Saig_ManRegNum(p->pAig) );
1072             p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
1073             p->vMapPpi2Ff = Vec_IntAlloc( 100 );
1074 //            Vec_IntForEachEntry( p->vPrio, Prio, i )
1075 //                if ( Prio >> p->nPrioShift  )
1076 //                    Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
1077         }
1078         //if ( p->pPars->fUseAbs && p->vAbsFlops )
1079         //    printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
1080         p->nFrames = iFrame;
1081         assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
1082         p->iUseFrame = Abc_MaxInt(iFrame, 1);
1083         Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
1084         {
1085             // skip disproved outputs
1086             if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
1087                 continue;
1088             // skip output whose time has run out
1089             if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
1090                 continue;
1091             // check if the output is trivially solved
1092             if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
1093                 continue;
1094             // check if the output is trivially solved
1095             if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
1096             {
1097                 if ( !p->pPars->fSolveAll )
1098                 {
1099                     pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
1100                     p->pAig->pSeqModel = pCexNew;
1101                     return 0; // SAT
1102                 }
1103                 pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
1104                 p->pPars->nFailOuts++;
1105                 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
1106                 if ( !p->pPars->fNotVerbose )
1107                 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
1108                     nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
1109                 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
1110                 if ( p->pPars->fUseBridge )
1111                     Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1112                 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
1113                 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
1114                 {
1115                     if ( p->pPars->fVerbose )
1116                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1117                     if ( !p->pPars->fSilent )
1118                         Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
1119                     p->pPars->iFrame = iFrame;
1120                     return -1;
1121                 }
1122                 if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
1123                     return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
1124                 p->pPars->timeLastSolved = Abc_Clock();
1125                 continue;
1126             }
1127             // try to solve this output
1128             if ( p->pTime4Outs )
1129             {
1130                 assert( p->pTime4Outs[p->iOutCur] > 0 );
1131                 clkOne = Abc_Clock();
1132                 p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
1133             }
1134             while ( 1 )
1135             {
1136                 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1137                 {
1138                     if ( p->pPars->fVerbose )
1139                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1140                     if ( !p->pPars->fSilent )
1141                         Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
1142                     p->pPars->iFrame = iFrame;
1143                     return -1;
1144                 }
1145                 RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
1146                 if ( RetValue == 1 )
1147                     break;
1148                 if ( RetValue == -1 )
1149                 {
1150                     if ( p->pPars->fVerbose )
1151                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1152                     if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1153                         Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
1154                     else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1155                         Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
1156                     else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1157                     {
1158                         Pdr_QueueClean( p );
1159                         pCube = NULL;
1160                         break; // keep solving
1161                     }
1162                     else if ( p->pPars->nConfLimit )
1163                         Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
1164                     else if ( p->pPars->fVerbose )
1165                         Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
1166                     p->pPars->iFrame = iFrame;
1167                     return -1;
1168                 }
1169                 if ( RetValue == 0 )
1170                 {
1171                     RetValue = Pdr_ManBlockCube( p, pCube );
1172                     if ( RetValue == -1 )
1173                     {
1174                         if ( p->pPars->fVerbose )
1175                             Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1176                         if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1177                             Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
1178                         else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1179                             Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
1180                         else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1181                         {
1182                             Pdr_QueueClean( p );
1183                             pCube = NULL;
1184                             break; // keep solving
1185                         }
1186                         else if ( p->pPars->nConfLimit )
1187                             Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
1188                         else if ( p->pPars->fVerbose )
1189                             Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
1190                         p->pPars->iFrame = iFrame;
1191                         return -1;
1192                     }
1193                     if ( RetValue == 0 )
1194                     {
1195                         if ( fPrintClauses )
1196                         {
1197                             Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1198                             Pdr_ManPrintClauses( p, 0 );
1199                         }
1200                         if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
1201                             Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
1202                         p->pPars->iFrame = iFrame;
1203                         if ( !p->pPars->fSolveAll )
1204                         {
1205                             abctime clk = Abc_Clock();
1206                             Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
1207                             p->tAbs += Abc_Clock() - clk;
1208                             if ( pCex == NULL )
1209                             {
1210                                 assert( p->pPars->fUseAbs );
1211                                 Pdr_QueueClean( p );
1212                                 pCube = NULL;
1213                                 fRefined = 1;
1214                                 break; // keep solving
1215                             }
1216                             p->pAig->pSeqModel = pCex;
1217                             return 0; // SAT
1218                         }
1219                         p->pPars->nFailOuts++;
1220                         pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
1221                         if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
1222                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
1223                         if ( p->pPars->fUseBridge )
1224                             Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1225                         Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
1226                         if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
1227                         {
1228                             if ( p->pPars->fVerbose )
1229                                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1230                             if ( !p->pPars->fSilent )
1231                                 Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
1232                             p->pPars->iFrame = iFrame;
1233                             return -1;
1234                         }
1235                         if ( !p->pPars->fNotVerbose )
1236                             Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
1237                                 nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
1238                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
1239                             return 0; // all SAT
1240                         Pdr_QueueClean( p );
1241                         pCube = NULL;
1242                         break; // keep solving
1243                     }
1244                     if ( p->pPars->fVerbose )
1245                         Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
1246                 }
1247             }
1248             if ( fRefined )
1249                 break;
1250             if ( p->pTime4Outs )
1251             {
1252                 abctime timeSince = Abc_Clock() - clkOne;
1253                 assert( p->pTime4Outs[p->iOutCur] > 0 );
1254                 p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
1255                 if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
1256                 {
1257                     p->pPars->nDropOuts++;
1258                     if ( p->pPars->vOutMap )
1259                         Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
1260                     if ( !p->pPars->fNotVerbose )
1261                         Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
1262                 }
1263                 p->timeToStopOne = 0;
1264             }
1265         }
1266         if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
1267         {
1268             int i, Used;
1269             Vec_IntForEachEntry( p->vAbsFlops, Used, i )
1270                 if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
1271                     Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
1272         }
1273         if ( p->pPars->fVerbose )
1274             Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
1275         if ( fRefined )
1276             continue;
1277         //if ( p->pPars->fUseAbs && p->vAbsFlops )
1278         //    printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
1279         // open a new timeframe
1280         p->nQueLim = p->pPars->nRestLimit;
1281         assert( pCube == NULL );
1282         Pdr_ManSetPropertyOutput( p, iFrame );
1283         Pdr_ManCreateSolver( p, ++iFrame );
1284         if ( fPrintClauses )
1285         {
1286             Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1287             Pdr_ManPrintClauses( p, 0 );
1288         }
1289         // push clauses into this timeframe
1290         RetValue = Pdr_ManPushClauses( p );
1291         if ( RetValue == -1 )
1292         {
1293             if ( p->pPars->fVerbose )
1294                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1295             if ( !p->pPars->fSilent )
1296             {
1297                 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1298                     Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
1299                 else
1300                     Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
1301             }
1302             p->pPars->iFrame = iFrame;
1303             return -1;
1304         }
1305         if ( RetValue )
1306         {
1307             if ( p->pPars->fVerbose )
1308                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1309             if ( !p->pPars->fSilent )
1310                 Pdr_ManReportInvariant( p );
1311             if ( !p->pPars->fSilent )
1312                 Pdr_ManVerifyInvariant( p );
1313             p->pPars->iFrame = iFrame;
1314             // count the number of UNSAT outputs
1315             p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
1316             // convert previously 'unknown' into 'unsat'
1317             if ( p->pPars->vOutMap )
1318                 for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
1319                     if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
1320                     {
1321                         Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
1322                         if ( p->pPars->fUseBridge )
1323                             Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
1324                     }
1325             if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
1326                 return 1; // UNSAT
1327             if ( p->pPars->nFailOuts > 0 )
1328                 return 0; // SAT
1329             return -1;
1330         }
1331         if ( p->pPars->fVerbose )
1332             Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
1333 
1334         // check termination
1335         if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
1336         {
1337             p->pPars->iFrame = iFrame;
1338             return -1;
1339         }
1340         if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1341         {
1342             if ( fPrintClauses )
1343             {
1344                 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1345                 Pdr_ManPrintClauses( p, 0 );
1346             }
1347             if ( p->pPars->fVerbose )
1348                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1349             if ( !p->pPars->fSilent )
1350                 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
1351             p->pPars->iFrame = iFrame;
1352             return -1;
1353         }
1354         if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1355         {
1356             if ( fPrintClauses )
1357             {
1358                 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1359                 Pdr_ManPrintClauses( p, 0 );
1360             }
1361             if ( p->pPars->fVerbose )
1362                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1363             if ( !p->pPars->fSilent )
1364                 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
1365             p->pPars->iFrame = iFrame;
1366             return -1;
1367         }
1368         if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
1369         {
1370             if ( p->pPars->fVerbose )
1371                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1372             if ( !p->pPars->fSilent )
1373                 Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
1374             p->pPars->iFrame = iFrame;
1375             return -1;
1376         }
1377     }
1378     assert( 0 );
1379     return -1;
1380 }
1381 
1382 /**Function*************************************************************
1383 
1384   Synopsis    []
1385 
1386   Description []
1387 
1388   SideEffects []
1389 
1390   SeeAlso     []
1391 
1392 ***********************************************************************/
Pdr_ManSolve(Aig_Man_t * pAig,Pdr_Par_t * pPars)1393 int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
1394 {
1395     Pdr_Man_t * p;
1396     int k, RetValue;
1397     abctime clk = Abc_Clock();
1398     if ( pPars->nTimeOutOne && !pPars->fSolveAll )
1399         pPars->nTimeOutOne = 0;
1400     if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
1401         pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
1402     if ( pPars->fVerbose )
1403     {
1404 //    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
1405         Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
1406             pPars->nRecycle,
1407             pPars->nFrameMax,
1408             pPars->nRestLimit,
1409             pPars->nTimeOut );
1410         Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
1411             pPars->fMonoCnf ?     "yes" : "no",
1412             pPars->fSkipGeneral ? "yes" : "no",
1413             pPars->fSolveAll ?    "yes" : "no" );
1414     }
1415     ABC_FREE( pAig->pSeqModel );
1416     p = Pdr_ManStart( pAig, pPars, NULL );
1417     RetValue = Pdr_ManSolveInt( p );
1418     if ( RetValue == 0 )
1419         assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
1420     if ( p->vCexes )
1421     {
1422         assert( p->pAig->vSeqModelVec == NULL );
1423         p->pAig->vSeqModelVec = p->vCexes;
1424         p->vCexes = NULL;
1425     }
1426     if ( p->pPars->fDumpInv )
1427     {
1428         char * pFileName = pPars->pInvFileName ? pPars->pInvFileName : Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
1429         Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
1430         Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
1431         printf( "Dumped inductive invariant in file \"%s\".\n", pFileName );
1432     }
1433     else if ( RetValue == 1 )
1434         Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
1435     p->tTotal += Abc_Clock() - clk;
1436     Pdr_ManStop( p );
1437     pPars->iFrame--;
1438     // convert all -2 (unknown) entries into -1 (undec)
1439     if ( pPars->vOutMap )
1440         for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
1441             if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
1442                 Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
1443     if ( pPars->fUseBridge )
1444         Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
1445     return RetValue;
1446 }
1447 
1448 ////////////////////////////////////////////////////////////////////////
1449 ///                       END OF FILE                                ///
1450 ////////////////////////////////////////////////////////////////////////
1451 
1452 
1453 ABC_NAMESPACE_IMPL_END
1454