ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
pdrCore.c
Go to the documentation of this file.
1
20
21#include "pdrInt.h"
22#include "base/main/main.h"
23#include "misc/hash/hash.h"
24
25ABC_NAMESPACE_IMPL_START
26
27
31
32extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
33extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
34
38
50void 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 pPars->fBlocking = 0; // clause pushing with blocking
84}
85
97Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
98{
99 Pdr_Set_t * pCubeMin;
100 Vec_Int_t * vLits;
101 int i, Entry, nCoreLits, * pCoreLits;
102 // get relevant SAT literals
103 nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
104 // translate them into register literals and remove auxiliary
105 vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
106 // skip if there is no improvement
107 if ( Vec_IntSize(vLits) == pCube->nLits )
108 return NULL;
109 assert( Vec_IntSize(vLits) < pCube->nLits );
110 // if the cube overlaps with init, add any literal
111 Vec_IntForEachEntry( vLits, Entry, i )
112 if ( Abc_LitIsCompl(Entry) == 0 ) // positive literal
113 break;
114 if ( i == Vec_IntSize(vLits) ) // only negative literals
115 {
116 // add the first positive literal
117 for ( i = 0; i < pCube->nLits; i++ )
118 if ( Abc_LitIsCompl(pCube->Lits[i]) == 0 ) // positive literal
119 {
120 Vec_IntPush( vLits, pCube->Lits[i] );
121 break;
122 }
123 assert( i < pCube->nLits );
124 }
125 // generate a starting cube
126 pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
127 assert( !Pdr_SetIsInit(pCubeMin, -1) );
128/*
129 // make sure the cube works
130 {
131 int RetValue;
132 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
133 assert( RetValue );
134 }
135*/
136 return pCubeMin;
137}
138
150int Pdr_ManPushClauses( Pdr_Man_t * p )
151{
152 Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
153 Vec_Ptr_t * vArrayK, * vArrayK1;
154 int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
155 int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
156 int Counter = 0;
157 abctime clk = Abc_Clock();
158 assert( p->iUseFrame > 0 );
159 Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
160 {
161 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
162 vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
163 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
164 {
165 Counter++;
166
167 // remove cubes in the same frame that are contained by pCubeK
168 Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
169 {
170 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
171 continue;
172 Pdr_SetDeref( pTemp );
173 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
174 Vec_PtrPop(vArrayK);
175 m--;
176 }
177
178 // check if the clause can be moved to the next frame
179 RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
180 if ( RetValue2 == -1 )
181 return -1;
182 if ( !RetValue2 )
183 continue;
184
185 {
186 Pdr_Set_t * pCubeMin;
187 pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
188 if ( pCubeMin != NULL )
189 {
190// Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
191 Pdr_SetDeref( pCubeK );
192 pCubeK = pCubeMin;
193 }
194 }
195
196 // if it can be moved, add it to the next frame
197 Pdr_ManSolverAddClause( p, k+1, pCubeK );
198 // check if the clause subsumes others
199 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
200 {
201 if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
202 continue;
203 Pdr_SetDeref( pCubeK1 );
204 Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
205 Vec_PtrPop(vArrayK1);
206 i--;
207 }
208 // add the last clause
209 Vec_PtrPush( vArrayK1, pCubeK );
210 Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
211 Vec_PtrPop(vArrayK);
212 j--;
213 }
214 if ( Vec_PtrSize(vArrayK) == 0 )
215 RetValue = 1;
216 }
217
218 // clean up the last one
219 vArrayK = Vec_VecEntry( p->vClauses, kMax );
220 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
221 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
222 {
223 // remove cubes in the same frame that are contained by pCubeK
224 Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
225 {
226 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
227 continue;
228/*
229 Abc_Print( 1, "===\n" );
230 Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
231 Abc_Print( 1, "\n" );
232 Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
233 Abc_Print( 1, "\n" );
234*/
235 Pdr_SetDeref( pTemp );
236 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
237 Vec_PtrPop(vArrayK);
238 m--;
239 }
240 }
241 p->tPush += Abc_Clock() - clk;
242 return RetValue;
243}
244
245int ZPdr_ManDown_Exhaustive( Pdr_Man_t *, int, Pdr_Set_t **, Pdr_Set_t *, Hash_Int_t *, Pdr_Set_t *, int * );
246int Pdr_ManPushAndBlockClauses( Pdr_Man_t * p )
247{
248 Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
249 Vec_Ptr_t * vArrayK, * vArrayK1;
250 int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
251 int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
252 int Counter = 0;
253
254 int blockCount;
255 int blockAttemp;
256 int added;
257 int l;
258 int RetValue3;
259 Pdr_Set_t *pPred = NULL;
260 Pdr_Set_t *pCubeCpy = NULL;
261
262 abctime clk = Abc_Clock();
263 assert( p->iUseFrame > 0 );
264 Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
265 {
266 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
267 vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
268 blockCount = 0;
269 blockAttemp = 0;
270 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
271 {
272 Counter++;
273
274 // remove cubes in the same frame that are contained by pCubeK
275 Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
276 {
277 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
278 continue;
279 Pdr_SetDeref( pTemp );
280 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
281 Vec_PtrPop(vArrayK);
282 m--;
283 }
284
285 // check if the clause can be moved to the next frame
286 added = 1;
287 RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, &pPred, 0, 0, 1 ); // ************************
288 if ( RetValue2 == -1 )
289 return -1;
290 if ( !RetValue2 ) // try to block before pushing
291 {
292 if ( blockCount < blockAttemp )
293 continue;
294 else
295 {
296 blockAttemp++;
297 pCubeCpy = Pdr_SetDup(pCubeK);
298 RetValue3 = ZPdr_ManDown_Exhaustive( p, k, &pCubeCpy, pPred, Hash_IntAlloc( 1 ), NULL, &added );
299 if ( RetValue3 == -1 )
300 {
301 Pdr_SetDeref( pCubeCpy );
302 return -1;
303 }
304 if ( RetValue3 == 0 )
305 {
306 Pdr_SetDeref( pCubeCpy );
307 continue;
308 }
309 Pdr_SetDeref( pCubeK );
310 pCubeK = pCubeCpy;
311
312 for ( l = 1; l <= k; l++ )
313 Pdr_ManSolverAddClause( p, l, pCubeK );
314 blockCount++;
315 }
316 }
317 else // directly push
318 {
319 Pdr_Set_t * pCubeMin;
320 pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
321 if ( pCubeMin != NULL )
322 {
323// Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
324 Pdr_SetDeref( pCubeK );
325 pCubeK = pCubeMin;
326 }
327 }
328
329 // if it can be moved, add it to the next frame
330 Pdr_ManSolverAddClause( p, k+1, pCubeK );
331 // check if the clause subsumes others
332 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
333 {
334 if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
335 continue;
336 Pdr_SetDeref( pCubeK1 );
337 Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
338 Vec_PtrPop(vArrayK1);
339 i--;
340 }
341 // add the last clause
342 Vec_PtrPush( vArrayK1, pCubeK );
343 Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
344 Vec_PtrPop(vArrayK);
345 j--;
346 }
347 // printf("%d, %d\n", blockCount, blockAtemp);
348 if ( Vec_PtrSize(vArrayK) == 0 )
349 RetValue = 1;
350 }
351
352 // clean up the last one
353 vArrayK = Vec_VecEntry( p->vClauses, kMax );
354 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
355 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
356 {
357 // remove cubes in the same frame that are contained by pCubeK
358 Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
359 {
360 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
361 continue;
362/*
363 Abc_Print( 1, "===\n" );
364 Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
365 Abc_Print( 1, "\n" );
366 Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
367 Abc_Print( 1, "\n" );
368*/
369 Pdr_SetDeref( pTemp );
370 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
371 Vec_PtrPop(vArrayK);
372 m--;
373 }
374 }
375 p->tPush += Abc_Clock() - clk;
376 return RetValue;
377}
378
390int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
391{
392 Pdr_Set_t * pThis;
393 Vec_Ptr_t * vArrayK;
394 int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
395 Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
396 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
397 if ( Pdr_SetContains( pSet, pThis ) )
398 return 1;
399 return 0;
400}
401
402
414int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
415{
416 int * pPrios = Vec_IntArray(p->vPrio);
417 int * pArray = p->pOrder;
418 int temp, i, j, best_i, nSize = pCube->nLits;
419 // initialize variable order
420 for ( i = 0; i < nSize; i++ )
421 pArray[i] = i;
422 for ( i = 0; i < nSize-1; i++ )
423 {
424 best_i = i;
425 for ( j = i+1; j < nSize; j++ )
426// if ( pArray[j] < pArray[best_i] )
427 if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
428 best_i = j;
429 temp = pArray[i];
430 pArray[i] = pArray[best_i];
431 pArray[best_i] = temp;
432 }
433/*
434 for ( i = 0; i < pCube->nLits; i++ )
435 Abc_Print( 1, "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
436 Abc_Print( 1, "\n" );
437*/
438 return pArray;
439}
440
441
453int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
454{
455 int * pOrder;
456 int i, j, Lit, RetValue;
457 Pdr_Set_t * pCubeTmp;
458 // perform generalization
459 if ( p->pPars->fSkipGeneral )
460 return 0;
461
462 // sort literals by their occurences
463 pOrder = Pdr_ManSortByPriority( p, *ppCube );
464 // try removing literals
465 for ( j = 0; j < (*ppCube)->nLits; j++ )
466 {
467 // use ordering
468 // i = j;
469 i = pOrder[j];
470
471 assert( (*ppCube)->Lits[i] != -1 );
472 // check init state
473 if ( Pdr_SetIsInit(*ppCube, i) )
474 continue;
475 // try removing this literal
476 Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1;
477 RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0, 1 );
478 if ( RetValue == -1 )
479 return -1;
480 (*ppCube)->Lits[i] = Lit;
481 if ( RetValue == 0 )
482 continue;
483
484 // success - update the cube
485 *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i );
486 Pdr_SetDeref( pCubeTmp );
487 assert( (*ppCube)->nLits > 0 );
488
489 // get the ordering by decreasing priority
490 pOrder = Pdr_ManSortByPriority( p, *ppCube );
491 j--;
492 }
493 return 0;
494}
495
496
497
509int 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 )
510{
511 int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
512 int kMax = Vec_PtrSize(p->vSolvers)-1;
513 Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
514 while ( RetValue == 0 )
515 {
516 ctgAttempts = 0;
517 while ( p->pPars->fCtgs && RetValue == 0 && k > 1 && ctgAttempts < 3 )
518 {
519 pCtg = Pdr_SetDup( pPred );
520 //Check CTG for inductiveness
521 if ( Pdr_SetIsInit( pCtg, -1 ) )
522 {
523 Pdr_SetDeref( pCtg );
524 break;
525 }
526 if (*added == 0)
527 {
528 for ( i = 1; i <= k; i++ )
529 Pdr_ManSolverAddClause( p, i, pIndCube);
530 *added = 1;
531 }
532 ctgAttempts++;
533 CtgRetValue = Pdr_ManCheckCube( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0, 1 );
534 if ( CtgRetValue != 1 )
535 {
536 Pdr_SetDeref( pCtg );
537 break;
538 }
539 pCubeMin = Pdr_ManReduceClause( p, k-1, pCtg );
540 if ( pCubeMin == NULL )
541 pCubeMin = Pdr_SetDup ( pCtg );
542
543 for ( l = k; l < kMax; l++ )
544 if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0, 1 ) )
545 break;
546 micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
547 assert ( micResult != -1 );
548
549 // add new clause
550 if ( p->pPars->fVeryVerbose )
551 {
552 Abc_Print( 1, "Adding cube " );
553 Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
554 Abc_Print( 1, " to frame %d.\n", l );
555 }
556 // set priority flops
557 for ( i = 0; i < pCubeMin->nLits; i++ )
558 {
559 assert( pCubeMin->Lits[i] >= 0 );
560 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
561 if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
562 p->nAbsFlops++;
563 Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
564 }
565
566 Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref
567 p->nCubes++;
568 // add clause
569 for ( i = 1; i <= l; i++ )
570 Pdr_ManSolverAddClause( p, i, pCubeMin );
571 Pdr_SetDeref( pPred );
572 RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
573 assert( RetValue >= 0 );
574 Pdr_SetDeref( pCtg );
575 if ( RetValue == 1 )
576 {
577 //printf ("IT'S A ONE\n");
578 return 1;
579 }
580 }
581
582 //join
583 if ( p->pPars->fVeryVerbose )
584 {
585 printf("Cube:\n");
586 ZPdr_SetPrint( *ppCube );
587 printf("\nPred:\n");
588 ZPdr_SetPrint( pPred );
589 }
590 *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
591 Pdr_SetDeref( pCubeTmp );
592 Pdr_SetDeref( pPred );
593 if ( *ppCube == NULL )
594 return 0;
595 if ( p->pPars->fVeryVerbose )
596 {
597 printf("Intersection:\n");
598 ZPdr_SetPrint( *ppCube );
599 }
600 if ( Pdr_SetIsInit( *ppCube, -1 ) )
601 {
602 if ( p->pPars->fVeryVerbose )
603 printf ("Failed initiation\n");
604 return 0;
605 }
606 RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
607 if ( RetValue == -1 )
608 return -1;
609 if ( RetValue == 1 )
610 {
611 //printf ("*********IT'S A ONE\n");
612 break;
613 }
614 if ( RetValue == 0 && (*ppCube)->nLits == 1)
615 {
616 Pdr_SetDeref( pPred ); // fixed memory leak
617 // A workaround for the incomplete assignment returned by the SAT
618 // solver
619 return 0;
620 }
621 }
622 return 1;
623}
624
625int ZPdr_ManDown_Exhaustive( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added )
626{
627 int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
628 int j;
629 int kMax = Vec_PtrSize(p->vSolvers)-1;
630 int kTmp = k;
631 Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
632 Pdr_Set_t * pPredTmp = pPred, * pCubePre = *ppCube;
633 Pdr_Set_t * pCubeMinCopy;
634 while ( RetValue == 0 )
635 {
636 ctgAttempts = 0;
637 while ( RetValue == 0 && kTmp > 1 && ctgAttempts < 3 )
638 {
639 pCtg = Pdr_SetDup( pPredTmp );
640 //Check CTG for inductiveness
641 if ( Pdr_SetIsInit( pCtg, -1 ) )
642 {
643 Pdr_SetDeref( pCtg );
644 break;
645 }
646 if (*added == 0)
647 {
648 for ( i = 1; i <= k; i++ )
649 Pdr_ManSolverAddClause( p, i, pIndCube);
650 *added = 1;
651 }
652 if ( pPredTmp != pPred )
653 Pdr_SetDeref( pPredTmp );
654 CtgRetValue = Pdr_ManCheckCube( p, kTmp-1, pCtg, &pPredTmp, p->pPars->nConfLimit, 0, 1 );
655 if ( CtgRetValue == -1 )
656 {
657 Pdr_SetDeref( pCtg );
658 Pdr_SetDeref( pPred );
659 if ( pCubePre != *ppCube )
660 Pdr_SetDeref( pCubePre );
661 return -1;
662 }
663 if ( CtgRetValue == 0 )
664 {
665 if (pCubePre != *ppCube)
666 Pdr_SetDeref( pCubePre );
667 if (kTmp == 1)
668 {
669 Pdr_SetDeref( pCtg );
670 ctgAttempts++;
671 kTmp = k;
672 pPredTmp = pPred;
673 pCubePre = *ppCube;
674 }
675 else
676 {
677 pCubePre = pCtg;
678 kTmp = kTmp - 1;
679 }
680 continue;
681 }
682
683
684 pCubeMin = Pdr_ManReduceClause( p, kTmp-1, pCtg );
685 if ( pCubeMin == NULL )
686 pCubeMin = Pdr_SetDup( pCtg );
687
688 pCubeMinCopy = Pdr_SetDup( pCubeMin );
689 // generalize before pushing
690 micResult = ZPdr_ManSimpleMic( p, kTmp-1, &pCubeMin );
691 if ( micResult == -1 )
692 {
693 Pdr_SetDeref( pCtg );
694 Pdr_SetDeref( pCubeMin );
695 Pdr_SetDeref( pCubeMinCopy );
696 Pdr_SetDeref( pPred );
697 if ( pCubePre != *ppCube )
698 Pdr_SetDeref( pCubePre );
699 return -1;
700 }
701 for ( l = kTmp; l < kMax; l++ )
702 if ( Pdr_ManCheckCube( p, l, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 ) != 1 )
703 break;
704 // add clause
705 for ( i = 1; i <= l; i++ )
706 Pdr_ManSolverAddClause( p, i, pCubeMin );
707 Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref
708 p->nCubes++;
709
710 // try to push the original cube farther
711 for ( j = l; j < kMax; j++ )
712 if ( Pdr_ManCheckCube( p, j, pCubeMinCopy, NULL, p->pPars->nConfLimit, 0, 1 ) != 1 )
713 break;
714 if ( j > l )
715 {
716 micResult = ZPdr_ManSimpleMic( p, j-1, &pCubeMinCopy );
717 if ( micResult == -1 )
718 {
719 Pdr_SetDeref( pCtg );
720 Pdr_SetDeref( pCubeMinCopy );
721 Pdr_SetDeref( pPred );
722 if ( pCubePre != *ppCube )
723 Pdr_SetDeref( pCubePre );
724 return -1;
725 }
726 // add clause
727 for ( i = 1; i <= j; i++ )
728 Pdr_ManSolverAddClause( p, i, pCubeMinCopy );
729 Vec_VecPush( p->vClauses, j, pCubeMinCopy );
730 p->nCubes++;
731 }
732
733 // add new clause
734 if ( p->pPars->fVeryVerbose )
735 {
736 Abc_Print( 1, "Adding cube " );
737 Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
738 Abc_Print( 1, " to frame %d.\n", l );
739 }
740 // set priority flops for both cubes
741 for ( i = 0; i < pCubeMin->nLits; i++ )
742 {
743 assert( pCubeMin->Lits[i] >= 0 );
744 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
745 if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
746 p->nAbsFlops++;
747 Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
748 }
749 for ( i = 0; i < pCubeMinCopy->nLits; i++ )
750 {
751 assert( pCubeMinCopy->Lits[i] >= 0 );
752 assert( (pCubeMinCopy->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
753 if ( (Vec_IntEntry(p->vPrio, pCubeMinCopy->Lits[i] / 2) >> p->nPrioShift) == 0 )
754 p->nAbsFlops++;
755 Vec_IntAddToEntry( p->vPrio, pCubeMinCopy->Lits[i] / 2, 1 << p->nPrioShift );
756 }
757
758 Pdr_SetDeref( pPred );
759 RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
760 if ( RetValue == -1 )
761 {
762 if ( pCubePre != *ppCube )
763 Pdr_SetDeref( pCubePre );
764 Pdr_SetDeref( pCtg );
765 return -1;
766 }
767 Pdr_SetDeref( pCtg );
768 if ( RetValue == 1 )
769 {
770 //printf ("IT'S A ONE\n");
771 if ( pCubePre != *ppCube )
772 Pdr_SetDeref( pCubePre );
773 return 1;
774 }
775 RetValue = Pdr_ManCheckCube( p, kTmp, pCubePre, &pPredTmp, p->pPars->nConfLimit, 0, 1 );
776 if ( RetValue == -1 )
777 {
778 if ( pCubePre != *ppCube )
779 Pdr_SetDeref( pCubePre );
780 Pdr_SetDeref( pPred );
781 return -1;
782 }
783 if (RetValue == 1)
784 {
785 ctgAttempts++;
786 if ( pCubePre != *ppCube )
787 Pdr_SetDeref( pCubePre );
788 kTmp = k;
789 pPredTmp = pPred;
790 pCubePre = *ppCube;
791 }
792 }
793
794 if (pCubePre != *ppCube)
795 Pdr_SetDeref( pCubePre );
796 if ( pPredTmp != pPred )
797 Pdr_SetDeref( pPredTmp );
798 //join
799 if ( p->pPars->fVeryVerbose )
800 {
801 printf("Cube:\n");
802 ZPdr_SetPrint( *ppCube );
803 printf("\nPred:\n");
804 ZPdr_SetPrint( pPred );
805 }
806 *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
807 Pdr_SetDeref( pCubeTmp );
808 Pdr_SetDeref( pPred );
809 if ( *ppCube == NULL )
810 return 0;
811 if ( p->pPars->fVeryVerbose )
812 {
813 printf("Intersection:\n");
814 ZPdr_SetPrint( *ppCube );
815 }
816 if ( Pdr_SetIsInit( *ppCube, -1 ) )
817 {
818 if ( p->pPars->fVeryVerbose )
819 printf ("Failed initiation\n");
820 return 0;
821 }
822 RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
823 if ( RetValue == -1 )
824 return -1;
825 if ( RetValue == 1 )
826 {
827 //printf ("*********IT'S A ONE\n");
828 break;
829 }
830 if ( RetValue == 0 && (*ppCube)->nLits == 1)
831 {
832 Pdr_SetDeref( pPred ); // fixed memory leak
833 // A workaround for the incomplete assignment returned by the SAT
834 // solver
835 return 0;
836 }
837 kTmp = k;
838 pPredTmp = pPred;
839 pCubePre = *ppCube;
840 }
841 return 1;
842}
843
855static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
856{
857 int i, j, best_i;
858 for ( i = 0; i < nSize-1; i++ )
859 {
860 best_i = i;
861 for ( j = i+1; j < nSize; j++ )
862 if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
863 best_i = j;
864 ABC_SWAP( int, pArray[i], pArray[best_i] );
865 }
866 return 1;
867}
868
880int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
881{
882#if 0
883 int fUseMinAss = 0;
884 sat_solver * pSat = Pdr_ManFetchSolver( p, k );
885 int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
886 Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
887 int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
888 // create free variables
889 int i, iUseVar, iAndVar;
890 iAndVar = Pdr_ManFreeVar(p, k);
891 for ( i = 1; i < nLits; i++ )
892 Pdr_ManFreeVar(p, k);
893 iUseVar = Pdr_ManFreeVar(p, k);
894 for ( i = 1; i < nLits; i++ )
895 Pdr_ManFreeVar(p, k);
896 assert( iUseVar == iAndVar + nLits );
897 // if there is only one positive literal, put it in front and always assume
898 if ( fUseMinAss )
899 {
900 for ( i = 0; i < pCube->nLits && Count < 2; i++ )
901 Count += !Abc_LitIsCompl(pCube->Lits[i]);
902 if ( Count == 1 )
903 {
904 for ( i = 0; i < pCube->nLits; i++ )
905 if ( !Abc_LitIsCompl(pCube->Lits[i]) )
906 break;
907 assert( i < pCube->nLits );
908 iLit = pCube->Lits[i];
909 for ( ; i > 0; i-- )
910 pCube->Lits[i] = pCube->Lits[i-1];
911 pCube->Lits[0] = iLit;
912 }
913 }
914 // add clauses for the additional AND-gates
915 Vec_IntForEachEntry( vLits1, iLit, i )
916 {
917 sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
918 Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
919 }
920 // add clauses for the additional OR-gate
921 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
922 assert( RetValue == 1 );
923 // add implications
924 vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
925 assert( Vec_IntSize(vLits1) == nLits );
926 Vec_IntForEachEntry( vLits1, iLit, i )
927 {
928 Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
929 Lits[1] = iLit;
930 RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
931 assert( RetValue == 1 );
932 Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
933 }
934 sat_solver_compress( pSat );
935 // perform minimization
936 if ( fUseMinAss )
937 {
938 if ( Count == 1 ) // always assume the only positive literal
939 {
940 if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
941 nLits = 1;
942 else
943 nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
944 sat_solver_pop(pSat); // unassume the first literal
945 }
946 else
947 nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
948 Vec_IntShrink( vLits1, nLits );
949 }
950 else
951 {
952 // try removing one literal at a time in the old-fashioned way
953 int k, Entry;
954 Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
955 for ( i = nLits - 1; i >= 0; i-- )
956 {
957 // if we are about to remove a positive lit, make sure at least one positive lit remains
958 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
959 {
960 Vec_IntForEachEntry( vLits1, iLit, k )
961 if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
962 break;
963 if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
964 continue;
965 }
966 // load remaining literals
967 Vec_IntClear( vTemp );
968 Vec_IntForEachEntry( vLits1, Entry, k )
969 if ( Entry != -1 && k != i )
970 Vec_IntPush( vTemp, Entry );
971 else if ( Entry != -1 ) // assume opposite literal
972 Vec_IntPush( vTemp, Abc_LitNot(Entry) );
973 // solve with assumptions
974 RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
975 // commit the literal
976 if ( RetValue == l_False )
977 {
978 int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
979 int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
980 assert( RetValue );
981 }
982 // update the clause
983 if ( RetValue == l_False )
984 Vec_IntWriteEntry( vLits1, i, -1 );
985 }
986 Vec_IntFree( vTemp );
987 // compact
988 k = 0;
989 Vec_IntForEachEntry( vLits1, Entry, i )
990 if ( Entry != -1 )
991 Vec_IntWriteEntry( vLits1, k++, Entry );
992 Vec_IntShrink( vLits1, k );
993 }
994 // remap auxiliary literals into original literals
995 Vec_IntForEachEntry( vLits1, iLit, i )
996 Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
997 // make sure the cube has at least one positive literal
998 if ( fUseMinAss )
999 {
1000 Vec_IntForEachEntry( vLits1, iLit, i )
1001 if ( !Abc_LitIsCompl(iLit) )
1002 break;
1003 if ( i == Vec_IntSize(vLits1) ) // has no positive literals
1004 {
1005 // find positive lit in the cube
1006 for ( i = 0; i < pCube->nLits; i++ )
1007 if ( !Abc_LitIsCompl(pCube->Lits[i]) )
1008 break;
1009 assert( i < pCube->nLits );
1010 Vec_IntPush( vLits1, pCube->Lits[i] );
1011// printf( "-" );
1012 }
1013// else
1014// printf( "+" );
1015 }
1016 // create a subset cube
1017 *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
1018 assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
1019 Order = 0;
1020#endif
1021 return 0;
1022}
1023
1035int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
1036{
1037 Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL;
1038 int i, j, Lit, RetValue;
1039 abctime clk = Abc_Clock();
1040 int * pOrder;
1041 int added = 0;
1042 Hash_Int_t * keep = NULL;
1043 // if there is no induction, return
1044 *ppCubeMin = NULL;
1045 if ( p->pPars->fFlopOrder )
1046 Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
1047 RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
1048 if ( p->pPars->fFlopOrder )
1049 Vec_IntSelectSort( pCube->Lits, pCube->nLits );
1050 if ( RetValue == -1 )
1051 return -1;
1052 if ( RetValue == 0 )
1053 {
1054 p->tGeneral += Abc_Clock() - clk;
1055 return 0;
1056 }
1057
1058 // reduce clause using assumptions
1059// pCubeMin = Pdr_SetDup( pCube );
1060 pCubeMin = Pdr_ManReduceClause( p, k, pCube );
1061 if ( pCubeMin == NULL )
1062 pCubeMin = Pdr_SetDup( pCube );
1063
1064 // perform simplified generalization
1065 if ( p->pPars->fSimpleGeneral )
1066 {
1067 assert( pCubeMin->nLits > 0 );
1068 if ( pCubeMin->nLits > 1 )
1069 {
1070 RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
1071 Pdr_SetDeref( pCubeMin );
1072 assert( ppCubeMin != NULL );
1073 pCubeMin = *ppCubeMin;
1074 }
1075 *ppCubeMin = pCubeMin;
1076 if ( p->pPars->fVeryVerbose )
1077 {
1078 printf("Cube:\n");
1079 for ( i = 0; i < pCubeMin->nLits; i++)
1080 printf ("%d ", pCubeMin->Lits[i]);
1081 printf("\n");
1082 }
1083 p->tGeneral += Abc_Clock() - clk;
1084 return 1;
1085 }
1086
1087 keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
1088
1089 // perform generalization
1090 if ( !p->pPars->fSkipGeneral )
1091 {
1092 // assume the unminimized cube
1093 if ( p->pPars->fSimpleGeneral )
1094 {
1095 sat_solver * pSat = Pdr_ManFetchSolver( p, k );
1096 Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
1097 int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
1098 assert( RetValue1 == 1 );
1099 sat_solver_compress( pSat );
1100 }
1101
1102 // sort literals by their occurences
1103 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
1104 // try removing literals
1105 for ( j = 0; j < pCubeMin->nLits; j++ )
1106 {
1107 // use ordering
1108 // i = j;
1109 i = pOrder[j];
1110
1111 assert( pCubeMin->Lits[i] != -1 );
1112 if ( keep && Hash_IntExists( keep, pCubeMin->Lits[i] ) )
1113 {
1114 //printf("Undroppable\n");
1115 continue;
1116 }
1117
1118 // check init state
1119 if ( Pdr_SetIsInit(pCubeMin, i) )
1120 continue;
1121
1122 // try removing this literal
1123 Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
1124 if ( p->pPars->fSkipDown )
1125 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
1126 else
1127 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
1128 if ( RetValue == -1 )
1129 {
1130 Pdr_SetDeref( pCubeMin );
1131 return -1;
1132 }
1133 pCubeMin->Lits[i] = Lit;
1134 if ( RetValue == 0 )
1135 {
1136 if ( p->pPars->fSkipDown )
1137 continue;
1138 pCubeCpy = Pdr_SetCreateFrom( pCubeMin, i );
1139 RetValue = ZPdr_ManDown( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
1140 if ( p->pPars->fCtgs )
1141 //CTG handling code messes up with the internal order array
1142 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
1143 if ( RetValue == -1 )
1144 {
1145 Pdr_SetDeref( pCubeMin );
1146 Pdr_SetDeref( pCubeCpy );
1147 Pdr_SetDeref( pPred );
1148 return -1;
1149 }
1150 if ( RetValue == 0 )
1151 {
1152 if ( keep )
1153 Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
1154 if ( pCubeCpy )
1155 Pdr_SetDeref( pCubeCpy );
1156 continue;
1157 }
1158 //Inductive subclause
1159 added = 0;
1160 Pdr_SetDeref( pCubeMin );
1161 pCubeMin = pCubeCpy;
1162 assert( pCubeMin->nLits > 0 );
1163 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
1164 j = -1;
1165 continue;
1166 }
1167 added = 0;
1168
1169 // success - update the cube
1170 pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
1171 Pdr_SetDeref( pCubeTmp );
1172 assert( pCubeMin->nLits > 0 );
1173
1174 // assume the minimized cube
1175 if ( p->pPars->fSimpleGeneral )
1176 {
1177 sat_solver * pSat = Pdr_ManFetchSolver( p, k );
1178 Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
1179 int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
1180 assert( RetValue1 == 1 );
1181 sat_solver_compress( pSat );
1182 }
1183
1184 // get the ordering by decreasing priority
1185 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
1186 j--;
1187 }
1188
1189 if ( p->pPars->fTwoRounds )
1190 for ( j = 0; j < pCubeMin->nLits; j++ )
1191 {
1192 // use ordering
1193 // i = j;
1194 i = pOrder[j];
1195
1196 // check init state
1197 assert( pCubeMin->Lits[i] != -1 );
1198 if ( Pdr_SetIsInit(pCubeMin, i) )
1199 continue;
1200 // try removing this literal
1201 Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
1202 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 );
1203 if ( RetValue == -1 )
1204 {
1205 Pdr_SetDeref( pCubeMin );
1206 return -1;
1207 }
1208 pCubeMin->Lits[i] = Lit;
1209 if ( RetValue == 0 )
1210 continue;
1211
1212 // success - update the cube
1213 pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
1214 Pdr_SetDeref( pCubeTmp );
1215 assert( pCubeMin->nLits > 0 );
1216
1217 // get the ordering by decreasing priority
1218 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
1219 j--;
1220 }
1221 }
1222
1223 assert( ppCubeMin != NULL );
1224 if ( p->pPars->fVeryVerbose )
1225 {
1226 printf("Cube:\n");
1227 for ( i = 0; i < pCubeMin->nLits; i++)
1228 printf ("%d ", pCubeMin->Lits[i]);
1229 printf("\n");
1230 }
1231 *ppCubeMin = pCubeMin;
1232 p->tGeneral += Abc_Clock() - clk;
1233 if ( keep ) Hash_IntFree( keep );
1234 return 1;
1235}
1236
1248int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
1249{
1250 Pdr_Obl_t * pThis;
1251 Pdr_Set_t * pPred, * pCubeMin;
1252 int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
1253 int kMax = Vec_PtrSize(p->vSolvers)-1;
1254 abctime clk;
1255 p->nBlocks++;
1256 // create first proof obligation
1257// assert( p->pQueue == NULL );
1258 pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
1259 Pdr_QueuePush( p, pThis );
1260 // try to solve it recursively
1261 while ( !Pdr_QueueIsEmpty(p) )
1262 {
1263 Counter++;
1264 pThis = Pdr_QueueHead( p );
1265 if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
1266 return 0; // SAT
1267 if ( pThis->iFrame > kMax ) // finished this level
1268 return 1;
1269 if ( p->nQueLim && p->nQueCur >= p->nQueLim )
1270 {
1271 p->nQueLim = p->nQueLim * 3 / 2;
1272 Pdr_QueueStop( p );
1273 return 1; // restart
1274 }
1275 pThis = Pdr_QueuePop( p );
1276 assert( pThis->iFrame > 0 );
1277 assert( !Pdr_SetIsInit(pThis->pState, -1) );
1278 p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame );
1279 clk = Abc_Clock();
1280 if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
1281 {
1282 p->tContain += Abc_Clock() - clk;
1283 Pdr_OblDeref( pThis );
1284 continue;
1285 }
1286 p->tContain += Abc_Clock() - clk;
1287
1288 // check if the cube is already contained
1289 RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
1290 if ( RetValue == -1 ) // resource limit is reached
1291 {
1292 Pdr_OblDeref( pThis );
1293 return -1;
1294 }
1295 if ( RetValue ) // cube is blocked by clauses in this frame
1296 {
1297 Pdr_OblDeref( pThis );
1298 continue;
1299 }
1300
1301 // check if the cube holds with relative induction
1302 pCubeMin = NULL;
1303 RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
1304 if ( RetValue == -1 ) // resource limit is reached
1305 {
1306 Pdr_OblDeref( pThis );
1307 return -1;
1308 }
1309 if ( RetValue ) // cube is blocked inductively in this frame
1310 {
1311 assert( pCubeMin != NULL );
1312 // k is the last frame where pCubeMin holds
1313 k = pThis->iFrame;
1314 // check other frames
1315 assert( pPred == NULL );
1316 for ( k = pThis->iFrame; k < kMax; k++ )
1317 {
1318 RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
1319 if ( RetValue == -1 )
1320 {
1321 Pdr_OblDeref( pThis );
1322 return -1;
1323 }
1324 if ( !RetValue )
1325 break;
1326 }
1327 // add new clause
1328 if ( p->pPars->fVeryVerbose )
1329 {
1330 Abc_Print( 1, "Adding cube " );
1331 Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
1332 Abc_Print( 1, " to frame %d.\n", k );
1333 }
1334 // set priority flops
1335 for ( i = 0; i < pCubeMin->nLits; i++ )
1336 {
1337 assert( pCubeMin->Lits[i] >= 0 );
1338 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
1339 if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
1340 p->nAbsFlops++;
1341 Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
1342 }
1343 Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
1344 p->nCubes++;
1345 // add clause
1346 for ( i = 1; i <= k; i++ )
1347 Pdr_ManSolverAddClause( p, i, pCubeMin );
1348 // schedule proof obligation
1349 if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
1350 {
1351 pThis->iFrame = k+1;
1352 pThis->prio = Prio--;
1353 Pdr_QueuePush( p, pThis );
1354 }
1355 else
1356 {
1357 Pdr_OblDeref( pThis );
1358 }
1359 }
1360 else
1361 {
1362 assert( pCubeMin == NULL );
1363 assert( pPred != NULL );
1364 pThis->prio = Prio--;
1365 Pdr_QueuePush( p, pThis );
1366 pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
1367 Pdr_QueuePush( p, pThis );
1368 }
1369
1370 // check termination
1371 if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
1372 return -1;
1373 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1374 return -1;
1375 if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1376 return -1;
1377 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1378 return -1;
1379 }
1380 return 1;
1381}
1382
1394int Pdr_ManSolveInt( Pdr_Man_t * p )
1395{
1396 int fPrintClauses = 0;
1397 Pdr_Set_t * pCube = NULL;
1398 Aig_Obj_t * pObj;
1399 Abc_Cex_t * pCexNew;
1400 int iFrame, RetValue = -1;
1401 int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
1402 abctime clkStart = Abc_Clock(), clkOne = 0;
1403 p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1404 assert( Vec_PtrSize(p->vSolvers) == 0 );
1405 // in the multi-output mode, mark trivial POs (those fed by const0) as solved
1406 if ( p->pPars->fSolveAll )
1407 Saig_ManForEachPo( p->pAig, pObj, iFrame )
1408 if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
1409 {
1410 Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
1411 p->pPars->nProveOuts++;
1412 if ( p->pPars->fUseBridge )
1413 Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
1414 }
1415 // create the first timeframe
1416 p->pPars->timeLastSolved = Abc_Clock();
1417 Pdr_ManCreateSolver( p, (iFrame = 0) );
1418 while ( 1 )
1419 {
1420 int fRefined = 0;
1421 if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
1422 {
1423// int i, Prio;
1424 assert( p->vAbsFlops == NULL );
1425 p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
1426 p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
1427 p->vMapPpi2Ff = Vec_IntAlloc( 100 );
1428// Vec_IntForEachEntry( p->vPrio, Prio, i )
1429// if ( Prio >> p->nPrioShift )
1430// Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
1431 }
1432 //if ( p->pPars->fUseAbs && p->vAbsFlops )
1433 // printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
1434 p->nFrames = iFrame;
1435 assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
1436 p->iUseFrame = Abc_MaxInt(iFrame, 1);
1437 Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
1438 {
1439 // skip disproved outputs
1440 if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
1441 continue;
1442 // skip output whose time has run out
1443 if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
1444 continue;
1445 // check if the output is trivially solved
1446 if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
1447 continue;
1448 // check if the output is trivially solved
1449 if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
1450 {
1451 if ( !p->pPars->fSolveAll )
1452 {
1453 pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
1454 p->pAig->pSeqModel = pCexNew;
1455 return 0; // SAT
1456 }
1457 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;
1458 p->pPars->nFailOuts++;
1459 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
1460 if ( !p->pPars->fNotVerbose )
1461 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
1462 nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
1463 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
1464 if ( p->pPars->fUseBridge )
1465 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1466 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
1467 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
1468 {
1469 if ( p->pPars->fVerbose )
1470 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1471 if ( !p->pPars->fSilent )
1472 Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
1473 p->pPars->iFrame = iFrame;
1474 return -1;
1475 }
1476 if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
1477 return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
1478 p->pPars->timeLastSolved = Abc_Clock();
1479 continue;
1480 }
1481 // try to solve this output
1482 if ( p->pTime4Outs )
1483 {
1484 assert( p->pTime4Outs[p->iOutCur] > 0 );
1485 clkOne = Abc_Clock();
1486 p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
1487 }
1488 while ( 1 )
1489 {
1490 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1491 {
1492 if ( p->pPars->fVerbose )
1493 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1494 if ( !p->pPars->fSilent )
1495 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
1496 p->pPars->iFrame = iFrame;
1497 return -1;
1498 }
1499 RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
1500 if ( RetValue == 1 )
1501 break;
1502 if ( RetValue == -1 )
1503 {
1504 if ( p->pPars->fVerbose )
1505 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1506 if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
1507 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
1508 else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1509 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
1510 else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1511 {
1512 Pdr_QueueClean( p );
1513 pCube = NULL;
1514 break; // keep solving
1515 }
1516 else if ( p->pPars->nConfLimit )
1517 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
1518 else if ( p->pPars->fVerbose )
1519 Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
1520 p->pPars->iFrame = iFrame;
1521 return -1;
1522 }
1523 if ( RetValue == 0 )
1524 {
1525 RetValue = Pdr_ManBlockCube( p, pCube );
1526 if ( RetValue == -1 )
1527 {
1528 if ( p->pPars->fVerbose )
1529 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1530 if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
1531 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
1532 else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1533 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
1534 else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
1535 {
1536 Pdr_QueueClean( p );
1537 pCube = NULL;
1538 break; // keep solving
1539 }
1540 else if ( p->pPars->nConfLimit )
1541 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
1542 else if ( p->pPars->fVerbose )
1543 Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
1544 p->pPars->iFrame = iFrame;
1545 return -1;
1546 }
1547 if ( RetValue == 0 )
1548 {
1549 if ( fPrintClauses )
1550 {
1551 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1552 Pdr_ManPrintClauses( p, 0 );
1553 }
1554 if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
1555 Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
1556 p->pPars->iFrame = iFrame;
1557 if ( !p->pPars->fSolveAll )
1558 {
1559 abctime clk = Abc_Clock();
1560 Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
1561 p->tAbs += Abc_Clock() - clk;
1562 if ( pCex == NULL )
1563 {
1564 assert( p->pPars->fUseAbs );
1565 Pdr_QueueClean( p );
1566 pCube = NULL;
1567 fRefined = 1;
1568 break; // keep solving
1569 }
1570 p->pAig->pSeqModel = pCex;
1571 return 0; // SAT
1572 }
1573 p->pPars->nFailOuts++;
1574 pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
1575 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
1576 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
1577 if ( p->pPars->fUseBridge )
1578 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1579 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
1580 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
1581 {
1582 if ( p->pPars->fVerbose )
1583 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1584 if ( !p->pPars->fSilent )
1585 Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
1586 p->pPars->iFrame = iFrame;
1587 return -1;
1588 }
1589 if ( !p->pPars->fNotVerbose )
1590 Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
1591 nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
1592 if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
1593 return 0; // all SAT
1594 Pdr_QueueClean( p );
1595 pCube = NULL;
1596 break; // keep solving
1597 }
1598 if ( p->pPars->fVerbose )
1599 Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
1600 }
1601 }
1602 if ( fRefined )
1603 break;
1604 if ( p->pTime4Outs )
1605 {
1606 abctime timeSince = Abc_Clock() - clkOne;
1607 assert( p->pTime4Outs[p->iOutCur] > 0 );
1608 p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
1609 if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
1610 {
1611 p->pPars->nDropOuts++;
1612 if ( p->pPars->vOutMap )
1613 Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
1614 if ( !p->pPars->fNotVerbose )
1615 Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
1616 }
1617 p->timeToStopOne = 0;
1618 }
1619 }
1620 if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
1621 {
1622 int i, Used;
1623 Vec_IntForEachEntry( p->vAbsFlops, Used, i )
1624 if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
1625 Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
1626 }
1627 if ( p->pPars->fVerbose )
1628 Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
1629 if ( fRefined )
1630 continue;
1631 //if ( p->pPars->fUseAbs && p->vAbsFlops )
1632 // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
1633 // open a new timeframe
1634 p->nQueLim = p->pPars->nRestLimit;
1635 assert( pCube == NULL );
1636 Pdr_ManSetPropertyOutput( p, iFrame );
1637 Pdr_ManCreateSolver( p, ++iFrame );
1638 if ( fPrintClauses )
1639 {
1640 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1641 Pdr_ManPrintClauses( p, 0 );
1642 }
1643 // push clauses into this timeframe
1644 if (p->pPars->fBlocking) // clause pushing with blocking
1645 {
1646 RetValue = Pdr_ManPushAndBlockClauses( p );
1647 if ( RetValue == -1 )
1648 {
1649 if ( p->pPars->fVerbose )
1650 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1651 if ( !p->pPars->fSilent )
1652 {
1653 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1654 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
1655 else
1656 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
1657 }
1658 p->pPars->iFrame = iFrame;
1659 return -1;
1660 }
1661 }
1662 RetValue = Pdr_ManPushClauses( p );
1663 if ( RetValue == -1 )
1664 {
1665 if ( p->pPars->fVerbose )
1666 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1667 if ( !p->pPars->fSilent )
1668 {
1669 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1670 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
1671 else
1672 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
1673 }
1674 p->pPars->iFrame = iFrame;
1675 return -1;
1676 }
1677 if ( RetValue )
1678 {
1679 if ( p->pPars->fVerbose )
1680 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1681 if ( !p->pPars->fSilent )
1682 Pdr_ManReportInvariant( p );
1683 if ( !p->pPars->fSilent )
1684 Pdr_ManVerifyInvariant( p );
1685 p->pPars->iFrame = iFrame;
1686 // count the number of UNSAT outputs
1687 p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
1688 // convert previously 'unknown' into 'unsat'
1689 if ( p->pPars->vOutMap )
1690 for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
1691 if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
1692 {
1693 Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
1694 if ( p->pPars->fUseBridge )
1695 Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
1696 }
1697 if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
1698 return 1; // UNSAT
1699 if ( p->pPars->nFailOuts > 0 )
1700 return 0; // SAT
1701 return -1;
1702 }
1703 if ( p->pPars->fVerbose )
1704 Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
1705
1706 // check termination
1707 if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
1708 {
1709 p->pPars->iFrame = iFrame;
1710 return -1;
1711 }
1712 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
1713 {
1714 if ( fPrintClauses )
1715 {
1716 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1717 Pdr_ManPrintClauses( p, 0 );
1718 }
1719 if ( p->pPars->fVerbose )
1720 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1721 if ( !p->pPars->fSilent )
1722 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
1723 p->pPars->iFrame = iFrame;
1724 return -1;
1725 }
1726 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
1727 {
1728 if ( fPrintClauses )
1729 {
1730 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
1731 Pdr_ManPrintClauses( p, 0 );
1732 }
1733 if ( p->pPars->fVerbose )
1734 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1735 if ( !p->pPars->fSilent )
1736 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
1737 p->pPars->iFrame = iFrame;
1738 return -1;
1739 }
1740 if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
1741 {
1742 if ( p->pPars->fVerbose )
1743 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
1744 if ( !p->pPars->fSilent )
1745 Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
1746 p->pPars->iFrame = iFrame;
1747 return -1;
1748 }
1749 }
1750 assert( 0 );
1751 return -1;
1752}
1753
1765int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
1766{
1767 Pdr_Man_t * p;
1768 int k, RetValue;
1769 abctime clk = Abc_Clock();
1770 if ( pPars->nTimeOutOne && !pPars->fSolveAll )
1771 pPars->nTimeOutOne = 0;
1772 if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
1773 pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
1774 if ( pPars->fVerbose )
1775 {
1776// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
1777 Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
1778 pPars->nRecycle,
1779 pPars->nFrameMax,
1780 pPars->nRestLimit,
1781 pPars->nTimeOut );
1782 Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
1783 pPars->fMonoCnf ? "yes" : "no",
1784 pPars->fSkipGeneral ? "yes" : "no",
1785 pPars->fSolveAll ? "yes" : "no" );
1786 }
1787 ABC_FREE( pAig->pSeqModel );
1788 p = Pdr_ManStart( pAig, pPars, NULL );
1789 RetValue = Pdr_ManSolveInt( p );
1790 if ( RetValue == 0 )
1791 assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
1792 if ( p->vCexes )
1793 {
1794 assert( p->pAig->vSeqModelVec == NULL );
1795 p->pAig->vSeqModelVec = p->vCexes;
1796 p->vCexes = NULL;
1797 }
1798 if ( p->pPars->fDumpInv )
1799 {
1800 char * pFileName = pPars->pInvFileName ? pPars->pInvFileName : Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
1801 Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
1802 Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
1803 printf( "Dumped inductive invariant in file \"%s\".\n", pFileName );
1804 }
1805 else if ( RetValue == 1 )
1806 Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
1807 p->tTotal += Abc_Clock() - clk;
1808 Pdr_ManStop( p );
1809 pPars->iFrame--;
1810 // convert all -2 (unknown) entries into -1 (undec)
1811 if ( pPars->vOutMap )
1812 for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
1813 if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
1814 Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
1815 if ( pPars->fUseBridge )
1816 Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
1817 return RetValue;
1818}
1819
1823
1824
1825ABC_NAMESPACE_IMPL_END
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Abc_FrameSetInv
ABC_DLL void Abc_FrameSetInv(Vec_Int_t *vInv)
Definition mainFrame.c:104
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Hash_Int_t
struct Hash_Int_t_ Hash_Int_t
PARAMETERS ///.
Definition hashInt.h:45
Pdr_ManFreeVar
int Pdr_ManFreeVar(Pdr_Man_t *p, int k)
Definition pdrCnf.c:332
Pdr_ManBlockCube
int Pdr_ManBlockCube(Pdr_Man_t *p, Pdr_Set_t *pCube)
Definition pdrCore.c:1248
Pdr_ManSetDefaultParams
void Pdr_ManSetDefaultParams(Pdr_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition pdrCore.c:50
Pdr_ManGeneralize
int Pdr_ManGeneralize(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, Pdr_Set_t **ppCubeMin)
Definition pdrCore.c:1035
Pdr_ManSortByPriority
int * Pdr_ManSortByPriority(Pdr_Man_t *p, Pdr_Set_t *pCube)
Definition pdrCore.c:414
ZPdr_ManSimpleMic
int ZPdr_ManSimpleMic(Pdr_Man_t *p, int k, Pdr_Set_t **ppCube)
Definition pdrCore.c:453
Pdr_ManPushClauses
int Pdr_ManPushClauses(Pdr_Man_t *p)
Definition pdrCore.c:150
Pdr_ManSolveInt
int Pdr_ManSolveInt(Pdr_Man_t *p)
Definition pdrCore.c:1394
Pdr_ManReduceClause
Pdr_Set_t * Pdr_ManReduceClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrCore.c:97
Pdr_ManSolve
int Pdr_ManSolve(Aig_Man_t *pAig, Pdr_Par_t *pPars)
Definition pdrCore.c:1765
Pdr_ManGeneralize2
int Pdr_ManGeneralize2(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppCubeMin)
Definition pdrCore.c:880
ZPdr_ManDown
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)
Definition pdrCore.c:509
Gia_ManToBridgeAbort
int Gia_ManToBridgeAbort(FILE *pFile, int Size, unsigned char *pBuffer)
Definition utilBridge.c:178
Pdr_ManCheckContainment
int Pdr_ManCheckContainment(Pdr_Man_t *p, int k, Pdr_Set_t *pSet)
Definition pdrCore.c:390
Gia_ManToBridgeResult
ABC_NAMESPACE_IMPL_START int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition utilBridge.c:287
ZPdr_ManDown_Exhaustive
int ZPdr_ManDown_Exhaustive(Pdr_Man_t *, int, Pdr_Set_t **, Pdr_Set_t *, Hash_Int_t *, Pdr_Set_t *, int *)
Definition pdrCore.c:625
Pdr_ManPushAndBlockClauses
int Pdr_ManPushAndBlockClauses(Pdr_Man_t *p)
Definition pdrCore.c:246
Pdr_QueueStop
void Pdr_QueueStop(Pdr_Man_t *p)
Definition pdrUtil.c:699
Pdr_ManDeriveInfinityClauses
Vec_Int_t * Pdr_ManDeriveInfinityClauses(Pdr_Man_t *p, int fReduce)
Definition pdrInv.c:595
Pdr_ManFetchSolver
sat_solver * Pdr_ManFetchSolver(Pdr_Man_t *p, int k)
Definition pdrSat.c:77
Pdr_ManPrintClauses
void Pdr_ManPrintClauses(Pdr_Man_t *p, int kStart)
Definition pdrInv.c:244
Pdr_ManCheckCubeCs
int Pdr_ManCheckCubeCs(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrSat.c:262
Pdr_QueueClean
void Pdr_QueueClean(Pdr_Man_t *p)
Definition pdrUtil.c:632
Pdr_ManDumpClauses
void Pdr_ManDumpClauses(Pdr_Man_t *p, char *pFileName, int fProved)
Definition pdrInv.c:352
Pdr_OblDeref
void Pdr_OblDeref(Pdr_Obl_t *p)
Definition pdrUtil.c:556
Pdr_OblRef
Pdr_Obl_t * Pdr_OblRef(Pdr_Obl_t *p)
Definition pdrUtil.c:539
ZPdr_SetIntersection
Pdr_Set_t * ZPdr_SetIntersection(Pdr_Set_t *p1, Pdr_Set_t *p2, Hash_Int_t *keep)
Definition pdrUtil.c:283
Pdr_SetDup
Pdr_Set_t * Pdr_SetDup(Pdr_Set_t *pSet)
Definition pdrUtil.c:166
Pdr_ManCheckCube
int Pdr_ManCheckCube(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, int nConfLimit, int fTryConf, int fUseLit)
Definition pdrSat.c:290
Pdr_Set_t
struct Pdr_Set_t_ Pdr_Set_t
Definition pdrInt.h:74
Pdr_ManStart
Pdr_Man_t * Pdr_ManStart(Aig_Man_t *pAig, Pdr_Par_t *pPars, Vec_Int_t *vPrioInit)
Definition pdrMan.c:248
Pdr_SetDeref
void Pdr_SetDeref(Pdr_Set_t *p)
Definition pdrUtil.c:208
Pdr_OblStart
Pdr_Obl_t * Pdr_OblStart(int k, int prio, Pdr_Set_t *pState, Pdr_Obl_t *pNext)
Definition pdrUtil.c:515
Pdr_QueueIsEmpty
int Pdr_QueueIsEmpty(Pdr_Man_t *p)
Definition pdrUtil.c:578
Pdr_ManDeriveCexAbs
Abc_Cex_t * Pdr_ManDeriveCexAbs(Pdr_Man_t *p)
Definition pdrMan.c:448
Pdr_SetContains
int Pdr_SetContains(Pdr_Set_t *pOld, Pdr_Set_t *pNew)
Definition pdrUtil.c:382
Pdr_QueuePush
void Pdr_QueuePush(Pdr_Man_t *p, Pdr_Obl_t *pObl)
Definition pdrUtil.c:651
Pdr_ManStop
void Pdr_ManStop(Pdr_Man_t *p)
Definition pdrMan.c:318
Pdr_ManPrintProgress
void Pdr_ManPrintProgress(Pdr_Man_t *p, int fClose, abctime Time)
DECLARATIONS ///.
Definition pdrInv.c:48
Pdr_SetPrint
void Pdr_SetPrint(FILE *pFile, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
Definition pdrUtil.c:225
Pdr_SetCreateFrom
Pdr_Set_t * Pdr_SetCreateFrom(Pdr_Set_t *pSet, int iRemove)
Definition pdrUtil.c:98
Pdr_ManSetPropertyOutput
void Pdr_ManSetPropertyOutput(Pdr_Man_t *p, int k)
Definition pdrSat.c:179
Pdr_QueuePop
Pdr_Obl_t * Pdr_QueuePop(Pdr_Man_t *p)
Definition pdrUtil.c:610
Pdr_Obl_t
struct Pdr_Obl_t_ Pdr_Obl_t
Definition pdrInt.h:84
Pdr_SetIsInit
int Pdr_SetIsInit(Pdr_Set_t *p, int iRemove)
Definition pdrUtil.c:460
Pdr_ManReportInvariant
void Pdr_ManReportInvariant(Pdr_Man_t *p)
Definition pdrInv.c:477
Pdr_ManLitsToCube
Vec_Int_t * Pdr_ManLitsToCube(Pdr_Man_t *p, int k, int *pArray, int nArray)
Definition pdrSat.c:117
ZPdr_SetPrint
void ZPdr_SetPrint(Pdr_Set_t *p)
Definition pdrUtil.c:263
Pdr_SetCompare
int Pdr_SetCompare(Pdr_Set_t **pp1, Pdr_Set_t **pp2)
Definition pdrUtil.c:485
Pdr_ManCreateSolver
sat_solver * Pdr_ManCreateSolver(Pdr_Man_t *p, int k)
DECLARATIONS ///.
Definition pdrSat.c:45
Pdr_ManVerifyInvariant
void Pdr_ManVerifyInvariant(Pdr_Man_t *p)
Definition pdrInv.c:500
Pdr_Man_t
struct Pdr_Man_t_ Pdr_Man_t
Definition pdrInt.h:95
Pdr_QueueHead
Pdr_Obl_t * Pdr_QueueHead(Pdr_Man_t *p)
Definition pdrUtil.c:594
Pdr_ManCubeToLits
Vec_Int_t * Pdr_ManCubeToLits(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, int fCompl, int fNext)
Definition pdrSat.c:144
Pdr_ManDeriveCex
Abc_Cex_t * Pdr_ManDeriveCex(Pdr_Man_t *p)
Definition pdrMan.c:408
Pdr_ManSolverAddClause
void Pdr_ManSolverAddClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrSat.c:213
Pdr_SetCreateSubset
Pdr_Set_t * Pdr_SetCreateSubset(Pdr_Set_t *pSet, int *pLits, int nLits)
Definition pdrUtil.c:132
Pdr_Par_t
typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_ Pdr_Par_t
INCLUDES ///.
Definition pdr.h:40
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
sat_solver_push
int sat_solver_push(sat_solver *s, int p)
Definition satSolver.c:2002
sat_solver_pop
void sat_solver_pop(sat_solver *s)
Definition satSolver.c:2045
sat_solver_minimize_assumptions2
int sat_solver_minimize_assumptions2(sat_solver *s, int *pLits, int nLits, int nConfLimit)
Definition satSolver.c:2284
Pdr_Obl_t_::prio
int prio
Definition pdrInt.h:88
Pdr_Obl_t_::pState
Pdr_Set_t * pState
Definition pdrInt.h:90
Pdr_Obl_t_::iFrame
int iFrame
Definition pdrInt.h:87
Pdr_Set_t_::Lits
int Lits[0]
Definition pdrInt.h:81
Pdr_Set_t_::nLits
int nLits
Definition pdrInt.h:80
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition utilCex.c:85
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_VecForEachLevelStartStop
#define Vec_VecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecVec.h:61