1 /**CFile****************************************************************
2
3 FileName [fraClau.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Induction with clause strengthening.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 /*
29 This code is inspired by the paper: Aaron Bradley and Zohar Manna,
30 "Checking safety by inductive generalization of counterexamples to
31 induction", FMCAD '07.
32 */
33
34 ////////////////////////////////////////////////////////////////////////
35 /// DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 typedef struct Cla_Man_t_ Cla_Man_t;
39 struct Cla_Man_t_
40 {
41 // SAT solvers
42 sat_solver * pSatMain;
43 sat_solver * pSatTest;
44 sat_solver * pSatBmc;
45 // CNF for the test solver
46 // Cnf_Dat_t * pCnfTest;
47 // SAT variables
48 Vec_Int_t * vSatVarsMainCs;
49 Vec_Int_t * vSatVarsTestCs;
50 Vec_Int_t * vSatVarsTestNs;
51 Vec_Int_t * vSatVarsBmcNs;
52 // helper variables
53 int nSatVarsTestBeg;
54 int nSatVarsTestCur;
55 // counter-examples
56 Vec_Int_t * vCexMain0;
57 Vec_Int_t * vCexMain;
58 Vec_Int_t * vCexTest;
59 Vec_Int_t * vCexBase;
60 Vec_Int_t * vCexAssm;
61 Vec_Int_t * vCexBmc;
62 // mapping of CS into NS var numbers
63 int * pMapCsMainToCsTest;
64 int * pMapCsTestToCsMain;
65 int * pMapCsTestToNsTest;
66 int * pMapCsTestToNsBmc;
67 };
68
69 ////////////////////////////////////////////////////////////////////////
70 /// FUNCTION DEFINITIONS ///
71 ////////////////////////////////////////////////////////////////////////
72
73 /**Function*************************************************************
74
75 Synopsis [Saves variables corresponding to latch outputs.]
76
77 Description []
78
79 SideEffects []
80
81 SeeAlso []
82
83 ***********************************************************************/
Fra_ClauSaveLatchVars(Aig_Man_t * pMan,Cnf_Dat_t * pCnf,int fCsVars)84 Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars )
85 {
86 Vec_Int_t * vVars;
87 Aig_Obj_t * pObjLo, * pObjLi;
88 int i;
89 vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) );
90 Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
91 Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] );
92 return vVars;
93 }
94
95 /**Function*************************************************************
96
97 Synopsis [Saves variables corresponding to latch outputs.]
98
99 Description []
100
101 SideEffects []
102
103 SeeAlso []
104
105 ***********************************************************************/
Fra_ClauSaveOutputVars(Aig_Man_t * pMan,Cnf_Dat_t * pCnf)106 Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
107 {
108 Vec_Int_t * vVars;
109 Aig_Obj_t * pObj;
110 int i;
111 vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) );
112 Aig_ManForEachCo( pMan, pObj, i )
113 Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
114 return vVars;
115 }
116
117 /**Function*************************************************************
118
119 Synopsis [Saves variables corresponding to latch outputs.]
120
121 Description []
122
123 SideEffects []
124
125 SeeAlso []
126
127 ***********************************************************************/
Fra_ClauSaveInputVars(Aig_Man_t * pMan,Cnf_Dat_t * pCnf,int nStarting)128 Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting )
129 {
130 Vec_Int_t * vVars;
131 Aig_Obj_t * pObj;
132 int i;
133 vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting );
134 Aig_ManForEachCi( pMan, pObj, i )
135 {
136 if ( i < nStarting )
137 continue;
138 Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
139 }
140 return vVars;
141 }
142
143 /**Function*************************************************************
144
145 Synopsis [Saves variables corresponding to latch outputs.]
146
147 Description []
148
149 SideEffects []
150
151 SeeAlso []
152
153 ***********************************************************************/
Fra_ClauCreateMapping(Vec_Int_t * vSatVarsFrom,Vec_Int_t * vSatVarsTo,int nVarsMax)154 int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax )
155 {
156 int * pMapping, Var, i;
157 assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
158 pMapping = ABC_ALLOC( int, nVarsMax );
159 for ( i = 0; i < nVarsMax; i++ )
160 pMapping[i] = -1;
161 Vec_IntForEachEntry( vSatVarsFrom, Var, i )
162 pMapping[Var] = Vec_IntEntry(vSatVarsTo,i);
163 return pMapping;
164 }
165
166
167 /**Function*************************************************************
168
169 Synopsis [Deletes the manager.]
170
171 Description []
172
173 SideEffects []
174
175 SeeAlso []
176
177 ***********************************************************************/
Fra_ClauStop(Cla_Man_t * p)178 void Fra_ClauStop( Cla_Man_t * p )
179 {
180 ABC_FREE( p->pMapCsMainToCsTest );
181 ABC_FREE( p->pMapCsTestToCsMain );
182 ABC_FREE( p->pMapCsTestToNsTest );
183 ABC_FREE( p->pMapCsTestToNsBmc );
184 Vec_IntFree( p->vSatVarsMainCs );
185 Vec_IntFree( p->vSatVarsTestCs );
186 Vec_IntFree( p->vSatVarsTestNs );
187 Vec_IntFree( p->vSatVarsBmcNs );
188 Vec_IntFree( p->vCexMain0 );
189 Vec_IntFree( p->vCexMain );
190 Vec_IntFree( p->vCexTest );
191 Vec_IntFree( p->vCexBase );
192 Vec_IntFree( p->vCexAssm );
193 Vec_IntFree( p->vCexBmc );
194 if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
195 if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
196 if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
197 ABC_FREE( p );
198 }
199
200 /**Function*************************************************************
201
202 Synopsis [Takes the AIG with the single output to be checked.]
203
204 Description []
205
206 SideEffects []
207
208 SeeAlso []
209
210 ***********************************************************************/
Fra_ClauStart(Aig_Man_t * pMan)211 Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
212 {
213 Cla_Man_t * p;
214 Cnf_Dat_t * pCnfMain;
215 Cnf_Dat_t * pCnfTest;
216 Cnf_Dat_t * pCnfBmc;
217 Aig_Man_t * pFramesMain;
218 Aig_Man_t * pFramesTest;
219 Aig_Man_t * pFramesBmc;
220 assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
221
222 // start the manager
223 p = ABC_ALLOC( Cla_Man_t, 1 );
224 memset( p, 0, sizeof(Cla_Man_t) );
225 p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
226 p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) );
227 p->vCexTest = Vec_IntAlloc( Aig_ManRegNum(pMan) );
228 p->vCexBase = Vec_IntAlloc( Aig_ManRegNum(pMan) );
229 p->vCexAssm = Vec_IntAlloc( Aig_ManRegNum(pMan) );
230 p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) );
231
232 // derive two timeframes to be checked
233 pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
234 //Aig_ManShow( pFramesMain, 0, NULL );
235 assert( Aig_ManCoNum(pFramesMain) == 2 );
236 Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output
237 pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
238 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
239 p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
240 /*
241 {
242 int i;
243 Aig_Obj_t * pObj;
244 Aig_ManForEachObj( pFramesMain, pObj, i )
245 printf( "%d -> %d \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] );
246 printf( "\n" );
247 }
248 */
249
250 // derive one timeframe to be checked
251 pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
252 assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) );
253 pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
254 p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
255 p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
256
257 // derive one timeframe to be checked for BMC
258 pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
259 //Aig_ManShow( pFramesBmc, 0, NULL );
260 assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
261 pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
262 p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
263
264 // create variable sets
265 p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) );
266 p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
267 p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
268 p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
269 assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) );
270 assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) );
271
272 // create mapping of CS into NS vars
273 p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) );
274 p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) );
275 p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) );
276 p->pMapCsTestToNsBmc = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs, Aig_ManObjNumMax(pFramesTest) );
277
278 // cleanup
279 Cnf_DataFree( pCnfMain );
280 Cnf_DataFree( pCnfTest );
281 Cnf_DataFree( pCnfBmc );
282 Aig_ManStop( pFramesMain );
283 Aig_ManStop( pFramesTest );
284 Aig_ManStop( pFramesBmc );
285 if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL )
286 {
287 Fra_ClauStop( p );
288 return NULL;
289 }
290 return p;
291 }
292
293 /**Function*************************************************************
294
295 Synopsis [Splits off second half and returns it as a new vector.]
296
297 Description []
298
299 SideEffects []
300
301 SeeAlso []
302
303 ***********************************************************************/
Vec_IntSplitHalf(Vec_Int_t * vVec)304 static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
305 {
306 Vec_Int_t * vPart;
307 int Entry, i;
308 assert( Vec_IntSize(vVec) > 1 );
309 vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 );
310 Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 )
311 Vec_IntPush( vPart, Entry );
312 Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 );
313 return vPart;
314 }
315
316 /**Function*************************************************************
317
318 Synopsis [Complements all literals in the clause.]
319
320 Description []
321
322 SideEffects []
323
324 SeeAlso []
325
326 ***********************************************************************/
Vec_IntComplement(Vec_Int_t * vVec)327 static void Vec_IntComplement( Vec_Int_t * vVec )
328 {
329 int i;
330 for ( i = 0; i < Vec_IntSize(vVec); i++ )
331 vVec->pArray[i] = lit_neg( vVec->pArray[i] );
332 }
333
334 /**Function*************************************************************
335
336 Synopsis [Checks if the property holds. Returns counter-example if not.]
337
338 Description []
339
340 SideEffects []
341
342 SeeAlso []
343
344 ***********************************************************************/
Fra_ClauCheckProperty(Cla_Man_t * p,Vec_Int_t * vCex)345 int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
346 {
347 int nBTLimit = 0;
348 int RetValue, iVar, i;
349 sat_solver_act_var_clear( p->pSatMain );
350 RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
351 Vec_IntClear( vCex );
352 if ( RetValue == l_False )
353 return 1;
354 assert( RetValue == l_True );
355 Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i )
356 Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) );
357 /*
358 {
359 int i;
360 for (i = 0; i < p->pSatMain->size; i++)
361 printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True );
362 printf( "\n" );
363 }
364 */
365 return 0;
366 }
367
368 /**Function*************************************************************
369
370 Synopsis [Checks if the clause holds using BMC.]
371
372 Description []
373
374 SideEffects []
375
376 SeeAlso []
377
378 ***********************************************************************/
Fra_ClauCheckBmc(Cla_Man_t * p,Vec_Int_t * vClause)379 int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
380 {
381 int nBTLimit = 0;
382 int RetValue;
383 RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause),
384 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
385 if ( RetValue == l_False )
386 return 1;
387 assert( RetValue == l_True );
388 return 0;
389 }
390
391 /**Function*************************************************************
392
393 Synopsis [Lifts the clause to depend on NS variables.]
394
395 Description []
396
397 SideEffects []
398
399 SeeAlso []
400
401 ***********************************************************************/
Fra_ClauRemapClause(int * pMap,Vec_Int_t * vClause,Vec_Int_t * vRemapped,int fInv)402 void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv )
403 {
404 int iLit, i;
405 Vec_IntClear( vRemapped );
406 Vec_IntForEachEntry( vClause, iLit, i )
407 {
408 assert( pMap[lit_var(iLit)] >= 0 );
409 iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv );
410 Vec_IntPush( vRemapped, iLit );
411 }
412 }
413
414 /**Function*************************************************************
415
416 Synopsis [Checks if the clause holds. Returns counter example if not.]
417
418 Description [Uses test SAT solver.]
419
420 SideEffects []
421
422 SeeAlso []
423
424 ***********************************************************************/
Fra_ClauCheckClause(Cla_Man_t * p,Vec_Int_t * vClause,Vec_Int_t * vCex)425 int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
426 {
427 int nBTLimit = 0;
428 int RetValue, iVar, i;
429 // complement literals
430 Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive
431 Vec_IntComplement( vClause ); // helper negative (the clause is C v h')
432 // add the clause
433 RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
434 assert( RetValue == 1 );
435 // complement all literals
436 Vec_IntPop( vClause ); // helper removed
437 Vec_IntComplement( vClause );
438 // create the assumption in terms of NS variables
439 Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 );
440 // add helper literals
441 for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ )
442 Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative
443 Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
444 // try to solve
445 RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm),
446 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
447 if ( vCex )
448 Vec_IntClear( vCex );
449 if ( RetValue == l_False )
450 return 1;
451 assert( RetValue == l_True );
452 if ( vCex )
453 {
454 Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i )
455 Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) );
456 }
457 return 0;
458 }
459
460 /**Function*************************************************************
461
462 Synopsis [Reduces the counter-example by removing complemented literals.]
463
464 Description [Removes literals from vMain that differ from those in the
465 counter-example (vNew). Relies on the fact that the PI variables are
466 assigned in the increasing order.]
467
468 SideEffects []
469
470 SeeAlso []
471
472 ***********************************************************************/
Fra_ClauReduceClause(Vec_Int_t * vMain,Vec_Int_t * vNew)473 void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
474 {
475 int LitM, LitN, VarM, VarN, i, j, k;
476 assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
477 for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
478 {
479 LitM = Vec_IntEntry( vMain, i );
480 LitN = Vec_IntEntry( vNew, j );
481 VarM = lit_var( LitM );
482 VarN = lit_var( LitN );
483 if ( VarM < VarN )
484 {
485 assert( 0 );
486 }
487 else if ( VarM > VarN )
488 {
489 j++;
490 }
491 else // if ( VarM == VarN )
492 {
493 i++;
494 j++;
495 if ( LitM == LitN )
496 Vec_IntWriteEntry( vMain, k++, LitM );
497 }
498 }
499 assert( i == Vec_IntSize(vMain) );
500 Vec_IntShrink( vMain, k );
501 }
502
503 /**Function*************************************************************
504
505 Synopsis [Computes the minimal invariant that holds.]
506
507 Description [On entrace, vBasis does not hold, vBasis+vExtra holds but
508 is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.]
509
510 SideEffects []
511
512 SeeAlso []
513
514 ***********************************************************************/
Fra_ClauMinimizeClause_rec(Cla_Man_t * p,Vec_Int_t * vBasis,Vec_Int_t * vExtra)515 void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
516 {
517 Vec_Int_t * vExtra2;
518 int nSizeOld;
519 if ( Vec_IntSize(vExtra) == 1 )
520 return;
521 nSizeOld = Vec_IntSize( vBasis );
522 vExtra2 = Vec_IntSplitHalf( vExtra );
523
524 // try the first half
525 Vec_IntAppend( vBasis, vExtra );
526 if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
527 {
528 Vec_IntShrink( vBasis, nSizeOld );
529 Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
530 return;
531 }
532 Vec_IntShrink( vBasis, nSizeOld );
533
534 // try the second half
535 Vec_IntAppend( vBasis, vExtra2 );
536 if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
537 {
538 Vec_IntShrink( vBasis, nSizeOld );
539 Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
540 return;
541 }
542 // Vec_IntShrink( vBasis, nSizeOld );
543
544 // find the smallest with the second half added
545 Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
546 Vec_IntShrink( vBasis, nSizeOld );
547 Vec_IntAppend( vBasis, vExtra );
548 // find the smallest with the second half added
549 Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
550 Vec_IntShrink( vBasis, nSizeOld );
551 Vec_IntAppend( vExtra, vExtra2 );
552 Vec_IntFree( vExtra2 );
553 }
554
555 /**Function*************************************************************
556
557 Synopsis [Minimizes the clauses using a simple method.]
558
559 Description [The input and output clause are in vExtra.]
560
561 SideEffects []
562
563 SeeAlso []
564
565 ***********************************************************************/
Fra_ClauMinimizeClause(Cla_Man_t * p,Vec_Int_t * vBasis,Vec_Int_t * vExtra)566 void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
567 {
568 int iLit, iLit2, i, k;
569 Vec_IntForEachEntryReverse( vExtra, iLit, i )
570 {
571 // copy literals without the given one
572 Vec_IntClear( vBasis );
573 Vec_IntForEachEntry( vExtra, iLit2, k )
574 if ( k != i )
575 Vec_IntPush( vBasis, iLit2 );
576 // try whether it is inductive
577 if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
578 continue;
579 // the clause is inductive
580 // remove the literal
581 for ( k = i; k < Vec_IntSize(vExtra)-1; k++ )
582 Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
583 Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
584 }
585 }
586
587 /**Function*************************************************************
588
589 Synopsis [Prints the clause.]
590
591 Description []
592
593 SideEffects []
594
595 SeeAlso []
596
597 ***********************************************************************/
Fra_ClauPrintClause(Vec_Int_t * vSatCsVars,Vec_Int_t * vCex)598 void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
599 {
600 int LitM, VarM, VarN, i, j, k;
601 assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) );
602 for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); )
603 {
604 LitM = Vec_IntEntry( vCex, i );
605 VarM = lit_var( LitM );
606 VarN = Vec_IntEntry( vSatCsVars, j );
607 if ( VarM < VarN )
608 {
609 assert( 0 );
610 }
611 else if ( VarM > VarN )
612 {
613 j++;
614 printf( "-" );
615 }
616 else // if ( VarM == VarN )
617 {
618 i++;
619 j++;
620 printf( "%d", !lit_sign(LitM) );
621 }
622 }
623 assert( i == Vec_IntSize(vCex) );
624 }
625
626 /**Function*************************************************************
627
628 Synopsis [Takes the AIG with the single output to be checked.]
629
630 Description []
631
632 SideEffects []
633
634 SeeAlso []
635
636 ***********************************************************************/
Fra_Clau(Aig_Man_t * pMan,int nIters,int fVerbose,int fVeryVerbose)637 int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
638 {
639 Cla_Man_t * p;
640 int Iter, RetValue, fFailed, i;
641 assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
642 // create the manager
643 p = Fra_ClauStart( pMan );
644 if ( p == NULL )
645 {
646 printf( "The property is trivially inductive.\n" );
647 return 1;
648 }
649 // generate counter-examples and expand them
650 for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ )
651 {
652 if ( fVerbose )
653 printf( "%4d : ", Iter );
654 // remap clause into the test manager
655 Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
656 if ( fVerbose && fVeryVerbose )
657 Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
658 // the main counter-example is in p->vCexMain
659 // intermediate counter-examples are in p->vCexTest
660 // generate the reduced counter-example to the inductive property
661 fFailed = 0;
662 for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ )
663 {
664 Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
665 Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
666
667 // if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
668 if ( Vec_IntSize(p->vCexMain) < 1 )
669 {
670 Vec_IntComplement( p->vCexMain0 );
671 RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) );
672 if ( RetValue == 0 )
673 {
674 printf( "\nProperty is proved after %d iterations.\n", Iter+1 );
675 return 0;
676 }
677 fFailed = 1;
678 break;
679 }
680 }
681 if ( fFailed )
682 {
683 if ( fVerbose )
684 printf( " Reducing failed after %d iterations (BMC failed).\n", i );
685 continue;
686 }
687 if ( Vec_IntSize(p->vCexMain) == 0 )
688 {
689 if ( fVerbose )
690 printf( " Reducing failed after %d iterations (nothing left).\n", i );
691 continue;
692 }
693 if ( fVerbose )
694 printf( " " );
695 if ( fVerbose && fVeryVerbose )
696 Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
697 if ( fVerbose )
698 printf( " LitsInd = %3d. ", Vec_IntSize(p->vCexMain) );
699 // minimize the inductive property
700 Vec_IntClear( p->vCexBase );
701 if ( Vec_IntSize(p->vCexMain) > 1 )
702 // Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
703 Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
704 assert( Vec_IntSize(p->vCexMain) > 0 );
705 if ( fVerbose && fVeryVerbose )
706 Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
707 if ( fVerbose )
708 printf( " LitsRed = %3d. ", Vec_IntSize(p->vCexMain) );
709 if ( fVerbose )
710 printf( "\n" );
711 // add the clause to the solver
712 Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 );
713 RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) );
714 if ( RetValue == 0 )
715 {
716 Iter++;
717 break;
718 }
719 if ( p->pSatMain->qtail != p->pSatMain->qhead )
720 {
721 RetValue = sat_solver_simplify(p->pSatMain);
722 assert( RetValue != 0 );
723 assert( p->pSatMain->qtail == p->pSatMain->qhead );
724 }
725 }
726
727 // report the results
728 if ( Iter == nIters )
729 {
730 printf( "Property is not proved after %d iterations.\n", nIters );
731 return 0;
732 }
733 printf( "Property is proved after %d iterations.\n", Iter );
734 Fra_ClauStop( p );
735 return 1;
736 }
737
738
739 ////////////////////////////////////////////////////////////////////////
740 /// END OF FILE ///
741 ////////////////////////////////////////////////////////////////////////
742
743
744 ABC_NAMESPACE_IMPL_END
745
746