abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcBmcAnd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcBmcAnd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Memory-efficient BMC engine]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcBmcAnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "aig/gia/giaAig.h"
23 #include "sat/bsat/satStore.h"
24 #include "sat/cnf/cnf.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 typedef struct Bmc_Mna_t_ Bmc_Mna_t;
34 struct Bmc_Mna_t_
35 {
36  Gia_Man_t * pFrames; // time frames
37  Cnf_Dat_t * pCnf; // CNF derived for the timeframes
38  Vec_Int_t * vPiMap; // maps unrolled GIA PIs into user GIA PIs
39  Vec_Int_t * vId2Var; // maps GIA IDs into SAT vars
40  Vec_Int_t * vInputs; // inputs of the cone
41  Vec_Int_t * vOutputs; // outputs of the cone
42  Vec_Int_t * vNodes; // internal nodes of the cone
43  sat_solver * pSat; // SAT solver
44  int nSatVars; // the counter of SAT variables
45  abctime clkStart; // starting time
46 };
47 
48 static inline int Gia_ManTerSimInfoGet( unsigned * pInfo, int i )
49 {
50  return 3 & (pInfo[i >> 4] >> ((i & 15) << 1));
51 }
52 static inline void Gia_ManTerSimInfoSet( unsigned * pInfo, int i, int Value )
53 {
54  assert( Value >= GIA_ZER && Value <= GIA_UND );
55  Value ^= Gia_ManTerSimInfoGet( pInfo, i );
56  pInfo[i >> 4] ^= (Value << ((i & 15) << 1));
57 }
58 
59 ////////////////////////////////////////////////////////////////////////
60 /// FUNCTION DEFINITIONS ///
61 ////////////////////////////////////////////////////////////////////////
62 
63 /**Function*************************************************************
64 
65  Synopsis [Performs ternary simulation of the manager.]
66 
67  Description []
68 
69  SideEffects []
70 
71  SeeAlso []
72 
73 ***********************************************************************/
74 Vec_Ptr_t * Bmc_MnaTernary( Gia_Man_t * p, int nFrames, int nFramesAdd, int fVerbose, int * iFirst )
75 {
76  Vec_Ptr_t * vStates;
77  unsigned * pState;
78  int nStateWords = Abc_BitWordNum( 2*Gia_ManCoNum(p) );
79  Gia_Obj_t * pObj, * pObjRo;
80  int f, i, Count[4];
81  abctime clk = Abc_Clock();
82  Gia_ManConst0(p)->Value = GIA_ZER;
83  Gia_ManForEachPi( p, pObj, i )
84  pObj->Value = GIA_UND;
85  Gia_ManForEachRi( p, pObj, i )
86  pObj->Value = GIA_ZER;
87  *iFirst = -1;
88  vStates = Vec_PtrAlloc( 100 );
89  for ( f = 0; ; f++ )
90  {
91  // if frames are given, break at frames
92  if ( nFrames && f == nFrames )
93  break;
94  // if frames are not given, break after nFramesAdd from the first x-valued
95  if ( !nFrames && *iFirst >= 0 && f == *iFirst + nFramesAdd )
96  break;
97  // aassign CI values
98  Gia_ManForEachRiRo( p, pObj, pObjRo, i )
99  pObjRo->Value = pObj->Value;
100  Gia_ManForEachAnd( p, pObj, i )
101  pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
102  // compute and save CO values
103  pState = ABC_ALLOC( unsigned, nStateWords );
104  Gia_ManForEachCo( p, pObj, i )
105  {
106  pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
107  Gia_ManTerSimInfoSet( pState, i, pObj->Value );
108  if ( *iFirst == -1 && i < Gia_ManPoNum(p) && pObj->Value == GIA_UND )
109  *iFirst = f;
110  }
111  Vec_PtrPush( vStates, pState );
112  // print statistics
113  if ( !fVerbose )
114  continue;
115  Count[0] = Count[1] = Count[2] = Count[3] = 0;
116  Gia_ManForEachRi( p, pObj, i )
117  Count[pObj->Value]++;
118  printf( "%5d : 0 =%7d 1 =%7d x =%7d all =%7d out = %s\n",
119  f, Count[GIA_ZER], Count[GIA_ONE], Count[GIA_UND], Gia_ManRegNum(p),
120  Gia_ManPo(p, 0)->Value == GIA_UND ? "x" : "0" );
121  }
122 // assert( Vec_PtrSize(vStates) == nFrames );
123  if ( fVerbose )
124  printf( "Finished %d frames. First x-valued PO is in frame %d. ", nFrames, *iFirst );
125  if ( fVerbose )
126  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
127  return vStates;
128 }
129 
130 
131 /**Function*************************************************************
132 
133  Synopsis [Collect AIG nodes for the group of POs.]
134 
135  Description []
136 
137  SideEffects []
138 
139  SeeAlso []
140 
141 ***********************************************************************/
142 void Bmc_MnaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, unsigned * pState )
143 {
144  if ( pObj->fPhase )
145  return;
146  pObj->fPhase = 1;
147  if ( Gia_ObjIsAnd(pObj) )
148  {
149  Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
150  Bmc_MnaCollect_rec( p, Gia_ObjFanin1(pObj), vNodes, pState );
151  pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
152  }
153  else if ( Gia_ObjIsRo(p, pObj) )
154  pObj->Value = pState ? Gia_ManTerSimInfoGet( pState, Gia_ObjCioId(Gia_ObjRoToRi(p, pObj)) ) : GIA_ZER;
155  else if ( Gia_ObjIsPi(p, pObj) )
156  pObj->Value = GIA_UND;
157  else assert( 0 );
158  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
159 }
160 void Bmc_MnaCollect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, unsigned * pState )
161 {
162  Gia_Obj_t * pObj;
163  int i;
164  Vec_IntClear( vNodes );
165  Gia_ManConst0(p)->fPhase = 1;
166  Gia_ManConst0(p)->Value = GIA_ZER;
167  Gia_ManForEachObjVec( vCos, p, pObj, i )
168  {
169  assert( Gia_ObjIsCo(pObj) );
170  Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
171  pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
172  assert( pObj->Value == GIA_UND );
173  }
174 }
175 
176 /**Function*************************************************************
177 
178  Synopsis [Select related logic cones for the COs.]
179 
180  Description []
181 
182  SideEffects []
183 
184  SeeAlso []
185 
186 ***********************************************************************/
187 void Bmc_MnaSelect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves )
188 {
189  if ( !pObj->fPhase )
190  return;
191  pObj->fPhase = 0;
192  assert( pObj->Value == GIA_UND );
193  if ( Gia_ObjIsAnd(pObj) )
194  {
195  if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
196  Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
197  else assert( Gia_ObjFanin0(pObj)->Value + Gia_ObjFaninC0(pObj) == GIA_ONE );
198  if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
199  Bmc_MnaSelect_rec( p, Gia_ObjFanin1(pObj), vLeaves );
200  else assert( Gia_ObjFanin1(pObj)->Value + Gia_ObjFaninC1(pObj) == GIA_ONE );
201  }
202  else if ( Gia_ObjIsRo(p, pObj) )
203  Vec_IntPush( vLeaves, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
204 }
205 void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
206 {
207  Gia_Obj_t * pObj;
208  int i;
209  Vec_IntClear( vLeaves );
210  Gia_ManForEachObjVec( vCos, p, pObj, i )
211  Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
212  Gia_ManConst0(p)->fPhase = 0;
213  Gia_ManForEachObjVec( vNodes, p, pObj, i )
214  pObj->fPhase = 0;
215 }
216 
217 /**Function*************************************************************
218 
219  Synopsis [Build AIG for the selected cones.]
220 
221  Description []
222 
223  SideEffects []
224 
225  SeeAlso []
226 
227 ***********************************************************************/
228 void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
229 {
230  if ( !pObj->fPhase )
231  return;
232  pObj->fPhase = 0;
233  assert( pObj->Value == GIA_UND );
234  if ( Gia_ObjIsAnd(pObj) )
235  {
236  int iLit0 = 1, iLit1 = 1;
237  if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
238  Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
239  if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
240  Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap, vPiMap );
241  if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
242  iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
243  if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
244  iLit1 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId1p(p, pObj)), Gia_ObjFaninC1(pObj) );
245  Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManHashAnd(pNew, iLit0, iLit1) );
246  }
247  else if ( Gia_ObjIsRo(p, pObj) )
248  assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 );
249  else if ( Gia_ObjIsPi(p, pObj) )
250  {
251  Vec_IntPush( vPiMap, Gia_ObjCioId(pObj) );
252  Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
253  }
254  else assert( 0 );
255 }
256 void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
257 {
258  Gia_Obj_t * pObj;
259  int i, iLit;
260  Gia_ManForEachObjVec( vCos, p, pObj, i )
261  {
262  assert( Gia_ObjIsCo(pObj) );
263  Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
264  iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
265  Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit );
266  }
267  Gia_ManConst0(p)->fPhase = 0;
268  Gia_ManForEachObjVec( vNodes, p, pObj, i )
269  pObj->fPhase = 0;
270 }
271 
272 
273 /**Function*************************************************************
274 
275  Synopsis [Compute the first non-trivial timeframe.]
276 
277  Description []
278 
279  SideEffects []
280 
281  SeeAlso []
282 
283 ***********************************************************************/
284 Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose, Vec_Int_t ** pvPiMap )
285 {
286  Gia_Obj_t * pObj;
287  Gia_Man_t * pNew, * pTemp;
288  Vec_Ptr_t * vStates, * vBegins;
289  Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap;
290  unsigned * pStateF, * pStateP;
291  int f, i, iFirst;
292  Gia_ManCleanPhase( pGia );
293  vCone = Vec_IntAlloc( 1000 );
294  vLeaves = Vec_IntAlloc( 1000 );
295  // perform ternary simulation
296  vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst );
297  // go backward
298  *pvPiMap = Vec_IntAlloc( 1000 );
299  vBegins = Vec_PtrStart( Vec_PtrSize(vStates) );
300  for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- )
301  {
302  // get ternary states
303  pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
304  pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
305  // collect roots of this frame
306  vRoots = Vec_IntAlloc( 100 );
307  Gia_ManForEachPo( pGia, pObj, i )
308  if ( Gia_ManTerSimInfoGet( pStateF, Gia_ObjCioId(pObj) ) == GIA_UND )
309  Vec_IntPush( vRoots, Gia_ObjId(pGia, pObj) );
310  // add leaves from the previous frame
311  Vec_IntAppend( vRoots, vLeaves );
312  Vec_PtrWriteEntry( vBegins, f, vRoots );
313  // find the cone
314  Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
315  Bmc_MnaSelect( pGia, vRoots, vCone, vLeaves ); // computes vLeaves
316  if ( fVerbose )
317  printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n",
318  f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
319  if ( Vec_IntSize(vLeaves) == 0 )
320  break;
321  // it is possible that some of the POs are still ternary...
322  }
323  assert( f >= 0 );
324  // go forward
325  vMap = Vec_IntStartFull( Gia_ManObjNum(pGia) );
326  pNew = Gia_ManStart( 10000 );
327  pNew->pName = Abc_UtilStrsav( pGia->pName );
328  Gia_ManHashStart( pNew );
329  for ( f = 0; f < Vec_PtrSize(vStates); f++ )
330  {
331  vRoots = (Vec_Int_t *)Vec_PtrEntry( vBegins, f );
332  if ( vRoots == NULL )
333  {
334  Gia_ManForEachPo( pGia, pObj, i )
335  Gia_ManAppendCo( pNew, 0 );
336  continue;
337  }
338  // get ternary states
339  pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
340  pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
341  // clean POs
342  Gia_ManForEachPo( pGia, pObj, i )
343  Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 );
344  // find the cone
345  Vec_IntPush( *pvPiMap, -f-1 );
346  Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
347  Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap, *pvPiMap ); // computes pNew
348  if ( fVerbose )
349  printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n",
350  f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
351  // create POs
352  Gia_ManForEachPo( pGia, pObj, i )
353  Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
354  // set a new map
355  Gia_ManForEachObjVec( vRoots, pGia, pObj, i )
356  if ( Gia_ObjIsRi(pGia, pObj) )
357  Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, Gia_ObjRiToRo(pGia, pObj)), Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
358 // else if ( Gia_ObjIsPo(pGia, pObj) )
359 // Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
360 // else assert( 0 );
361  }
362  Gia_ManHashStop( pNew );
363  Vec_VecFree( (Vec_Vec_t *)vBegins );
364  Vec_PtrFreeFree( vStates );
365  Vec_IntFree( vLeaves );
366  Vec_IntFree( vCone );
367  Vec_IntFree( vMap );
368  // cleanup
369 // Gia_ManPrintStats( pNew, NULL );
370  pNew = Gia_ManCleanup( pTemp = pNew );
371  Gia_ManStop( pTemp );
372 // Gia_ManPrintStats( pNew, NULL );
373  return pNew;
374 }
375 
376 
377 
378 /**Function*************************************************************
379 
380  Synopsis [BMC manager manipulation.]
381 
382  Description []
383 
384  SideEffects []
385 
386  SeeAlso []
387 
388 ***********************************************************************/
389 Bmc_Mna_t * Bmc_MnaAlloc()
390 {
391  Bmc_Mna_t * p;
392  p = ABC_CALLOC( Bmc_Mna_t, 1 );
393  p->vId2Var = Vec_IntAlloc( 0 );
394  p->vInputs = Vec_IntAlloc( 1000 );
395  p->vOutputs = Vec_IntAlloc( 1000 );
396  p->vNodes = Vec_IntAlloc( 10000 );
397  p->pSat = sat_solver_new();
398  p->nSatVars = 1;
399  p->clkStart = Abc_Clock();
400  sat_solver_setnvars( p->pSat, 1000 );
401  return p;
402 }
403 void Bmc_MnaFree( Bmc_Mna_t * p )
404 {
405  Cnf_DataFree( p->pCnf );
406  Vec_IntFreeP( &p->vPiMap );
407  Vec_IntFreeP( &p->vId2Var );
408  Vec_IntFreeP( &p->vInputs );
409  Vec_IntFreeP( &p->vOutputs );
410  Vec_IntFreeP( &p->vNodes );
411  sat_solver_delete( p->pSat );
412  ABC_FREE( p );
413 }
414 
415 /**Function*************************************************************
416 
417  Synopsis [Derives GIA for the given cone.]
418 
419  Description []
420 
421  SideEffects []
422 
423  SeeAlso []
424 
425 ***********************************************************************/
426 Gia_Man_t * Gia_ManBmcDupCone( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts )
427 {
428  Gia_Man_t * pNew;
429  Vec_Int_t * vTempIn, * vTempNode;
430  Gia_Obj_t * pObj;
431  int i;
432  // save values
433  vTempIn = Vec_IntAlloc( Vec_IntSize(vIns) );
434  Gia_ManForEachObjVec( vIns, p, pObj, i )
435  Vec_IntPush( vTempIn, pObj->Value );
436  // save values
437  vTempNode = Vec_IntAlloc( Vec_IntSize(vNodes) );
438  Gia_ManForEachObjVec( vNodes, p, pObj, i )
439  Vec_IntPush( vTempNode, pObj->Value );
440  // derive new GIA
441  pNew = Gia_ManDupFromVecs( p, vIns, vNodes, vOuts, 0 );
442  // reset values
443  Gia_ManForEachObjVec( vIns, p, pObj, i )
444  pObj->Value = Vec_IntEntry( vTempIn, i );
445  // reset values
446  Gia_ManForEachObjVec( vNodes, p, pObj, i )
447  pObj->Value = Vec_IntEntry( vTempNode, i );
448  // reset values
449  Gia_ManForEachObjVec( vOuts, p, pObj, i )
450  pObj->Value = 0;
451  Vec_IntFree( vTempIn );
452  Vec_IntFree( vTempNode );
453  return pNew;
454 }
455 
456 /**Function*************************************************************
457 
458  Synopsis [Derives GIA for the given cone.]
459 
460  Description []
461 
462  SideEffects []
463 
464  SeeAlso []
465 
466 ***********************************************************************/
467 int Gia_ManBmcAssignVarIds( Bmc_Mna_t * p, Vec_Int_t * vIns, Vec_Int_t * vUsed, Vec_Int_t * vOuts )
468 {
469  int i, iObj, VarC0 = p->nSatVars++;
470  Vec_IntForEachEntry( vIns, iObj, i )
471  if ( Vec_IntEntry( p->vId2Var, iObj ) == 0 )
472  Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
473  Vec_IntForEachEntryReverse( vUsed, iObj, i )
474  {
475  assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
476  Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
477  }
478  Vec_IntForEachEntry( vOuts, iObj, i )
479  {
480  assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
481  Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
482  }
483  // extend the SAT solver
484  if ( p->nSatVars > sat_solver_nvars(p->pSat) )
485  sat_solver_setnvars( p->pSat, p->nSatVars );
486  return VarC0;
487 }
488 
489 /**Function*************************************************************
490 
491  Synopsis [Derives CNF for the given cone.]
492 
493  Description []
494 
495  SideEffects []
496 
497  SeeAlso []
498 
499 ***********************************************************************/
500 void Gia_ManBmcAddCnf( Bmc_Mna_t * p, Gia_Man_t * pGia, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts )
501 {
502  Gia_Man_t * pNew = Gia_ManBmcDupCone( pGia, vIns, vNodes, vOuts );
503  Aig_Man_t * pAig = Gia_ManToAigSimple( pNew );
504  Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
505  Vec_Int_t * vUsed, * vMap;
506  Gia_Obj_t * pObj;
507  int i, iObj, VarC0;
508  // collect used variables
509  vUsed = Vec_IntAlloc( pCnf->nVars - Vec_IntSize(vIns) - Vec_IntSize(vOuts) );
510  Gia_ManForEachAnd( pNew, pObj, i )
511  if ( pCnf->pVarNums[i] >= 0 )
512  Vec_IntPush( vUsed, Vec_IntEntry(vNodes, i - Vec_IntSize(vIns) - 1) );
513  // assign variable IDs
514  VarC0 = Gia_ManBmcAssignVarIds( p, vIns, vUsed, vOuts );
515  Vec_IntFree( vUsed );
516  // create variable map from CNF vars into SAT vars
517  vMap = Vec_IntStartFull( pCnf->nVars );
518  assert( pCnf->pVarNums[0] > 0 );
519  Vec_IntWriteEntry( vMap, pCnf->pVarNums[0], VarC0 );
520  Gia_ManForEachObj1( pNew, pObj, i )
521  {
522  if ( pCnf->pVarNums[i] < 0 )
523  continue;
524  assert( pCnf->pVarNums[i] >= 0 && pCnf->pVarNums[i] < pCnf->nVars );
525  if ( Gia_ObjIsCi(pObj) )
526  iObj = Vec_IntEntry( vIns, i - 1 );
527  else if ( Gia_ObjIsAnd(pObj) )
528  iObj = Vec_IntEntry( vNodes, i - Vec_IntSize(vIns) - 1 );
529  else if ( Gia_ObjIsCo(pObj) )
530  iObj = Vec_IntEntry( vOuts, i - Vec_IntSize(vIns) - Vec_IntSize(vNodes) - 1 );
531  else assert( 0 );
532  assert( Vec_IntEntry(p->vId2Var, iObj) > 0 );
533  Vec_IntWriteEntry( vMap, pCnf->pVarNums[i], Vec_IntEntry(p->vId2Var, iObj) );
534  }
535 //Vec_IntPrint( vMap );
536  // remap CNF
537  for ( i = 0; i < pCnf->nLiterals; i++ )
538  {
539  assert( pCnf->pClauses[0][i] > 1 && pCnf->pClauses[0][i] < 2 * pCnf->nVars );
540  pCnf->pClauses[0][i] = Abc_Lit2LitV( Vec_IntArray(vMap), pCnf->pClauses[0][i] );
541  }
542  Vec_IntFree( vMap );
543  // add clauses
544  for ( i = 0; i < pCnf->nClauses; i++ )
545  {
546 /*
547  int v;
548  for ( v = 0; v < pCnf->pClauses[i+1] - pCnf->pClauses[i]; v++ )
549  printf( "%d ", pCnf->pClauses[i][v] );
550  printf( "\n" );
551 */
552  if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
553  break;
554  }
555  if ( i < pCnf->nClauses )
556  printf( "SAT solver became UNSAT after adding clauses.\n" );
557  Aig_ManStop( pAig );
558  Cnf_DataFree( pCnf );
559  Gia_ManStop( pNew );
560 }
561 
562 /**Function*************************************************************
563 
564  Synopsis [Collects new nodes.]
565 
566  Description []
567 
568  SideEffects []
569 
570  SeeAlso []
571 
572 ***********************************************************************/
573 void Gia_ManBmcAddCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
574 {
575  int iObj;
576  if ( pObj->fMark0 )
577  return;
578  pObj->fMark0 = 1;
579  iObj = Gia_ObjId( p->pFrames, pObj );
580  if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(p->vId2Var, iObj) == 0 )
581  {
582  Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
583  Gia_ManBmcAddCone_rec( p, Gia_ObjFanin1(pObj) );
584  Vec_IntPush( p->vNodes, iObj );
585  }
586  else
587  Vec_IntPush( p->vInputs, iObj );
588 }
589 void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart, int iStop )
590 {
591  Gia_Obj_t * pObj;
592  int i;
593  Vec_IntClear( p->vNodes );
594  Vec_IntClear( p->vInputs );
595  Vec_IntClear( p->vOutputs );
596  Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
597  for ( i = iStart; i < iStop; i++ )
598  {
599  pObj = Gia_ManPo(p->pFrames, i);
600  if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
601  continue;
602  Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
603  Vec_IntPush( p->vOutputs, Gia_ObjId(p->pFrames, pObj) );
604  }
605  // clean attributes and create new variables
606  Gia_ManForEachObjVec( p->vNodes, p->pFrames, pObj, i )
607  pObj->fMark0 = 0;
608  Gia_ManForEachObjVec( p->vInputs, p->pFrames, pObj, i )
609  pObj->fMark0 = 0;
610 }
611 
612 /**Function*************************************************************
613 
614  Synopsis []
615 
616  Description []
617 
618  SideEffects []
619 
620  SeeAlso []
621 
622 ***********************************************************************/
623 int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart, int iStop )
624 {
625  int i;
626  for ( i = iStart; i < iStop; i++ )
627  if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
628  return 0;
629  return 1;
630 }
631 int Gia_ManBmcFindFirst( Gia_Man_t * pFrames )
632 {
633  Gia_Obj_t * pObj;
634  int i;
635  Gia_ManForEachPo( pFrames, pObj, i )
636  if ( Gia_ObjChild0(pObj) != Gia_ManConst0(pFrames) )
637  return i;
638  return -1;
639 }
640 
641 /**Function*************************************************************
642 
643  Synopsis []
644 
645  Description []
646 
647  SideEffects []
648 
649  SeeAlso []
650 
651 ***********************************************************************/
652 int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
653 {
654  Unr_Man_t * pUnroll;
655  Bmc_Mna_t * p;
656  int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
657  int f, i=0, Lit, status, RetValue = -2;
658  p = Bmc_MnaAlloc();
659  pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
660  for ( f = 0; f < nFramesMax; f++ )
661  {
662  p->pFrames = Unr_ManUnrollFrame( pUnroll, f );
663  if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
664  {
665  // create another slice
666  Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
667  // create CNF in the SAT solver
668  Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
669  // try solving the outputs
670  for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
671  {
672  Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
673  if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
674  continue;
675  Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
676  status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
677  if ( status == l_False ) // unsat
678  continue;
679  if ( status == l_True ) // sat
680  RetValue = 0;
681  if ( status == l_Undef ) // undecided
682  RetValue = -1;
683  break;
684  }
685  }
686  // report statistics
687  if ( pPars->fVerbose )
688  {
689  printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
690  f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
691  p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
692  sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
693  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
694  }
695  if ( RetValue != -2 )
696  {
697  if ( RetValue == -1 )
698  printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
699  else
700  {
701  printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
702  i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
703  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
704  }
705  break;
706  }
707  }
708  if ( RetValue == -2 )
709  RetValue = -1;
710  // dump unfolded frames
711  if ( pPars->fDumpFrames )
712  {
713  p->pFrames = Gia_ManCleanup( p->pFrames );
714  Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
715  printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
716  Gia_ManStop( p->pFrames );
717  }
718  // cleanup
719  Unr_ManFree( pUnroll );
720  Bmc_MnaFree( p );
721  return RetValue;
722 }
723 
724 /**Function*************************************************************
725 
726  Synopsis [Generate counter-example.]
727 
728  Description []
729 
730  SideEffects []
731 
732  SeeAlso []
733 
734 ***********************************************************************/
735 Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
736 {
737  Abc_Cex_t * pCex;
738  int i, iObjId, iSatVar, iOrigPi;
739  int iFramePi = 0, iFrame = -1;
740  pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), iOut / Gia_ManPoNum(p) + 1 );
741  pCex->iFrame = iOut / Gia_ManPoNum(p);
742  pCex->iPo = iOut % Gia_ManPoNum(p);
743  // fill in the input values
744  Vec_IntForEachEntry( pMan->vPiMap, iOrigPi, i )
745  {
746  if ( iOrigPi < 0 )
747  {
748  iFrame = -iOrigPi-1;
749  continue;
750  }
751  // iOrigPi in iFrame of pGia has PI index iFramePi in pMan->pFrames,
752  iObjId = Gia_ObjId( pMan->pFrames, Gia_ManPi(pMan->pFrames, iFramePi) );
753  iSatVar = Vec_IntEntry( pMan->vId2Var, iObjId );
754  if ( sat_solver_var_value(pMan->pSat, iSatVar) )
755  Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + Gia_ManPiNum(p) * iFrame + iOrigPi );
756  iFramePi++;
757  }
758  assert( iFramePi == Gia_ManPiNum(pMan->pFrames) );
759  return pCex;
760 }
761 
762 /**Function*************************************************************
763 
764  Synopsis []
765 
766  Description []
767 
768  SideEffects []
769 
770  SeeAlso []
771 
772 ***********************************************************************/
773 int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
774 {
775  Bmc_Mna_t * p;
776  int nFramesMax, f, i=0, Lit, status, RetValue = -2;
777  abctime clk = Abc_Clock();
778  p = Bmc_MnaAlloc();
779  p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
780  nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
781  if ( pPars->fVerbose )
782  {
783  printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
784  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
785  }
786  if ( pPars->fUseSynth )
787  {
788  Gia_Man_t * pTemp = p->pFrames;
789  p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, 0, pPars->fVerbose, 0 );
790  Gia_ManStop( pTemp );
791  }
792  else if ( pPars->fVerbose )
793  Gia_ManPrintStats( p->pFrames, NULL );
794  if ( pPars->fDumpFrames )
795  {
796  Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
797  printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
798  }
799  for ( f = 0; f < nFramesMax; f++ )
800  {
801  if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
802  {
803  // create another slice
804  Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
805  // create CNF in the SAT solver
806  Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
807  // try solving the outputs
808  for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
809  {
810  Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
811  if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
812  continue;
813  Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
814  status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
815  if ( status == l_False ) // unsat
816  continue;
817  if ( status == l_True ) // sat
818  RetValue = 0;
819  if ( status == l_Undef ) // undecided
820  RetValue = -1;
821  break;
822  }
823  // report statistics
824  if ( pPars->fVerbose )
825  {
826  printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
827  f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
828  p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
829  sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
830  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
831  }
832  }
833  if ( RetValue != -2 )
834  {
835  if ( RetValue == -1 )
836  printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
837  else
838  {
839  ABC_FREE( pGia->pCexSeq );
840  pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
841  printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
842  i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
843  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
844  }
845  break;
846  }
847  pPars->iFrame = f;
848  }
849  if ( RetValue == -2 )
850  RetValue = -1;
851  // cleanup
852  Gia_ManStop( p->pFrames );
853  Bmc_MnaFree( p );
854  return RetValue;
855 }
856 
857 /**Function*************************************************************
858 
859  Synopsis []
860 
861  Description []
862 
863  SideEffects []
864 
865  SeeAlso []
866 
867 ***********************************************************************/
868 void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
869 {
870  int iObj = Gia_ObjId( p->pFrames, pObj );
871  if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
872  {
873  Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
874  Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
875  return;
876  }
877  if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
878  return;
879  Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
880  if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
881  {
882  int i, nClas, iCla;
883  Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
884  if ( Gia_ObjIsAnd(pObj) )
885  Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
886  // extend the SAT solver
887  if ( p->nSatVars > sat_solver_nvars(p->pSat) )
888  sat_solver_setnvars( p->pSat, p->nSatVars );
889  // add clauses
890  nClas = p->pCnf->pObj2Count[iObj];
891  iCla = p->pCnf->pObj2Clause[iObj];
892  for ( i = 0; i < nClas; i++ )
893  {
894  int nLits, pLits[8];
895  int * pClauseThis = p->pCnf->pClauses[iCla+i];
896  int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
897  for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
898  {
899  if ( pClauseThis[nLits] < 2 )
900  printf( "\n\n\nError in CNF generation: Constant literal!\n\n\n" );
901  assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
902  pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
903  }
904  assert( nLits < 8 );
905  if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
906  break;
907  }
908  if ( i < nClas )
909  printf( "SAT solver became UNSAT after adding clauses.\n" );
910  }
911  else assert( Gia_ObjIsCi(pObj) );
912 }
913 void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop )
914 {
915  Gia_Obj_t * pObj;
916  int i;
917  for ( i = iStart; i < iStop; i++ )
918  {
919  pObj = Gia_ManPo(p->pFrames, i);
920  if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p->pFrames) )
921  continue;
922  Gia_ManBmcAddCnfNew_rec( p, pObj );
923  }
924 }
925 
926 /**Function*************************************************************
927 
928  Synopsis []
929 
930  Description []
931 
932  SideEffects []
933 
934  SeeAlso []
935 
936 ***********************************************************************/
937 static inline Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p )
938 {
939  Aig_Man_t * pAig = Gia_ManToAigSimple( p );
940  Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 );
941  Aig_ManStop( pAig );
942  return pCnf;
943 }
944 
945 /**Function*************************************************************
946 
947  Synopsis []
948 
949  Description []
950 
951  SideEffects []
952 
953  SeeAlso []
954 
955 ***********************************************************************/
956 int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
957 {
958  Bmc_Mna_t * p;
959  Gia_Man_t * pTemp;
960  int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
961  abctime clk = Abc_Clock();
962  p = Bmc_MnaAlloc();
963  sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
964  p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
965  nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
966  if ( pPars->fVerbose )
967  {
968  printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
969  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
970  }
971  if ( pPars->fUseSynth )
972  {
973  p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, 0, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
974  }
975  else if ( pPars->fVerbose )
976  Gia_ManPrintStats( p->pFrames, NULL );
977  if ( pPars->fDumpFrames )
978  {
979  Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
980  printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
981  }
982  if ( pPars->fUseOldCnf )
983  p->pCnf = Cnf_DeriveGia( p->pFrames );
984  else
985  {
986  p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp );
987  p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
988 // extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
989 // p->pCnf = Mf_ManGenerateCnf( p->pFrames, 6, 1, 0, 0 );
990  }
991  Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
992  // create clauses for constant node
993 // sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
994  for ( f = 0; f < nFramesMax; f++ )
995  {
996  if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
997  {
998  // create another slice
999  Gia_ManBmcAddCnfNew( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
1000  // try solving the outputs
1001  for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
1002  {
1003  Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
1004  if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
1005  continue;
1006  if ( Gia_ObjChild0(pObj) == Gia_ManConst1(p->pFrames) )
1007  {
1008  printf( "Output %d is trivially SAT.\n", i );
1009  continue;
1010  }
1011  Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
1012  status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1013  if ( status == l_False ) // unsat
1014  continue;
1015  if ( status == l_True ) // sat
1016  RetValue = 0;
1017  if ( status == l_Undef ) // undecided
1018  RetValue = -1;
1019  break;
1020  }
1021  // report statistics
1022  if ( pPars->fVerbose )
1023  {
1024  printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
1025  f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
1026  p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
1027  sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
1028  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1029  }
1030  }
1031  if ( RetValue != -2 )
1032  {
1033  if ( RetValue == -1 )
1034  printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
1035  else
1036  {
1037  ABC_FREE( pGia->pCexSeq );
1038  pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
1039  printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
1040  i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
1041  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1042  }
1043  break;
1044  }
1045  pPars->iFrame = f;
1046  }
1047  if ( RetValue == -2 )
1048  RetValue = -1;
1049  // cleanup
1050  Gia_ManStop( p->pFrames );
1051  Bmc_MnaFree( p );
1052  return RetValue;
1053 }
1054 
1055 /**Function*************************************************************
1056 
1057  Synopsis []
1058 
1059  Description []
1060 
1061  SideEffects []
1062 
1063  SeeAlso []
1064 
1065 ***********************************************************************/
1066 int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
1067 {
1068  abctime TimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
1069  if ( pPars->nFramesAdd == 0 )
1070  return Gia_ManBmcPerformInt( pGia, pPars );
1071  // iterate over the engine until we read the global timeout
1072  assert( pPars->nTimeOut >= 0 );
1073  while ( 1 )
1074  {
1075  if ( TimeToStop && TimeToStop < Abc_Clock() )
1076  return -1;
1077  if ( Gia_ManBmcPerformInt( pGia, pPars ) == 0 )
1078  return 0;
1079  // set the new runtime limit
1080  if ( pPars->nTimeOut )
1081  {
1082  pPars->nTimeOut = Abc_MinInt( pPars->nTimeOut-1, (int)((TimeToStop - Abc_Clock()) / CLOCKS_PER_SEC) );
1083  if ( pPars->nTimeOut <= 0 )
1084  return -1;
1085  }
1086  else
1087  return -1;
1088  // set the new frames limit
1089  pPars->nFramesAdd *= 2;
1090  }
1091  return -1;
1092 }
1093 
1094 ////////////////////////////////////////////////////////////////////////
1095 /// END OF FILE ///
1096 ////////////////////////////////////////////////////////////////////////
1097 
1098 
1099 ABC_NAMESPACE_IMPL_END
1100 
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Bmc_AndPar_t_::nFramesMax
int nFramesMax
Definition: bmc.h:82
Unr_Man_t
typedefABC_NAMESPACE_HEADER_START struct Unr_Man_t_ Unr_Man_t
INCLUDES ///.
Definition: bmc.h:43
Gia_ManCleanPhase
void Gia_ManCleanPhase(Gia_Man_t *p)
Definition: giaUtil.c:431
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
GIA_UND
#define GIA_UND
Definition: gia.h:749
Abc_Lit2LitV
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
Gia_ManBmcPerformInt
int Gia_ManBmcPerformInt(Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
Definition: bmcBmcAnd.c:956
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Bmc_MnaBuild_rec
void Bmc_MnaBuild_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew, Vec_Int_t *vMap, Vec_Int_t *vPiMap)
Definition: bmcBmcAnd.c:228
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Bmc_MnaCollect_rec
void Bmc_MnaCollect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes, unsigned *pState)
Definition: bmcBmcAnd.c:142
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
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
Gia_ManBmcUnroll
Gia_Man_t * Gia_ManBmcUnroll(Gia_Man_t *pGia, int nFramesMax, int nFramesAdd, int fVerbose, Vec_Int_t **pvPiMap)
Definition: bmcBmcAnd.c:284
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Bmc_Mna_t_::nSatVars
int nSatVars
Definition: bmcBmcAnd.c:44
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_IntFillExtra
static void Vec_IntFillExtra(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:376
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Unr_ManUnrollFrame
Gia_Man_t * Unr_ManUnrollFrame(Unr_Man_t *p, int f)
Definition: bmcUnroll.c:379
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
Gia_ManName
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Bmc_MnaAlloc
Bmc_Mna_t * Bmc_MnaAlloc()
Definition: bmcBmcAnd.c:389
Bmc_Mna_t_::vOutputs
Vec_Int_t * vOutputs
Definition: bmcBmcAnd.c:41
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
Gia_ManBmcCexGen
Abc_Cex_t * Gia_ManBmcCexGen(Bmc_Mna_t *pMan, Gia_Man_t *p, int iOut)
Definition: bmcBmcAnd.c:735
Bmc_Mna_t_::pFrames
Gia_Man_t * pFrames
Definition: bmcBmcAnd.c:36
Gia_ManTerSimInfoSet
static void Gia_ManTerSimInfoSet(unsigned *pInfo, int i, int Value)
Definition: bmcBmcAnd.c:52
GIA_ZER
#define GIA_ZER
Definition: gia.h:747
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Bmc_AndPar_t_::nFramesAdd
int nFramesAdd
Definition: bmc.h:83
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_PtrFreeFree
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition: vecInt.h:62
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Gia_ObjFaninId1p
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Bmc_Mna_t_::pSat
sat_solver * pSat
Definition: bmcBmcAnd.c:43
Gia_ManBmcPerform_Unr
int Gia_ManBmcPerform_Unr(Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
Definition: bmcBmcAnd.c:652
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Bmc_AndPar_t_::nTimeOut
int nTimeOut
Definition: bmc.h:85
l_True
#define l_True
Definition: SolverTypes.h:84
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Bmc_MnaFree
void Bmc_MnaFree(Bmc_Mna_t *p)
Definition: bmcBmcAnd.c:403
Jf_ManDeriveCnf
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition: giaJf.c:1746
Gia_XsimNotCond
static int Gia_XsimNotCond(int Value, int fCompl)
Definition: gia.h:751
Gia_XsimAndCond
static int Gia_XsimAndCond(int Value0, int fCompl0, int Value1, int fCompl1)
Definition: gia.h:759
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Unr_ManUnrollStart
Unr_Man_t * Unr_ManUnrollStart(Gia_Man_t *pGia, int fVerbose)
Definition: bmcUnroll.c:368
Gia_ManBmcDupCone
Gia_Man_t * Gia_ManBmcDupCone(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vNodes, Vec_Int_t *vOuts)
Definition: bmcBmcAnd.c:426
Bmc_Mna_t_
Definition: bmcBmcAnd.c:34
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Cnf_Dat_t_
Definition: cnf.h:56
Bmc_AndPar_t_::fDumpFrames
int fDumpFrames
Definition: bmc.h:87
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Bmc_AndPar_t_::fUseSynth
int fUseSynth
Definition: bmc.h:88
Gia_ManDupFromVecs
Gia_Man_t * Gia_ManDupFromVecs(Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, int nRegs)
Definition: giaDup.c:2853
Bmc_AndPar_t_::fVerbose
int fVerbose
Definition: bmc.h:90
Gia_Obj_t_
Definition: gia.h:75
Gia_ManConst1
static Gia_Obj_t * Gia_ManConst1(Gia_Man_t *p)
Definition: gia.h:401
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Gia_ManBmcAddCnfNew
void Gia_ManBmcAddCnfNew(Bmc_Mna_t *p, int iStart, int iStop)
Definition: bmcBmcAnd.c:913
Gia_ManTerSimInfoGet
static int Gia_ManTerSimInfoGet(unsigned *pInfo, int i)
Definition: bmcBmcAnd.c:48
Gia_ManBmcPerform
int Gia_ManBmcPerform(Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
Definition: bmcBmcAnd.c:1066
Bmc_Mna_t
typedefABC_NAMESPACE_IMPL_START struct Bmc_Mna_t_ Bmc_Mna_t
DECLARATIONS ///.
Definition: bmcBmcAnd.c:33
Bmc_AndPar_t_::fUseOldCnf
int fUseOldCnf
Definition: bmc.h:89
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
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
Gia_ManBmcAddCnfNew_rec
void Gia_ManBmcAddCnfNew_rec(Bmc_Mna_t *p, Gia_Obj_t *pObj)
Definition: bmcBmcAnd.c:868
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Bmc_MnaBuild
void Bmc_MnaBuild(Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, Gia_Man_t *pNew, Vec_Int_t *vMap, Vec_Int_t *vPiMap)
Definition: bmcBmcAnd.c:256
Gia_ManBmcAddCone
void Gia_ManBmcAddCone(Bmc_Mna_t *p, int iStart, int iStop)
Definition: bmcBmcAnd.c:589
Bmc_Mna_t_::vNodes
Vec_Int_t * vNodes
Definition: bmcBmcAnd.c:42
Gia_ManAigSyn2
Gia_Man_t * Gia_ManAigSyn2(Gia_Man_t *p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose)
Definition: giaScript.c:69
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Bmc_Mna_t_::vId2Var
Vec_Int_t * vId2Var
Definition: bmcBmcAnd.c:39
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Bmc_AndPar_t_
Definition: bmc.h:79
Gia_ObjIsRi
static int Gia_ObjIsRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:444
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
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
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManBmcAddCnf
void Gia_ManBmcAddCnf(Bmc_Mna_t *p, Gia_Man_t *pGia, Vec_Int_t *vIns, Vec_Int_t *vNodes, Vec_Int_t *vOuts)
Definition: bmcBmcAnd.c:500
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
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
Unr_ManFree
void Unr_ManFree(Unr_Man_t *p)
Definition: bmcUnroll.c:340
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Cnf_DeriveOther
Cnf_Dat_t * Cnf_DeriveOther(Aig_Man_t *pAig, int fSkipTtMin)
Definition: cnfCore.c:219
Bmc_AndPar_t_::fVeryVerbose
int fVeryVerbose
Definition: bmc.h:91
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Bmc_MnaCollect
void Bmc_MnaCollect(Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, unsigned *pState)
Definition: bmcBmcAnd.c:160
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
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
Bmc_MnaTernary
Vec_Ptr_t * Bmc_MnaTernary(Gia_Man_t *p, int nFrames, int nFramesAdd, int fVerbose, int *iFirst)
FUNCTION DEFINITIONS ///.
Definition: bmcBmcAnd.c:74
Bmc_Mna_t_::vPiMap
Vec_Int_t * vPiMap
Definition: bmcBmcAnd.c:38
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Bmc_MnaSelect_rec
void Bmc_MnaSelect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves)
Definition: bmcBmcAnd.c:187
Bmc_Mna_t_::vInputs
Vec_Int_t * vInputs
Definition: bmcBmcAnd.c:40
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Bmc_AndPar_t_::nConfLimit
int nConfLimit
Definition: bmc.h:84
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Bmc_MnaSelect
void Bmc_MnaSelect(Gia_Man_t *p, Vec_Int_t *vCos, Vec_Int_t *vNodes, Vec_Int_t *vLeaves)
Definition: bmcBmcAnd.c:205
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManBmcAssignVarIds
int Gia_ManBmcAssignVarIds(Bmc_Mna_t *p, Vec_Int_t *vIns, Vec_Int_t *vUsed, Vec_Int_t *vOuts)
Definition: bmcBmcAnd.c:467
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRiToRo
static Gia_Obj_t * Gia_ObjRiToRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:447
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ObjIsPo
static int Gia_ObjIsPo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:442
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Gia_ManBmcAddCone_rec
void Gia_ManBmcAddCone_rec(Bmc_Mna_t *p, Gia_Obj_t *pObj)
Definition: bmcBmcAnd.c:573
sat_solver_t
Definition: satSolver.h:91
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManMemory
double Gia_ManMemory(Gia_Man_t *p)
Definition: giaMan.c:156
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Bmc_Mna_t_::pCnf
Cnf_Dat_t * pCnf
Definition: bmcBmcAnd.c:37
Gia_ManBmcFindFirst
int Gia_ManBmcFindFirst(Gia_Man_t *pFrames)
Definition: bmcBmcAnd.c:631
Cnf_Dat_t_::nLiterals
int nLiterals
Definition: cnf.h:60
Bmc_AndPar_t_::iFrame
int iFrame
Definition: bmc.h:93
Cnf_DeriveGia
static Cnf_Dat_t * Cnf_DeriveGia(Gia_Man_t *p)
Definition: bmcBmcAnd.c:937
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Bmc_Mna_t_::clkStart
abctime clkStart
Definition: bmcBmcAnd.c:45
Gia_ManBmcPerform_old_cnf
int Gia_ManBmcPerform_old_cnf(Gia_Man_t *pGia, Bmc_AndPar_t *pPars)
Definition: bmcBmcAnd.c:773
GIA_ONE
#define GIA_ONE
Definition: gia.h:748
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_ManBmcCheckOutputs
int Gia_ManBmcCheckOutputs(Gia_Man_t *pFrames, int iStart, int iStop)
Definition: bmcBmcAnd.c:623