ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bmcCexTools.c
Go to the documentation of this file.
1
20
21#include "bmc.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30static inline word Bmc_CexBitMask( int iBit ) { assert( iBit < 64 ); return ~(((word)1) << iBit); }
31static inline void Bmc_CexCopySim( Vec_Wrd_t * vSims, int iObjTo, int iObjFrom ) { Vec_WrdWriteEntry( vSims, iObjTo, iObjFrom ); }
32static inline void Bmc_CexAndSim( Vec_Wrd_t * vSims, int iObjTo, int i, int j ) { Vec_WrdWriteEntry( vSims, iObjTo, Vec_WrdEntry(vSims, i) & Vec_WrdEntry(vSims, j) ); }
33static inline void Bmc_CexOrSim( Vec_Wrd_t * vSims, int iObjTo, int i, int j ) { Vec_WrdWriteEntry( vSims, iObjTo, Vec_WrdEntry(vSims, i) | Vec_WrdEntry(vSims, j) ); }
34static inline int Bmc_CexSim( Vec_Wrd_t * vSims, int iObj, int i ) { return (Vec_WrdEntry(vSims, iObj) >> i) & 1; }
35
39
51int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
52{
53 int k, Counter = 0, Counter2 = 0;
54 if ( p == NULL )
55 {
56 printf( "The counter example is NULL.\n" );
57 return -1;
58 }
59 for ( k = 0; k < p->nBits; k++ )
60 {
61 Counter += Abc_InfoHasBit(p->pData, k);
62 if ( (k - p->nRegs) % p->nPis < nInputs )
63 Counter2 += Abc_InfoHasBit(p->pData, k);
64 }
65 return Counter2;
66}
67
78void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, abctime clk )
79{
80 int nInputs = Gia_ManPiNum(p);
81 int nBitsTotal = (pCex->iFrame + 1) * nInputs;
82 int nBitsCare = Bmc_CexBitCount(pCexCare, nInputs);
83 int nBitsDC = nBitsTotal - nBitsCare;
84 int nBitsEss = Bmc_CexBitCount(pCexEss, nInputs);
85 int nBitsOpt = nBitsCare - nBitsEss;
86 int nBitsMin = Bmc_CexBitCount(pCexMin, nInputs);
87
88 FILE * pTable = fopen( "cex/stats.txt", "a+" );
89 fprintf( pTable, "%s ", p->pName );
90 fprintf( pTable, "%d ", nInputs );
91 fprintf( pTable, "%d ", Gia_ManRegNum(p) );
92 fprintf( pTable, "%d ", pCex->iFrame + 1 );
93 fprintf( pTable, "%d ", nBitsTotal );
94 fprintf( pTable, "%.2f ", 100.0 * nBitsDC / nBitsTotal );
95 fprintf( pTable, "%.2f ", 100.0 * nBitsOpt / nBitsTotal );
96 fprintf( pTable, "%.2f ", 100.0 * nBitsEss / nBitsTotal );
97 fprintf( pTable, "%.2f ", 100.0 * nBitsMin / nBitsTotal );
98 fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
99 fprintf( pTable, "\n" );
100 fclose( pTable );
101}
102
103
115void Bmc_CexDumpAogStats( Gia_Man_t * p, abctime clk )
116{
117 FILE * pTable = fopen( "cex/aig_stats.txt", "a+" );
118 fprintf( pTable, "%s ", p->pName );
119 fprintf( pTable, "%d ", Gia_ManPiNum(p) );
120 fprintf( pTable, "%d ", Gia_ManAndNum(p) );
121 fprintf( pTable, "%d ", Gia_ManLevelNum(p) );
122 fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
123 fprintf( pTable, "\n" );
124 fclose( pTable );
125}
126
138Gia_Man_t * Bmc_CexPerformUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex )
139{
140 Gia_Man_t * pNew, * pTemp;
141 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
142 int i, k;
143 assert( Gia_ManRegNum(p) > 0 );
144 pNew = Gia_ManStart( (pCex->iFrame + 1) * Gia_ManObjNum(p) );
145 pNew->pName = Abc_UtilStrsav( p->pName );
146 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
147 Gia_ManConst0(p)->Value = 0;
148 Gia_ManForEachRi( p, pObj, k )
149 pObj->Value = 0;
150 Gia_ManHashAlloc( pNew );
151 for ( i = 0; i <= pCex->iFrame; i++ )
152 {
153 Gia_ManForEachPi( p, pObj, k )
154 pObj->Value = Gia_ManAppendCi( pNew );
155 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
156 pObjRo->Value = pObjRi->Value;
157 Gia_ManForEachAnd( p, pObj, k )
158 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
159 Gia_ManForEachCo( p, pObj, k )
160 pObj->Value = Gia_ObjFanin0Copy(pObj);
161 }
162 Gia_ManHashStop( pNew );
163 pObj = Gia_ManPo(p, pCex->iPo);
164 Gia_ManAppendCo( pNew, pObj->Value );
165 // cleanup
166 pNew = Gia_ManCleanup( pTemp = pNew );
167 Gia_ManStop( pTemp );
168 return pNew;
169}
170void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
171{
172 Gia_Man_t * pNew;
173 abctime clk = Abc_Clock();
174 pNew = Bmc_CexPerformUnrolling( p, pCex );
175 Gia_ManPrintStats( pNew, NULL );
176 Gia_AigerWrite( pNew, "unroll.aig", 0, 0, 0 );
177//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
178 Gia_ManStop( pNew );
179 printf( "CE-induced network is written into file \"unroll.aig\".\n" );
180 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
181}
182
183
195Gia_Man_t * Bmc_CexBuildNetwork( Gia_Man_t * p, Abc_Cex_t * pCex )
196{
197 Gia_Man_t * pNew, * pTemp;
198 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
199 int fCompl0, fCompl1;
200 int i, k, iBit = pCex->nRegs;
201 // start the manager
202 pNew = Gia_ManStart( 1000 );
203 pNew->pName = Abc_UtilStrsav( "unate" );
204 // set const0
205 Gia_ManConst0(p)->fMark0 = 0;
206 Gia_ManConst0(p)->fMark1 = 1;
207 Gia_ManConst0(p)->Value = ~0;
208 // set init state
209 Gia_ManForEachRi( p, pObj, k )
210 {
211 pObj->fMark0 = 0;
212 pObj->fMark1 = 1;
213 pObj->Value = ~0;
214 }
215 Gia_ManHashAlloc( pNew );
216 for ( i = 0; i <= pCex->iFrame; i++ )
217 {
218 // primary inputs
219 Gia_ManForEachPi( p, pObj, k )
220 {
221 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
222 pObj->fMark1 = 0;
223 pObj->Value = Gia_ManAppendCi(pNew);
224 }
225 // transfer
226 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
227 {
228 pObjRo->fMark0 = pObjRi->fMark0;
229 pObjRo->fMark1 = pObjRi->fMark1;
230 pObjRo->Value = pObjRi->Value;
231 }
232 // internal nodes
233 Gia_ManForEachAnd( p, pObj, k )
234 {
235 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
236 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
237 pObj->fMark0 = fCompl0 & fCompl1;
238 if ( pObj->fMark0 )
239 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
240 else if ( !fCompl0 && !fCompl1 )
241 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
242 else if ( !fCompl0 )
243 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
244 else if ( !fCompl1 )
245 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
246 else assert( 0 );
247 pObj->Value = ~0;
248 if ( pObj->fMark1 )
249 continue;
250 if ( pObj->fMark0 )
251 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
252 else if ( !fCompl0 && !fCompl1 )
253 pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
254 else if ( !fCompl0 )
255 pObj->Value = Gia_ObjFanin0(pObj)->Value;
256 else if ( !fCompl1 )
257 pObj->Value = Gia_ObjFanin1(pObj)->Value;
258 else assert( 0 );
259 assert( pObj->Value > 0 );
260 }
261 // combinational outputs
262 Gia_ManForEachCo( p, pObj, k )
263 {
264 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
265 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
266 pObj->Value = Gia_ObjFanin0(pObj)->Value;
267 }
268 }
269 Gia_ManHashStop( pNew );
270 assert( iBit == pCex->nBits );
271 // create primary output
272 pObj = Gia_ManPo(p, pCex->iPo);
273 assert( pObj->fMark0 == 1 );
274 assert( pObj->fMark1 == 0 );
275 assert( pObj->Value > 0 );
276 Gia_ManAppendCo( pNew, pObj->Value );
277 // cleanup
278 pNew = Gia_ManCleanup( pTemp = pNew );
279 Gia_ManStop( pTemp );
280 return pNew;
281}
282void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
283{
284 Gia_Man_t * pNew;
285 abctime clk = Abc_Clock();
286 pNew = Bmc_CexBuildNetwork( p, pCex );
287 Gia_ManPrintStats( pNew, NULL );
288 Gia_AigerWrite( pNew, "unate.aig", 0, 0, 0 );
289//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
290 Gia_ManStop( pNew );
291 printf( "CE-induced network is written into file \"unate.aig\".\n" );
292 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
293}
294
295
307void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose )
308{
309 int i, k, Count, iBit = pCex->nRegs;
310 Abc_CexPrintStatsInputs( pCex, nRealPis );
311 if ( !fVerbose )
312 return;
313
314 for ( i = 0; i <= pCex->iFrame; i++ )
315 {
316 Count = 0;
317 printf( "%3d : ", i );
318 for ( k = 0; k < nRealPis; k++ )
319 {
320 Count += Abc_InfoHasBit(pCex->pData, iBit);
321 printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
322 }
323 printf( " %3d ", Count );
324 Count = 0;
325 for ( ; k < pCex->nPis; k++ )
326 {
327 Count += Abc_InfoHasBit(pCex->pData, iBit);
328 printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
329 }
330 printf( " %3d\n", Count );
331 }
332 assert( iBit == pCex->nBits );
333}
334
346int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
347{
348 Gia_Obj_t * pObj;
349 int i, k;
350// assert( pCex->nRegs > 0 );
351// assert( pCexCare->nRegs == 0 );
352 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
353 Gia_ManForEachRi( p, pObj, k )
354 Gia_ObjTerSimSet0( pObj );
355 for ( i = 0; i <= pCex->iFrame; i++ )
356 {
357 Gia_ManForEachPi( p, pObj, k )
358 {
359 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
360 Gia_ObjTerSimSetX( pObj );
361 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
362 Gia_ObjTerSimSet1( pObj );
363 else
364 Gia_ObjTerSimSet0( pObj );
365 }
366 Gia_ManForEachRo( p, pObj, k )
367 Gia_ObjTerSimRo( p, pObj );
368 Gia_ManForEachAnd( p, pObj, k )
369 Gia_ObjTerSimAnd( pObj );
370 Gia_ManForEachCo( p, pObj, k )
371 Gia_ObjTerSimCo( pObj );
372 }
373 pObj = Gia_ManPo( p, pCex->iPo );
374 return Gia_ObjTerSimGet1(pObj);
375}
376
388int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
389{
390 Gia_Obj_t * pObj;
391 int i, k;
392// assert( pCex->nRegs > 0 );
393// assert( pCexCare->nRegs == 0 );
394 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
395 Gia_ManForEachRi( p, pObj, k )
396 Gia_ObjTerSimSet0( pObj );
397 for ( i = 0; i <= pCex->iFrame; i++ )
398 {
399 Gia_ManForEachPi( p, pObj, k )
400 {
401 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
402 Gia_ObjTerSimSetX( pObj );
403 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
404 Gia_ObjTerSimSet1( pObj );
405 else
406 Gia_ObjTerSimSet0( pObj );
407 }
408 Gia_ManForEachRo( p, pObj, k )
409 Gia_ObjTerSimRo( p, pObj );
410 Gia_ManForEachAnd( p, pObj, k )
411 Gia_ObjTerSimAnd( pObj );
412 Gia_ManForEachCo( p, pObj, k )
413 Gia_ObjTerSimCo( pObj );
414 }
415 for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
416 {
417 pObj = Gia_ManPo( p, i );
418 if (Gia_ObjTerSimGet1(pObj))
419 return i;
420 }
421 return -1;
422}
423
435Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose )
436{
437 Abc_Cex_t * pNew, * pNew2;
438 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
439 int fCompl0, fCompl1;
440 int i, k, iBit = 0;
441 assert( pCex->nRegs > 0 );
442 // start the counter-example
443 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
444 pNew->iFrame = pCex->iFrame;
445 pNew->iPo = pCex->iPo;
446 // start the counter-example
447 pNew2 = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
448 pNew2->iFrame = pCex->iFrame;
449 pNew2->iPo = pCex->iPo;
450 // set initial state
451 Gia_ManCleanMark01(p);
452 // set const0
453 Gia_ManConst0(p)->fMark0 = 0;
454 Gia_ManConst0(p)->fMark1 = 1;
455 // set init state
456 Gia_ManForEachRi( p, pObjRi, k )
457 {
458 pObjRi->fMark0 = 0;
459 pObjRi->fMark1 = 1;
460 }
461 iBit = pCex->nRegs;
462 for ( i = 0; i <= pCex->iFrame; i++ )
463 {
464 Gia_ManForEachPi( p, pObj, k )
465 pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
466 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
467 {
468 pObjRo->fMark0 = pObjRi->fMark0;
469 pObjRo->fMark1 = pObjRi->fMark1;
470 }
471 Gia_ManForEachCi( p, pObj, k )
472 {
473 if ( pObj->fMark0 )
474 Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k );
475 if ( pObj->fMark1 )
476 Abc_InfoSetBit( pNew2->pData, pNew2->nPis * i + k );
477 }
478 Gia_ManForEachAnd( p, pObj, k )
479 {
480 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
481 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
482 pObj->fMark0 = fCompl0 & fCompl1;
483 if ( pObj->fMark0 )
484 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
485 else if ( !fCompl0 && !fCompl1 )
486 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
487 else if ( !fCompl0 )
488 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
489 else if ( !fCompl1 )
490 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
491 else assert( 0 );
492 }
493 Gia_ManForEachCo( p, pObj, k )
494 {
495 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
496 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
497 }
498
499/*
500 // print input/state/output
501 printf( "%3d : ", i );
502 Gia_ManForEachPi( p, pObj, k )
503 printf( "%d", pObj->fMark0 );
504 printf( " " );
505 Gia_ManForEachRo( p, pObj, k )
506 printf( "%d", pObj->fMark0 );
507 printf( " " );
508 Gia_ManForEachPo( p, pObj, k )
509 printf( "%d", pObj->fMark0 );
510 printf( "\n" );
511*/
512 }
513 assert( iBit == pCex->nBits );
514 assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );
515
516 printf( "Inner states: " );
517 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
518 printf( "Implications: " );
519 Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
520 if ( ppCexImpl )
521 *ppCexImpl = pNew2;
522 else
523 Abc_CexFree( pNew2 );
524 return pNew;
525}
526
538void Bmc_CexCareBits_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
539{
540 int fCompl0, fCompl1;
541 if ( Gia_ObjIsConst0(pObj) )
542 return;
543 if ( pObj->fMark1 )
544 return;
545 pObj->fMark1 = 1;
546 if ( Gia_ObjIsCi(pObj) )
547 return;
548 assert( Gia_ObjIsAnd(pObj) );
549 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
550 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
551 if ( pObj->fMark0 )
552 {
553 assert( fCompl0 == 1 && fCompl1 == 1 );
554 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
555 Bmc_CexCareBits_rec( p, Gia_ObjFanin1(pObj) );
556 }
557 else
558 {
559 assert( fCompl0 == 0 || fCompl1 == 0 );
560 if ( fCompl0 == 0 )
561 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
562 if ( fCompl1 == 0 )
563 Bmc_CexCareBits_rec( p, Gia_ObjFanin1(pObj) );
564 }
565}
566void Bmc_CexCareBits2_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
567{
568 int fCompl0, fCompl1;
569 if ( Gia_ObjIsConst0(pObj) )
570 return;
571 if ( pObj->fMark1 )
572 return;
573 pObj->fMark1 = 1;
574 if ( Gia_ObjIsCi(pObj) )
575 return;
576 assert( Gia_ObjIsAnd(pObj) );
577 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
578 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
579 if ( pObj->fMark0 )
580 {
581 assert( fCompl0 == 1 && fCompl1 == 1 );
582 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
583 Bmc_CexCareBits2_rec( p, Gia_ObjFanin1(pObj) );
584 }
585 else
586 {
587 assert( fCompl0 == 0 || fCompl1 == 0 );
588 if ( fCompl0 == 0 )
589 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
590 /**/
591 else
592 /**/
593 if ( fCompl1 == 0 )
594 Bmc_CexCareBits2_rec( p, Gia_ObjFanin1(pObj) );
595 }
596}
597Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose )
598{
599 Abc_Cex_t * pNew;
600 Gia_Obj_t * pObj;
601 int fCompl0, fCompl1;
602 int i, k, iBit;
603 assert( pCexState->nRegs == 0 );
604 // start the counter-example
605 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
606 pNew->iFrame = pCexState->iFrame;
607 pNew->iPo = pCexState->iPo;
608 // set initial state
609 Gia_ManCleanMark01(p);
610 // set const0
611 Gia_ManConst0(p)->fMark0 = 0;
612 Gia_ManConst0(p)->fMark1 = 1;
613 for ( i = pCexState->iFrame; i >= 0; i-- )
614 {
615 // set correct values
616 iBit = pCexState->nPis * i;
617 Gia_ManForEachCi( p, pObj, k )
618 {
619 pObj->fMark0 = Abc_InfoHasBit(pCexState->pData, iBit+k);
620 pObj->fMark1 = 0;
621 if ( pCexImpl )
622 pObj->fMark1 |= Abc_InfoHasBit(pCexImpl->pData, iBit+k);
623 if ( pCexEss )
624 pObj->fMark1 |= Abc_InfoHasBit(pCexEss->pData, iBit+k);
625 }
626 Gia_ManForEachAnd( p, pObj, k )
627 {
628 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
629 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
630 pObj->fMark0 = fCompl0 & fCompl1;
631 if ( pObj->fMark0 )
632 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
633 else if ( !fCompl0 && !fCompl1 )
634 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
635 else if ( !fCompl0 )
636 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
637 else if ( !fCompl1 )
638 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
639 else assert( 0 );
640 }
641 Gia_ManForEachCo( p, pObj, k )
642 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
643 // move values from COs to CIs
644 if ( i == pCexState->iFrame )
645 {
646 assert( Gia_ManPo(p, pCexState->iPo)->fMark0 == 1 );
647 if ( fFindAll )
648 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
649 else
650 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
651 }
652 else
653 {
654 Gia_ManForEachRi( p, pObj, k )
655 if ( Abc_InfoHasBit(pNew->pData, pNew->nPis * (i+1) + Gia_ManPiNum(p) + k) )
656 {
657 if ( fFindAll )
658 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
659 else
660 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
661 }
662 }
663 // save the results
664 Gia_ManForEachCi( p, pObj, k )
665 if ( pObj->fMark1 )
666 {
667 pObj->fMark1 = 0;
668 if ( pCexImpl == NULL || !Abc_InfoHasBit(pCexImpl->pData, pNew->nPis * i + k) )
669 Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
670 }
671 }
672 if ( pCexEss )
673 printf( "Minimized: " );
674 else
675 printf( "Care bits: " );
676 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
677 return pNew;
678}
679
691Abc_Cex_t * Bmc_CexEssentialBitOne( Gia_Man_t * p, Abc_Cex_t * pCexState, int iBit, Abc_Cex_t * pCexPrev, int * pfEqual )
692{
693 Abc_Cex_t * pNew;
694 Gia_Obj_t * pObj;
695 int i, k, fCompl0, fCompl1;
696 assert( pCexState->nRegs == 0 );
697 assert( iBit < pCexState->nBits );
698 if ( pfEqual )
699 *pfEqual = 0;
700 // start the counter-example
701 pNew = Abc_CexAllocFull( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
702 pNew->iFrame = pCexState->iFrame;
703 pNew->iPo = pCexState->iPo;
704 // clean bit
705 Abc_InfoXorBit( pNew->pData, iBit );
706 // simulate the remaining frames
707 Gia_ManConst0(p)->fMark0 = 0;
708 Gia_ManConst0(p)->fMark1 = 1;
709 for ( i = iBit / pCexState->nPis; i <= pCexState->iFrame; i++ )
710 {
711 Gia_ManForEachCi( p, pObj, k )
712 {
713 pObj->fMark0 = Abc_InfoHasBit( pCexState->pData, i * pCexState->nPis + k );
714 pObj->fMark1 = Abc_InfoHasBit( pNew->pData, i * pCexState->nPis + k );
715 }
716 Gia_ManForEachAnd( p, pObj, k )
717 {
718 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
719 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
720 pObj->fMark0 = fCompl0 & fCompl1;
721 if ( pObj->fMark0 )
722 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
723 else if ( !fCompl0 && !fCompl1 )
724 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
725 else if ( !fCompl0 )
726 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
727 else if ( !fCompl1 )
728 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
729 else assert( 0 );
730 }
731 Gia_ManForEachCo( p, pObj, k )
732 {
733 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
734 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
735 }
736 if ( i < pCexState->iFrame )
737 {
738 int fChanges = 0;
739 int fEqual = (pCexPrev != NULL);
740 int iBitShift = (i + 1) * pCexState->nPis + Gia_ManPiNum(p);
741 Gia_ManForEachRi( p, pObj, k )
742 {
743 if ( fEqual && pCexPrev && (int)pObj->fMark1 != Abc_InfoHasBit(pCexPrev->pData, iBitShift + k) )
744 fEqual = 0;
745 if ( !pObj->fMark1 )
746 {
747 fChanges = 1;
748 Abc_InfoXorBit( pNew->pData, iBitShift + k );
749 }
750 }
751 if ( !fChanges || fEqual )
752 {
753 if ( pfEqual )
754 *pfEqual = fEqual;
755 Abc_CexFree( pNew );
756 return NULL;
757 }
758 }
759/*
760 if ( i == 20 )
761 {
762 printf( "Frame %d : ", i );
763 Gia_ManForEachRi( p, pObj, k )
764 printf( "%d", pObj->fMark1 );
765 printf( "\n" );
766 }
767*/
768 }
769 return pNew;
770}
771void Bmc_CexEssentialBitTest( Gia_Man_t * p, Abc_Cex_t * pCexState )
772{
773 Abc_Cex_t * pNew;
774 int b;
775 for ( b = 0; b < pCexState->nBits; b++ )
776 {
777 if ( b % 100 )
778 continue;
779 pNew = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, NULL );
780 Bmc_CexPrint( pNew, Gia_ManPiNum(p), 0 );
781
782 if ( Gia_ManPo(p, pCexState->iPo)->fMark1 )
783 printf( "Not essential\n" );
784 else
785 printf( "Essential\n" );
786
787 Abc_CexFree( pNew );
788 }
789}
790
802Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose )
803{
804 Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
805 int b, fEqual = 0, fPrevStatus = 0;
806// abctime clk = Abc_Clock();
807 assert( pCexState->nBits == pCexCare->nBits );
808 // start the counter-example
809 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
810 pNew->iFrame = pCexState->iFrame;
811 pNew->iPo = pCexState->iPo;
812 // iterate through care-bits
813 for ( b = 0; b < pCexState->nBits; b++ )
814 {
815 // skip don't-care bits
816 if ( !Abc_InfoHasBit(pCexCare->pData, b) )
817 continue;
818
819 // skip state bits
820 if ( b % pCexCare->nPis >= Gia_ManPiNum(p) )
821 {
822 Abc_InfoSetBit( pNew->pData, b );
823 continue;
824 }
825
826 // check if this is an essential bit
827 pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, pPrev, &fEqual );
828// pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, &fEqual );
829 if ( pTemp == NULL )
830 {
831 if ( fEqual && fPrevStatus )
832 Abc_InfoSetBit( pNew->pData, b );
833 continue;
834 }
835// Bmc_CexPrint( pTemp, Gia_ManPiNum(p), fVerbose );
836 Abc_CexFree( pPrev );
837 pPrev = pTemp;
838
839 // record essential bit
840 fPrevStatus = !Gia_ManPo(p, pCexState->iPo)->fMark1;
841 if ( !Gia_ManPo(p, pCexState->iPo)->fMark1 )
842 Abc_InfoSetBit( pNew->pData, b );
843 }
844 Abc_CexFreeP( &pPrev );
845// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
846 printf( "Essentials: " );
847 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
848 return pNew;
849}
850
851
863void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
864{
865 abctime clk = Abc_Clock();
866 Abc_Cex_t * pCexImpl = NULL;
867 Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
868 Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
869 Abc_Cex_t * pCexEss, * pCexMin;
870
871 if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
872 printf( "Counter-example care-set verification has failed.\n" );
873
874 pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
875 pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
876
877 if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
878 printf( "Counter-example min-set verification has failed.\n" );
879
880// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
881
882 Abc_CexFreeP( &pCexStates );
883 Abc_CexFreeP( &pCexImpl );
884 Abc_CexFreeP( &pCexCare );
885 Abc_CexFreeP( &pCexEss );
886 Abc_CexFreeP( &pCexMin );
887
888 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
889// Bmc_CexBuildNetworkTest( p, pCex );
890// Bmc_CexPerformUnrollingTest( p, pCex );
891}
892
893
894
906void Gia_ManCountCareBits( Gia_Man_t * p, Vec_Wec_t * vPats )
907{
908 Gia_Obj_t * pObj;
909 int i, k, fCompl0, fCompl1;
910 word Counter = 0;
911 Vec_Int_t * vPat;
912 Vec_WecForEachLevel( vPats, vPat, i )
913 {
914 int Count = 0;
915 assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
916
917 // propagate forward
918 Gia_ManConst0(p)->fMark0 = 0;
919 Gia_ManConst0(p)->fMark1 = 0;
920 Gia_ManForEachCi( p, pObj, k )
921 {
922 pObj->fMark0 = Vec_IntEntry(vPat, k);
923 pObj->fMark1 = 0;
924 }
925 Gia_ManForEachAnd( p, pObj, k )
926 {
927 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
928 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
929 pObj->fMark0 = fCompl0 & fCompl1;
930 pObj->fMark1 = 0;
931 }
932 Gia_ManForEachCo( p, pObj, k )
933 {
934 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
935 Gia_ObjFanin0(pObj)->fMark1 = 1;
936 }
937 // propagate backward
938 Gia_ManForEachAndReverse( p, pObj, k )
939 {
940 if ( !pObj->fMark1 )
941 continue;
942 if ( pObj->fMark0 == 0 )
943 {
944 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
945 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
946 assert( fCompl0 == 0 || fCompl1 == 0 );
947 if ( fCompl1 == 0 )
948 Gia_ObjFanin1(pObj)->fMark1 = 1;
949 else if ( fCompl0 == 0 )
950 Gia_ObjFanin0(pObj)->fMark1 = 1;
951
952 }
953 else
954 {
955 Gia_ObjFanin0(pObj)->fMark1 = 1;
956 Gia_ObjFanin1(pObj)->fMark1 = 1;
957 }
958 }
959 Gia_ManForEachAnd( p, pObj, k )
960 Count += pObj->fMark1;
961 Counter += Count;
962
963 //printf( "%3d = %8d\n", i, Count );
964 }
965 Counter /= Vec_WecSize(vPats);
966 printf( "Stats over %d patterns: Average care-nodes = %d (%6.2f %%)\n", Vec_WecSize(vPats), (int)Counter, 100.0*(int)Counter/Gia_ManAndNum(p) );
967}
968
969unsigned char * Mnist_ReadImages1_()
970{
971 int Size = 60000 * 28 * 28 + 16;
972 unsigned char * pData = (unsigned char *)malloc( Size );
973 FILE * pFile = fopen( "train-images.idx3-ubyte", "rb" );
974 int RetValue = fread( pData, 1, Size, pFile );
975 assert( RetValue == Size );
976 fclose( pFile );
977 return pData;
978}
979Vec_Wec_t * Mnist_ReadImages_( int nPats )
980{
981 Vec_Wec_t * vPats = Vec_WecStart( nPats );
982 unsigned char * pL1 = Mnist_ReadImages1_();
983 int i, k, x;
984 for ( i = 0; i < nPats; i++ )
985 for ( x = 0; x < 784; x++ )
986 for ( k = 0; k < 8; k++ )
987 Vec_WecPush( vPats, i, (pL1[16 + i * 784 + x] >> k) & 1 );
988 free( pL1 );
989 return vPats;
990}
991void Gia_ManCountCareBitsTest( Gia_Man_t * p )
992{
993 Vec_Wec_t * vPats = Mnist_ReadImages_( 100 );
994 Gia_ManCountCareBits( p, vPats );
995 Vec_WecFree( vPats );
996}
997
998
1002
1003
1004ABC_NAMESPACE_IMPL_END
1005
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Bmc_CexCareBits
Abc_Cex_t * Bmc_CexCareBits(Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
Definition bmcCexTools.c:597
Mnist_ReadImages1_
unsigned char * Mnist_ReadImages1_()
Definition bmcCexTools.c:969
Bmc_CexBuildNetworkTest
void Bmc_CexBuildNetworkTest(Gia_Man_t *p, Abc_Cex_t *pCex)
Definition bmcCexTools.c:282
Bmc_CexPerformUnrollingTest
void Bmc_CexPerformUnrollingTest(Gia_Man_t *p, Abc_Cex_t *pCex)
Definition bmcCexTools.c:170
Bmc_CexDumpStats
void Bmc_CexDumpStats(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare, Abc_Cex_t *pCexEss, Abc_Cex_t *pCexMin, abctime clk)
Definition bmcCexTools.c:78
Bmc_CexPrint
void Bmc_CexPrint(Abc_Cex_t *pCex, int nRealPis, int fVerbose)
Definition bmcCexTools.c:307
Bmc_CexCareBits_rec
void Bmc_CexCareBits_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcCexTools.c:538
Bmc_CexPerformUnrolling
Gia_Man_t * Bmc_CexPerformUnrolling(Gia_Man_t *p, Abc_Cex_t *pCex)
Definition bmcCexTools.c:138
Gia_ManCountCareBitsTest
void Gia_ManCountCareBitsTest(Gia_Man_t *p)
Definition bmcCexTools.c:991
Bmc_CexEssentialBits
Abc_Cex_t * Bmc_CexEssentialBits(Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexCare, int fVerbose)
Definition bmcCexTools.c:802
Bmc_CexEssentialBitOne
Abc_Cex_t * Bmc_CexEssentialBitOne(Gia_Man_t *p, Abc_Cex_t *pCexState, int iBit, Abc_Cex_t *pCexPrev, int *pfEqual)
Definition bmcCexTools.c:691
Bmc_CexDumpAogStats
void Bmc_CexDumpAogStats(Gia_Man_t *p, abctime clk)
Definition bmcCexTools.c:115
Bmc_CexEssentialBitTest
void Bmc_CexEssentialBitTest(Gia_Man_t *p, Abc_Cex_t *pCexState)
Definition bmcCexTools.c:771
Bmc_CexBuildNetwork
Gia_Man_t * Bmc_CexBuildNetwork(Gia_Man_t *p, Abc_Cex_t *pCex)
Definition bmcCexTools.c:195
Bmc_CexInnerStates
Abc_Cex_t * Bmc_CexInnerStates(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
DECLARATIONS ///.
Definition bmcCexTools.c:435
Bmc_CexVerifyAnyPo
int Bmc_CexVerifyAnyPo(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:388
Mnist_ReadImages_
Vec_Wec_t * Mnist_ReadImages_(int nPats)
Definition bmcCexTools.c:979
Bmc_CexVerify
int Bmc_CexVerify(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:346
Bmc_CexTest
void Bmc_CexTest(Gia_Man_t *p, Abc_Cex_t *pCex, int fVerbose)
Definition bmcCexTools.c:863
Bmc_CexCareBits2_rec
void Bmc_CexCareBits2_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcCexTools.c:566
Gia_ManCountCareBits
void Gia_ManCountCareBits(Gia_Man_t *p, Vec_Wec_t *vPats)
Definition bmcCexTools.c:906
Bmc_CexBitCount
int Bmc_CexBitCount(Abc_Cex_t *p, int nInputs)
FUNCTION DEFINITIONS ///.
Definition bmcCexTools.c:51
p
Cube * p
Definition exorList.c:222
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition giaUtil.c:218
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Abc_CexPrintStatsInputs
void Abc_CexPrintStatsInputs(Abc_Cex_t *p, int nRealPis)
Definition utilCex.c:275
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexAllocFull
Abc_Cex_t * Abc_CexAllocFull(int nRegs, int nRealPis, int nFrames)
Definition utilCex.c:62
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
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
free
VOID_HACK free()
malloc
char * malloc()
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42