abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraClau.c
Go to the documentation of this file.
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
memset
char * memset()
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Cla_Man_t_::vCexBmc
Vec_Int_t * vCexBmc
Definition: fraClau.c:61
Cla_Man_t_::vCexBase
Vec_Int_t * vCexBase
Definition: fraClau.c:59
Fra_ClauMinimizeClause_rec
void Fra_ClauMinimizeClause_rec(Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
Definition: fraClau.c:515
Cla_Man_t_::pMapCsTestToNsTest
int * pMapCsTestToNsTest
Definition: fraClau.c:65
Fra_ClauSaveLatchVars
Vec_Int_t * Fra_ClauSaveLatchVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int fCsVars)
FUNCTION DEFINITIONS ///.
Definition: fraClau.c:84
Fra_ClauMinimizeClause
void Fra_ClauMinimizeClause(Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
Definition: fraClau.c:566
Cla_Man_t_::nSatVarsTestBeg
int nSatVarsTestBeg
Definition: fraClau.c:53
Cla_Man_t_::pMapCsTestToNsBmc
int * pMapCsTestToNsBmc
Definition: fraClau.c:66
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fra_ClauPrintClause
void Fra_ClauPrintClause(Vec_Int_t *vSatCsVars, Vec_Int_t *vCex)
Definition: fraClau.c:598
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Cla_Man_t_::pSatBmc
sat_solver * pSatBmc
Definition: fraClau.c:44
Cla_Man_t_::vCexMain0
Vec_Int_t * vCexMain0
Definition: fraClau.c:56
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition: vecInt.h:62
Fra_Clau
int Fra_Clau(Aig_Man_t *pMan, int nIters, int fVerbose, int fVeryVerbose)
Definition: fraClau.c:637
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Fra_ClauReduceClause
void Fra_ClauReduceClause(Vec_Int_t *vMain, Vec_Int_t *vNew)
Definition: fraClau.c:473
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Fra_ClauSaveInputVars
Vec_Int_t * Fra_ClauSaveInputVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int nStarting)
Definition: fraClau.c:128
Cnf_Dat_t_
Definition: cnf.h:56
Aig_ManFrames
Aig_Man_t * Aig_ManFrames(Aig_Man_t *pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t ***ppObjMap)
FUNCTION DEFINITIONS ///.
Definition: aigFrames.c:51
Fra_ClauSaveOutputVars
Vec_Int_t * Fra_ClauSaveOutputVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf)
Definition: fraClau.c:106
Cla_Man_t_::pSatMain
sat_solver * pSatMain
Definition: fraClau.c:42
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Fra_ClauCheckClause
int Fra_ClauCheckClause(Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
Definition: fraClau.c:425
Cla_Man_t_::pMapCsMainToCsTest
int * pMapCsMainToCsTest
Definition: fraClau.c:63
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
toLit
static lit toLit(int v)
Definition: satVec.h:142
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Vec_IntComplement
static void Vec_IntComplement(Vec_Int_t *vVec)
Definition: fraClau.c:327
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cla_Man_t_::vCexMain
Vec_Int_t * vCexMain
Definition: fraClau.c:57
Fra_ClauStop
void Fra_ClauStop(Cla_Man_t *p)
Definition: fraClau.c:178
Cla_Man_t_::vCexAssm
Vec_Int_t * vCexAssm
Definition: fraClau.c:60
Vec_IntPop
static int Vec_IntPop(Vec_Int_t *p)
Definition: extraZddTrunc.c:110
sat_solver_act_var_clear
static void sat_solver_act_var_clear(sat_solver *s)
Definition: satSolver.h:210
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntAppend
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
Definition: extraZddTrunc.c:126
Cla_Man_t_::vSatVarsMainCs
Vec_Int_t * vSatVarsMainCs
Definition: fraClau.c:48
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Aig_ObjChild0Flip
static void Aig_ObjChild0Flip(Aig_Obj_t *pObj)
Definition: aig.h:316
Cla_Man_t_::nSatVarsTestCur
int nSatVarsTestCur
Definition: fraClau.c:54
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Cla_Man_t_::pMapCsTestToCsMain
int * pMapCsTestToCsMain
Definition: fraClau.c:64
Fra_ClauStart
Cla_Man_t * Fra_ClauStart(Aig_Man_t *pMan)
Definition: fraClau.c:211
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Cla_Man_t_::vSatVarsTestNs
Vec_Int_t * vSatVarsTestNs
Definition: fraClau.c:50
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
Fra_ClauRemapClause
void Fra_ClauRemapClause(int *pMap, Vec_Int_t *vClause, Vec_Int_t *vRemapped, int fInv)
Definition: fraClau.c:402
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
sat_solver_var_literal
static int sat_solver_var_literal(sat_solver *s, int v)
Definition: satSolver.h:205
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cla_Man_t
typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_ Cla_Man_t
DECLARATIONS ///.
Definition: fraClau.c:38
Fra_ClauCreateMapping
int * Fra_ClauCreateMapping(Vec_Int_t *vSatVarsFrom, Vec_Int_t *vSatVarsTo, int nVarsMax)
Definition: fraClau.c:154
l_False
#define l_False
Definition: SolverTypes.h:85
Minisat::Var
int Var
Definition: SolverTypes.h:42
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Cla_Man_t_::vSatVarsTestCs
Vec_Int_t * vSatVarsTestCs
Definition: fraClau.c:49
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Cla_Man_t_::vCexTest
Vec_Int_t * vCexTest
Definition: fraClau.c:58
Cla_Man_t_::vSatVarsBmcNs
Vec_Int_t * vSatVarsBmcNs
Definition: fraClau.c:51
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_IntSplitHalf
static Vec_Int_t * Vec_IntSplitHalf(Vec_Int_t *vVec)
Definition: fraClau.c:304
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Cla_Man_t_::pSatTest
sat_solver * pSatTest
Definition: fraClau.c:43
Fra_ClauCheckBmc
int Fra_ClauCheckBmc(Cla_Man_t *p, Vec_Int_t *vClause)
Definition: fraClau.c:379
Cla_Man_t_
Definition: fraClau.c:39
Fra_ClauCheckProperty
int Fra_ClauCheckProperty(Cla_Man_t *p, Vec_Int_t *vCex)
Definition: fraClau.c:345