1 /**CFile****************************************************************
2
3 FileName [pdrInv.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [Invariant computation, printing, verification.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "pdrInt.h"
22 #include "base/abc/abc.h" // for Abc_NtkCollectCioNames()
23 #include "base/main/main.h" // for Abc_FrameReadGlobalFrame()
24 #include "aig/ioa/ioa.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis []
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Pdr_ManPrintProgress(Pdr_Man_t * p,int fClose,abctime Time)48 void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
49 {
50 Vec_Ptr_t * vVec;
51 int i, ThisSize, Length, LengthStart;
52 if ( Vec_PtrSize(p->vSolvers) < 2 )
53 {
54 Abc_Print(1, "Frame " );
55 Abc_Print(1, "Clauses " );
56 Abc_Print(1, "Max Queue " );
57 Abc_Print(1, "Flops " );
58 Abc_Print(1, "Cex " );
59 Abc_Print(1, "Time" );
60 Abc_Print(1, "\n" );
61 return;
62 }
63 if ( Abc_FrameIsBatchMode() && !fClose )
64 return;
65 // count the total length of the printout
66 Length = 0;
67 Vec_VecForEachLevel( p->vClauses, vVec, i )
68 Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
69 // determine the starting point
70 LengthStart = Abc_MaxInt( 0, Length - 60 );
71 Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 );
72 ThisSize = 5;
73 if ( LengthStart > 0 )
74 {
75 Abc_Print( 1, " ..." );
76 ThisSize += 4;
77 }
78 Length = 0;
79 Vec_VecForEachLevel( p->vClauses, vVec, i )
80 {
81 if ( Length < LengthStart )
82 {
83 Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
84 continue;
85 }
86 Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
87 Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
88 ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
89 }
90 for ( i = ThisSize; i < 70; i++ )
91 Abc_Print( 1, " " );
92 Abc_Print( 1, "%5d", p->nQueMax );
93 Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
94 if ( p->pPars->fUseAbs )
95 Abc_Print( 1, "%4d", p->nCexes );
96 Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
97 if ( p->pPars->fSolveAll )
98 Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
99 if ( p->pPars->nTimeOutOne )
100 Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts );
101 Abc_Print( 1, "%s", fClose ? "\n":"\r" );
102 if ( fClose )
103 p->nQueMax = 0, p->nCexes = 0;
104 fflush( stdout );
105 }
106
107 /**Function*************************************************************
108
109 Synopsis [Counts how many times each flop appears in the set of cubes.]
110
111 Description []
112
113 SideEffects []
114
115 SeeAlso []
116
117 ***********************************************************************/
Pdr_ManCountFlops(Pdr_Man_t * p,Vec_Ptr_t * vCubes)118 Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
119 {
120 Vec_Int_t * vFlopCount;
121 Pdr_Set_t * pCube;
122 int i, n;
123 vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
124 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
125 {
126 if ( pCube->nRefs == -1 )
127 continue;
128 for ( n = 0; n < pCube->nLits; n++ )
129 {
130 assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
131 Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
132 }
133 }
134 return vFlopCount;
135 }
136
137 /**Function*************************************************************
138
139 Synopsis []
140
141 Description []
142
143 SideEffects []
144
145 SeeAlso []
146
147 ***********************************************************************/
Pdr_ManFindInvariantStart(Pdr_Man_t * p)148 int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
149 {
150 Vec_Ptr_t * vArrayK;
151 int k, kMax = Vec_PtrSize(p->vSolvers)-1;
152 Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
153 if ( Vec_PtrSize(vArrayK) == 0 )
154 return k;
155 // return -1;
156 // if there is no starting point (as in case of SAT or undecided), return the last frame
157 // Abc_Print( 1, "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
158 return kMax;
159 }
160
161 /**Function*************************************************************
162
163 Synopsis [Counts the number of variables used in the clauses.]
164
165 Description []
166
167 SideEffects []
168
169 SeeAlso []
170
171 ***********************************************************************/
Pdr_ManCollectCubes(Pdr_Man_t * p,int kStart)172 Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
173 {
174 Vec_Ptr_t * vResult;
175 Vec_Ptr_t * vArrayK;
176 Pdr_Set_t * pSet;
177 int i, j;
178 vResult = Vec_PtrAlloc( 100 );
179 Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
180 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
181 Vec_PtrPush( vResult, pSet );
182 return vResult;
183 }
184
185 /**Function*************************************************************
186
187 Synopsis []
188
189 Description []
190
191 SideEffects []
192
193 SeeAlso []
194
195 ***********************************************************************/
Pdr_ManCountFlopsInv(Pdr_Man_t * p)196 Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p )
197 {
198 int kStart = Pdr_ManFindInvariantStart(p);
199 Vec_Ptr_t *vCubes = Pdr_ManCollectCubes(p, kStart);
200 Vec_Int_t * vInv = Pdr_ManCountFlops( p, vCubes );
201 Vec_PtrFree(vCubes);
202 return vInv;
203 }
204
205 /**Function*************************************************************
206
207 Synopsis [Counts the number of variables used in the clauses.]
208
209 Description []
210
211 SideEffects []
212
213 SeeAlso []
214
215 ***********************************************************************/
Pdr_ManCountVariables(Pdr_Man_t * p,int kStart)216 int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
217 {
218 Vec_Int_t * vFlopCounts;
219 Vec_Ptr_t * vCubes;
220 int i, Entry, Counter = 0;
221 if ( p->vInfCubes == NULL )
222 vCubes = Pdr_ManCollectCubes( p, kStart );
223 else
224 vCubes = Vec_PtrDup( p->vInfCubes );
225 vFlopCounts = Pdr_ManCountFlops( p, vCubes );
226 Vec_IntForEachEntry( vFlopCounts, Entry, i )
227 Counter += (Entry > 0);
228 Vec_IntFreeP( &vFlopCounts );
229 Vec_PtrFree( vCubes );
230 return Counter;
231 }
232
233 /**Function*************************************************************
234
235 Synopsis []
236
237 Description []
238
239 SideEffects []
240
241 SeeAlso []
242
243 ***********************************************************************/
Pdr_ManPrintClauses(Pdr_Man_t * p,int kStart)244 void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
245 {
246 Vec_Ptr_t * vArrayK;
247 Pdr_Set_t * pCube;
248 int i, k, Counter = 0;
249 Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
250 {
251 Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
252 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
253 {
254 Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
255 Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
256 Abc_Print( 1, "\n" );
257 }
258 }
259 }
260
261 /**Function*************************************************************
262
263 Synopsis []
264
265 Description []
266
267 SideEffects []
268
269 SeeAlso []
270
271 ***********************************************************************/
Pdr_SetPrintOne(Pdr_Set_t * p)272 void Pdr_SetPrintOne( Pdr_Set_t * p )
273 {
274 int i;
275 Abc_Print(1, "Clause: {" );
276 for ( i = 0; i < p->nLits; i++ )
277 Abc_Print(1, " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) );
278 Abc_Print(1, " }\n" );
279 }
280
281 /**Function*************************************************************
282
283 Synopsis []
284
285 Description []
286
287 SideEffects []
288
289 SeeAlso []
290
291 ***********************************************************************/
Pdr_ManDupAigWithClauses(Aig_Man_t * p,Vec_Ptr_t * vCubes)292 Aig_Man_t * Pdr_ManDupAigWithClauses( Aig_Man_t * p, Vec_Ptr_t * vCubes )
293 {
294 Aig_Man_t * pNew;
295 Aig_Obj_t * pObj, * pObjNew, * pLit;
296 Pdr_Set_t * pCube;
297 int i, n;
298 // create the new manager
299 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
300 pNew->pName = Abc_UtilStrsav( p->pName );
301 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
302 // create the PIs
303 Aig_ManCleanData( p );
304 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
305 Aig_ManForEachCi( p, pObj, i )
306 pObj->pData = Aig_ObjCreateCi( pNew );
307 // create outputs for each cube
308 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
309 {
310 // Pdr_SetPrintOne( pCube );
311 pObjNew = Aig_ManConst1(pNew);
312 for ( n = 0; n < pCube->nLits; n++ )
313 {
314 assert( Abc_Lit2Var(pCube->Lits[n]) < Saig_ManRegNum(p) );
315 pLit = Aig_NotCond( Aig_ManCi(pNew, Saig_ManPiNum(p) + Abc_Lit2Var(pCube->Lits[n])), Abc_LitIsCompl(pCube->Lits[n]) );
316 pObjNew = Aig_And( pNew, pObjNew, pLit );
317 }
318 Aig_ObjCreateCo( pNew, pObjNew );
319 }
320 // duplicate internal nodes
321 Aig_ManForEachNode( p, pObj, i )
322 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
323 // add the POs
324 Saig_ManForEachLi( p, pObj, i )
325 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
326 Aig_ManCleanup( pNew );
327 Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
328 // check the resulting network
329 if ( !Aig_ManCheck(pNew) )
330 Abc_Print(1, "Aig_ManDupSimple(): The check has failed.\n" );
331 return pNew;
332 }
Pdr_ManDumpAig(Aig_Man_t * p,Vec_Ptr_t * vCubes)333 void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes )
334 {
335 Aig_Man_t * pNew = Pdr_ManDupAigWithClauses( p, vCubes );
336 Ioa_WriteAiger( pNew, "aig_with_clauses.aig", 0, 0 );
337 Aig_ManStop( pNew );
338 Abc_Print(1, "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" );
339 }
340
341 /**Function*************************************************************
342
343 Synopsis []
344
345 Description []
346
347 SideEffects []
348
349 SeeAlso []
350
351 ***********************************************************************/
Pdr_ManDumpClauses(Pdr_Man_t * p,char * pFileName,int fProved)352 void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
353 {
354 FILE * pFile;
355 Vec_Int_t * vFlopCounts;
356 Vec_Ptr_t * vCubes;
357 Pdr_Set_t * pCube;
358 char ** pNamesCi;
359 int i, kStart, Count = 0;
360 // create file
361 pFile = fopen( pFileName, "w" );
362 if ( pFile == NULL )
363 {
364 Abc_Print( 1, "Cannot open file \"%s\" for writing invariant.\n", pFileName );
365 return;
366 }
367 // collect cubes
368 kStart = Pdr_ManFindInvariantStart( p );
369 if ( fProved )
370 vCubes = Pdr_ManCollectCubes( p, kStart );
371 else
372 vCubes = Vec_PtrDup( p->vInfCubes );
373 Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
374 // Pdr_ManDumpAig( p->pAig, vCubes );
375 // count cubes
376 Count = 0;
377 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
378 {
379 if ( pCube->nRefs == -1 )
380 continue;
381 Count++;
382 }
383 // collect variable appearances
384 vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
385 // output the header
386 if ( fProved )
387 fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
388 else
389 fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
390 fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
391 fprintf( pFile, ".i %d\n", p->pPars->fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
392 fprintf( pFile, ".o 1\n" );
393 fprintf( pFile, ".p %d\n", Count );
394 // output flop names
395 pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
396 if ( pNamesCi )
397 {
398 fprintf( pFile, ".ilb" );
399 for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
400 if ( !p->pPars->fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
401 fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
402 fprintf( pFile, "\n" );
403 ABC_FREE( pNamesCi );
404 fprintf( pFile, ".ob inv\n" );
405 }
406 // output cubes
407 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
408 {
409 if ( pCube->nRefs == -1 )
410 continue;
411 Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
412 fprintf( pFile, " 1\n" );
413 }
414 fprintf( pFile, ".e\n\n" );
415 fclose( pFile );
416 Vec_IntFreeP( &vFlopCounts );
417 Vec_PtrFree( vCubes );
418 if ( fProved )
419 Abc_Print( 1, "Inductive invariant was written into file \"%s\".\n", pFileName );
420 else
421 Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
422 }
423
424 /**Function*************************************************************
425
426 Synopsis []
427
428 Description []
429
430 SideEffects []
431
432 SeeAlso []
433
434 ***********************************************************************/
Pdr_ManDumpString(Pdr_Man_t * p)435 Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
436 {
437 Vec_Str_t * vStr;
438 Vec_Int_t * vFlopCounts;
439 Vec_Ptr_t * vCubes;
440 Pdr_Set_t * pCube;
441 int i, kStart;
442 vStr = Vec_StrAlloc( 1000 );
443 // collect cubes
444 kStart = Pdr_ManFindInvariantStart( p );
445 if ( p->vInfCubes == NULL )
446 vCubes = Pdr_ManCollectCubes( p, kStart );
447 else
448 vCubes = Vec_PtrDup( p->vInfCubes );
449 Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
450 // collect variable appearances
451 vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
452 // output cubes
453 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
454 {
455 if ( pCube->nRefs == -1 )
456 continue;
457 Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
458 }
459 Vec_IntFreeP( &vFlopCounts );
460 Vec_PtrFree( vCubes );
461 Vec_StrPush( vStr, '\0' );
462 return vStr;
463 }
464
465
466 /**Function*************************************************************
467
468 Synopsis []
469
470 Description []
471
472 SideEffects []
473
474 SeeAlso []
475
476 ***********************************************************************/
Pdr_ManReportInvariant(Pdr_Man_t * p)477 void Pdr_ManReportInvariant( Pdr_Man_t * p )
478 {
479 Vec_Ptr_t * vCubes;
480 int kStart = Pdr_ManFindInvariantStart( p );
481 vCubes = Pdr_ManCollectCubes( p, kStart );
482 Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n",
483 kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns );
484 // Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
485 // kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
486 Vec_PtrFree( vCubes );
487 }
488
489 /**Function*************************************************************
490
491 Synopsis []
492
493 Description []
494
495 SideEffects []
496
497 SeeAlso []
498
499 ***********************************************************************/
Pdr_ManVerifyInvariant(Pdr_Man_t * p)500 void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
501 {
502 sat_solver * pSat;
503 Vec_Int_t * vLits;
504 Vec_Ptr_t * vCubes;
505 Pdr_Set_t * pCube;
506 int i, kStart, kThis, RetValue, Counter = 0;
507 abctime clk = Abc_Clock();
508 // collect cubes used in the inductive invariant
509 kStart = Pdr_ManFindInvariantStart( p );
510 vCubes = Pdr_ManCollectCubes( p, kStart );
511 // create solver with the cubes
512 kThis = Vec_PtrSize(p->vSolvers);
513 pSat = Pdr_ManCreateSolver( p, kThis );
514 // add the property output
515 // Pdr_ManSetPropertyOutput( p, kThis );
516 // add the clauses
517 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
518 {
519 vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
520 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
521 assert( RetValue );
522 sat_solver_compress( pSat );
523 }
524 // check each clause
525 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
526 {
527 vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
528 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
529 if ( RetValue != l_False )
530 {
531 Abc_Print( 1, "Verification of clause %d failed.\n", i );
532 Counter++;
533 }
534 }
535 if ( Counter )
536 Abc_Print( 1, "Verification of %d clauses has failed.\n", Counter );
537 else
538 {
539 Abc_Print( 1, "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
540 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
541 }
542 // sat_solver_delete( pSat );
543 Vec_PtrFree( vCubes );
544 }
545
546 /**Function*************************************************************
547
548 Synopsis []
549
550 Description []
551
552 SideEffects []
553
554 SeeAlso []
555
556 ***********************************************************************/
Pdr_ManDeriveMarkNonInductive(Pdr_Man_t * p,Vec_Ptr_t * vCubes)557 int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
558 {
559 sat_solver * pSat;
560 Vec_Int_t * vLits;
561 Pdr_Set_t * pCube;
562 int i, kThis, RetValue, fChanges = 0, Counter = 0;
563 // create solver with the cubes
564 kThis = Vec_PtrSize(p->vSolvers);
565 pSat = Pdr_ManCreateSolver( p, kThis );
566 // add the clauses
567 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
568 {
569 if ( pCube->nRefs == -1 ) // skip non-inductive
570 continue;
571 vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
572 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
573 assert( RetValue );
574 sat_solver_compress( pSat );
575 }
576 // check each clause
577 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
578 {
579 if ( pCube->nRefs == -1 ) // skip non-inductive
580 continue;
581 vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
582 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
583 if ( RetValue != l_False ) // mark as non-inductive
584 {
585 pCube->nRefs = -1;
586 fChanges = 1;
587 }
588 else
589 Counter++;
590 }
591 //Abc_Print(1, "Clauses = %d.\n", Counter );
592 //sat_solver_delete( pSat );
593 return fChanges;
594 }
Pdr_ManDeriveInfinityClauses(Pdr_Man_t * p,int fReduce)595 Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
596 {
597 Vec_Int_t * vResult;
598 Vec_Ptr_t * vCubes;
599 Pdr_Set_t * pCube;
600 int i, v, kStart;
601 // collect cubes used in the inductive invariant
602 kStart = Pdr_ManFindInvariantStart( p );
603 vCubes = Pdr_ManCollectCubes( p, kStart );
604 // refine as long as there are changes
605 if ( fReduce )
606 while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
607 // collect remaining clauses
608 vResult = Vec_IntAlloc( 1000 );
609 Vec_IntPush( vResult, 0 );
610 Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
611 {
612 if ( pCube->nRefs == -1 ) // skip non-inductive
613 continue;
614 Vec_IntAddToEntry( vResult, 0, 1 );
615 Vec_IntPush( vResult, pCube->nLits );
616 for ( v = 0; v < pCube->nLits; v++ )
617 Vec_IntPush( vResult, pCube->Lits[v] );
618 }
619 //Vec_PtrFree( vCubes );
620 Vec_PtrFreeP( &p->vInfCubes );
621 p->vInfCubes = vCubes;
622 Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
623 return vResult;
624 }
625
626
627
628 /**Function*************************************************************
629
630 Synopsis [Remove clauses while maintaining the invariant.]
631
632 Description []
633
634 SideEffects []
635
636 SeeAlso []
637
638 ***********************************************************************/
639 #define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
640
Pdr_InvMap(Vec_Int_t * vCounts)641 Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
642 {
643 int i, k = 0, Count;
644 Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
645 Vec_IntForEachEntry( vCounts, Count, i )
646 if ( Count )
647 Vec_IntWriteEntry( vMap, i, k++ );
648 return vMap;
649 }
Pdr_InvCounts(Vec_Int_t * vInv)650 Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
651 {
652 int i, k, * pCube, * pList = Vec_IntArray(vInv);
653 Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
654 Pdr_ForEachCube( pList, pCube, i )
655 for ( k = 0; k < pCube[0]; k++ )
656 Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
657 return vCounts;
658 }
Pdr_InvUsedFlopNum(Vec_Int_t * vInv)659 int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
660 {
661 Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
662 int nZeros = Vec_IntCountZero( vCounts );
663 Vec_IntFree( vCounts );
664 return Vec_IntEntryLast(vInv) - nZeros;
665 }
666
Pdr_InvPrintStr(Vec_Int_t * vInv,Vec_Int_t * vCounts)667 Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
668 {
669 Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
670 Vec_Int_t * vMap = Pdr_InvMap( vCounts );
671 int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
672 int i, k, * pCube, * pList = Vec_IntArray(vInv);
673 char * pBuffer = ABC_ALLOC( char, (size_t)(unsigned)nVars );
674 for ( i = 0; i < nVars; i++ )
675 pBuffer[i] = '-';
676 Pdr_ForEachCube( pList, pCube, i )
677 {
678 for ( k = 0; k < pCube[0]; k++ )
679 pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
680 for ( k = 0; k < nVars; k++ )
681 Vec_StrPush( vStr, pBuffer[k] );
682 Vec_StrPush( vStr, ' ' );
683 Vec_StrPush( vStr, '1' );
684 Vec_StrPush( vStr, '\n' );
685 for ( k = 0; k < pCube[0]; k++ )
686 pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
687 }
688 Vec_StrPush( vStr, '\0' );
689 ABC_FREE( pBuffer );
690 Vec_IntFree( vMap );
691 return vStr;
692 }
Pdr_InvPrint(Vec_Int_t * vInv,int fVerbose)693 void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose )
694 {
695 Abc_Print(1, "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
696 if ( fVerbose )
697 {
698 Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
699 Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
700 Abc_Print(1, "%s", Vec_StrArray( vStr ) );
701 Vec_IntFree( vCounts );
702 Vec_StrFree( vStr );
703 }
704 }
705
Pdr_InvCheck_int(Gia_Man_t * p,Vec_Int_t * vInv,int fVerbose,sat_solver * pSat,int fSkip)706 int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver * pSat, int fSkip )
707 {
708 int nBTLimit = 0;
709 int fCheckProperty = 1;
710 int i, k, status, nFailed = 0, nFailedOuts = 0;
711 // collect cubes
712 int * pCube, * pList = Vec_IntArray(vInv);
713 // create variables
714 Vec_Int_t * vLits = Vec_IntAlloc(100);
715 int iFoVarBeg = sat_solver_nvars(pSat) - Gia_ManRegNum(p);
716 int iFiVarBeg = 1 + Gia_ManPoNum(p);
717 // add cubes
718 Pdr_ForEachCube( pList, pCube, i )
719 {
720 // collect literals
721 Vec_IntClear( vLits );
722 for ( k = 0; k < pCube[0]; k++ )
723 if ( pCube[k+1] != -1 )
724 Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
725 if ( Vec_IntSize(vLits) == 0 )
726 {
727 Vec_IntFree( vLits );
728 return 1;
729 }
730 // add it to the solver
731 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
732 assert( status == 1 );
733 }
734 // verify property output
735 if ( fCheckProperty )
736 {
737 for ( i = 0; i < Gia_ManPoNum(p); i++ )
738 {
739 Vec_IntFill( vLits, 1, Abc_Var2Lit(1+i, 0) );
740 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
741 if ( status == l_Undef ) // timeout
742 break;
743 if ( status == l_True ) // sat - property fails
744 {
745 if ( fVerbose )
746 Abc_Print(1, "Coverage check failed for output %d.\n", i );
747 nFailedOuts++;
748 if ( fSkip )
749 {
750 Vec_IntFree( vLits );
751 return 1;
752 }
753 continue;
754 }
755 assert( status == l_False ); // unsat - property holds
756 }
757 }
758 // iterate through cubes in the direct order
759 Pdr_ForEachCube( pList, pCube, i )
760 {
761 // collect cube
762 Vec_IntClear( vLits );
763 for ( k = 0; k < pCube[0]; k++ )
764 if ( pCube[k+1] != -1 )
765 Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
766 // check if this cube intersects with the complement of other cubes in the solver
767 // if it does not intersect, then it is redundant and can be skipped
768 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
769 if ( status != l_True && fVerbose )
770 Abc_Print(1, "Finished checking clause %d (out of %d)...\r", i, pList[0] );
771 if ( status == l_Undef ) // timeout
772 break;
773 if ( status == l_False ) // unsat -- correct
774 continue;
775 assert( status == l_True );
776 if ( fVerbose )
777 Abc_Print(1, "Inductiveness check failed for clause %d.\n", i );
778 nFailed++;
779 if ( fSkip )
780 {
781 Vec_IntFree( vLits );
782 return 1;
783 }
784 }
785 Vec_IntFree( vLits );
786 return nFailed + nFailedOuts;
787 }
788
Pdr_InvCheck(Gia_Man_t * p,Vec_Int_t * vInv,int fVerbose)789 int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
790 {
791 int RetValue;
792 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
793 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
794 assert( sat_solver_nvars(pSat) == pCnf->nVars );
795 Cnf_DataFree( pCnf );
796 RetValue = Pdr_InvCheck_int( p, vInv, fVerbose, pSat, 0 );
797 sat_solver_delete( pSat );
798 return RetValue;
799 }
800
Pdr_InvMinimize(Gia_Man_t * p,Vec_Int_t * vInv,int fVerbose)801 Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
802 {
803 int nBTLimit = 0;
804 int fCheckProperty = 1;
805 abctime clk = Abc_Clock();
806 int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
807 Vec_Int_t * vRes = NULL;
808 // create SAT solver
809 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
810 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
811 int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
812 // create variables
813 Vec_Int_t * vLits = Vec_IntAlloc(100);
814 Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
815 int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
816 int iFiVarBeg = 1 + Gia_ManPoNum(p);
817 int iAuxVarBeg = sat_solver_nvars(pSat);
818 // allocate auxiliary variables
819 assert( sat_solver_nvars(pSat) == pCnf->nVars );
820 sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
821 // add clauses
822 Pdr_ForEachCube( pList, pCube, i )
823 {
824 // collect literals
825 Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
826 for ( k = 0; k < pCube[0]; k++ )
827 Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
828 // add it to the solver
829 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
830 assert( status == 1 );
831 }
832 // iterate through clauses
833 Pdr_ForEachCube( pList, pCube, i )
834 {
835 if ( Vec_BitEntry(vRemoved, i) )
836 continue;
837 // collect aux literals for remaining clauses
838 Vec_IntClear( vLits );
839 for ( k = 0; k < nCubes; k++ )
840 if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
841 Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
842 nLits = Vec_IntSize( vLits );
843 // check if the property still holds
844 if ( fCheckProperty )
845 {
846 for ( k = 0; k < Gia_ManPoNum(p); k++ )
847 {
848 Vec_IntShrink( vLits, nLits );
849 Vec_IntPush( vLits, Abc_Var2Lit(1+k, 0) );
850 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
851 if ( status == l_Undef ) // timeout
852 {
853 fFailed = 1;
854 break;
855 }
856 if ( status == l_True ) // sat - property fails
857 break;
858 assert( status == l_False ); // unsat - property holds
859 }
860 if ( fFailed )
861 break;
862 if ( k < Gia_ManPoNum(p) )
863 continue;
864 }
865 // check other clauses
866 fCannot = 0;
867 Pdr_ForEachCube( pList, pCube, n )
868 {
869 if ( Vec_BitEntry(vRemoved, n) || n == i )
870 continue;
871 // collect cube
872 Vec_IntShrink( vLits, nLits );
873 for ( k = 0; k < pCube[0]; k++ )
874 Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
875 // check if this cube intersects with the complement of other cubes in the solver
876 // if it does not intersect, then it is redundant and can be skipped
877 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
878 if ( status == l_Undef ) // timeout
879 {
880 fFailed = 1;
881 break;
882 }
883 if ( status == l_False ) // unsat -- correct
884 continue;
885 assert( status == l_True );
886 // cannot remove
887 fCannot = 1;
888 break;
889 }
890 if ( fFailed )
891 break;
892 if ( fCannot )
893 continue;
894 if ( fVerbose )
895 Abc_Print(1, "Removing clause %d.\n", i );
896 Vec_BitWriteEntry( vRemoved, i, 1 );
897 nRemoved++;
898 }
899 if ( nRemoved )
900 Abc_Print(1, "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes );
901 else
902 Abc_Print(1, "Invariant minimization did not change the invariant. " );
903 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
904 // cleanup cover
905 if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
906 {
907 vRes = Vec_IntAlloc( 1000 );
908 Vec_IntPush( vRes, nCubes-nRemoved );
909 Pdr_ForEachCube( pList, pCube, i )
910 if ( !Vec_BitEntry(vRemoved, i) )
911 for ( k = 0; k <= pCube[0]; k++ )
912 Vec_IntPush( vRes, pCube[k] );
913 Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
914 }
915 Cnf_DataFree( pCnf );
916 sat_solver_delete( pSat );
917 Vec_BitFree( vRemoved );
918 Vec_IntFree( vLits );
919 return vRes;
920 }
921
Pdr_InvMinimizeLits(Gia_Man_t * p,Vec_Int_t * vInv,int fVerbose)922 Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
923 {
924 Vec_Int_t * vRes = NULL;
925 abctime clk = Abc_Clock();
926 int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
927 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
928 sat_solver * pSat;
929 // sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
930 Pdr_ForEachCube( pList, pCube, i )
931 {
932 nLits += pCube[0];
933 for ( k = 0; k < pCube[0]; k++ )
934 {
935 int Save = pCube[k+1];
936 pCube[k+1] = -1;
937 //sat_solver_bookmark( pSat );
938 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
939 if ( Pdr_InvCheck_int(p, vInv, 0, pSat, 1) )
940 pCube[k+1] = Save;
941 else
942 {
943 if ( fVerbose )
944 Abc_Print(1, "Removing lit %d from clause %d.\n", k, i );
945 nRemoved++;
946 }
947 sat_solver_delete( pSat );
948 //sat_solver_rollback( pSat );
949 //sat_solver_bookmark( pSat );
950 }
951 }
952 Cnf_DataFree( pCnf );
953 //sat_solver_delete( pSat );
954 if ( nRemoved )
955 Abc_Print(1, "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits );
956 else
957 Abc_Print(1, "Invariant minimization did not change the invariant. " );
958 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
959 if ( nRemoved > 0 ) // finished without timeout and removed some lits
960 {
961 vRes = Vec_IntAlloc( 1000 );
962 Vec_IntPush( vRes, pList[0] );
963 Pdr_ForEachCube( pList, pCube, i )
964 {
965 int nLits = 0;
966 for ( k = 0; k < pCube[0]; k++ )
967 if ( pCube[k+1] != -1 )
968 nLits++;
969 Vec_IntPush( vRes, nLits );
970 for ( k = 0; k < pCube[0]; k++ )
971 if ( pCube[k+1] != -1 )
972 Vec_IntPush( vRes, pCube[k+1] );
973 }
974 Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
975 }
976 return vRes;
977 }
978
979 ////////////////////////////////////////////////////////////////////////
980 /// END OF FILE ///
981 ////////////////////////////////////////////////////////////////////////
982
983
984 ABC_NAMESPACE_IMPL_END
985
986