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