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