ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bmcBmc3.c
Go to the documentation of this file.
1
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
30ABC_NAMESPACE_IMPL_START
31
35
36typedef struct Gia_ManBmc_t_ Gia_ManBmc_t;
37struct 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
73extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
74
75void 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
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
92static 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
101static 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
110static 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
115static 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
122static 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
140int 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
163unsigned * 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
213Vec_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
242void 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
267int 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}
285void 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
309int 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}
317Vec_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}
337void 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
358void 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
383Vec_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
405Vec_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
453void 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
478void 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
502Vec_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
536int 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
559void 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
585void 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
670void 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
690Vec_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
721Gia_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
799void 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
855static 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
873static 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
896static 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
925static 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}
930static 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}
935static 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
960static 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
993static 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
1052int 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
1139void 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
1179int 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
1254int 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
1308int 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
1334void 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
1369abctime 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
1393Abc_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
1433int 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
1461int 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
1606clk2 = Abc_Clock();
1607 Saig_ManBmcCreateCnf( p, pObj, f );
1608clkOther += 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
1642clk2 = Abc_Clock();
1643 Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1644clkOther += 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 }
1659clk2 = Abc_Clock();
1660 status = Saig_ManCallSolver( p, Lit );
1661clkSatRun = 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 {
1676nTimeUnsat += 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 {
1707nTimeSat += 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 Abc_Cex_t * pCexDup;
1776 if ( k >= Saig_ManPoNum(pAig) )
1777 break;
1778 // skip solved outputs
1779 if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
1780 continue;
1781 // check if this output is solved
1782 Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1783 if ( p->pSat2 )
1784 {
1785 if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
1786 continue;
1787 }
1788 else if ( p->pSat3 )
1789 {
1790 if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
1791 continue;
1792 }
1793 else
1794 {
1795 if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
1796 continue;
1797 }
1798 // write entry
1799 pPars->nFailOuts++;
1800 if ( !pPars->fNotVerbose )
1801 Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
1802 nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
1803 // report to the bridge
1804 if ( p->pPars->fUseBridge )
1805 {
1806 // set the output number
1807 pCexNew0->iPo = k;
1808 Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
1809 }
1810 // remember solved output
1811 //Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
1812 pCexDup = Abc_CexDup(pCexNew, Saig_ManRegNum(pAig));
1813 pCexDup->iPo = k;
1814 Vec_PtrWriteEntry( p->vCexes, k, pCexDup );
1815 }
1816 Abc_CexFreeP( &pCexNew0 );
1817 Abc_CexFree( pCexNew );
1818 }
1819 else
1820 {
1821nTimeUndec += clkSatRun;
1822 assert( status == l_Undef );
1823 if ( pPars->nFramesJump )
1824 {
1825 pPars->nConfLimit = pPars->nConfLimitJump;
1826 nJumpFrame = f + pPars->nFramesJump;
1827 fUnfinished = 1;
1828 break;
1829 }
1830 if ( p->pTime4Outs == NULL )
1831 goto finish;
1832 }
1833 }
1834 if ( pPars->fVerbose )
1835 {
1836 if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
1837 {
1838 fFirst = 0;
1839// Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
1840 }
1841 Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
1842 Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
1843// Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
1844 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)) );
1845 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)) );
1846// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
1847// Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
1848 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)) );
1849 if ( pPars->fSolveAll )
1850 Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
1851 if ( pPars->nTimeOutOne )
1852 Abc_Print( 1, "T/O =%4d. ", pPars->nDropOuts );
1853// ABC_PRT( "Time", Abc_Clock() - clk );
1854// Abc_Print( 1, "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
1855 Abc_Print( 1, "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );
1856 Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
1857// Abc_Print( 1, " %6d %6d ", p->nLitUsed, p->nLitUseless );
1858 Abc_Print( 1, "%9.2f sec ", 1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
1859// Abc_Print( 1, "\n" );
1860// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
1861// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
1862// Abc_Print( 1, "Simples = %6d. ", p->nBufNum );
1863// Abc_Print( 1, "Dups = %6d. ", p->nDupNum );
1864 Abc_Print( 1, "\n" );
1865 fflush( stdout );
1866 }
1867 }
1868 // consider the next timeframe
1869 if ( nJumpFrame && pPars->nStart == 0 )
1870 pPars->iFrame = nJumpFrame - pPars->nFramesJump;
1871 else if ( RetValue == -1 && pPars->nStart == 0 )
1872 pPars->iFrame = f-1;
1873//ABC_PRT( "CNF generation runtime", clkOther );
1874finish:
1875 if ( pPars->fVerbose )
1876 {
1877 Abc_Print( 1, "Runtime: " );
1878 Abc_Print( 1, "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(Abc_Clock() - clkTotal) );
1879 Abc_Print( 1, "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
1880 Abc_Print( 1, "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(Abc_Clock() - clkTotal) );
1881 Abc_Print( 1, "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
1882 Abc_Print( 1, "\n" );
1883 }
1884 Saig_Bmc3ManStop( p );
1885 fflush( stdout );
1886 if ( pLogFile )
1887 fclose( pLogFile );
1888 return RetValue;
1889}
1890
1894
1895
1896ABC_NAMESPACE_IMPL_END
1897
bmcg_sat_solver_conflictnum
int bmcg_sat_solver_conflictnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:257
bmcg_sat_solver_set_runtime_limit
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver *s, abctime Limit)
Definition AbcGlucose.cpp:230
bmcg_sat_solver_learntnum
int bmcg_sat_solver_learntnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:253
bmcg_sat_solver_varnum
int bmcg_sat_solver_varnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:245
bmcg_sat_solver_addvar
int bmcg_sat_solver_addvar(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:181
bmcg_sat_solver_start
bmcg_sat_solver * bmcg_sat_solver_start()
MACRO DEFINITIONS ///.
Definition AbcGlucose.cpp:146
bmcg_sat_solver_solve
int bmcg_sat_solver_solve(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:170
bmcg_sat_solver_addclause
int bmcg_sat_solver_addclause(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:160
bmcg_sat_solver_set_conflict_budget
void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver *s, int Limit)
Definition AbcGlucose.cpp:237
bmcg_sat_solver_read_cex_varvalue
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver *s, int ivar)
Definition AbcGlucose.cpp:220
bmcg_sat_solver_clausenum
int bmcg_sat_solver_clausenum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:249
bmcg_sat_solver_stop
void bmcg_sat_solver_stop(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:150
bmcg_sat_solver
void bmcg_sat_solver
Definition AbcGlucose.h:63
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ManLevelNum
int Aig_ManLevelNum(Aig_Man_t *p)
Definition aigDfs.c:500
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Saig_Bmc3ManStart
Gia_ManBmc_t * Saig_Bmc3ManStart(Aig_Man_t *pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose)
Definition bmcBmc3.c:721
Saig_ManBmcCreateCnf
int Saig_ManBmcCreateCnf(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition bmcBmc3.c:1254
Saig_ManGenerateCex
Abc_Cex_t * Saig_ManGenerateCex(Gia_ManBmc_t *p, int f, int i)
Definition bmcBmc3.c:1393
SAIG_TER_UND
#define SAIG_TER_UND
Definition bmcBmc3.c:90
Saig_ParBmcSetDefaultParams
void Saig_ParBmcSetDefaultParams(Saig_ParBmc_t *p)
Definition bmcBmc3.c:1334
Saig_ManBmcTerSimCount01Po
int Saig_ManBmcTerSimCount01Po(Aig_Man_t *p, unsigned *pInfo)
Definition bmcBmc3.c:309
Saig_ManBmcCountRefed
int Saig_ManBmcCountRefed(Aig_Man_t *p, Vec_Ptr_t *vSuper)
Definition bmcBmc3.c:536
Saig_ManBmcWriteBlif
void Saig_ManBmcWriteBlif(Aig_Man_t *p, Vec_Int_t *vMapping, char *pFileName)
Definition bmcBmc3.c:585
Saig_ManBmcTimeToStop
abctime Saig_ManBmcTimeToStop(Saig_ParBmc_t *pPars, abctime nTimeToStopNG)
Definition bmcBmc3.c:1369
Saig_ManBmcMappingTest
void Saig_ManBmcMappingTest(Aig_Man_t *p)
Definition bmcBmc3.c:670
Saig_ManBmcTerSimPo
Vec_Ptr_t * Saig_ManBmcTerSimPo(Aig_Man_t *p)
Definition bmcBmc3.c:317
Saig_ManBmcTerSimTest
void Saig_ManBmcTerSimTest(Aig_Man_t *p)
Definition bmcBmc3.c:242
Saig_ManBmcScalable
int Saig_ManBmcScalable(Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
Definition bmcBmc3.c:1461
Gia_ManToBridgeResult
int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition utilBridge.c:287
Saig_ManBmcCreateCnf_rec
int Saig_ManBmcCreateCnf_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition bmcBmc3.c:1052
Saig_ManBmcSupergateTest
void Saig_ManBmcSupergateTest(Aig_Man_t *p)
Definition bmcBmc3.c:559
Saig_ManBmcCountNonternary
void Saig_ManBmcCountNonternary(Aig_Man_t *p, Vec_Ptr_t *vInfos, int iFrame)
Definition bmcBmc3.c:285
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:267
Gia_ManReportProgress
void Gia_ManReportProgress(FILE *pFile, int prop_no, int depth)
Definition bmcBmc3.c:75
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition bmcBmc3.c:88
Gia_ManBmc_t
typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t
DECLARATIONS ///.
Definition bmcBmc3.c:36
Saig_ManBmcSupergate
Vec_Ptr_t * Saig_ManBmcSupergate(Aig_Man_t *p, int iPo)
Definition bmcBmc3.c:502
Saig_ManBmcSupergate_rec
void Saig_ManBmcSupergate_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition bmcBmc3.c:478
SAIG_TER_NON
#define SAIG_TER_NON
FUNCTION DEFINITIONS ///.
Definition bmcBmc3.c:87
Saig_ManBmcRunTerSim_rec
int Saig_ManBmcRunTerSim_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition bmcBmc3.c:1179
Saig_ManBmcDfsNodes
Vec_Ptr_t * Saig_ManBmcDfsNodes(Aig_Man_t *p, Vec_Ptr_t *vRoots)
Definition bmcBmc3.c:383
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition bmcBmc3.c:89
Saig_ManBmcSections
Vec_Vec_t * Saig_ManBmcSections(Aig_Man_t *p)
Definition bmcBmc3.c:405
Saig_ManBmcSectionsTest
void Saig_ManBmcSectionsTest(Aig_Man_t *p)
Definition bmcBmc3.c:453
Saig_ManBmcTerSimOne
unsigned * Saig_ManBmcTerSimOne(Aig_Man_t *p, unsigned *pPrev)
Definition bmcBmc3.c:163
Saig_ManCallSolver
int Saig_ManCallSolver(Gia_ManBmc_t *p, int Lit)
Definition bmcBmc3.c:1433
Saig_ManBmcTerSimTestPo
void Saig_ManBmcTerSimTestPo(Aig_Man_t *p)
Definition bmcBmc3.c:337
Saig_ManBmcTerSim
Vec_Ptr_t * Saig_ManBmcTerSim(Aig_Man_t *p)
Definition bmcBmc3.c:213
Saig_ManBmcTerSimCount01
int Saig_ManBmcTerSimCount01(Aig_Man_t *p, unsigned *pInfo)
Definition bmcBmc3.c:140
Saig_ManBmcCreateCnf_iter
void Saig_ManBmcCreateCnf_iter(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
Definition bmcBmc3.c:1139
Aig_NodeCompareRefsIncrease
int Aig_NodeCompareRefsIncrease(Aig_Obj_t **pp1, Aig_Obj_t **pp2)
Definition bmcBmc3.c:1308
Saig_ManBmcComputeMappingRefs
Vec_Int_t * Saig_ManBmcComputeMappingRefs(Aig_Man_t *p, Vec_Int_t *vMap)
Definition bmcBmc3.c:690
Saig_ManBmcDfs_rec
void Saig_ManBmcDfs_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition bmcBmc3.c:358
Saig_Bmc3ManStop
void Saig_Bmc3ManStop(Gia_ManBmc_t *p)
Definition bmcBmc3.c:799
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Saig_ParBmc_t
struct Saig_ParBmc_t_ Saig_ParBmc_t
Definition bmc.h:105
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_DeriveMappingArray
Vec_Int_t * Cnf_DeriveMappingArray(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition cnfCore.c:78
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition cnfData.c:4537
Dar_CutSortVars
unsigned Dar_CutSortVars(unsigned uTruth, int *pVars)
Definition darCut.c:521
p
Cube * p
Definition exorList.c:222
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
sat_solver_memory
double sat_solver_memory(sat_solver *s)
Definition satSolver.c:1479
satoko_varnum
int satoko_varnum(satoko_t *)
Definition solver_api.c:625
satoko_set_stop_func
void satoko_set_stop_func(satoko_t *s, int(*fnct)(int))
Definition solver_api.c:650
satoko_setnvars
void satoko_setnvars(satoko_t *, int)
Definition solver_api.c:230
satoko_conflictnum
int satoko_conflictnum(satoko_t *)
Definition solver_api.c:640
satoko_opts_t
struct satoko_opts satoko_opts_t
Definition satoko.h:37
satoko_set_runtime_limit
abctime satoko_set_runtime_limit(satoko_t *, abctime)
Definition solver_api.c:665
satoko_solve_assumptions_limit
int satoko_solve_assumptions_limit(satoko_t *s, int *plits, int nlits, int nconflim)
Definition solver_api.c:364
satoko_set_runid
void satoko_set_runid(satoko_t *, int)
Definition solver_api.c:655
satoko_default_opts
void satoko_default_opts(satoko_opts_t *)
Definition solver_api.c:161
satoko_add_clause
int satoko_add_clause(satoko_t *, int *, int)
Definition solver_api.c:255
satoko_t
struct solver_t_ satoko_t
Definition satoko.h:35
satoko_clausenum
int satoko_clausenum(satoko_t *)
Definition solver_api.c:630
satoko_learntnum
int satoko_learntnum(satoko_t *)
Definition solver_api.c:635
satoko_read_cex_varvalue
int satoko_read_cex_varvalue(satoko_t *, int)
Definition solver_api.c:660
satoko_destroy
void satoko_destroy(satoko_t *)
Definition solver_api.c:132
satoko_create
satoko_t * satoko_create(void)
Definition solver_api.c:88
satoko_configure
void satoko_configure(satoko_t *, satoko_opts_t *)
Definition solver_api.c:196
Gia_ManBmc_t_
Definition bmcBmc3.c:38
Gia_ManBmc_t_::nLitUsed
int nLitUsed
Definition bmcBmc3.c:61
Gia_ManBmc_t_::pSat2
satoko_t * pSat2
Definition bmcBmc3.c:65
Gia_ManBmc_t_::pAig
Aig_Man_t * pAig
Definition bmcBmc3.c:41
Gia_ManBmc_t_::vId2Var
Vec_Ptr_t * vId2Var
Definition bmcBmc3.c:49
Gia_ManBmc_t_::vData
Vec_Int_t * vData
Definition bmcBmc3.c:53
Gia_ManBmc_t_::pPars
Saig_ParBmc_t * pPars
Definition bmcBmc3.c:40
Gia_ManBmc_t_::vMapping
Vec_Int_t * vMapping
Definition bmcBmc3.c:44
Gia_ManBmc_t_::pSat
sat_solver * pSat
Definition bmcBmc3.c:64
Gia_ManBmc_t_::nUniProps
int nUniProps
Definition bmcBmc3.c:60
Gia_ManBmc_t_::pTime4Outs
abctime * pTime4Outs
Definition bmcBmc3.c:51
Gia_ManBmc_t_::vId2Lit
Vec_Int_t * vId2Lit
Definition bmcBmc3.c:55
Gia_ManBmc_t_::pSops
char ** pSops
Definition bmcBmc3.c:70
Gia_ManBmc_t_::vVisited
Vec_Wec_t * vVisited
Definition bmcBmc3.c:50
Gia_ManBmc_t_::nBufNum
int nBufNum
Definition bmcBmc3.c:58
Gia_ManBmc_t_::vCexes
Vec_Ptr_t * vCexes
Definition bmcBmc3.c:42
Gia_ManBmc_t_::nHashMiss
int nHashMiss
Definition bmcBmc3.c:57
Gia_ManBmc_t_::nWordNum
int nWordNum
Definition bmcBmc3.c:69
Gia_ManBmc_t_::nHashHit
int nHashHit
Definition bmcBmc3.c:56
Gia_ManBmc_t_::vId2Num
Vec_Int_t * vId2Num
Definition bmcBmc3.c:47
Gia_ManBmc_t_::pSopSizes
char * pSopSizes
Definition bmcBmc3.c:70
Gia_ManBmc_t_::nLitUseless
int nLitUseless
Definition bmcBmc3.c:62
Gia_ManBmc_t_::nObjNums
int nObjNums
Definition bmcBmc3.c:68
Gia_ManBmc_t_::vMapRefs
Vec_Int_t * vMapRefs
Definition bmcBmc3.c:45
Gia_ManBmc_t_::nDupNum
int nDupNum
Definition bmcBmc3.c:59
Gia_ManBmc_t_::vTerInfo
Vec_Ptr_t * vTerInfo
Definition bmcBmc3.c:48
Gia_ManBmc_t_::vHash
Hsh_IntMan_t * vHash
Definition bmcBmc3.c:54
Gia_ManBmc_t_::nSatVars
int nSatVars
Definition bmcBmc3.c:67
Gia_ManBmc_t_::pSat3
bmcg_sat_solver * pSat3
Definition bmcBmc3.c:66
Saig_ParBmc_t_::nTimeOut
int nTimeOut
Definition bmc.h:113
Saig_ParBmc_t_::nTimeOutOne
int nTimeOutOne
Definition bmc.h:115
Saig_ParBmc_t_::fVerbose
int fVerbose
Definition bmc.h:129
Saig_ParBmc_t_::nConfLimit
int nConfLimit
Definition bmc.h:110
Saig_ParBmc_t_::pFuncOnFail
int(* pFuncOnFail)(int, Abc_Cex_t *)
Definition bmc.h:137
Saig_ParBmc_t_::fUseSatoko
int fUseSatoko
Definition bmc.h:124
Saig_ParBmc_t_::timeLastSolved
abctime timeLastSolved
Definition bmc.h:136
Saig_ParBmc_t_::fSolveAll
int fSolveAll
Definition bmc.h:117
Saig_ParBmc_t_::fStoreCex
int fStoreCex
Definition bmc.h:118
Saig_ParBmc_t_::nTimeOutGap
int nTimeOutGap
Definition bmc.h:114
Saig_ParBmc_t_::fNotVerbose
int fNotVerbose
Definition bmc.h:130
Saig_ParBmc_t_::fUseGlucose
int fUseGlucose
Definition bmc.h:125
Saig_ParBmc_t_::nFramesMax
int nFramesMax
Definition bmc.h:109
Saig_ParBmc_t_::pLogFileName
char * pLogFileName
Definition bmc.h:131
Saig_ParBmc_t_::nDropOuts
int nDropOuts
Definition bmc.h:135
Saig_ParBmc_t_::nFailOuts
int nFailOuts
Definition bmc.h:134
Saig_ParBmc_t_::fSilent
int fSilent
Definition bmc.h:132
Saig_ParBmc_t_::iFrame
int iFrame
Definition bmc.h:133
Saig_ParBmc_t_::nFramesJump
int nFramesJump
Definition bmc.h:112
Saig_ParBmc_t_::nConfLimitJump
int nConfLimitJump
Definition bmc.h:111
Saig_ParBmc_t_::nStart
int nStart
Definition bmc.h:108
satoko_opts::conf_limit
long conf_limit
Definition satoko.h:40
Gia_ManToBridgeProgress
int Gia_ManToBridgeProgress(FILE *pFile, int Size, unsigned char *pBuffer)
Definition utilBridge.c:185
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexDup
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition utilCex.c:145
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition utilCex.c:85
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
strlen
int strlen()
sprintf
char * sprintf()
free
VOID_HACK free()
Hsh_IntMan_t
struct Hsh_IntMan_t_ Hsh_IntMan_t
Definition vecHsh.h:66
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_VecForEachLevel
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecVec.h:55
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Vec_WecForEachLevelReverse
#define Vec_WecForEachLevelReverse(vGlob, vVec, i)
Definition vecWec.h:65
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42