ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
pdrIncr.c
Go to the documentation of this file.
1
20
21#include "pdrInt.h"
22#include "base/main/main.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
30extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
31extern int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube );
32extern int Pdr_ManPushClauses( Pdr_Man_t * p );
33extern Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
34extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
35extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
36
37
41
42Vec_Ptr_t * IPdr_ManPushClausesK( Pdr_Man_t * p, int k )
43{
44 Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
45 Vec_Ptr_t * vArrayK, * vArrayK1;
46 int i, j, m, RetValue;
47
48 assert( Vec_VecSize(p->vClauses) == k + 1 );
49 vArrayK = Vec_VecEntry( p->vClauses, k );
50 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
51 vArrayK1 = Vec_PtrAlloc( 100 );
52 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
53 {
54 // remove cubes in the same frame that are contained by pCubeK
55 Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
56 {
57 if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
58 continue;
59 Pdr_SetDeref( pTemp );
60 Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
61 Vec_PtrPop(vArrayK);
62 m--;
63 }
64
65 // check if the clause can be moved to the next frame
66 RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
67 assert( RetValue != -1 );
68 if ( !RetValue )
69 continue;
70
71 {
72 Pdr_Set_t * pCubeMin;
73 pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
74 if ( pCubeMin != NULL )
75 {
76 // Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
77 Pdr_SetDeref( pCubeK );
78 pCubeK = pCubeMin;
79 }
80 }
81
82 // check if the clause subsumes others
83 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
84 {
85 if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
86 continue;
87 Pdr_SetDeref( pCubeK1 );
88 Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
89 Vec_PtrPop(vArrayK1);
90 i--;
91 }
92 // add the last clause
93 Vec_PtrPush( vArrayK1, pCubeK );
94 Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
95 Vec_PtrPop(vArrayK);
96 j--;
97 }
98
99 return vArrayK1;
100}
101
113void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
114{
115 Vec_Ptr_t * vArrayK;
116 Pdr_Set_t * pCube;
117 int i, k, Counter = 0;
118 Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
119 {
120 Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
121 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
122 {
123 Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
124 // Pdr_SetPrint( stdout, pCube, nRegs, NULL );
125 ZPdr_SetPrint( pCube );
126 Abc_Print( 1, "\n" );
127 }
128 }
129}
130
144int IPdr_ManCheckClauses( Pdr_Man_t * p )
145{
146 Pdr_Set_t * pCubeK;
147 Vec_Ptr_t * vArrayK;
148 int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers);
149 int iStartFrame = 1;
150 int counter = 0;
151
152 Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
153 {
154 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
155 {
156 ++counter;
157 RetValue = Pdr_ManCheckCube( p, k - 1, pCubeK, NULL, 0, 0, 1 );
158
159 if ( !RetValue ) {
160 printf( "Cube[%d][%d] not inductive!\n", k, j );
161 }
162
163 if ( RetValue == -1 )
164 return -1;
165 }
166 }
167
168 return 1;
169}
170
182Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
183{
184 int i, k;
185 Vec_Vec_t * vClausesSaved;
186 Pdr_Set_t * pCla;
187
188 if ( Vec_VecSize( p->vClauses ) == 1 )
189 return NULL;
190 if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast )
191 return NULL;
192
193 if ( fDropLast )
194 vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
195 else
196 vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) );
197
198 Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) )
199 Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla));
200
201 return vClausesSaved;
202}
203
204
216sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int fSetPropOutput )
217{
218 sat_solver * pSat;
219 Vec_Ptr_t * vArrayK;
220 Pdr_Set_t * pCube;
221 int i, j;
222
223 assert( Vec_PtrSize(p->vSolvers) == k );
224 assert( Vec_IntSize(p->vActVars) == k );
225
226 pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
227 pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
228 Vec_PtrPush( p->vSolvers, pSat );
229 Vec_IntPush( p->vActVars, 0 );
230
231 // set the property output
232 if ( fSetPropOutput )
233 Pdr_ManSetPropertyOutput( p, k );
234
235 if (k == 0)
236 return pSat;
237
238 // add the clauses
239 Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
240 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
241 Pdr_ManSolverAddClause( p, k, pCube );
242 return pSat;
243}
244
256int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
257{
258 Vec_Ptr_t * vArrayK;
259 Pdr_Set_t * pCube;
260 int i, j;
261 int RetValue = -1;
262 int nCubes = 0;
263
264 if ( vClauses == NULL )
265 return RetValue;
266
267 assert( Vec_VecSize(vClauses) >= 2 );
268 assert( Vec_VecSize(p->vClauses) == 0 );
269 Vec_VecExpand( p->vClauses, 1 );
270
271 IPdr_ManSetSolver( p, 0, 1 );
272
273 // push clauses from R0 to R1
274 Vec_VecForEachLevelStart( vClauses, vArrayK, i, 1 )
275 {
276 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
277 {
278 ++nCubes;
279
280 RetValue = Pdr_ManCheckCube( p, 0, pCube, NULL, 0, 0, 1 );
281 Vec_IntWriteEntry( p->vActVars, 0, 0 );
282
283 assert( RetValue != -1 );
284
285 if ( RetValue == 0 )
286 {
287 Abc_Print( 1, "Cube[%d][%d] cannot be pushed from R0 to R1.\n", i, j );
288 Pdr_SetDeref( pCube );
289 continue;
290 }
291
292 Vec_VecPush( p->vClauses, 1, pCube );
293 }
294 }
295 Abc_Print( 1, "RebuildClauses: %d out of %d cubes reused in R1.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, 1)), nCubes );
296 IPdr_ManSetSolver( p, 1, 0 );
297 Vec_VecFree( vClauses );
298
299 /*
300 for ( i = 1; i < Vec_VecSize( vClauses ) - 1; ++i )
301 {
302 vArrayK = IPdr_ManPushClausesK( p, i );
303 if ( Vec_PtrSize(vArrayK) == 0 )
304 {
305 Abc_Print( 1, "RebuildClauses: stopped at frame %d.\n", i );
306 break;
307 }
308
309 Vec_PtrGrow( (Vec_Ptr_t *)(p->vClauses), i + 2 );
310 p->vClauses->nSize = i + 2;
311 p->vClauses->pArray[i+1] = vArrayK;
312 IPdr_ManSetSolver( p, i + 1, 0 );
313 }
314
315 Abc_Print( 1, "After rebuild:" );
316 Vec_VecForEachLevel( p->vClauses, vArrayK, i )
317 Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) );
318 Abc_Print( 1, "\n" );
319 */
320
321 return 0;
322}
323
324int IPdr_ManRestoreAbsFlops( Pdr_Man_t * p )
325{
326 Pdr_Set_t * pSet; int i, j, k;
327
328 Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
329 {
330 for ( k = 0; k < pSet->nLits; k++ )
331 {
332 Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
333 }
334 }
335 return 0;
336}
337
338int IPdr_ManRestoreClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap )
339{
340 int i;
341
342 assert(vClauses);
343
344 Vec_VecFree(p->vClauses);
345 p->vClauses = vClauses;
346
347 // remap clause literals using mapping (old flop -> new flop) found in array vMap
348 if ( vMap )
349 {
350 Pdr_Set_t * pSet; int j, k;
351 Vec_VecForEachEntry( Pdr_Set_t *, vClauses, pSet, i, j )
352 for ( k = 0; k < pSet->nLits; k++ )
353 pSet->Lits[k] = Abc_Lit2LitV( Vec_IntArray(vMap), pSet->Lits[k] );
354 }
355
356 for ( i = 0; i < Vec_VecSize(p->vClauses); ++i )
357 IPdr_ManSetSolver( p, i, i < Vec_VecSize( p->vClauses ) - 1 );
358
359 return 0;
360}
361
373int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
374{
375 int fPrintClauses = 0;
376 Pdr_Set_t * pCube = NULL;
377 Aig_Obj_t * pObj;
378 Abc_Cex_t * pCexNew;
379 int iFrame, RetValue = -1;
380 int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
381 abctime clkStart = Abc_Clock(), clkOne = 0;
382 p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
383 // assert( Vec_PtrSize(p->vSolvers) == 0 );
384 // in the multi-output mode, mark trivial POs (those fed by const0) as solved
385 if ( p->pPars->fSolveAll )
386 Saig_ManForEachPo( p->pAig, pObj, iFrame )
387 if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
388 {
389 Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
390 p->pPars->nProveOuts++;
391 if ( p->pPars->fUseBridge )
392 Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
393 }
394 // create the first timeframe
395 p->pPars->timeLastSolved = Abc_Clock();
396
397 if ( Vec_VecSize(p->vClauses) == 0 )
398 Pdr_ManCreateSolver( p, (iFrame = 0) );
399 else {
400 iFrame = Vec_VecSize(p->vClauses) - 1;
401
402 if ( fCheckClauses )
403 {
404 if ( p->pPars->fVerbose )
405 Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
406 IPdr_ManCheckClauses( p );
407 if ( p->pPars->fVerbose )
408 Abc_Print( 1, " Passed!\n" ) ;
409 }
410
411 if ( fPushClauses )
412 {
413 p->iUseFrame = Abc_MaxInt(iFrame, 1);
414
415 if ( p->pPars->fVerbose )
416 {
417 Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
418 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
419 }
420
421 RetValue = Pdr_ManPushClauses( p );
422
423 if ( p->pPars->fVerbose )
424 {
425 Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
426 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
427 }
428
429 if ( RetValue )
430 {
431 Pdr_ManReportInvariant( p );
432 Pdr_ManVerifyInvariant( p );
433 return 1;
434 }
435 }
436
437 if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 )
438 {
439 assert( p->vAbsFlops == NULL );
440 p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
441 p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
442 p->vMapPpi2Ff = Vec_IntAlloc( 100 );
443
444 IPdr_ManRestoreAbsFlops( p );
445 }
446
447 }
448 while ( 1 )
449 {
450 int fRefined = 0;
451 if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
452 {
453// int i, Prio;
454 assert( p->vAbsFlops == NULL );
455 p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
456 p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
457 p->vMapPpi2Ff = Vec_IntAlloc( 100 );
458// Vec_IntForEachEntry( p->vPrio, Prio, i )
459// if ( Prio >> p->nPrioShift )
460// Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
461 }
462 //if ( p->pPars->fUseAbs && p->vAbsFlops )
463 // printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
464 p->nFrames = iFrame;
465 assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
466 p->iUseFrame = Abc_MaxInt(iFrame, 1);
467 Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
468 {
469 // skip disproved outputs
470 if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
471 continue;
472 // skip output whose time has run out
473 if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
474 continue;
475 // check if the output is trivially solved
476 if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
477 continue;
478 // check if the output is trivially solved
479 if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
480 {
481 if ( !p->pPars->fSolveAll )
482 {
483 pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
484 p->pAig->pSeqModel = pCexNew;
485 return 0; // SAT
486 }
487 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;
488 p->pPars->nFailOuts++;
489 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
490 if ( !p->pPars->fNotVerbose )
491 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
492 nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
493 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
494 if ( p->pPars->fUseBridge )
495 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
496 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
497 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
498 {
499 if ( p->pPars->fVerbose )
500 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
501 if ( !p->pPars->fSilent )
502 Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
503 p->pPars->iFrame = iFrame;
504 return -1;
505 }
506 if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
507 return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
508 p->pPars->timeLastSolved = Abc_Clock();
509 continue;
510 }
511 // try to solve this output
512 if ( p->pTime4Outs )
513 {
514 assert( p->pTime4Outs[p->iOutCur] > 0 );
515 clkOne = Abc_Clock();
516 p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
517 }
518 while ( 1 )
519 {
520 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
521 {
522 if ( p->pPars->fVerbose )
523 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
524 if ( !p->pPars->fSilent )
525 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
526 p->pPars->iFrame = iFrame;
527 return -1;
528 }
529 RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
530 if ( RetValue == 1 )
531 break;
532 if ( RetValue == -1 )
533 {
534 if ( p->pPars->fVerbose )
535 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
536 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
537 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
538 else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
539 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
540 else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
541 {
542 Pdr_QueueClean( p );
543 pCube = NULL;
544 break; // keep solving
545 }
546 else if ( p->pPars->nConfLimit )
547 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
548 else if ( p->pPars->fVerbose )
549 Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
550 p->pPars->iFrame = iFrame;
551 return -1;
552 }
553 if ( RetValue == 0 )
554 {
555 RetValue = Pdr_ManBlockCube( p, pCube );
556 if ( RetValue == -1 )
557 {
558 if ( p->pPars->fVerbose )
559 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
560 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
561 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
562 else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
563 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
564 else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
565 {
566 Pdr_QueueClean( p );
567 pCube = NULL;
568 break; // keep solving
569 }
570 else if ( p->pPars->nConfLimit )
571 Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
572 else if ( p->pPars->fVerbose )
573 Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
574 p->pPars->iFrame = iFrame;
575 return -1;
576 }
577 if ( RetValue == 0 )
578 {
579 if ( fPrintClauses )
580 {
581 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
582 Pdr_ManPrintClauses( p, 0 );
583 }
584 if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
585 Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
586 p->pPars->iFrame = iFrame;
587 if ( !p->pPars->fSolveAll )
588 {
589 abctime clk = Abc_Clock();
590 Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
591 p->tAbs += Abc_Clock() - clk;
592 if ( pCex == NULL )
593 {
594 assert( p->pPars->fUseAbs );
595 Pdr_QueueClean( p );
596 pCube = NULL;
597 fRefined = 1;
598 break; // keep solving
599 }
600 p->pAig->pSeqModel = pCex;
601
602 if ( p->pPars->fVerbose && p->pPars->fUseAbs )
603 Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
604 return 0; // SAT
605 }
606 p->pPars->nFailOuts++;
607 pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
608 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
609 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
610 if ( p->pPars->fUseBridge )
611 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
612 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
613 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
614 {
615 if ( p->pPars->fVerbose )
616 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
617 if ( !p->pPars->fSilent )
618 Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
619 p->pPars->iFrame = iFrame;
620 return -1;
621 }
622 if ( !p->pPars->fNotVerbose )
623 Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
624 nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
625 if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
626 return 0; // all SAT
627 Pdr_QueueClean( p );
628 pCube = NULL;
629 break; // keep solving
630 }
631 if ( p->pPars->fVerbose )
632 Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
633 }
634 }
635 if ( fRefined )
636 break;
637 if ( p->pTime4Outs )
638 {
639 abctime timeSince = Abc_Clock() - clkOne;
640 assert( p->pTime4Outs[p->iOutCur] > 0 );
641 p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
642 if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
643 {
644 p->pPars->nDropOuts++;
645 if ( p->pPars->vOutMap )
646 Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
647 if ( !p->pPars->fNotVerbose )
648 Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
649 }
650 p->timeToStopOne = 0;
651 }
652 }
653 /*
654 if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
655 {
656 int i, Used;
657 Vec_IntForEachEntry( p->vAbsFlops, Used, i )
658 if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
659 Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
660 }
661 */
662 if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
663 {
664 Pdr_Set_t * pSet;
665 int i, j, k;
666 Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 );
667 Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
668 for ( k = 0; k < pSet->nLits; k++ )
669 Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
670 }
671
672 if ( p->pPars->fVerbose )
673 Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
674 if ( fRefined )
675 continue;
676 //if ( p->pPars->fUseAbs && p->vAbsFlops )
677 // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
678 // open a new timeframe
679 p->nQueLim = p->pPars->nRestLimit;
680 assert( pCube == NULL );
681 Pdr_ManSetPropertyOutput( p, iFrame );
682 Pdr_ManCreateSolver( p, ++iFrame );
683 if ( fPrintClauses )
684 {
685 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
686 Pdr_ManPrintClauses( p, 0 );
687 }
688 // push clauses into this timeframe
689 RetValue = Pdr_ManPushClauses( p );
690 if ( RetValue == -1 )
691 {
692 if ( p->pPars->fVerbose )
693 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
694 if ( !p->pPars->fSilent )
695 {
696 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
697 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
698 else
699 Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame );
700 }
701 p->pPars->iFrame = iFrame;
702 return -1;
703 }
704 if ( RetValue )
705 {
706 if ( p->pPars->fVerbose )
707 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
708 if ( !p->pPars->fSilent )
709 Pdr_ManReportInvariant( p );
710 if ( !p->pPars->fSilent )
711 Pdr_ManVerifyInvariant( p );
712 p->pPars->iFrame = iFrame;
713 // count the number of UNSAT outputs
714 p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
715 // convert previously 'unknown' into 'unsat'
716 if ( p->pPars->vOutMap )
717 for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
718 if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
719 {
720 Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
721 if ( p->pPars->fUseBridge )
722 Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
723 }
724 if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
725 return 1; // UNSAT
726 if ( p->pPars->nFailOuts > 0 )
727 return 0; // SAT
728 return -1;
729 }
730 if ( p->pPars->fVerbose )
731 Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
732
733 // check termination
734 if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
735 {
736 p->pPars->iFrame = iFrame;
737 return -1;
738 }
739 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
740 {
741 if ( fPrintClauses )
742 {
743 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
744 Pdr_ManPrintClauses( p, 0 );
745 }
746 if ( p->pPars->fVerbose )
747 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
748 if ( !p->pPars->fSilent )
749 Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
750 p->pPars->iFrame = iFrame;
751 return -1;
752 }
753 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
754 {
755 if ( fPrintClauses )
756 {
757 Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
758 Pdr_ManPrintClauses( p, 0 );
759 }
760 if ( p->pPars->fVerbose )
761 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
762 if ( !p->pPars->fSilent )
763 Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
764 p->pPars->iFrame = iFrame;
765 return -1;
766 }
767 if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
768 {
769 if ( p->pPars->fVerbose )
770 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
771 if ( !p->pPars->fSilent )
772 Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
773 p->pPars->iFrame = iFrame;
774 return -1;
775 }
776 }
777 assert( 0 );
778 return -1;
779}
780
792int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
793{
794 Pdr_Man_t * p;
795 int k, RetValue;
796 Vec_Vec_t * vClausesSaved;
797
798 abctime clk = Abc_Clock();
799 if ( pPars->nTimeOutOne && !pPars->fSolveAll )
800 pPars->nTimeOutOne = 0;
801 if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
802 pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
803 if ( pPars->fVerbose )
804 {
805// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
806 Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
807 pPars->nRecycle,
808 pPars->nFrameMax,
809 pPars->nRestLimit,
810 pPars->nTimeOut );
811 Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
812 pPars->fMonoCnf ? "yes" : "no",
813 pPars->fSkipGeneral ? "yes" : "no",
814 pPars->fSolveAll ? "yes" : "no" );
815 }
816 ABC_FREE( pAig->pSeqModel );
817
818
819 p = Pdr_ManStart( pAig, pPars, NULL );
820 while ( 1 ) {
821 RetValue = IPdr_ManSolveInt( p, 1, 0 );
822
823 if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
824 vClausesSaved = IPdr_ManSaveClauses( p, 1 );
825
826 Pdr_ManStop( p );
827
828 p = Pdr_ManStart( pAig, pPars, NULL );
829 IPdr_ManRestoreClauses( p, vClausesSaved, NULL );
830
831 pPars->nFrameMax = pPars->nFrameMax << 1;
832
833 continue;
834 }
835
836 if ( RetValue == 0 )
837 assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
838 if ( p->vCexes )
839 {
840 assert( p->pAig->vSeqModelVec == NULL );
841 p->pAig->vSeqModelVec = p->vCexes;
842 p->vCexes = NULL;
843 }
844 if ( p->pPars->fDumpInv )
845 {
846 char * pFileName = pPars->pInvFileName ? pPars->pInvFileName : Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
847 Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
848 Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
849 }
850 else if ( RetValue == 1 )
851 Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
852
853 p->tTotal += Abc_Clock() - clk;
854 Pdr_ManStop( p );
855
856 break;
857 }
858
859
860 pPars->iFrame--;
861 // convert all -2 (unknown) entries into -1 (undec)
862 if ( pPars->vOutMap )
863 for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
864 if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
865 Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
866 if ( pPars->fUseBridge )
867 Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
868 return RetValue;
869}
870
871int IPdr_ManCheckCombUnsat( Pdr_Man_t * p )
872{
873 int iFrame, RetValue = -1;
874
875 Pdr_ManCreateSolver( p, (iFrame = 0) );
876 Pdr_ManCreateSolver( p, (iFrame = 1) );
877
878 p->nFrames = iFrame;
879 p->iUseFrame = Abc_MaxInt(iFrame, 1);
880
881 RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
882 return RetValue;
883}
884
885int IPdr_ManCheckCubeReduce( Pdr_Man_t * p, Vec_Ptr_t * vClauses, Pdr_Set_t * pCube, int nConfLimit )
886{
887 sat_solver * pSat;
888 Vec_Int_t * vLits, * vLitsA;
889 int Lit, RetValue = l_True;
890 int i;
891 Pdr_Set_t * pCla;
892 int iActVar = 0;
893 abctime clk = Abc_Clock();
894
895 pSat = Pdr_ManSolver( p, 1 );
896
897 if ( pCube == NULL ) // solve the property
898 {
899 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
900 RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
901 assert( RetValue == 1 );
902
903 vLitsA = Vec_IntStart( Vec_PtrSize( vClauses ) );
904 iActVar = Pdr_ManFreeVar( p, 1 );
905 for ( i = 1; i < Vec_PtrSize( vClauses ); ++i )
906 Pdr_ManFreeVar( p, 1 );
907 Vec_PtrForEachEntry( Pdr_Set_t *, vClauses, pCla, i )
908 {
909 vLits = Pdr_ManCubeToLits( p, 1, pCla, 1, 0 );
910 Lit = Abc_Var2Lit( iActVar + i, 1 );
911 Vec_IntPush( vLits, Lit );
912
913 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
914 assert( RetValue == 1 );
915 Vec_IntWriteEntry( vLitsA, i, Abc_Var2Lit( iActVar + i, 0 ) );
916 }
917 sat_solver_compress( pSat );
918
919 // solve
920 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLitsA), Vec_IntArray(vLitsA) + Vec_IntSize(vLitsA), nConfLimit, 0, 0, 0 );
921 Vec_IntFree( vLitsA );
922
923 if ( RetValue == l_Undef )
924 return -1;
925 }
926
927 assert( RetValue != l_Undef );
928 if ( RetValue == l_False ) // UNSAT
929 {
930 int ncorelits, *pcorelits;
931 Vec_Ptr_t * vTemp = NULL;
932 Vec_Bit_t * vMark = NULL;
933
934 ncorelits = sat_solver_final(pSat, &pcorelits);
935 Abc_Print( 1, "UNSAT at the last frame. nCores = %d (out of %d).", ncorelits, Vec_PtrSize( vClauses ) );
936 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
937
938 vTemp = Vec_PtrDup( vClauses );
939 vMark = Vec_BitStart( Vec_PtrSize( vClauses) );
940 Vec_PtrClear( vClauses );
941 for ( i = 0; i < ncorelits; ++i )
942 {
943 //Abc_Print( 1, "Core[%d] = lit(%d) = var(%d) = %d-th set\n", i, pcorelits[i], Abc_Lit2Var(pcorelits[i]), Abc_Lit2Var(pcorelits[i]) - iActVar );
944 Vec_BitWriteEntry( vMark, Abc_Lit2Var( pcorelits[i] ) - iActVar, 1 );
945 }
946
947 Vec_PtrForEachEntry( Pdr_Set_t *, vTemp, pCla, i )
948 {
949 if ( Vec_BitEntry( vMark, i ) )
950 {
951 Vec_PtrPush( vClauses, pCla );
952 continue;
953 }
954 Pdr_SetDeref( pCla );
955 }
956
957 Vec_PtrFree( vTemp );
958 Vec_BitFree( vMark );
959 RetValue = 1;
960 }
961 else // SAT
962 {
963 Abc_Print( 1, "SAT at the last frame." );
964 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
965 RetValue = 0;
966 }
967
968 return RetValue;
969}
970
971int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
972{
973 int iFrame, RetValue = -1;
974 Vec_Ptr_t * vLast = NULL;
975
976 Pdr_ManCreateSolver( p, (iFrame = 0) );
977 Pdr_ManCreateSolver( p, (iFrame = 1) );
978
979 p->nFrames = iFrame;
980 p->iUseFrame = Abc_MaxInt(iFrame, 1);
981
982 vLast = Vec_VecEntry( vClauses, Vec_VecSize( vClauses ) - 1 );
983 RetValue = IPdr_ManCheckCubeReduce( p, vLast, NULL, p->pPars->nConfLimit );
984 return RetValue;
985}
986
998int Abc_NtkDarIPdr ( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
999{
1000 int RetValue = -1;
1001 abctime clk = Abc_Clock();
1002 Aig_Man_t * pMan;
1003 pMan = Abc_NtkToDar( pNtk, 0, 1 );
1004
1005 RetValue = IPdr_ManSolve( pMan, pPars );
1006
1007 if ( RetValue == 1 )
1008 Abc_Print( 1, "Property proved. " );
1009 else
1010 {
1011 if ( RetValue == 0 )
1012 {
1013 if ( pMan->pSeqModel == NULL )
1014 Abc_Print( 1, "Counter-example is not available.\n" );
1015 else
1016 {
1017 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
1018 if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
1019 Abc_Print( 1, "Counter-example verification has FAILED.\n" );
1020 }
1021 }
1022 else if ( RetValue == -1 )
1023 Abc_Print( 1, "Property UNDECIDED. " );
1024 else
1025 assert( 0 );
1026 }
1027 ABC_PRT( "Time", Abc_Clock() - clk );
1028
1029
1030 ABC_FREE( pNtk->pSeqModel );
1031 pNtk->pSeqModel = pMan->pSeqModel;
1032 pMan->pSeqModel = NULL;
1033 if ( pNtk->vSeqModelVec )
1034 Vec_PtrFreeFree( pNtk->vSeqModelVec );
1035 pNtk->vSeqModelVec = pMan->vSeqModelVec;
1036 pMan->vSeqModelVec = NULL;
1037 Aig_ManStop( pMan );
1038 return RetValue;
1039}
1040
1044
1045
1046ABC_NAMESPACE_IMPL_END
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
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_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
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_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
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
Pdr_ManNewSolver
sat_solver * Pdr_ManNewSolver(sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)
Definition pdrCnf.c:439
Pdr_ManFreeVar
int Pdr_ManFreeVar(Pdr_Man_t *p, int k)
Definition pdrCnf.c:332
Pdr_ObjSatVar
int Pdr_ObjSatVar(Pdr_Man_t *p, int k, int Pol, Aig_Obj_t *pObj)
FUNCTION DECLARATIONS ///.
Definition pdrCnf.c:241
IPdr_ManCheckClauses
int IPdr_ManCheckClauses(Pdr_Man_t *p)
Definition pdrIncr.c:144
IPdr_ManSaveClauses
Vec_Vec_t * IPdr_ManSaveClauses(Pdr_Man_t *p, int fDropLast)
DECLARATIONS ///.
Definition pdrIncr.c:182
Pdr_ManBlockCube
int Pdr_ManBlockCube(Pdr_Man_t *p, Pdr_Set_t *pCube)
Definition pdrCore.c:1248
IPdr_ManSolveInt
int IPdr_ManSolveInt(Pdr_Man_t *p, int fCheckClauses, int fPushClauses)
Definition pdrIncr.c:373
IPdr_ManPushClausesK
Vec_Ptr_t * IPdr_ManPushClausesK(Pdr_Man_t *p, int k)
FUNCTION DEFINITIONS ///.
Definition pdrIncr.c:42
IPdr_ManReduceClauses
int IPdr_ManReduceClauses(Pdr_Man_t *p, Vec_Vec_t *vClauses)
Definition pdrIncr.c:971
IPdr_ManCheckCombUnsat
int IPdr_ManCheckCombUnsat(Pdr_Man_t *p)
Definition pdrIncr.c:871
IPdr_ManRebuildClauses
int IPdr_ManRebuildClauses(Pdr_Man_t *p, Vec_Vec_t *vClauses)
Definition pdrIncr.c:256
IPdr_ManRestoreAbsFlops
int IPdr_ManRestoreAbsFlops(Pdr_Man_t *p)
Definition pdrIncr.c:324
IPdr_ManRestoreClauses
int IPdr_ManRestoreClauses(Pdr_Man_t *p, Vec_Vec_t *vClauses, Vec_Int_t *vMap)
Definition pdrIncr.c:338
Gia_ManToBridgeResult
int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition utilBridge.c:287
Pdr_ManPushClauses
int Pdr_ManPushClauses(Pdr_Man_t *p)
Definition pdrCore.c:150
Abc_NtkToDar
ABC_NAMESPACE_IMPL_START Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition abcDar.c:237
Pdr_ManReduceClause
Pdr_Set_t * Pdr_ManReduceClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrCore.c:97
Abc_NtkDarIPdr
int Abc_NtkDarIPdr(Abc_Ntk_t *pNtk, Pdr_Par_t *pPars)
Definition pdrIncr.c:998
IPdr_ManSetSolver
sat_solver * IPdr_ManSetSolver(Pdr_Man_t *p, int k, int fSetPropOutput)
Definition pdrIncr.c:216
Gia_ManToBridgeAbort
int Gia_ManToBridgeAbort(FILE *pFile, int Size, unsigned char *pBuffer)
Definition utilBridge.c:178
IPdr_ManPrintClauses
void IPdr_ManPrintClauses(Vec_Vec_t *vClauses, int kStart, int nRegs)
Definition pdrIncr.c:113
IPdr_ManCheckCubeReduce
int IPdr_ManCheckCubeReduce(Pdr_Man_t *p, Vec_Ptr_t *vClauses, Pdr_Set_t *pCube, int nConfLimit)
Definition pdrIncr.c:885
IPdr_ManSolve
int IPdr_ManSolve(Aig_Man_t *pAig, Pdr_Par_t *pPars)
Definition pdrIncr.c:792
Pdr_ManDeriveInfinityClauses
Vec_Int_t * Pdr_ManDeriveInfinityClauses(Pdr_Man_t *p, int fReduce)
Definition pdrInv.c:595
Pdr_ManPrintClauses
void Pdr_ManPrintClauses(Pdr_Man_t *p, int kStart)
Definition pdrInv.c:244
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_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_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_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_ManSetPropertyOutput
void Pdr_ManSetPropertyOutput(Pdr_Man_t *p, int k)
Definition pdrSat.c:179
Pdr_ManReportInvariant
void Pdr_ManReportInvariant(Pdr_Man_t *p)
Definition pdrInv.c:477
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_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_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
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:281
zsat_solver_new_seed
sat_solver * zsat_solver_new_seed(double seed)
Definition satSolver.c:1202
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::pSeqModel
Abc_Cex_t * pSeqModel
Definition abc.h:199
Abc_Ntk_t_::vSeqModelVec
Vec_Ptr_t * vSeqModelVec
Definition abc.h:200
Pdr_Set_t_::Lits
int Lits[0]
Definition pdrInt.h:81
Pdr_Set_t_::nLits
int nLits
Definition pdrInt.h:80
counter
Definition walk.c:35
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
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
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_VecForEachEntry
#define Vec_VecForEachEntry(Type, vGlob, pEntry, i, k)
Definition vecVec.h:87
Vec_VecForEachLevelStart
#define Vec_VecForEachLevelStart(vGlob, vVec, i, LevelStart)
Definition vecVec.h:57
Vec_VecForEachLevelStartStop
#define Vec_VecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecVec.h:61
Vec_VecForEachEntryStartStop
#define Vec_VecForEachEntryStartStop(Type, vGlob, pEntry, i, k, LevelStart, LevelStop)
Definition vecVec.h:95
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42