abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcBmc3.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcBmc3.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 in collaboration with Niklas Een.]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcBmc3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "proof/fra/fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "misc/vec/vecHsh.h"
25 #include "misc/vec/vecWec.h"
26 #include "bmc.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 typedef struct Gia_ManBmc_t_ Gia_ManBmc_t;
35 struct Gia_ManBmc_t_
36 {
37  // input/output data
38  Saig_ParBmc_t * pPars; // parameters
39  Aig_Man_t * pAig; // user AIG
40  Vec_Ptr_t * vCexes; // counter-examples
41  // intermediate data
42  Vec_Int_t * vMapping; // mapping
43  Vec_Int_t * vMapRefs; // mapping references
44 // Vec_Vec_t * vSects; // sections
45  Vec_Int_t * vId2Num; // number of each node
46  Vec_Ptr_t * vTerInfo; // ternary information
47  Vec_Ptr_t * vId2Var; // SAT vars for each object
48  Vec_Wec_t * vVisited; // visited nodes
49  abctime * pTime4Outs; // timeout per output
50  // hash table
51  Vec_Int_t * vData; // storage for cuts
52  Hsh_IntMan_t * vHash; // hash table
53  Vec_Int_t * vId2Lit; // mapping cuts into literals
54  int nHashHit; // hash table hits
55  int nHashMiss; // hash table misses
56  int nBufNum; // the number of simple nodes
57  int nDupNum; // the number of simple nodes
58  int nUniProps; // propagating learned clause values
59  int nLitUsed; // used literals
60  int nLitUseless; // useless literals
61  // SAT solver
62  sat_solver * pSat; // SAT solver
63  int nSatVars; // SAT variables
64  int nObjNums; // SAT objects
65  int nWordNum; // unsigned words for ternary simulation
66  char * pSopSizes, ** pSops; // CNF representation
67 };
68 
69 extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
70 
71 void Gia_ManReportProgress( FILE * pFile, int prop_no, int depth )
72 {
73  extern int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer );
74  char buf[100];
75  sprintf(buf, "property: safe<%d>\nbug-free-depth: %d\n", prop_no, depth);
76  Gia_ManToBridgeProgress(pFile, strlen(buf), (unsigned char *)buf);
77 }
78 
79 ////////////////////////////////////////////////////////////////////////
80 /// FUNCTION DEFINITIONS ///
81 ////////////////////////////////////////////////////////////////////////
82 
83 #define SAIG_TER_NON 0
84 #define SAIG_TER_ZER 1
85 #define SAIG_TER_ONE 2
86 #define SAIG_TER_UND 3
87 
88 static inline int Saig_ManBmcSimInfoNot( int Value )
89 {
90  if ( Value == SAIG_TER_ZER )
91  return SAIG_TER_ONE;
92  if ( Value == SAIG_TER_ONE )
93  return SAIG_TER_ZER;
94  return SAIG_TER_UND;
95 }
96 
97 static inline int Saig_ManBmcSimInfoAnd( int Value0, int Value1 )
98 {
99  if ( Value0 == SAIG_TER_ZER || Value1 == SAIG_TER_ZER )
100  return SAIG_TER_ZER;
101  if ( Value0 == SAIG_TER_ONE && Value1 == SAIG_TER_ONE )
102  return SAIG_TER_ONE;
103  return SAIG_TER_UND;
104 }
105 
106 static inline int Saig_ManBmcSimInfoGet( unsigned * pInfo, Aig_Obj_t * pObj )
107 {
108  return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
109 }
110 
111 static inline void Saig_ManBmcSimInfoSet( unsigned * pInfo, Aig_Obj_t * pObj, int Value )
112 {
113  assert( Value >= SAIG_TER_ZER && Value <= SAIG_TER_UND );
114  Value ^= Saig_ManBmcSimInfoGet( pInfo, pObj );
115  pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
116 }
117 
118 static inline int Saig_ManBmcSimInfoClear( unsigned * pInfo, Aig_Obj_t * pObj )
119 {
120  int Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
121  pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
122  return Value;
123 }
124 
125 /**Function*************************************************************
126 
127  Synopsis [Returns the number of LIs with binary ternary info.]
128 
129  Description []
130 
131  SideEffects []
132 
133  SeeAlso []
134 
135 ***********************************************************************/
136 int Saig_ManBmcTerSimCount01( Aig_Man_t * p, unsigned * pInfo )
137 {
138  Aig_Obj_t * pObj;
139  int i, Counter = 0;
140  if ( pInfo == NULL )
141  return Saig_ManRegNum(p);
142  Saig_ManForEachLi( p, pObj, i )
143  if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
144  Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
145  return Counter;
146 }
147 
148 /**Function*************************************************************
149 
150  Synopsis [Performs ternary simulation of one frame.]
151 
152  Description []
153 
154  SideEffects []
155 
156  SeeAlso []
157 
158 ***********************************************************************/
159 unsigned * Saig_ManBmcTerSimOne( Aig_Man_t * p, unsigned * pPrev )
160 {
161  Aig_Obj_t * pObj, * pObjLi;
162  unsigned * pInfo;
163  int i, Val0, Val1;
164  pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) );
165  Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE );
166  Saig_ManForEachPi( p, pObj, i )
167  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
168  if ( pPrev == NULL )
169  {
170  Saig_ManForEachLo( p, pObj, i )
171  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
172  }
173  else
174  {
175  Saig_ManForEachLiLo( p, pObjLi, pObj, i )
176  Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoGet(pPrev, pObjLi) );
177  }
178  Aig_ManForEachNode( p, pObj, i )
179  {
180  Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
181  Val1 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin1(pObj) );
182  if ( Aig_ObjFaninC0(pObj) )
183  Val0 = Saig_ManBmcSimInfoNot( Val0 );
184  if ( Aig_ObjFaninC1(pObj) )
185  Val1 = Saig_ManBmcSimInfoNot( Val1 );
186  Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoAnd(Val0, Val1) );
187  }
188  Aig_ManForEachCo( p, pObj, i )
189  {
190  Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
191  if ( Aig_ObjFaninC0(pObj) )
192  Val0 = Saig_ManBmcSimInfoNot( Val0 );
193  Saig_ManBmcSimInfoSet( pInfo, pObj, Val0 );
194  }
195  return pInfo;
196 }
197 
198 /**Function*************************************************************
199 
200  Synopsis [Collects internal nodes and PIs in the DFS order.]
201 
202  Description []
203 
204  SideEffects []
205 
206  SeeAlso []
207 
208 ***********************************************************************/
209 Vec_Ptr_t * Saig_ManBmcTerSim( Aig_Man_t * p )
210 {
211  Vec_Ptr_t * vInfos;
212  unsigned * pInfo = NULL;
213  int i, TerPrev = ABC_INFINITY, TerCur, CountIncrease = 0;
214  vInfos = Vec_PtrAlloc( 100 );
215  for ( i = 0; i < 1000 && CountIncrease < 5 && TerPrev > 0; i++ )
216  {
217  TerCur = Saig_ManBmcTerSimCount01( p, pInfo );
218  if ( TerCur >= TerPrev )
219  CountIncrease++;
220  TerPrev = TerCur;
221  pInfo = Saig_ManBmcTerSimOne( p, pInfo );
222  Vec_PtrPush( vInfos, pInfo );
223  }
224  return vInfos;
225 }
226 
227 /**Function*************************************************************
228 
229  Synopsis []
230 
231  Description []
232 
233  SideEffects []
234 
235  SeeAlso []
236 
237 ***********************************************************************/
238 void Saig_ManBmcTerSimTest( Aig_Man_t * p )
239 {
240  Vec_Ptr_t * vInfos;
241  unsigned * pInfo;
242  int i;
243  vInfos = Saig_ManBmcTerSim( p );
244  Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i )
245  Abc_Print( 1, "%d=%d ", i, Saig_ManBmcTerSimCount01(p, pInfo) );
246  Abc_Print( 1, "\n" );
247  Vec_PtrFreeFree( vInfos );
248 }
249 
250 
251 
252 /**Function*************************************************************
253 
254  Synopsis [Count the number of non-ternary per frame.]
255 
256  Description []
257 
258  SideEffects []
259 
260  SeeAlso []
261 
262 ***********************************************************************/
263 int Saig_ManBmcCountNonternary_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vInfos, unsigned * pInfo, int f, int * pCounter )
264 {
265  int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
266  if ( Value == SAIG_TER_NON )
267  return 0;
268  assert( f >= 0 );
269  pCounter[f] += (Value == SAIG_TER_UND);
270  if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
271  return 0;
272  if ( Saig_ObjIsLi(p, pObj) )
273  return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
274  if ( Saig_ObjIsLo(p, pObj) )
275  return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
276  assert( Aig_ObjIsNode(pObj) );
277  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
278  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
279  return 0;
280 }
281 void Saig_ManBmcCountNonternary( Aig_Man_t * p, Vec_Ptr_t * vInfos, int iFrame )
282 {
283  int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
284  unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
285  assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
286  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
287  for ( i = 0; i <= iFrame; i++ )
288  Abc_Print( 1, "%d=%d ", i, pCounters[i] );
289  Abc_Print( 1, "\n" );
290  ABC_FREE( pCounters );
291 }
292 
293 
294 /**Function*************************************************************
295 
296  Synopsis [Returns the number of POs with binary ternary info.]
297 
298  Description []
299 
300  SideEffects []
301 
302  SeeAlso []
303 
304 ***********************************************************************/
305 int Saig_ManBmcTerSimCount01Po( Aig_Man_t * p, unsigned * pInfo )
306 {
307  Aig_Obj_t * pObj;
308  int i, Counter = 0;
309  Saig_ManForEachPo( p, pObj, i )
310  Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
311  return Counter;
312 }
313 Vec_Ptr_t * Saig_ManBmcTerSimPo( Aig_Man_t * p )
314 {
315  Vec_Ptr_t * vInfos;
316  unsigned * pInfo = NULL;
317  int i, nPoBin;
318  vInfos = Vec_PtrAlloc( 100 );
319  for ( i = 0; ; i++ )
320  {
321  if ( i % 100 == 0 )
322  Abc_Print( 1, "Frame %5d\n", i );
323  pInfo = Saig_ManBmcTerSimOne( p, pInfo );
324  Vec_PtrPush( vInfos, pInfo );
325  nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
326  if ( nPoBin < Saig_ManPoNum(p) )
327  break;
328  }
329  Abc_Print( 1, "Detected terminary PO in frame %d.\n", i );
330  Saig_ManBmcCountNonternary( p, vInfos, i );
331  return vInfos;
332 }
333 void Saig_ManBmcTerSimTestPo( Aig_Man_t * p )
334 {
335  Vec_Ptr_t * vInfos;
336  vInfos = Saig_ManBmcTerSimPo( p );
337  Vec_PtrFreeFree( vInfos );
338 }
339 
340 
341 
342 
343 /**Function*************************************************************
344 
345  Synopsis [Collects internal nodes in the DFS order.]
346 
347  Description []
348 
349  SideEffects []
350 
351  SeeAlso []
352 
353 ***********************************************************************/
354 void Saig_ManBmcDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
355 {
356  assert( !Aig_IsComplement(pObj) );
357  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
358  return;
359  Aig_ObjSetTravIdCurrent(p, pObj);
360  if ( Aig_ObjIsNode(pObj) )
361  {
362  Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
363  Saig_ManBmcDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
364  }
365  Vec_PtrPush( vNodes, pObj );
366 }
367 
368 /**Function*************************************************************
369 
370  Synopsis [Collects internal nodes and PIs in the DFS order.]
371 
372  Description []
373 
374  SideEffects []
375 
376  SeeAlso []
377 
378 ***********************************************************************/
379 Vec_Ptr_t * Saig_ManBmcDfsNodes( Aig_Man_t * p, Vec_Ptr_t * vRoots )
380 {
381  Vec_Ptr_t * vNodes;
382  Aig_Obj_t * pObj;
383  int i;
384  vNodes = Vec_PtrAlloc( 100 );
385  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
386  Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
387  return vNodes;
388 }
389 
390 /**Function*************************************************************
391 
392  Synopsis []
393 
394  Description []
395 
396  SideEffects []
397 
398  SeeAlso []
399 
400 ***********************************************************************/
401 Vec_Vec_t * Saig_ManBmcSections( Aig_Man_t * p )
402 {
403  Vec_Ptr_t * vSects, * vRoots, * vCone;
404  Aig_Obj_t * pObj, * pObjPo;
405  int i;
406  Aig_ManIncrementTravId( p );
407  Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
408  // start the roots
409  vRoots = Vec_PtrAlloc( 1000 );
410  Saig_ManForEachPo( p, pObjPo, i )
411  {
412  Aig_ObjSetTravIdCurrent( p, pObjPo );
413  Vec_PtrPush( vRoots, pObjPo );
414  }
415  // compute the cones
416  vSects = Vec_PtrAlloc( 20 );
417  while ( Vec_PtrSize(vRoots) > 0 )
418  {
419  vCone = Saig_ManBmcDfsNodes( p, vRoots );
420  Vec_PtrPush( vSects, vCone );
421  // get the next set of roots
422  Vec_PtrClear( vRoots );
423  Vec_PtrForEachEntry( Aig_Obj_t *, vCone, pObj, i )
424  {
425  if ( !Saig_ObjIsLo(p, pObj) )
426  continue;
427  pObjPo = Saig_ObjLoToLi( p, pObj );
428  if ( Aig_ObjIsTravIdCurrent(p, pObjPo) )
429  continue;
430  Aig_ObjSetTravIdCurrent( p, pObjPo );
431  Vec_PtrPush( vRoots, pObjPo );
432  }
433  }
434  Vec_PtrFree( vRoots );
435  return (Vec_Vec_t *)vSects;
436 }
437 
438 /**Function*************************************************************
439 
440  Synopsis []
441 
442  Description []
443 
444  SideEffects []
445 
446  SeeAlso []
447 
448 ***********************************************************************/
449 void Saig_ManBmcSectionsTest( Aig_Man_t * p )
450 {
451  Vec_Vec_t * vSects;
452  Vec_Ptr_t * vOne;
453  int i;
454  vSects = Saig_ManBmcSections( p );
455  Vec_VecForEachLevel( vSects, vOne, i )
456  Abc_Print( 1, "%d=%d ", i, Vec_PtrSize(vOne) );
457  Abc_Print( 1, "\n" );
458  Vec_VecFree( vSects );
459 }
460 
461 
462 
463 /**Function*************************************************************
464 
465  Synopsis [Collects the supergate.]
466 
467  Description []
468 
469  SideEffects []
470 
471  SeeAlso []
472 
473 ***********************************************************************/
474 void Saig_ManBmcSupergate_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
475 {
476  // if the new node is complemented or a PI, another gate begins
477  if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) )
478  {
479  Vec_PtrPushUnique( vSuper, Aig_Regular(pObj) );
480  return;
481  }
482  // go through the branches
483  Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
484  Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
485 }
486 
487 /**Function*************************************************************
488 
489  Synopsis [Collect the topmost supergate.]
490 
491  Description []
492 
493  SideEffects []
494 
495  SeeAlso []
496 
497 ***********************************************************************/
498 Vec_Ptr_t * Saig_ManBmcSupergate( Aig_Man_t * p, int iPo )
499 {
500  Vec_Ptr_t * vSuper;
501  Aig_Obj_t * pObj;
502  vSuper = Vec_PtrAlloc( 10 );
503  pObj = Aig_ManCo( p, iPo );
504  pObj = Aig_ObjChild0( pObj );
505  if ( !Aig_IsComplement(pObj) )
506  {
507  Vec_PtrPush( vSuper, pObj );
508  return vSuper;
509  }
510  pObj = Aig_Regular( pObj );
511  if ( !Aig_ObjIsNode(pObj) )
512  {
513  Vec_PtrPush( vSuper, pObj );
514  return vSuper;
515  }
516  Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
517  Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
518  return vSuper;
519 }
520 
521 /**Function*************************************************************
522 
523  Synopsis [Returns the number of nodes with ref counter more than 1.]
524 
525  Description []
526 
527  SideEffects []
528 
529  SeeAlso []
530 
531 ***********************************************************************/
532 int Saig_ManBmcCountRefed( Aig_Man_t * p, Vec_Ptr_t * vSuper )
533 {
534  Aig_Obj_t * pObj;
535  int i, Counter = 0;
536  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
537  {
538  assert( !Aig_IsComplement(pObj) );
539  Counter += (Aig_ObjRefs(pObj) > 1);
540  }
541  return Counter;
542 }
543 
544 /**Function*************************************************************
545 
546  Synopsis []
547 
548  Description []
549 
550  SideEffects []
551 
552  SeeAlso []
553 
554 ***********************************************************************/
555 void Saig_ManBmcSupergateTest( Aig_Man_t * p )
556 {
557  Vec_Ptr_t * vSuper;
558  Aig_Obj_t * pObj;
559  int i;
560  Abc_Print( 1, "Supergates: " );
561  Saig_ManForEachPo( p, pObj, i )
562  {
563  vSuper = Saig_ManBmcSupergate( p, i );
564  Abc_Print( 1, "%d=%d(%d) ", i, Vec_PtrSize(vSuper), Saig_ManBmcCountRefed(p, vSuper) );
565  Vec_PtrFree( vSuper );
566  }
567  Abc_Print( 1, "\n" );
568 }
569 
570 /**Function*************************************************************
571 
572  Synopsis []
573 
574  Description []
575 
576  SideEffects []
577 
578  SeeAlso []
579 
580 ***********************************************************************/
581 void Saig_ManBmcWriteBlif( Aig_Man_t * p, Vec_Int_t * vMapping, char * pFileName )
582 {
583  FILE * pFile;
584  char * pSopSizes, ** pSops;
585  Aig_Obj_t * pObj;
586  char Vals[4];
587  int i, k, b, iFan, iTruth, * pData;
588  pFile = fopen( pFileName, "w" );
589  if ( pFile == NULL )
590  {
591  Abc_Print( 1, "Cannot open file %s\n", pFileName );
592  return;
593  }
594  fprintf( pFile, ".model test\n" );
595  fprintf( pFile, ".inputs" );
596  Aig_ManForEachCi( p, pObj, i )
597  fprintf( pFile, " n%d", Aig_ObjId(pObj) );
598  fprintf( pFile, "\n" );
599  fprintf( pFile, ".outputs" );
600  Aig_ManForEachCo( p, pObj, i )
601  fprintf( pFile, " n%d", Aig_ObjId(pObj) );
602  fprintf( pFile, "\n" );
603  fprintf( pFile, ".names" );
604  fprintf( pFile, " n%d\n", Aig_ObjId(Aig_ManConst1(p)) );
605  fprintf( pFile, " 1\n" );
606 
607  Cnf_ReadMsops( &pSopSizes, &pSops );
608  Aig_ManForEachNode( p, pObj, i )
609  {
610  if ( Vec_IntEntry(vMapping, i) == 0 )
611  continue;
612  pData = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, i) );
613  fprintf( pFile, ".names" );
614  for ( iFan = 0; iFan < 4; iFan++ )
615  if ( pData[iFan+1] >= 0 )
616  fprintf( pFile, " n%d", pData[iFan+1] );
617  else
618  break;
619  fprintf( pFile, " n%d\n", i );
620  // write SOP
621  iTruth = pData[0] & 0xffff;
622  for ( k = 0; k < pSopSizes[iTruth]; k++ )
623  {
624  int Lit = pSops[iTruth][k];
625  for ( b = 3; b >= 0; b-- )
626  {
627  if ( Lit % 3 == 0 )
628  Vals[b] = '0';
629  else if ( Lit % 3 == 1 )
630  Vals[b] = '1';
631  else
632  Vals[b] = '-';
633  Lit = Lit / 3;
634  }
635  for ( b = 0; b < iFan; b++ )
636  fprintf( pFile, "%c", Vals[b] );
637  fprintf( pFile, " 1\n" );
638  }
639  }
640  free( pSopSizes );
641  free( pSops[1] );
642  free( pSops );
643 
644  Aig_ManForEachCo( p, pObj, i )
645  {
646  fprintf( pFile, ".names" );
647  fprintf( pFile, " n%d", Aig_ObjId(Aig_ObjFanin0(pObj)) );
648  fprintf( pFile, " n%d\n", Aig_ObjId(pObj) );
649  fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
650  }
651  fprintf( pFile, ".end\n" );
652  fclose( pFile );
653 }
654 
655 /**Function*************************************************************
656 
657  Synopsis []
658 
659  Description []
660 
661  SideEffects []
662 
663  SeeAlso []
664 
665 ***********************************************************************/
666 void Saig_ManBmcMappingTest( Aig_Man_t * p )
667 {
668  Vec_Int_t * vMapping;
669  vMapping = Cnf_DeriveMappingArray( p );
670  Saig_ManBmcWriteBlif( p, vMapping, "test.blif" );
671  Vec_IntFree( vMapping );
672 }
673 
674 
675 /**Function*************************************************************
676 
677  Synopsis []
678 
679  Description []
680 
681  SideEffects []
682 
683  SeeAlso []
684 
685 ***********************************************************************/
686 Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
687 {
688  Vec_Int_t * vRefs;
689  Aig_Obj_t * pObj;
690  int i, iFan, * pData;
691  vRefs = Vec_IntStart( Aig_ManObjNumMax(p) );
692  Aig_ManForEachCo( p, pObj, i )
693  Vec_IntAddToEntry( vRefs, Aig_ObjFaninId0(pObj), 1 );
694  Aig_ManForEachNode( p, pObj, i )
695  {
696  if ( Vec_IntEntry(vMap, i) == 0 )
697  continue;
698  pData = Vec_IntEntryP( vMap, Vec_IntEntry(vMap, i) );
699  for ( iFan = 0; iFan < 4; iFan++ )
700  if ( pData[iFan+1] >= 0 )
701  Vec_IntAddToEntry( vRefs, pData[iFan+1], 1 );
702  }
703  return vRefs;
704 }
705 
706 /**Function*************************************************************
707 
708  Synopsis [Create manager.]
709 
710  Description []
711 
712  SideEffects []
713 
714  SeeAlso []
715 
716 ***********************************************************************/
717 Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
718 {
719  Gia_ManBmc_t * p;
720  Aig_Obj_t * pObj;
721  int i;
722 // assert( Aig_ManRegNum(pAig) > 0 );
723  p = ABC_CALLOC( Gia_ManBmc_t, 1 );
724  p->pAig = pAig;
725  // create mapping
726  p->vMapping = Cnf_DeriveMappingArray( pAig );
727  p->vMapRefs = Saig_ManBmcComputeMappingRefs( pAig, p->vMapping );
728  // create sections
729 // p->vSects = Saig_ManBmcSections( pAig );
730  // map object IDs into their numbers and section numbers
731  p->nObjNums = 0;
732  p->vId2Num = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
733  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(Aig_ManConst1(pAig)), p->nObjNums++ );
734  Aig_ManForEachCi( pAig, pObj, i )
735  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
736  Aig_ManForEachNode( pAig, pObj, i )
737  if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) > 0 )
738  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
739  Aig_ManForEachCo( pAig, pObj, i )
740  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
741  p->vId2Var = Vec_PtrAlloc( 100 );
742  p->vTerInfo = Vec_PtrAlloc( 100 );
743  p->vVisited = Vec_WecAlloc( 100 );
744  // create solver
745  p->nSatVars = 1;
746  p->pSat = sat_solver_new();
747  sat_solver_setnvars( p->pSat, 1000 );
748  Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
749  // terminary simulation
750  p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
751  // hash table
752  p->vData = Vec_IntAlloc( 5 * 10000 );
753  p->vHash = Hsh_IntManStart( p->vData, 5, 10000 );
754  p->vId2Lit = Vec_IntAlloc( 10000 );
755  // time spent on each outputs
756  if ( nTimeOutOne )
757  {
758  p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
759  for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
760  p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
761  }
762  return p;
763 }
764 
765 /**Function*************************************************************
766 
767  Synopsis [Delete manager.]
768 
769  Description []
770 
771  SideEffects []
772 
773  SeeAlso []
774 
775 ***********************************************************************/
776 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
777 {
778  if ( p->pPars->fVerbose )
779  {
780  int nUsedVars = sat_solver_count_usedvars(p->pSat);
781  Abc_Print( 1, "LStart(P) = %d LDelta(Q) = %d LRatio(R) = %d ReduceDB = %d Vars = %d Used = %d (%.2f %%)\n",
782  p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio,
783  p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size );
784  Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
785  p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
786  }
787 // Aig_ManCleanMarkA( p->pAig );
788  if ( p->vCexes )
789  {
790  assert( p->pAig->vSeqModelVec == NULL );
791  p->pAig->vSeqModelVec = p->vCexes;
792  p->vCexes = NULL;
793  }
794 // Vec_PtrFreeFree( p->vCexes );
795  Vec_WecFree( p->vVisited );
796  Vec_IntFree( p->vMapping );
797  Vec_IntFree( p->vMapRefs );
798 // Vec_VecFree( p->vSects );
799  Vec_IntFree( p->vId2Num );
800  Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
801  Vec_PtrFreeFree( p->vTerInfo );
802  sat_solver_delete( p->pSat );
803  ABC_FREE( p->pTime4Outs );
804  Vec_IntFree( p->vData );
805  Hsh_IntManStop( p->vHash );
806  Vec_IntFree( p->vId2Lit );
807  ABC_FREE( p->pSopSizes );
808  ABC_FREE( p->pSops[1] );
809  ABC_FREE( p->pSops );
810  ABC_FREE( p );
811 }
812 
813 
814 /**Function*************************************************************
815 
816  Synopsis []
817 
818  Description []
819 
820  SideEffects []
821 
822  SeeAlso []
823 
824 ***********************************************************************/
825 static inline int * Saig_ManBmcMapping( Gia_ManBmc_t * p, Aig_Obj_t * pObj )
826 {
827  if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) == 0 )
828  return NULL;
829  return Vec_IntEntryP( p->vMapping, Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) );
830 }
831 
832 /**Function*************************************************************
833 
834  Synopsis []
835 
836  Description []
837 
838  SideEffects []
839 
840  SeeAlso []
841 
842 ***********************************************************************/
843 static inline int Saig_ManBmcLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
844 {
845  Vec_Int_t * vFrame;
846  int ObjNum;
847  assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
848  ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
849  assert( ObjNum >= 0 );
850  vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
851  assert( vFrame != NULL );
852  return Vec_IntEntry( vFrame, ObjNum );
853 }
854 
855 /**Function*************************************************************
856 
857  Synopsis []
858 
859  Description []
860 
861  SideEffects []
862 
863  SeeAlso []
864 
865 ***********************************************************************/
866 static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int iLit )
867 {
868  Vec_Int_t * vFrame;
869  int ObjNum;
870  assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
871  ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
872  vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
873  Vec_IntWriteEntry( vFrame, ObjNum, iLit );
874 /*
875  if ( Vec_IntEntry( p->vMapRefs, Aig_ObjId(pObj) ) > 1 )
876  p->nLitUsed++;
877  else
878  p->nLitUseless++;
879 */
880  return iLit;
881 }
882 
883 
884 /**Function*************************************************************
885 
886  Synopsis []
887 
888  Description []
889 
890  SideEffects []
891 
892  SeeAlso []
893 
894 ***********************************************************************/
895 static inline int Saig_ManBmcCof0( int t, int v )
896 {
897  static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
898  return 0xffff & ((t & ~s_Truth[v]) | ((t & ~s_Truth[v]) << (1<<v)));
899 }
900 static inline int Saig_ManBmcCof1( int t, int v )
901 {
902  static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
903  return 0xffff & ((t & s_Truth[v]) | ((t & s_Truth[v]) >> (1<<v)));
904 }
905 static inline int Saig_ManBmcCofEqual( int t, int v )
906 {
907  assert( v >= 0 && v <= 3 );
908  if ( v == 0 )
909  return ((t & 0xAAAA) >> 1) == (t & 0x5555);
910  if ( v == 1 )
911  return ((t & 0xCCCC) >> 2) == (t & 0x3333);
912  if ( v == 2 )
913  return ((t & 0xF0F0) >> 4) == (t & 0x0F0F);
914  if ( v == 3 )
915  return ((t & 0xFF00) >> 8) == (t & 0x00FF);
916  return -1;
917 }
918 
919 /**Function*************************************************************
920 
921  Synopsis [Derives CNF for one node.]
922 
923  Description []
924 
925  SideEffects []
926 
927  SeeAlso []
928 
929 ***********************************************************************/
930 static inline int Saig_ManBmcReduceTruth( int uTruth, int Lits[] )
931 {
932  int v;
933  for ( v = 0; v < 4; v++ )
934  if ( Lits[v] == 0 )
935  {
936  uTruth = Saig_ManBmcCof0(uTruth, v);
937  Lits[v] = -1;
938  }
939  else if ( Lits[v] == 1 )
940  {
941  uTruth = Saig_ManBmcCof1(uTruth, v);
942  Lits[v] = -1;
943  }
944  for ( v = 0; v < 4; v++ )
945  if ( Lits[v] == -1 )
946  assert( Saig_ManBmcCofEqual(uTruth, v) );
947  else if ( Saig_ManBmcCofEqual(uTruth, v) )
948  Lits[v] = -1;
949  return uTruth;
950 }
951 
952 /**Function*************************************************************
953 
954  Synopsis [Derives CNF for one node.]
955 
956  Description []
957 
958  SideEffects []
959 
960  SeeAlso []
961 
962 ***********************************************************************/
963 static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits[], int iLitOut )
964 {
965  int i, k, b, CutLit, nClaLits, ClaLits[5];
966  assert( uTruth > 0 && uTruth < 0xffff );
967  // write positive/negative polarity
968  for ( i = 0; i < 2; i++ )
969  {
970  if ( i )
971  uTruth = 0xffff & ~uTruth;
972 // Extra_PrintBinary( stdout, &uTruth, 16 ); Abc_Print( 1, "\n" );
973  for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
974  {
975  nClaLits = 0;
976  ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
977  CutLit = p->pSops[uTruth][k];
978  for ( b = 3; b >= 0; b-- )
979  {
980  if ( CutLit % 3 == 0 ) // value 0 --> write positive literal
981  {
982  assert( Lits[b] > 1 );
983  ClaLits[nClaLits++] = Lits[b];
984  }
985  else if ( CutLit % 3 == 1 ) // value 1 --> write negative literal
986  {
987  assert( Lits[b] > 1 );
988  ClaLits[nClaLits++] = lit_neg(Lits[b]);
989  }
990  CutLit = CutLit / 3;
991  }
992  if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
993  assert( 0 );
994  }
995  }
996 }
997 
998 /**Function*************************************************************
999 
1000  Synopsis [Derives CNF for one node.]
1001 
1002  Description []
1003 
1004  SideEffects []
1005 
1006  SeeAlso []
1007 
1008 ***********************************************************************/
1009 int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
1010 {
1011  extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
1012  int * pMapping, i, iLit, Lits[5], uTruth;
1013  iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
1014  if ( iLit != ~0 )
1015  return iLit;
1016  assert( iFrame >= 0 );
1017  if ( Aig_ObjIsCi(pObj) )
1018  {
1019  if ( Saig_ObjIsPi(p->pAig, pObj) )
1020  iLit = toLit( p->nSatVars++ );
1021  else
1022  iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
1023  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1024  }
1025  if ( Aig_ObjIsCo(pObj) )
1026  {
1027  iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
1028  if ( Aig_ObjFaninC0(pObj) )
1029  iLit = lit_neg(iLit);
1030  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1031  }
1032  assert( Aig_ObjIsNode(pObj) );
1033  pMapping = Saig_ManBmcMapping( p, pObj );
1034  for ( i = 0; i < 4; i++ )
1035  if ( pMapping[i+1] == -1 )
1036  Lits[i] = -1;
1037  else
1038  Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
1039  uTruth = 0xffff & (unsigned)pMapping[0];
1040  // propagate constants
1041  uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
1042  if ( uTruth == 0 || uTruth == 0xffff )
1043  {
1044  iLit = (uTruth == 0xffff);
1045  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1046  }
1047  // canonicize inputs
1048  uTruth = Dar_CutSortVars( uTruth, Lits );
1049  assert( uTruth != 0 && uTruth != 0xffff );
1050  if ( uTruth == 0xAAAA || uTruth == 0x5555 )
1051  {
1052  iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
1053  p->nBufNum++;
1054  }
1055  else
1056  {
1057  int iEntry, iRes;
1058  int fCompl = (uTruth & 1);
1059  Lits[4] = (uTruth & 1) ? 0xffff & ~uTruth : uTruth;
1060  iEntry = Vec_IntSize(p->vData) / 5;
1061  assert( iEntry * 5 == Vec_IntSize(p->vData) );
1062  for ( i = 0; i < 5; i++ )
1063  Vec_IntPush( p->vData, Lits[i] );
1064  iRes = Hsh_IntManAdd( p->vHash, iEntry );
1065  if ( iRes == iEntry )
1066  {
1067  iLit = toLit( p->nSatVars++ );
1068  Saig_ManBmcAddClauses( p, Lits[4], Lits, iLit );
1069  assert( iEntry == Vec_IntSize(p->vId2Lit) );
1070  Vec_IntPush( p->vId2Lit, iLit );
1071  p->nHashMiss++;
1072  }
1073  else
1074  {
1075  iLit = Vec_IntEntry( p->vId2Lit, iRes );
1076  Vec_IntShrink( p->vData, Vec_IntSize(p->vData) - 5 );
1077  p->nHashHit++;
1078  }
1079  iLit = Abc_LitNotCond( iLit, fCompl );
1080  }
1081  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1082 }
1083 
1084 
1085 /**Function*************************************************************
1086 
1087  Synopsis [Derives CNF for one node.]
1088 
1089  Description []
1090 
1091  SideEffects []
1092 
1093  SeeAlso []
1094 
1095 ***********************************************************************/
1096 void Saig_ManBmcCreateCnf_iter( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, Vec_Int_t * vVisit )
1097 {
1098  if ( Saig_ManBmcLiteral( p, pObj, iFrame ) != ~0 )
1099  return;
1100  if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
1101  return;
1102  Aig_ObjSetTravIdCurrent(p->pAig, pObj);
1103  if ( Aig_ObjIsCi(pObj) )
1104  {
1105  if ( Saig_ObjIsLo(p->pAig, pObj) )
1106  Vec_IntPush( vVisit, Saig_ObjLoToLi(p->pAig, pObj)->Id );
1107  return;
1108  }
1109  if ( Aig_ObjIsCo(pObj) )
1110  {
1111  Saig_ManBmcCreateCnf_iter( p, Aig_ObjFanin0(pObj), iFrame, vVisit );
1112  return;
1113  }
1114  else
1115  {
1116  int * pMapping, i;
1117  assert( Aig_ObjIsNode(pObj) );
1118  pMapping = Saig_ManBmcMapping( p, pObj );
1119  for ( i = 0; i < 4; i++ )
1120  if ( pMapping[i+1] != -1 )
1121  Saig_ManBmcCreateCnf_iter( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame, vVisit );
1122  }
1123 }
1124 
1125 /**Function*************************************************************
1126 
1127  Synopsis [Recursively performs terminary simulation.]
1128 
1129  Description []
1130 
1131  SideEffects []
1132 
1133  SeeAlso []
1134 
1135 ***********************************************************************/
1136 int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
1137 {
1138  unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
1139  int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
1140  if ( Value != SAIG_TER_NON )
1141  {
1142 /*
1143  // check the value of this literal in the SAT solver
1144  if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
1145  {
1146  int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
1147  if ( Lit >= 0 )
1148  {
1149  assert( Lit >= 2 );
1150  if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
1151  {
1152  p->nUniProps++;
1153  if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
1154  Value = SAIG_TER_ONE;
1155  else
1156  Value = SAIG_TER_ZER;
1157 
1158 // Value = SAIG_TER_UND; // disable!
1159 
1160  // use the new value
1161  Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
1162  // transfer to the unrolling
1163  if ( Value != SAIG_TER_UND )
1164  Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
1165  }
1166  }
1167  }
1168 */
1169  return Value;
1170  }
1171  if ( Aig_ObjIsCo(pObj) )
1172  {
1173  Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
1174  if ( Aig_ObjFaninC0(pObj) )
1175  Value = Saig_ManBmcSimInfoNot( Value );
1176  }
1177  else if ( Saig_ObjIsLo(p->pAig, pObj) )
1178  {
1179  assert( iFrame > 0 );
1180  Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
1181  }
1182  else if ( Aig_ObjIsNode(pObj) )
1183  {
1184  Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
1185  Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame );
1186  if ( Aig_ObjFaninC0(pObj) )
1187  Val0 = Saig_ManBmcSimInfoNot( Val0 );
1188  if ( Aig_ObjFaninC1(pObj) )
1189  Val1 = Saig_ManBmcSimInfoNot( Val1 );
1190  Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
1191  }
1192  else assert( 0 );
1193  Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
1194  // transfer to the unrolling
1195  if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
1196  Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
1197  return Value;
1198 }
1199 
1200 /**Function*************************************************************
1201 
1202  Synopsis [Derives CNF for one node.]
1203 
1204  Description []
1205 
1206  SideEffects []
1207 
1208  SeeAlso []
1209 
1210 ***********************************************************************/
1211 int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
1212 {
1213  Vec_Int_t * vVisit, * vVisit2;
1214  Aig_Obj_t * pTemp;
1215  int Lit, f, i;
1216  // perform ternary simulation
1217  int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
1218  if ( Value != SAIG_TER_UND )
1219  return (int)(Value == SAIG_TER_ONE);
1220  // construct CNF if value is ternary
1221 // Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
1222  Vec_WecClear( p->vVisited );
1223  vVisit = Vec_WecPushLevel( p->vVisited );
1224  Vec_IntPush( vVisit, Aig_ObjId(pObj) );
1225  for ( f = iFrame; f >= 0; f-- )
1226  {
1227  Aig_ManIncrementTravId( p->pAig );
1228  vVisit2 = Vec_WecPushLevel( p->vVisited );
1229  vVisit = Vec_WecEntry( p->vVisited, Vec_WecSize(p->vVisited)-2 );
1230  Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
1231  Saig_ManBmcCreateCnf_iter( p, pTemp, f, vVisit2 );
1232  if ( Vec_IntSize(vVisit2) == 0 )
1233  break;
1234  }
1235  Vec_WecForEachLevelReverse( p->vVisited, vVisit, f )
1236  Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
1237  Saig_ManBmcCreateCnf_rec( p, pTemp, iFrame-f );
1238  Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
1239  // extend the SAT solver
1240  if ( p->nSatVars > sat_solver_nvars(p->pSat) )
1241  sat_solver_setnvars( p->pSat, p->nSatVars );
1242  return Lit;
1243 }
1244 
1245 
1246 
1247 /**Function*************************************************************
1248 
1249  Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
1250 
1251  Description []
1252 
1253  SideEffects []
1254 
1255  SeeAlso []
1256 
1257 ***********************************************************************/
1258 int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
1259 {
1260  int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2);
1261  if ( Diff < 0 )
1262  return -1;
1263  if ( Diff > 0 )
1264  return 1;
1265  Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
1266  if ( Diff < 0 )
1267  return -1;
1268  if ( Diff > 0 )
1269  return 1;
1270  return 0;
1271 }
1272 
1273 /**Function*************************************************************
1274 
1275  Synopsis [This procedure sets default parameters.]
1276 
1277  Description []
1278 
1279  SideEffects []
1280 
1281  SeeAlso []
1282 
1283 ***********************************************************************/
1284 void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
1285 {
1286  memset( p, 0, sizeof(Saig_ParBmc_t) );
1287  p->nStart = 0; // maximum number of timeframes
1288  p->nFramesMax = 0; // maximum number of timeframes
1289  p->nConfLimit = 0; // maximum number of conflicts at a node
1290  p->nConfLimitJump = 0; // maximum number of conflicts after jumping
1291  p->nFramesJump = 0; // the number of tiemframes to jump
1292  p->nTimeOut = 0; // approximate timeout in seconds
1293  p->nTimeOutGap = 0; // time since the last CEX found
1294  p->nPisAbstract = 0; // the number of PIs to abstract
1295  p->fSolveAll = 0; // stops on the first SAT instance
1296  p->fDropSatOuts = 0; // replace sat outputs by constant 0
1297  p->nLearnedStart = 10000; // starting learned clause limit
1298  p->nLearnedDelta = 2000; // delta of learned clause limit
1299  p->nLearnedPerce = 80; // ratio of learned clause limit
1300  p->fVerbose = 0; // verbose
1301  p->fNotVerbose = 0; // skip line-by-line print-out
1302  p->iFrame = -1; // explored up to this frame
1303  p->nFailOuts = 0; // the number of failed outputs
1304  p->nDropOuts = 0; // the number of timed out outputs
1305  p->timeLastSolved = 0; // time when the last one was solved
1306 }
1307 
1308 /**Function*************************************************************
1309 
1310  Synopsis [Returns time to stop.]
1311 
1312  Description []
1313 
1314  SideEffects []
1315 
1316  SeeAlso []
1317 
1318 ***********************************************************************/
1319 abctime Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, abctime nTimeToStopNG )
1320 {
1321  abctime nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + Abc_Clock(): 0;
1322  abctime nTimeToStop = 0;
1323  if ( nTimeToStopNG && nTimeToStopGap )
1324  nTimeToStop = nTimeToStopNG < nTimeToStopGap ? nTimeToStopNG : nTimeToStopGap;
1325  else if ( nTimeToStopNG )
1326  nTimeToStop = nTimeToStopNG;
1327  else if ( nTimeToStopGap )
1328  nTimeToStop = nTimeToStopGap;
1329  return nTimeToStop;
1330 }
1331 
1332 /**Function*************************************************************
1333 
1334  Synopsis []
1335 
1336  Description []
1337 
1338  SideEffects []
1339 
1340  SeeAlso []
1341 
1342 ***********************************************************************/
1343 Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
1344 {
1345  Aig_Obj_t * pObjPi;
1346  Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), f*Saig_ManPoNum(p->pAig)+i );
1347  int j, k, iBit = Saig_ManRegNum(p->pAig);
1348  for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(p->pAig) )
1349  Saig_ManForEachPi( p->pAig, pObjPi, k )
1350  {
1351  int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
1352  if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
1353  Abc_InfoSetBit( pCex->pData, iBit + k );
1354  }
1355  return pCex;
1356 }
1357 
1358 
1359 /**Function*************************************************************
1360 
1361  Synopsis []
1362 
1363  Description []
1364 
1365  SideEffects []
1366 
1367  SeeAlso []
1368 
1369 ***********************************************************************/
1370 int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
1371 {
1372  if ( Lit == 0 )
1373  return l_False;
1374  if ( Lit == 1 )
1375  return l_True;
1376  return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1377 }
1378 
1379 /**Function*************************************************************
1380 
1381  Synopsis [Bounded model checking engine.]
1382 
1383  Description []
1384 
1385  SideEffects []
1386 
1387  SeeAlso []
1388 
1389 ***********************************************************************/
1390 int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
1391 {
1392  Gia_ManBmc_t * p;
1393  Aig_Obj_t * pObj;
1394  Abc_Cex_t * pCexNew, * pCexNew0;
1395  FILE * pLogFile = NULL;
1396  unsigned * pInfo;
1397  int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
1398  int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
1399  int i, f, k, Lit, status;
1400  abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
1401  abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
1402  abctime nTimeToStopNG, nTimeToStop;
1403  if ( pPars->pLogFileName )
1404  pLogFile = fopen( pPars->pLogFileName, "wb" );
1405  if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
1406  pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
1407  if ( pPars->nTimeOutOne && !pPars->fSolveAll )
1408  pPars->nTimeOutOne = 0;
1409  nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1410  nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
1411  // create BMC manager
1412  p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
1413  p->pPars = pPars;
1414  p->pSat->nLearntStart = p->pPars->nLearnedStart;
1415  p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1416  p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1417  p->pSat->nLearntMax = p->pSat->nLearntStart;
1418  if ( pPars->fSolveAll && p->vCexes == NULL )
1419  p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
1420  if ( pPars->fVerbose )
1421  {
1422  Abc_Print( 1, "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d.\n",// Sect =%3d.\n",
1423  Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
1424  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums );//, Vec_VecSize(p->vSects) );
1425  Abc_Print( 1, "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",
1426  pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
1427  }
1428  pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
1429  // set runtime limit
1430  if ( nTimeToStop )
1431  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
1432  // perform frames
1433  Aig_ManRandom( 1 );
1434  pPars->timeLastSolved = Abc_Clock();
1435  for ( f = 0; f < pPars->nFramesMax; f++ )
1436  {
1437  // stop BMC after exploring all reachable states
1438  if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
1439  {
1440  Abc_Print( 1, "Stopping BMC because all 2^%d reachable states are visited.\n", Aig_ManRegNum(pAig) );
1441  if ( p->pPars->fUseBridge )
1442  Saig_ManForEachPo( pAig, pObj, i )
1443  if ( !(p->vCexes && Vec_PtrEntry(p->vCexes, i)) && !(p->pTime4Outs && p->pTime4Outs[i] == 0) ) // not SAT and not timed out
1444  Gia_ManToBridgeResult( stdout, 1, NULL, i );
1445  RetValue = pPars->nFailOuts ? 0 : 1;
1446  goto finish;
1447  }
1448  // stop BMC if all targets are solved
1449  if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) )
1450  {
1451  Abc_Print( 1, "Stopping BMC because all targets are disproved or timed out.\n" );
1452  RetValue = pPars->nFailOuts ? 0 : 1;
1453  goto finish;
1454  }
1455  // consider the next timeframe
1456  if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
1457  pPars->iFrame = f-1;
1458  // map nodes of this section
1459  Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
1460  Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
1461 /*
1462  // cannot remove mapping of frame values for any timeframes
1463  // because with constant propagation they may be needed arbitrarily far
1464  if ( f > 2*Vec_VecSize(p->vSects) )
1465  {
1466  int iFrameOld = f - 2*Vec_VecSize( p->vSects );
1467  void * pMemory = Vec_IntReleaseArray( Vec_PtrEntry(p->vId2Var, iFrameOld) );
1468  ABC_FREE( pMemory );
1469  }
1470 */
1471  // prepare some nodes
1472  Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
1473  Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
1474  Saig_ManForEachPi( pAig, pObj, i )
1475  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
1476  if ( f == 0 )
1477  {
1478  Saig_ManForEachLo( p->pAig, pObj, i )
1479  {
1480  Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
1481  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
1482  }
1483  }
1484  if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
1485  continue;
1486  // create CNF upfront
1487  if ( pPars->fSolveAll )
1488  {
1489  Saig_ManForEachPo( pAig, pObj, i )
1490  {
1491  if ( i >= Saig_ManPoNum(pAig) )
1492  break;
1493  // check for timeout
1494  if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
1495  {
1496  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
1497  goto finish;
1498  }
1499  if ( nTimeToStop && Abc_Clock() > nTimeToStop )
1500  {
1501  if ( !pPars->fSilent )
1502  Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
1503  goto finish;
1504  }
1505  // skip solved outputs
1506  if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
1507  continue;
1508  // skip output whose time has run out
1509  if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
1510  continue;
1511  // add constraints for this output
1512 clk2 = Abc_Clock();
1513  Saig_ManBmcCreateCnf( p, pObj, f );
1514 clkOther += Abc_Clock() - clk2;
1515  }
1516  }
1517  // solve SAT
1518  clk = Abc_Clock();
1519  Saig_ManForEachPo( pAig, pObj, i )
1520  {
1521  if ( i >= Saig_ManPoNum(pAig) )
1522  break;
1523  // check for timeout
1524  if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
1525  {
1526  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
1527  goto finish;
1528  }
1529  if ( nTimeToStop && Abc_Clock() > nTimeToStop )
1530  {
1531  if ( !pPars->fSilent )
1532  Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
1533  goto finish;
1534  }
1535  // skip solved outputs
1536  if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
1537  continue;
1538  // skip output whose time has run out
1539  if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
1540  continue;
1541  // add constraints for this output
1542 clk2 = Abc_Clock();
1543  Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1544 clkOther += Abc_Clock() - clk2;
1545  // solve this output
1546  fUnfinished = 0;
1547  sat_solver_compress( p->pSat );
1548  if ( p->pTime4Outs )
1549  {
1550  assert( p->pTime4Outs[i] > 0 );
1551  clkOne = Abc_Clock();
1552  sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
1553  }
1554 clk2 = Abc_Clock();
1555  status = Saig_ManCallSolver( p, Lit );
1556 clkSatRun = Abc_Clock() - clk2;
1557  if ( pLogFile )
1558  fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d %8d\n", f, i,
1559  Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC),
1560  Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) );
1561  if ( p->pTime4Outs )
1562  {
1563  abctime timeSince = Abc_Clock() - clkOne;
1564  assert( p->pTime4Outs[i] > 0 );
1565  p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
1566  if ( p->pTime4Outs[i] == 0 && status != l_True )
1567  pPars->nDropOuts++;
1568  }
1569  if ( status == l_False )
1570  {
1571 nTimeUnsat += clkSatRun;
1572  if ( Lit != 0 )
1573  {
1574  // add final unit clause
1575  Lit = lit_neg( Lit );
1576  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
1577  assert( status );
1578  // add learned units
1579  for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
1580  {
1581  Lit = veci_begin(&p->pSat->unit_lits)[k];
1582  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
1583  assert( status );
1584  }
1585  veci_resize(&p->pSat->unit_lits, 0);
1586  // propagate units
1587  sat_solver_compress( p->pSat );
1588  }
1589  if ( p->pPars->fUseBridge )
1590  Gia_ManReportProgress( stdout, i, f );
1591  }
1592  else if ( status == l_True )
1593  {
1594 nTimeSat += clkSatRun;
1595  RetValue = 0;
1596  fFirst = 0;
1597  if ( !pPars->fSolveAll )
1598  {
1599  if ( pPars->fVerbose )
1600  {
1601  Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
1602  Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
1603  Abc_Print( 1, "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
1604  Abc_Print( 1, "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
1605 // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
1606  Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
1607 // ABC_PRT( "Time", Abc_Clock() - clk );
1608  Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
1609  Abc_Print( 1, "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
1610  Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
1611 // Abc_Print( 1, "\n" );
1612 // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
1613 // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
1614 // Abc_Print( 1, "S =%6d. ", p->nBufNum );
1615 // Abc_Print( 1, "D =%6d. ", p->nDupNum );
1616  Abc_Print( 1, "\n" );
1617  fflush( stdout );
1618  }
1619  ABC_FREE( pAig->pSeqModel );
1620  pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
1621  goto finish;
1622  }
1623  pPars->nFailOuts++;
1624  if ( !pPars->fNotVerbose )
1625  Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
1626  nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
1627  if ( p->vCexes == NULL )
1628  p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
1629  pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
1630  pCexNew0 = NULL;
1631  if ( p->pPars->fUseBridge )
1632  {
1633  Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1634  //Abc_CexFree( pCexNew );
1635  pCexNew0 = pCexNew;
1636  pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
1637  }
1638  Vec_PtrWriteEntry( p->vCexes, i, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
1639  if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
1640  {
1641  Abc_CexFreeP( &pCexNew0 );
1642  Abc_Print( 1, "Quitting due to callback on fail.\n" );
1643  goto finish;
1644  }
1645  // reset the timeout
1646  pPars->timeLastSolved = Abc_Clock();
1647  nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
1648  if ( nTimeToStop )
1649  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
1650 
1651  // check if other outputs failed under the same counter-example
1652  Saig_ManForEachPo( pAig, pObj, k )
1653  {
1654  if ( k >= Saig_ManPoNum(pAig) )
1655  break;
1656  // skip solved outputs
1657  if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
1658  continue;
1659  // check if this output is solved
1660  Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1661  if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
1662  continue;
1663  // write entry
1664  pPars->nFailOuts++;
1665  if ( !pPars->fNotVerbose )
1666  Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
1667  nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
1668  // report to the bridge
1669  if ( p->pPars->fUseBridge )
1670  {
1671  // set the output number
1672  pCexNew0->iPo = k;
1673  Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
1674  }
1675  // remember solved output
1676  Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
1677  }
1678  Abc_CexFreeP( &pCexNew0 );
1679  Abc_CexFree( pCexNew );
1680  }
1681  else
1682  {
1683 nTimeUndec += clkSatRun;
1684  assert( status == l_Undef );
1685  if ( pPars->nFramesJump )
1686  {
1687  pPars->nConfLimit = pPars->nConfLimitJump;
1688  nJumpFrame = f + pPars->nFramesJump;
1689  fUnfinished = 1;
1690  break;
1691  }
1692  if ( p->pTime4Outs == NULL )
1693  goto finish;
1694  }
1695  }
1696  if ( pPars->fVerbose )
1697  {
1698  if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 )
1699  {
1700  fFirst = 0;
1701 // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
1702  }
1703  Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
1704  Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
1705 // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
1706  Abc_Print( 1, "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
1707  Abc_Print( 1, "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
1708 // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
1709  Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
1710  if ( pPars->fSolveAll )
1711  Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
1712  if ( pPars->nTimeOutOne )
1713  Abc_Print( 1, "T/O =%4d. ", pPars->nDropOuts );
1714 // ABC_PRT( "Time", Abc_Clock() - clk );
1715 // Abc_Print( 1, "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
1716  Abc_Print( 1, "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );
1717  Abc_Print( 1, "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
1718 // Abc_Print( 1, " %6d %6d ", p->nLitUsed, p->nLitUseless );
1719  Abc_Print( 1, "%9.2f sec ", 1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
1720 // Abc_Print( 1, "\n" );
1721 // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
1722 // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
1723 // Abc_Print( 1, "Simples = %6d. ", p->nBufNum );
1724 // Abc_Print( 1, "Dups = %6d. ", p->nDupNum );
1725  Abc_Print( 1, "\n" );
1726  fflush( stdout );
1727  }
1728  }
1729  // consider the next timeframe
1730  if ( nJumpFrame && pPars->nStart == 0 )
1731  pPars->iFrame = nJumpFrame - pPars->nFramesJump;
1732  else if ( RetValue == -1 && pPars->nStart == 0 )
1733  pPars->iFrame = f-1;
1734 //ABC_PRT( "CNF generation runtime", clkOther );
1735 finish:
1736  if ( pPars->fVerbose )
1737  {
1738  Abc_Print( 1, "Runtime: " );
1739  Abc_Print( 1, "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(Abc_Clock() - clkTotal) );
1740  Abc_Print( 1, "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
1741  Abc_Print( 1, "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(Abc_Clock() - clkTotal) );
1742  Abc_Print( 1, "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
1743  Abc_Print( 1, "\n" );
1744  }
1745  Saig_Bmc3ManStop( p );
1746  fflush( stdout );
1747  if ( pLogFile )
1748  fclose( pLogFile );
1749  return RetValue;
1750 }
1751 
1752 ////////////////////////////////////////////////////////////////////////
1753 /// END OF FILE ///
1754 ////////////////////////////////////////////////////////////////////////
1755 
1756 
1757 ABC_NAMESPACE_IMPL_END
1758 
memset
char * memset()
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_VecForEachLevel
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Saig_ParBmc_t_::nConfLimitJump
int nConfLimitJump
Definition: bmc.h:51
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_ManBmcSimInfoClear
static int Saig_ManBmcSimInfoClear(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:118
Saig_ParBmc_t_::nLearnedPerce
int nLearnedPerce
Definition: bmc.h:65
SAIG_TER_NON
#define SAIG_TER_NON
FUNCTION DEFINITIONS ///.
Definition: bmcBmc3.c:83
Vec_WecAlloc
static Vec_Wec_t * Vec_WecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWec.h:87
Gia_ManBmc_t_::nSatVars
int nSatVars
Definition: bmcBmc3.c:63
Aig_NodeCompareRefsIncrease
int Aig_NodeCompareRefsIncrease(Aig_Obj_t **pp1, Aig_Obj_t **pp2)
Definition: bmcBmc3.c:1258
free
VOID_HACK free()
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition: vecWec.h:42
Saig_ManCallSolver
int Saig_ManCallSolver(Gia_ManBmc_t *p, int Lit)
Definition: bmcBmc3.c:1370
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Saig_ParBmc_t_::nDropOuts
int nDropOuts
Definition: bmc.h:72
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
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
Saig_ManGenerateCex
Abc_Cex_t * Saig_ManGenerateCex(Gia_ManBmc_t *p, int f, int i)
Definition: bmcBmc3.c:1343
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Gia_ManBmc_t_::nHashHit
int nHashHit
Definition: bmcBmc3.c:54
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManBmc_t_::pSopSizes
char * pSopSizes
Definition: bmcBmc3.c:66
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
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
Saig_ManBmcCountRefed
int Saig_ManBmcCountRefed(Aig_Man_t *p, Vec_Ptr_t *vSuper)
Definition: bmcBmc3.c:532
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Gia_ManBmc_t_::vTerInfo
Vec_Ptr_t * vTerInfo
Definition: bmcBmc3.c:46
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ParBmc_t_::nLearnedStart
int nLearnedStart
Definition: bmc.h:63
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
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
sat_solver_compress
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Vec_WecFree
static void Vec_WecFree(Vec_Wec_t *p)
Definition: vecWec.h:345
Gia_ManBmc_t_::vMapping
Vec_Int_t * vMapping
Definition: bmcBmc3.c:42
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
Saig_ParBmc_t_::nTimeOutOne
int nTimeOutOne
Definition: bmc.h:55
Vec_PtrFreeFree
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
Saig_ParBmc_t_
Definition: bmc.h:46
Vec_WecPushLevel
static Vec_Int_t * Vec_WecPushLevel(Vec_Wec_t *p)
Definition: vecWec.h:284
Gia_ManBmc_t_::vId2Lit
Vec_Int_t * vId2Lit
Definition: bmcBmc3.c:53
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Gia_ManBmc_t_::nUniProps
int nUniProps
Definition: bmcBmc3.c:58
Saig_ManBmcScalable
int Saig_ManBmcScalable(Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
Definition: bmcBmc3.c:1390
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Saig_ParBmc_t_::fVerbose
int fVerbose
Definition: bmc.h:66
Saig_ManBmcTerSimCount01
int Saig_ManBmcTerSimCount01(Aig_Man_t *p, unsigned *pInfo)
Definition: bmcBmc3.c:136
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Gia_ManBmc_t_::nBufNum
int nBufNum
Definition: bmcBmc3.c:56
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Saig_ParBmc_t_::nFailOuts
int nFailOuts
Definition: bmc.h:71
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Saig_ParBmc_t_::nStart
int nStart
Definition: bmc.h:48
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Saig_ParBmc_t_::pFuncOnFail
int(* pFuncOnFail)(int, Abc_Cex_t *)
Definition: bmc.h:74
Saig_ParBmc_t_::nTimeOutGap
int nTimeOutGap
Definition: bmc.h:54
Saig_ParBmc_t_::iFrame
int iFrame
Definition: bmc.h:70
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
Saig_ManBmcTerSim
Vec_Ptr_t * Saig_ManBmcTerSim(Aig_Man_t *p)
Definition: bmcBmc3.c:209
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Saig_ParBmc_t_::nConfLimit
int nConfLimit
Definition: bmc.h:50
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Saig_ManBmcCreateCnf_iter
void Saig_ManBmcCreateCnf_iter(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
Definition: bmcBmc3.c:1096
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
Saig_ManBmcLiteral
static int Saig_ManBmcLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:843
sat_solver_memory
double sat_solver_memory(sat_solver *s)
Definition: satSolver.c:1236
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Saig_ManBmcCountNonternary_rec
int Saig_ManBmcCountNonternary_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vInfos, unsigned *pInfo, int f, int *pCounter)
Definition: bmcBmc3.c:263
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
sat_solver_count_assigned
int sat_solver_count_assigned(sat_solver *s)
Definition: satSolver.c:609
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Saig_ManBmcRunTerSim_rec
int Saig_ManBmcRunTerSim_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1136
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_ManBmcCof1
static int Saig_ManBmcCof1(int t, int v)
Definition: bmcBmc3.c:900
Vec_WecSize
static int Vec_WecSize(Vec_Wec_t *p)
Definition: vecWec.h:193
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Saig_ManBmcCofEqual
static int Saig_ManBmcCofEqual(int t, int v)
Definition: bmcBmc3.c:905
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Gia_ManBmc_t_::pSat
sat_solver * pSat
Definition: bmcBmc3.c:62
Saig_ManBmcWriteBlif
void Saig_ManBmcWriteBlif(Aig_Man_t *p, Vec_Int_t *vMapping, char *pFileName)
Definition: bmcBmc3.c:581
Saig_ParBmc_t_::nTimeOut
int nTimeOut
Definition: bmc.h:53
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Cnf_DeriveMappingArray
Vec_Int_t * Cnf_DeriveMappingArray(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition: cnfCore.c:78
Saig_ParBmc_t_::nFramesMax
int nFramesMax
Definition: bmc.h:49
Vec_WecClear
static void Vec_WecClear(Vec_Wec_t *p)
Definition: vecWec.h:255
Gia_ManBmc_t_::nWordNum
int nWordNum
Definition: bmcBmc3.c:65
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
Gia_ManBmc_t_::pAig
Aig_Man_t * pAig
Definition: bmcBmc3.c:39
Gia_ManBmc_t_::vId2Num
Vec_Int_t * vId2Num
Definition: bmcBmc3.c:45
Saig_ParBmc_t_::timeLastSolved
abctime timeLastSolved
Definition: bmc.h:73
Saig_ParBmc_t_::fDropSatOuts
int fDropSatOuts
Definition: bmc.h:60
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Saig_ParBmcSetDefaultParams
void Saig_ParBmcSetDefaultParams(Saig_ParBmc_t *p)
Definition: bmcBmc3.c:1284
Saig_ManBmcTerSimOne
unsigned * Saig_ManBmcTerSimOne(Aig_Man_t *p, unsigned *pPrev)
Definition: bmcBmc3.c:159
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Saig_ManBmcSimInfoAnd
static int Saig_ManBmcSimInfoAnd(int Value0, int Value1)
Definition: bmcBmc3.c:97
Saig_ManBmcSimInfoSet
static void Saig_ManBmcSimInfoSet(unsigned *pInfo, Aig_Obj_t *pObj, int Value)
Definition: bmcBmc3.c:111
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition: cnfData.c:4537
Saig_ManBmcSimInfoNot
static int Saig_ManBmcSimInfoNot(int Value)
Definition: bmcBmc3.c:88
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Saig_Bmc3ManStart
Gia_ManBmc_t * Saig_Bmc3ManStart(Aig_Man_t *pAig, int nTimeOutOne)
Definition: bmcBmc3.c:717
Dar_CutSortVars
unsigned Dar_CutSortVars(unsigned uTruth, int *pVars)
Definition: darCut.c:521
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_Bmc3ManStop
void Saig_Bmc3ManStop(Gia_ManBmc_t *p)
Definition: bmcBmc3.c:776
Saig_ParBmc_t_::nFramesJump
int nFramesJump
Definition: bmc.h:52
toLit
static lit toLit(int v)
Definition: satVec.h:142
Saig_ParBmc_t_::fStoreCex
int fStoreCex
Definition: bmc.h:58
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Saig_ManBmcCreateCnf_rec
int Saig_ManBmcCreateCnf_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1009
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Saig_ManBmcSetLiteral
static int Saig_ManBmcSetLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, int iLit)
Definition: bmcBmc3.c:866
Saig_ManBmcSupergate_rec
void Saig_ManBmcSupergate_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: bmcBmc3.c:474
Gia_ManBmc_t_::vId2Var
Vec_Ptr_t * vId2Var
Definition: bmcBmc3.c:47
Saig_ManBmcAddClauses
static void Saig_ManBmcAddClauses(Gia_ManBmc_t *p, int uTruth, int Lits[], int iLitOut)
Definition: bmcBmc3.c:963
Gia_ManBmc_t
typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t
DECLARATIONS ///.
Definition: bmcBmc3.c:34
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
Gia_ManBmc_t_::pTime4Outs
abctime * pTime4Outs
Definition: bmcBmc3.c:49
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
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
Saig_ParBmc_t_::fNotVerbose
int fNotVerbose
Definition: bmc.h:67
if
if(last==0)
Definition: sparse_int.h:34
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Saig_ManBmcReduceTruth
static int Saig_ManBmcReduceTruth(int uTruth, int Lits[])
Definition: bmcBmc3.c:930
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Saig_ManBmcTerSimCount01Po
int Saig_ManBmcTerSimCount01Po(Aig_Man_t *p, unsigned *pInfo)
Definition: bmcBmc3.c:305
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
Hsh_IntManStop
static void Hsh_IntManStop(Hsh_IntMan_t *p)
Definition: vecHsh.h:119
Saig_ManBmcComputeMappingRefs
Vec_Int_t * Saig_ManBmcComputeMappingRefs(Aig_Man_t *p, Vec_Int_t *vMap)
Definition: bmcBmc3.c:686
Gia_ManBmc_t_
Definition: bmcBmc3.c:35
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Saig_ManBmcDfs_rec
void Saig_ManBmcDfs_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: bmcBmc3.c:354
Gia_ManBmc_t_::nObjNums
int nObjNums
Definition: bmcBmc3.c:64
Saig_ParBmc_t_::nPisAbstract
int nPisAbstract
Definition: bmc.h:56
Saig_ManBmcCountNonternary
void Saig_ManBmcCountNonternary(Aig_Man_t *p, Vec_Ptr_t *vInfos, int iFrame)
Definition: bmcBmc3.c:281
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Saig_ManBmcSections
Vec_Vec_t * Saig_ManBmcSections(Aig_Man_t *p)
Definition: bmcBmc3.c:401
Vec_WecEntry
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
Hsh_IntManAdd
static int Hsh_IntManAdd(Hsh_IntMan_t *p, int iData)
Definition: vecHsh.h:157
Gia_ManBmc_t_::vHash
Hsh_IntMan_t * vHash
Definition: bmcBmc3.c:52
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
Gia_ManBmc_t_::nDupNum
int nDupNum
Definition: bmcBmc3.c:57
Aig_ManLevelNum
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
Gia_ManBmc_t_::pPars
Saig_ParBmc_t * pPars
Definition: bmcBmc3.c:38
Saig_ManBmcSectionsTest
void Saig_ManBmcSectionsTest(Aig_Man_t *p)
Definition: bmcBmc3.c:449
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManBmcTimeToStop
abctime Saig_ManBmcTimeToStop(Saig_ParBmc_t *pPars, abctime nTimeToStopNG)
Definition: bmcBmc3.c:1319
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
Saig_ParBmc_t_::fSilent
int fSilent
Definition: bmc.h:69
sat_solver_count_usedvars
static int sat_solver_count_usedvars(sat_solver *s)
Definition: satSolver.h:265
Gia_ManBmc_t_::nLitUseless
int nLitUseless
Definition: bmcBmc3.c:60
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ManToBridgeProgress
int Gia_ManToBridgeProgress(FILE *pFile, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:182
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_CexDup
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ManBmc_t_::vVisited
Vec_Wec_t * vVisited
Definition: bmcBmc3.c:48
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Vec_WecForEachLevelReverse
#define Vec_WecForEachLevelReverse(vGlob, vVec, i)
Definition: vecWec.h:65
Gia_ManBmc_t_::pSops
char ** pSops
Definition: bmcBmc3.c:66
Saig_ManBmcDfsNodes
Vec_Ptr_t * Saig_ManBmcDfsNodes(Aig_Man_t *p, Vec_Ptr_t *vRoots)
Definition: bmcBmc3.c:379
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Saig_ManBmcCof0
static int Saig_ManBmcCof0(int t, int v)
Definition: bmcBmc3.c:895
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
Saig_ManBmcMappingTest
void Saig_ManBmcMappingTest(Aig_Man_t *p)
Definition: bmcBmc3.c:666
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
strlen
int strlen()
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManBmc_t_::vMapRefs
Vec_Int_t * vMapRefs
Definition: bmcBmc3.c:43
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Saig_ParBmc_t_::pLogFileName
char * pLogFileName
Definition: bmc.h:68
Saig_ManBmcCreateCnf
int Saig_ManBmcCreateCnf(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1211
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
Gia_ManReportProgress
void Gia_ManReportProgress(FILE *pFile, int prop_no, int depth)
Definition: bmcBmc3.c:71
Gia_ManBmc_t_::vCexes
Vec_Ptr_t * vCexes
Definition: bmcBmc3.c:40
Hsh_IntManStart
static Hsh_IntMan_t * Hsh_IntManStart(Vec_Int_t *vData, int nSize, int nEntries)
FUNCTION DEFINITIONS ///.
Definition: vecHsh.h:109
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
Gia_ManBmc_t_::nLitUsed
int nLitUsed
Definition: bmcBmc3.c:59
Gia_ManBmc_t_::vData
Vec_Int_t * vData
Definition: bmcBmc3.c:51
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManBmc_t_::nHashMiss
int nHashMiss
Definition: bmcBmc3.c:55
veci_begin
static int * veci_begin(veci *v)
Definition: satVec.h:45
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ManBmcSupergate
Vec_Ptr_t * Saig_ManBmcSupergate(Aig_Man_t *p, int iPo)
Definition: bmcBmc3.c:498
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Saig_ParBmc_t_::nLearnedDelta
int nLearnedDelta
Definition: bmc.h:64
veci_size
static int veci_size(veci *v)
Definition: satVec.h:46
Gia_ManToBridgeResult
int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition: utilBridge.c:284
Saig_ParBmc_t_::fSolveAll
int fSolveAll
Definition: bmc.h:57
Saig_ManBmcSupergateTest
void Saig_ManBmcSupergateTest(Aig_Man_t *p)
Definition: bmcBmc3.c:555
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManBmcTerSimTestPo
void Saig_ManBmcTerSimTestPo(Aig_Man_t *p)
Definition: bmcBmc3.c:333
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Saig_ManBmcTerSimTest
void Saig_ManBmcTerSimTest(Aig_Man_t *p)
Definition: bmcBmc3.c:238
Hsh_IntMan_t_
Definition: vecHsh.h:57
Saig_ManBmcTerSimPo
Vec_Ptr_t * Saig_ManBmcTerSimPo(Aig_Man_t *p)
Definition: bmcBmc3.c:313