abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcBmc2.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcBmc2.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Simple BMC package.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcBmc2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sat/cnf/cnf.h"
22 #include "sat/bsat/satStore.h"
23 #include "proof/ssw/ssw.h"
24 #include "bmc.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 //#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
33 
34 typedef struct Saig_Bmc_t_ Saig_Bmc_t;
35 struct Saig_Bmc_t_
36 {
37  // parameters
38  int nFramesMax; // the max number of timeframes to consider
39  int nNodesMax; // the max number of nodes to add
40  int nConfMaxOne; // the max number of conflicts at a target
41  int nConfMaxAll; // the max number of conflicts for all targets
42  int fVerbose; // enables verbose output
43  // AIG managers
44  Aig_Man_t * pAig; // the user's AIG manager
45  Aig_Man_t * pFrm; // Frames manager
46  Vec_Int_t * vVisited; // nodes visited in Frames
47  // node mapping
48  int nObjs; // the largest number of an AIG object
49  Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
50  // SAT solver
51  sat_solver * pSat; // SAT solver
52  int nSatVars; // the number of used SAT variables
53  Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
54  int nStitchVars;
55  // subproblems
56  Vec_Ptr_t * vTargets; // targets to be solved in this interval
57  int iFramePrev; // previous frame
58  int iFrameLast; // last frame
59  int iOutputLast; // last output
60  int iFrameFail; // failed frame
61  int iOutputFail; // failed output
62 };
63 
64 static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
65 {
66 // return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );
67  Aig_Obj_t * pRes;
68  Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
69  int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
70  if ( iObjLit == -1 )
71  return NULL;
72  pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
73  if ( pRes == NULL )
74  Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
75  else
76  pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
77  return pRes;
78 }
79 static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode )
80 {
81 // Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );
82  Vec_Int_t * vFrame;
83  int iObjLit;
84  if ( i == Vec_PtrSize(p->vAig2Frm) )
85  Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
86  assert( i < Vec_PtrSize(p->vAig2Frm) );
87  vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
88  if ( pNode == NULL )
89  iObjLit = -1;
90  else
91  iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
92  Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
93 }
94 
95 static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); }
96 static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); }
97 
98 static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
99 static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); }
100 
101 ////////////////////////////////////////////////////////////////////////
102 /// FUNCTION DEFINITIONS ///
103 ////////////////////////////////////////////////////////////////////////
104 
105 #define ABS_ZER 1
106 #define ABS_ONE 2
107 #define ABS_UND 3
108 
109 static inline int Abs_ManSimInfoNot( int Value )
110 {
111  if ( Value == ABS_ZER )
112  return ABS_ONE;
113  if ( Value == ABS_ONE )
114  return ABS_ZER;
115  return ABS_UND;
116 }
117 
118 static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
119 {
120  if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
121  return ABS_ZER;
122  if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
123  return ABS_ONE;
124  return ABS_UND;
125 }
126 
127 static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
128 {
129  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
130  return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
131 }
132 
133 static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
134 {
135  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
136  assert( Value >= ABS_ZER && Value <= ABS_UND );
137  Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
138  pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
139 }
140 
141 /**Function*************************************************************
142 
143  Synopsis [Performs ternary simulation for one node.]
144 
145  Description []
146 
147  SideEffects []
148 
149  SeeAlso []
150 
151 ***********************************************************************/
152 int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
153 {
154  int Value0, Value1, Value;
155  Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
156  if ( Value )
157  return Value;
158  if ( Aig_ObjIsCi(pObj) )
159  {
160  assert( Saig_ObjIsLo(p, pObj) );
161  Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
162  Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
163  return Value;
164  }
165  Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
166  if ( Aig_ObjFaninC0(pObj) )
167  Value0 = Abs_ManSimInfoNot( Value0 );
168  if ( Aig_ObjIsCo(pObj) )
169  {
170  Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
171  return Value0;
172  }
173  assert( Aig_ObjIsNode(pObj) );
174  if ( Value0 == ABS_ZER )
175  Value = ABS_ZER;
176  else
177  {
178  Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
179  if ( Aig_ObjFaninC1(pObj) )
180  Value1 = Abs_ManSimInfoNot( Value1 );
181  Value = Abs_ManSimInfoAnd( Value0, Value1 );
182  }
183  Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
184  assert( Value );
185  return Value;
186 }
187 
188 /**Function*************************************************************
189 
190  Synopsis [Performs ternary simulation for one design.]
191 
192  Description [The returned array contains the result of ternary
193  simulation for all the frames where the output could be proved 0.]
194 
195  SideEffects []
196 
197  SeeAlso []
198 
199 ***********************************************************************/
200 Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
201 {
202  Vec_Ptr_t * vSimInfo;
203  Aig_Obj_t * pObj;
204  int i, f, nFramesLimit, nFrameWords;
205  abctime clk = Abc_Clock();
206  assert( Aig_ManRegNum(p) > 0 );
207  // the maximum number of frames will be determined to use at most 200Mb of RAM
208  nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
209  nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax );
210  nFrameWords = Abc_BitWordNum( 2 * Aig_ManObjNum(p) );
211  // allocate simulation info
212  vSimInfo = Vec_PtrAlloc( nFramesLimit );
213  for ( f = 0; f < nFramesLimit; f++ )
214  {
215  Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
216  if ( f == 0 )
217  {
218  Saig_ManForEachLo( p, pObj, i )
219  Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
220  }
221  Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
222  Saig_ManForEachPi( p, pObj, i )
223  Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
224  Saig_ManForEachPo( p, pObj, i )
225  Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
226  // check if simulation has derived at least one fail or unknown
227  Saig_ManForEachPo( p, pObj, i )
228  if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
229  {
230  if ( fVerbose )
231  {
232  printf( "Ternary sim found non-zero output in frame %d. Used %5.2f MB. ",
233  f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
234  ABC_PRT( "Time", Abc_Clock() - clk );
235  }
236  return vSimInfo;
237  }
238  }
239  if ( fVerbose )
240  {
241  printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f MB. ",
242  nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
243  ABC_PRT( "Time", Abc_Clock() - clk );
244  }
245  return vSimInfo;
246 }
247 
248 /**Function*************************************************************
249 
250  Synopsis [Free the array of simulation info.]
251 
252  Description []
253 
254  SideEffects []
255 
256  SeeAlso []
257 
258 ***********************************************************************/
259 void Abs_ManFreeAray( Vec_Ptr_t * p )
260 {
261  void * pTemp;
262  int i;
263  Vec_PtrForEachEntry( void *, p, pTemp, i )
264  ABC_FREE( pTemp );
265  Vec_PtrFree( p );
266 }
267 
268 
269 /**Function*************************************************************
270 
271  Synopsis [Create manager.]
272 
273  Description []
274 
275  SideEffects []
276 
277  SeeAlso []
278 
279 ***********************************************************************/
280 Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
281 {
282  Saig_Bmc_t * p;
283  Aig_Obj_t * pObj;
284  int i, Lit;
285 // assert( Aig_ManRegNum(pAig) > 0 );
286  p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
287  memset( p, 0, sizeof(Saig_Bmc_t) );
288  // set parameters
289  p->nFramesMax = nFramesMax;
290  p->nNodesMax = nNodesMax;
291  p->nConfMaxOne = nConfMaxOne;
292  p->nConfMaxAll = nConfMaxAll;
293  p->fVerbose = fVerbose;
294  p->pAig = pAig;
295  p->nObjs = Aig_ManObjNumMax(pAig);
296  // create node and variable mappings
297  p->vAig2Frm = Vec_PtrAlloc( 100 );
298  p->vObj2Var = Vec_IntAlloc( 0 );
299  Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
300  // start the AIG manager and map primary inputs
301  p->pFrm = Aig_ManStart( p->nObjs );
302  Saig_ManForEachLo( pAig, pObj, i )
303  Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) );
304  // create SAT solver
305  p->nSatVars = 1;
306  p->pSat = sat_solver_new();
307  p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart;
308  p->pSat->nLearntDelta = 5000;//p->pPars->nLearnedDelta;
309  p->pSat->nLearntRatio = 75;//p->pPars->nLearnedPerce;
310  p->pSat->nLearntMax = p->pSat->nLearntStart;
311  sat_solver_setnvars( p->pSat, 2000 );
312  Lit = toLit( p->nSatVars );
313  sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
314  Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
315  // other data structures
316  p->vTargets = Vec_PtrAlloc( 1000 );
317  p->vVisited = Vec_IntAlloc( 1000 );
318  p->iOutputFail = -1;
319  p->iFrameFail = -1;
320  return p;
321 }
322 
323 /**Function*************************************************************
324 
325  Synopsis [Delete manager.]
326 
327  Description []
328 
329  SideEffects []
330 
331  SeeAlso []
332 
333 ***********************************************************************/
334 void Saig_BmcManStop( Saig_Bmc_t * p )
335 {
336  Aig_ManStop( p->pFrm );
337  Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
338  Vec_IntFree( p->vObj2Var );
339  sat_solver_delete( p->pSat );
340  Vec_PtrFree( p->vTargets );
341  Vec_IntFree( p->vVisited );
342  ABC_FREE( p );
343 }
344 
345 /**Function*************************************************************
346 
347  Synopsis [Explores the possibility of constructing the output.]
348 
349  Description []
350 
351  SideEffects []
352 
353  SeeAlso []
354 
355 ***********************************************************************/
356 /*
357 Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
358 {
359  Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
360  pRes = Saig_BmcObjFrame( p, pObj, i );
361  if ( pRes != NULL )
362  return pRes;
363  if ( Saig_ObjIsPi( p->pAig, pObj ) )
364  pRes = AIG_VISITED;
365  else if ( Saig_ObjIsLo( p->pAig, pObj ) )
366  pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
367  else if ( Aig_ObjIsCo( pObj ) )
368  {
369  pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
370  if ( pRes != AIG_VISITED )
371  pRes = Saig_BmcObjChild0( p, pObj, i );
372  }
373  else
374  {
375  p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
376  if ( p0 != AIG_VISITED )
377  p0 = Saig_BmcObjChild0( p, pObj, i );
378  p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
379  if ( p1 != AIG_VISITED )
380  p1 = Saig_BmcObjChild1( p, pObj, i );
381 
382  if ( p0 == Aig_Not(p1) )
383  pRes = Aig_ManConst0(p->pFrm);
384  else if ( Aig_Regular(p0) == pConst1 )
385  pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
386  else if ( Aig_Regular(p1) == pConst1 )
387  pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
388  else
389  pRes = AIG_VISITED;
390 
391  if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
392  pRes = AIG_VISITED;
393  }
394  Saig_BmcObjSetFrame( p, pObj, i, pRes );
395  return pRes;
396 }
397 */
398 
399 /**Function*************************************************************
400 
401  Synopsis [Performs the actual construction of the output.]
402 
403  Description []
404 
405  SideEffects []
406 
407  SeeAlso []
408 
409 ***********************************************************************/
410 Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
411 {
412  Aig_Obj_t * pRes;
413  pRes = Saig_BmcObjFrame( p, pObj, i );
414  if ( pRes != NULL )
415  return pRes;
416  if ( Saig_ObjIsPi( p->pAig, pObj ) )
417  pRes = Aig_ObjCreateCi(p->pFrm);
418  else if ( Saig_ObjIsLo( p->pAig, pObj ) )
419  pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
420  else if ( Aig_ObjIsCo( pObj ) )
421  {
422  Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
423  pRes = Saig_BmcObjChild0( p, pObj, i );
424  }
425  else
426  {
427  Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
428  if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
429  pRes = Aig_ManConst0(p->pFrm);
430  else
431  {
432  Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
433  pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
434  }
435  }
436  assert( pRes != NULL );
437  Saig_BmcObjSetFrame( p, pObj, i, pRes );
438  Vec_IntPush( vVisited, Aig_ObjId(pObj) );
439  Vec_IntPush( vVisited, i );
440  return pRes;
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Adds new AIG nodes to the frames.]
446 
447  Description []
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 void Saig_BmcInterval( Saig_Bmc_t * p )
455 {
456  Aig_Obj_t * pTarget;
457  int i, iObj, iFrame;
458  int nNodes = Aig_ManObjNum( p->pFrm );
459  Vec_PtrClear( p->vTargets );
460  p->iFramePrev = p->iFrameLast;
461  for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
462  {
463  if ( p->iOutputLast == 0 )
464  {
465  Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
466  }
467  for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
468  {
469  if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
470  return;
471 // Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
472  Vec_IntClear( p->vVisited );
473  pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
474  Vec_PtrPush( p->vTargets, pTarget );
475  Aig_ObjCreateCo( p->pFrm, pTarget );
476  Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!!
477  // check if the node is gone
478  Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
479  Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
480  // it is not efficient to remove nodes, which may be used later!!!
481  }
482  }
483 }
484 
485 /**Function*************************************************************
486 
487  Synopsis [Performs the actual construction of the output.]
488 
489  Description []
490 
491  SideEffects []
492 
493  SeeAlso []
494 
495 ***********************************************************************/
496 Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
497 {
498  if ( pObj->pData )
499  return (Aig_Obj_t *)pObj->pData;
500  Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
501  if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
502  {
503  p->nStitchVars += !Aig_ObjIsCi(pObj);
504  return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew));
505  }
506  Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
507  Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
508  assert( pObj->pData == NULL );
509  return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
510 }
511 
512 /**Function*************************************************************
513 
514  Synopsis [Creates AIG of the newly added nodes.]
515 
516  Description []
517 
518  SideEffects []
519 
520  SeeAlso []
521 
522 ***********************************************************************/
523 Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
524 {
525  Aig_Man_t * pNew;
526  Aig_Obj_t * pObj, * pObjNew;
527  int i;
528  Aig_ManForEachObj( p->pFrm, pObj, i )
529  assert( pObj->pData == NULL );
530 
531  pNew = Aig_ManStart( p->nNodesMax );
532  Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
533  Vec_IntClear( p->vVisited );
534  Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
535  Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
536  {
537 // assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
538  pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
539  assert( !Aig_IsComplement(pObjNew) );
540  Aig_ObjCreateCo( pNew, pObjNew );
541  }
542  return pNew;
543 }
544 
545 /**Function*************************************************************
546 
547  Synopsis [Derives CNF for the newly added nodes.]
548 
549  Description []
550 
551  SideEffects []
552 
553  SeeAlso []
554 
555 ***********************************************************************/
556 void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
557 {
558  Aig_Obj_t * pObj, * pObjNew;
559  int i, Lits[2], VarNumOld, VarNumNew;
560  Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
561  {
562  // get the new variable of this node
563  pObjNew = (Aig_Obj_t *)pObj->pData;
564  pObj->pData = NULL;
565  VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
566  if ( VarNumNew == -1 )
567  continue;
568  // get the old variable of this node
569  VarNumOld = Saig_BmcSatNum( p, pObj );
570  if ( VarNumOld == 0 )
571  {
572  Saig_BmcSetSatNum( p, pObj, VarNumNew );
573  continue;
574  }
575  // add clauses connecting existing variables
576  Lits[0] = toLitCond( VarNumOld, 0 );
577  Lits[1] = toLitCond( VarNumNew, 1 );
578  if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
579  assert( 0 );
580  Lits[0] = toLitCond( VarNumOld, 1 );
581  Lits[1] = toLitCond( VarNumNew, 0 );
582  if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
583  assert( 0 );
584  }
585  // add CNF to the SAT solver
586  for ( i = 0; i < pCnf->nClauses; i++ )
587  if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
588  break;
589  if ( i < pCnf->nClauses )
590  printf( "SAT solver became UNSAT after adding clauses.\n" );
591 }
592 
593 /**Function*************************************************************
594 
595  Synopsis [Solves targets with the given resource limit.]
596 
597  Description []
598 
599  SideEffects []
600 
601  SeeAlso []
602 
603 ***********************************************************************/
604 void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
605 {
606  int k;
607  p->iOutputFail = p->iOutputLast;
608  p->iFrameFail = p->iFrameLast;
609  for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
610  {
611  if ( p->iOutputFail == 0 )
612  {
613  p->iOutputFail = Saig_ManPoNum(p->pAig);
614  p->iFrameFail--;
615  }
616  p->iOutputFail--;
617  }
618 }
619 
620 /**Function*************************************************************
621 
622  Synopsis [Solves targets with the given resource limit.]
623 
624  Description []
625 
626  SideEffects []
627 
628  SeeAlso []
629 
630 ***********************************************************************/
631 Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
632 {
633  Abc_Cex_t * pCex;
634  Aig_Obj_t * pObj, * pObjFrm;
635  int i, f, iVarNum;
636  // start the counter-example
637  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
638  pCex->iFrame = p->iFrameFail;
639  pCex->iPo = p->iOutputFail;
640  // copy the bit data
641  for ( f = 0; f <= p->iFrameFail; f++ )
642  {
643  Saig_ManForEachPi( p->pAig, pObj, i )
644  {
645  pObjFrm = Saig_BmcObjFrame( p, pObj, f );
646  if ( pObjFrm == NULL )
647  continue;
648  iVarNum = Saig_BmcSatNum( p, pObjFrm );
649  if ( iVarNum == 0 )
650  continue;
651  if ( sat_solver_var_value( p->pSat, iVarNum ) )
652  Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
653  }
654  }
655  // verify the counter example
656  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
657  {
658  printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
659  Abc_CexFree( pCex );
660  pCex = NULL;
661  }
662  return pCex;
663 }
664 
665 /**Function*************************************************************
666 
667  Synopsis [Solves targets with the given resource limit.]
668 
669  Description []
670 
671  SideEffects []
672 
673  SeeAlso []
674 
675 ***********************************************************************/
676 int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
677 {
678  Aig_Obj_t * pObj;
679  int i, k, VarNum, Lit, status, RetValue;
680  assert( Vec_PtrSize(p->vTargets) > 0 );
681  if ( p->pSat->qtail != p->pSat->qhead )
682  {
683  RetValue = sat_solver_simplify(p->pSat);
684  assert( RetValue != 0 );
685  }
686  Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
687  {
688  if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
689  continue;
690  if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
691  return l_Undef;
692  VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
693  Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
694  RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
695  if ( RetValue == l_False ) // unsat
696  {
697  // add final unit clause
698  Lit = lit_neg( Lit );
699  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
700  assert( status );
701  // add learned units
702  for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
703  {
704  Lit = veci_begin(&p->pSat->unit_lits)[k];
705  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
706  assert( status );
707  }
708  veci_resize(&p->pSat->unit_lits, 0);
709  // propagate units
710  sat_solver_compress( p->pSat );
711  continue;
712  }
713  if ( RetValue == l_Undef ) // undecided
714  return l_Undef;
715  // generate counter-example
716  Saig_BmcDeriveFailed( p, i );
717  p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
718 
719  {
720 // extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
721 // Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
722  }
723  return l_True;
724  }
725  return l_False;
726 }
727 
728 /**Function*************************************************************
729 
730  Synopsis []
731 
732  Description []
733 
734  SideEffects []
735 
736  SeeAlso []
737 
738 ***********************************************************************/
739 void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
740 {
741  Aig_Obj_t * pObj;
742  int i;
743  Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
744  Aig_ObjCreateCo( p->pFrm, pObj );
745  Aig_ManPrintStats( p->pFrm );
746  Aig_ManCleanup( p->pFrm );
747  Aig_ManPrintStats( p->pFrm );
748 }
749 
750 /**Function*************************************************************
751 
752  Synopsis [Performs BMC with the given parameters.]
753 
754  Description []
755 
756  SideEffects []
757 
758  SeeAlso []
759 
760 ***********************************************************************/
761 int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
762 {
763  Saig_Bmc_t * p;
764  Aig_Man_t * pNew;
765  Cnf_Dat_t * pCnf;
766  int nOutsSolved = 0;
767  int Iter, RetValue = -1;
768  abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
769  abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
770  int Status = -1;
771 /*
772  Vec_Ptr_t * vSimInfo;
773  vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
774  Abs_ManFreeAray( vSimInfo );
775 */
776  if ( fVerbose )
777  {
778  printf( "Running \"bmc2\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
779  Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
780  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
781  printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
782  nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
783  }
784  nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
785  p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
786  // set runtime limit
787  if ( nTimeOut )
788  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
789  for ( Iter = 0; ; Iter++ )
790  {
791  clk2 = Abc_Clock();
792  // add new logic interval to frames
793  Saig_BmcInterval( p );
794 // Saig_BmcAddTargetsAsPos( p );
795  if ( Vec_PtrSize(p->vTargets) == 0 )
796  break;
797  // convert logic slice into new AIG
798  pNew = Saig_BmcIntervalToAig( p );
799 //printf( "StitchVars = %d.\n", p->nStitchVars );
800  // derive CNF for the new AIG
801  pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
802  Cnf_DataLift( pCnf, p->nSatVars );
803  p->nSatVars += pCnf->nVars;
804  // add this CNF to the solver
805  Saig_BmcLoadCnf( p, pCnf );
806  Cnf_DataFree( pCnf );
807  Aig_ManStop( pNew );
808  // solve the targets
809  RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
810  if ( fVerbose )
811  {
812  printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ",
813  Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );
814  printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
815  printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
816  printf( "\n" );
817  fflush( stdout );
818  }
819  if ( RetValue != l_False )
820  break;
821  // check the timeout
822  if ( nTimeOut && Abc_Clock() > nTimeToStop )
823  {
824  if ( !fSilent )
825  printf( "Reached timeout (%d seconds).\n", nTimeOut );
826  if ( piFrames )
827  *piFrames = p->iFrameLast-1;
828  Saig_BmcManStop( p );
829  return Status;
830  }
831  }
832  if ( RetValue == l_True )
833  {
834  assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
835  if ( !fSilent )
836  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ",
837  p->iOutputFail, p->pAig->pName, p->iFrameFail );
838  Status = 0;
839  if ( piFrames )
840  *piFrames = p->iFrameFail - 1;
841  }
842  else // if ( RetValue == l_False || RetValue == l_Undef )
843  {
844  if ( !fSilent )
845  Abc_Print( 1, "No output failed in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) );
846  if ( piFrames )
847  {
848  if ( p->iOutputLast > 0 )
849  *piFrames = p->iFramePrev - 2;
850  else
851  *piFrames = p->iFramePrev - 1;
852  }
853  }
854  if ( !fSilent )
855  {
856  if ( fVerbOverwrite )
857  {
858  ABC_PRTr( "Time", Abc_Clock() - clk );
859  }
860  else
861  {
862  ABC_PRT( "Time", Abc_Clock() - clk );
863  }
864  if ( RetValue != l_True )
865  {
866  if ( p->iFrameLast >= p->nFramesMax )
867  printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
868  else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
869  printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
870  else if ( nTimeOut && Abc_Clock() > nTimeToStop )
871  printf( "Reached timeout (%d seconds).\n", nTimeOut );
872  else
873  printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
874  }
875  }
876  Saig_BmcManStop( p );
877  fflush( stdout );
878  return Status;
879 }
880 
881 
882 ////////////////////////////////////////////////////////////////////////
883 /// END OF FILE ///
884 ////////////////////////////////////////////////////////////////////////
885 
886 
887 ABC_NAMESPACE_IMPL_END
888 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Saig_Bmc_t_::nConfMaxOne
int nConfMaxOne
Definition: bmcBmc2.c:40
Saig_Bmc_t_::fVerbose
int fVerbose
Definition: bmcBmc2.c:42
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_Bmc_t_::iOutputLast
int iOutputLast
Definition: bmcBmc2.c:59
Saig_BmcIntervalToAig
Aig_Man_t * Saig_BmcIntervalToAig(Saig_Bmc_t *p)
Definition: bmcBmc2.c:523
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_Bmc_t_::nNodesMax
int nNodesMax
Definition: bmcBmc2.c:39
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
ABS_ONE
#define ABS_ONE
Definition: bmcBmc2.c:106
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
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
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
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Saig_Bmc_t_::nStitchVars
int nStitchVars
Definition: bmcBmc2.c:54
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
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
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
sat_solver_compress
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Abs_ManSimInfoAnd
static int Abs_ManSimInfoAnd(int Value0, int Value1)
Definition: bmcBmc2.c:118
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Saig_BmcSolveTargets
int Saig_BmcSolveTargets(Saig_Bmc_t *p, int nStart, int *pnOutsSolved)
Definition: bmcBmc2.c:676
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vec_IntSetEntry
static void Vec_IntSetEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:418
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
ABS_ZER
#define ABS_ZER
FUNCTION DEFINITIONS ///.
Definition: bmcBmc2.c:105
l_True
#define l_True
Definition: SolverTypes.h:84
Abs_ManSimInfoNot
static int Abs_ManSimInfoNot(int Value)
Definition: bmcBmc2.c:109
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Vec_IntGetEntry
static int Vec_IntGetEntry(Vec_Int_t *p, int i)
Definition: bblif.c:401
Saig_Bmc_t_::pSat
sat_solver * pSat
Definition: bmcBmc2.c:51
Saig_BmcAddTargetsAsPos
void Saig_BmcAddTargetsAsPos(Saig_Bmc_t *p)
Definition: bmcBmc2.c:739
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Abs_ManExtendOneEval_rec
int Abs_ManExtendOneEval_rec(Vec_Ptr_t *vSimInfo, Aig_Man_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc2.c:152
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Saig_BmcIntervalConstruct_rec
Aig_Obj_t * Saig_BmcIntervalConstruct_rec(Saig_Bmc_t *p, Aig_Obj_t *pObj, int i, Vec_Int_t *vVisited)
Definition: bmcBmc2.c:410
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Saig_Bmc_t_::nSatVars
int nSatVars
Definition: bmcBmc2.c:52
Saig_BmcLoadCnf
void Saig_BmcLoadCnf(Saig_Bmc_t *p, Cnf_Dat_t *pCnf)
Definition: bmcBmc2.c:556
Saig_BmcIntervalToAig_rec
Aig_Obj_t * Saig_BmcIntervalToAig_rec(Saig_Bmc_t *p, Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: bmcBmc2.c:496
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_Bmc_t_::nConfMaxAll
int nConfMaxAll
Definition: bmcBmc2.c:41
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
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
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Saig_Bmc_t_::nFramesMax
int nFramesMax
Definition: bmcBmc2.c:38
Saig_Bmc_t_::vVisited
Vec_Int_t * vVisited
Definition: bmcBmc2.c:46
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
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
Abs_ManSimInfoGet
static int Abs_ManSimInfoGet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc2.c:127
ABC_PRTr
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
Saig_Bmc_t_::vObj2Var
Vec_Int_t * vObj2Var
Definition: bmcBmc2.c:53
Saig_Bmc_t_::vTargets
Vec_Ptr_t * vTargets
Definition: bmcBmc2.c:56
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Saig_Bmc_t_::iFrameFail
int iFrameFail
Definition: bmcBmc2.c:60
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
if
if(last==0)
Definition: sparse_int.h:34
Saig_Bmc_t_::nObjs
int nObjs
Definition: bmcBmc2.c:48
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Saig_Bmc_t_::pAig
Aig_Man_t * pAig
Definition: bmcBmc2.c:44
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Saig_Bmc_t_::iFramePrev
int iFramePrev
Definition: bmcBmc2.c:57
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
ABS_UND
#define ABS_UND
Definition: bmcBmc2.c:107
Abs_ManSimInfoSet
static void Abs_ManSimInfoSet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
Definition: bmcBmc2.c:133
Saig_BmcObjFrame
static Aig_Obj_t * Saig_BmcObjFrame(Saig_Bmc_t *p, Aig_Obj_t *pObj, int i)
Definition: bmcBmc2.c:64
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_BmcObjSetFrame
static void Saig_BmcObjSetFrame(Saig_Bmc_t *p, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: bmcBmc2.c:79
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Saig_BmcSetSatNum
static void Saig_BmcSetSatNum(Saig_Bmc_t *p, Aig_Obj_t *pObj, int Num)
Definition: bmcBmc2.c:99
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Cnf_DataLift
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Saig_BmcDeriveFailed
void Saig_BmcDeriveFailed(Saig_Bmc_t *p, int iTargetFail)
Definition: bmcBmc2.c:604
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManLevelNum
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
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
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Saig_Bmc_t_::iFrameLast
int iFrameLast
Definition: bmcBmc2.c:58
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abs_ManFreeAray
void Abs_ManFreeAray(Vec_Ptr_t *p)
Definition: bmcBmc2.c:259
Saig_Bmc_t_
Definition: bmcBmc2.c:35
Saig_BmcPerform
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
Definition: bmcBmc2.c:761
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Saig_BmcSatNum
static int Saig_BmcSatNum(Saig_Bmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc2.c:98
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_BmcManStop
void Saig_BmcManStop(Saig_Bmc_t *p)
Definition: bmcBmc2.c:334
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Saig_BmcObjChild1
static Aig_Obj_t * Saig_BmcObjChild1(Saig_Bmc_t *p, Aig_Obj_t *pObj, int i)
Definition: bmcBmc2.c:96
Saig_BmcManStart
Saig_Bmc_t * Saig_BmcManStart(Aig_Man_t *pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose)
Definition: bmcBmc2.c:280
sat_solver_t
Definition: satSolver.h:91
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Saig_Bmc_t_::pFrm
Aig_Man_t * pFrm
Definition: bmcBmc2.c:45
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abs_ManTernarySimulate
Vec_Ptr_t * Abs_ManTernarySimulate(Aig_Man_t *p, int nFramesMax, int fVerbose)
Definition: bmcBmc2.c:200
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Saig_BmcInterval
void Saig_BmcInterval(Saig_Bmc_t *p)
Definition: bmcBmc2.c:454
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Saig_BmcObjChild0
static Aig_Obj_t * Saig_BmcObjChild0(Saig_Bmc_t *p, Aig_Obj_t *pObj, int i)
Definition: bmcBmc2.c:95
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Saig_Bmc_t_::vAig2Frm
Vec_Ptr_t * vAig2Frm
Definition: bmcBmc2.c:49
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
veci_begin
static int * veci_begin(veci *v)
Definition: satVec.h:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Saig_Bmc_t
typedefABC_NAMESPACE_IMPL_START struct Saig_Bmc_t_ Saig_Bmc_t
DECLARATIONS ///.
Definition: bmcBmc2.c:34
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
veci_size
static int veci_size(veci *v)
Definition: satVec.h:46
Saig_Bmc_t_::iOutputFail
int iOutputFail
Definition: bmcBmc2.c:61
Saig_BmcGenerateCounterExample
Abc_Cex_t * Saig_BmcGenerateCounterExample(Saig_Bmc_t *p)
Definition: bmcBmc2.c:631
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91