ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaSupp.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "sat/satoko/satoko.h"
23
24#ifdef ABC_USE_CUDD
25#include "bdd/extrab/extraBdd.h"
26#endif
27
28ABC_NAMESPACE_IMPL_START
29
33
34#ifdef ABC_USE_CUDD
35
36struct Gia_ManMin_t_
37{
38 // problem formulation
39 Gia_Man_t * pGia;
40 int iLits[2];
41 // structural information
42 Vec_Int_t * vCis[2];
43 Vec_Int_t * vObjs[2];
44 Vec_Int_t * vCleared;
45 // intermediate functions
46 DdManager * dd;
47 Vec_Ptr_t * vFuncs;
48 Vec_Int_t * vSupp;
49};
50
54
66Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia )
67{
68 Gia_ManMin_t * p;
69 p = ABC_CALLOC( Gia_ManMin_t, 1 );
70 p->pGia = pGia;
71 p->vCis[0] = Vec_IntAlloc( 512 );
72 p->vCis[1] = Vec_IntAlloc( 512 );
73 p->vObjs[0] = Vec_IntAlloc( 512 );
74 p->vObjs[1] = Vec_IntAlloc( 512 );
75 p->vCleared = Vec_IntAlloc( 512 );
76 p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
77// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
78 Cudd_AutodynDisable( p->dd );
79 p->vFuncs = Vec_PtrAlloc( 10000 );
80 p->vSupp = Vec_IntAlloc( 10000 );
81 return p;
82}
83void Gia_ManSuppStop( Gia_ManMin_t * p )
84{
85 Vec_IntFreeP( &p->vCis[0] );
86 Vec_IntFreeP( &p->vCis[1] );
87 Vec_IntFreeP( &p->vObjs[0] );
88 Vec_IntFreeP( &p->vObjs[1] );
89 Vec_IntFreeP( &p->vCleared );
90 Vec_PtrFreeP( &p->vFuncs );
91 Vec_IntFreeP( &p->vSupp );
92 printf( "Refs = %d. \n", Cudd_CheckZeroRef( p->dd ) );
93 Cudd_Quit( p->dd );
94 ABC_FREE( p );
95}
96
108int Gia_ManFindRemoved( Gia_ManMin_t * p )
109{
110 extern void ddSupportStep2( DdNode * f, int * support );
111 extern void ddClearFlag2( DdNode * f );
112
113 //int fVerbose = 1;
114 int nBddLimit = 100000;
115 int nPart0 = Vec_IntSize(p->vCis[0]);
116 int n, i, iObj, nVars = 0;
117 DdNode * bFunc0, * bFunc1, * bFunc;
118 Vec_PtrFillExtra( p->vFuncs, Gia_ManObjNum(p->pGia), NULL );
119 // assign variables
120 for ( n = 0; n < 2; n++ )
121 Vec_IntForEachEntry( p->vCis[n], iObj, i )
122 Vec_PtrWriteEntry( p->vFuncs, iObj, Cudd_bddIthVar(p->dd, nVars++) );
123 // create nodes
124 for ( n = 0; n < 2; n++ )
125 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
126 {
127 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
128 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId0(pObj, iObj)), Gia_ObjFaninC0(pObj) );
129 bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId1(pObj, iObj)), Gia_ObjFaninC1(pObj) );
130 bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit );
131 assert( bFunc != NULL );
132 Cudd_Ref( bFunc );
133 Vec_PtrWriteEntry( p->vFuncs, iObj, bFunc );
134 }
135 // create new node
136 bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[0])), Abc_LitIsCompl(p->iLits[0]) );
137 bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[1])), Abc_LitIsCompl(p->iLits[1]) );
138 bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit );
139 assert( bFunc != NULL );
140 Cudd_Ref( bFunc );
141 //if ( fVerbose ) Extra_bddPrint( p->dd, bFunc ), printf( "\n" );
142 // collect support
143 Vec_IntFill( p->vSupp, nVars, 0 );
144 ddSupportStep2( Cudd_Regular(bFunc), Vec_IntArray(p->vSupp) );
145 ddClearFlag2( Cudd_Regular(bFunc) );
146 // find variables not present in the support
147 Vec_IntClear( p->vCleared );
148 for ( i = 0; i < nVars; i++ )
149 if ( Vec_IntEntry(p->vSupp, i) == 0 )
150 Vec_IntPush( p->vCleared, i < nPart0 ? Vec_IntEntry(p->vCis[0], i) : Vec_IntEntry(p->vCis[1], i-nPart0) );
151 //printf( "%d(%d)%d ", Cudd_SupportSize(p->dd, bFunc), Vec_IntSize(p->vCleared), Cudd_DagSize(bFunc) );
152 // deref results
153 Cudd_RecursiveDeref( p->dd, bFunc );
154 for ( n = 0; n < 2; n++ )
155 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
156 Cudd_RecursiveDeref( p->dd, (DdNode *)Vec_PtrEntry(p->vFuncs, iObj) );
157 //Vec_IntPrint( p->vCleared );
158 return Vec_IntSize(p->vCleared);
159}
160
172int Gia_ManRebuildOne( Gia_ManMin_t * p, int n )
173{
174 int i, iObj, iGiaLitNew = -1;
175 Vec_Int_t * vTempIns = p->vCis[n];
176 Vec_Int_t * vTempNds = p->vObjs[n];
177 Vec_Int_t * vCopies = &p->pGia->vCopies;
178 Vec_IntFillExtra( vCopies, Gia_ManObjNum(p->pGia), -1 );
179 assert( p->iLits[n] >= 2 );
180 // process inputs
181 Vec_IntForEachEntry( vTempIns, iObj, i )
182 Vec_IntWriteEntry( vCopies, iObj, Abc_Var2Lit(iObj, 0) );
183 // process constants
184 assert( Vec_IntSize(p->vCleared) > 0 );
185 Vec_IntForEachEntry( p->vCleared, iObj, i )
186 Vec_IntWriteEntry( vCopies, iObj, 0 );
187 if ( Vec_IntSize(vTempNds) == 0 )
188 iGiaLitNew = Vec_IntEntry( vCopies, Abc_Lit2Var(p->iLits[n]) );
189 else
190 {
191 Vec_IntForEachEntry( vTempNds, iObj, i )
192 {
193 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
194 int iGiaLit0 = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
195 int iGiaLit1 = Vec_IntEntry( vCopies, Gia_ObjFaninId1p(p->pGia, pObj) );
196 iGiaLit0 = Abc_LitNotCond( iGiaLit0, Gia_ObjFaninC0(pObj) );
197 iGiaLit1 = Abc_LitNotCond( iGiaLit1, Gia_ObjFaninC1(pObj) );
198 iGiaLitNew = Gia_ManHashAnd( p->pGia, iGiaLit0, iGiaLit1 );
199 Vec_IntWriteEntry( vCopies, iObj, iGiaLitNew );
200 }
201 assert( Abc_Lit2Var(p->iLits[n]) == iObj );
202 }
203 return Abc_LitNotCond( iGiaLitNew, Abc_LitIsCompl(p->iLits[n]) );
204}
205
217static inline int Gia_ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs )
218{
219 int Val0, Val1;
220 Gia_Obj_t * pObj;
221 if ( Gia_ObjIsTravIdPreviousId(p, iObj) )
222 return 1;
223 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
224 return 0;
225 Gia_ObjSetTravIdCurrentId(p, iObj);
226 pObj = Gia_ManObj( p, iObj );
227 if ( Gia_ObjIsCi(pObj) )
228 {
229 Vec_IntPush( vCis, iObj );
230 return 0;
231 }
232 assert( Gia_ObjIsAnd(pObj) );
233 Val0 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs );
234 Val1 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs );
235 Vec_IntPush( vObjs, iObj );
236 return Val0 || Val1;
237}
238int Gia_ManGatherSupp( Gia_ManMin_t * p )
239{
240 int n, Overlap = 0;
241 Gia_ManIncrementTravId( p->pGia );
242 for ( n = 0; n < 2; n++ )
243 {
244 Vec_IntClear( p->vCis[n] );
245 Vec_IntClear( p->vObjs[n] );
246 Gia_ManIncrementTravId( p->pGia );
247 Overlap = Gia_ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] );
248 assert( n || !Overlap );
249 }
250 return Overlap;
251}
252
264int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 )
265{
266 int iLitNew0, iLitNew1;
267 p->iLits[0] = iLit0;
268 p->iLits[1] = iLit1;
269 if ( iLit0 < 2 || iLit1 < 2 || !Gia_ManGatherSupp(p) || !Gia_ManFindRemoved(p) )
270 return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
271 iLitNew0 = Gia_ManRebuildOne( p, 0 );
272 iLitNew1 = Gia_ManRebuildOne( p, 1 );
273 return Gia_ManHashAnd( p->pGia, iLitNew0, iLitNew1 );
274}
275
276
277#else
278
279Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) { return NULL; }
280int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) { return 0; }
281void Gia_ManSuppStop( Gia_ManMin_t * p ) {}
282
283#endif
284
285
297Gia_Man_t * Gia_ManSupportAndTest( Gia_Man_t * pGia )
298{
299 Gia_ManMin_t * pMan;
300 Gia_Man_t * pNew, * pTemp;
301 Gia_Obj_t * pObj;
302 int i;
303 Gia_ManFillValue( pGia );
304 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
305 pNew->pName = Abc_UtilStrsav( pGia->pName );
306 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
307 Gia_ManHashAlloc( pNew );
308 Gia_ManConst0(pGia)->Value = 0;
309 pMan = Gia_ManSuppStart( pNew );
310 Gia_ManForEachObj1( pGia, pObj, i )
311 {
312 if ( Gia_ObjIsAnd(pObj) )
313 {
314// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
315 pObj->Value = Gia_ManSupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
316 }
317 else if ( Gia_ObjIsCi(pObj) )
318 pObj->Value = Gia_ManAppendCi( pNew );
319 else if ( Gia_ObjIsCo(pObj) )
320 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
321 else assert( 0 );
322
323 if ( i % 10000 == 0 )
324 printf( "%d\n", i );
325 }
326 Gia_ManSuppStop( pMan );
327 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
328 pNew = Gia_ManCleanup( pTemp = pNew );
329 Gia_ManStop( pTemp );
330 return pNew;
331}
332
333
334
335
336struct Gia_Man2Min_t_
337{
338 // problem formulation
339 Gia_Man_t * pGia;
340 int iLits[2];
341 // structural information
342 Vec_Int_t * vCis[2];
343 Vec_Int_t * vObjs[2];
344 // SAT solving
345 satoko_t * pSat; // SAT solver
346 Vec_Wrd_t * vSims; // simulation
347 Vec_Ptr_t * vFrontier; // CNF construction
348 Vec_Ptr_t * vFanins; // CNF construction
349 Vec_Int_t * vSatVars; // nodes
350 int nCisOld; // previous number of CIs
351 int iPattern; // the next pattern to write
352 int nSatSat;
353 int nSatUnsat;
354 int nCalls;
355 int nSims;
356 int nSupps;
357};
358
359static inline int Gia_Min2ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); }
360static inline int Gia_Min2ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Gia_Min2ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; }
361static inline void Gia_Min2ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Gia_Min2ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); }
362
363
375Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia )
376{
377 Gia_Man2Min_t * p;
378 p = ABC_CALLOC( Gia_Man2Min_t, 1 );
379 p->pGia = pGia;
380 p->vCis[0] = Vec_IntAlloc( 512 );
381 p->vCis[1] = Vec_IntAlloc( 512 );
382 p->vObjs[0] = Vec_IntAlloc( 512 );
383 p->vObjs[1] = Vec_IntAlloc( 512 );
384 // SAT solving
385 p->pSat = satoko_create();
386 p->vSims = Vec_WrdAlloc( 1000 );
387 p->vFrontier = Vec_PtrAlloc( 1000 );
388 p->vFanins = Vec_PtrAlloc( 100 );
389 p->vSatVars = Vec_IntAlloc( 100 );
390 p->iPattern = 1;
391 satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection
392 return p;
393}
394void Gia_Man2SuppStop( Gia_Man2Min_t * p )
395{
396// printf( "Total calls = %8d. Supps = %6d. Sims = %6d. SAT = %6d. UNSAT = %6d.\n",
397// p->nCalls, p->nSupps, p->nSims, p->nSatSat, p->nSatUnsat );
398 Vec_IntFreeP( &p->vCis[0] );
399 Vec_IntFreeP( &p->vCis[1] );
400 Vec_IntFreeP( &p->vObjs[0] );
401 Vec_IntFreeP( &p->vObjs[1] );
402 Gia_ManCleanMark01( p->pGia );
403 satoko_destroy( p->pSat );
404 Vec_WrdFreeP( &p->vSims );
405 Vec_PtrFreeP( &p->vFrontier );
406 Vec_PtrFreeP( &p->vFanins );
407 Vec_IntFreeP( &p->vSatVars );
408 ABC_FREE( p );
409}
410
422void Gia_Min2AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat )
423{
424 int fPolarFlip = 0;
425 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
426 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
427
428 assert( !Gia_IsComplement( pNode ) );
429 assert( pNode->fMark0 );
430 // get nodes (I = if, T = then, E = else)
431 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
432 // get the variable numbers
433 VarF = Gia_Min2ObjSatId(p, pNode);
434 VarI = Gia_Min2ObjSatId(p, pNodeI);
435 VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT));
436 VarE = Gia_Min2ObjSatId(p, Gia_Regular(pNodeE));
437 // get the complementation flags
438 fCompT = Gia_IsComplement(pNodeT);
439 fCompE = Gia_IsComplement(pNodeE);
440
441 // f = ITE(i, t, e)
442
443 // i' + t' + f
444 // i' + t + f'
445 // i + e' + f
446 // i + e + f'
447
448 // create four clauses
449 pLits[0] = Abc_Var2Lit(VarI, 1);
450 pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
451 pLits[2] = Abc_Var2Lit(VarF, 0);
452 if ( fPolarFlip )
453 {
454 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
455 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
456 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
457 }
458 RetValue = satoko_add_clause( pSat, pLits, 3 );
459 assert( RetValue );
460 pLits[0] = Abc_Var2Lit(VarI, 1);
461 pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
462 pLits[2] = Abc_Var2Lit(VarF, 1);
463 if ( fPolarFlip )
464 {
465 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
466 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
467 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
468 }
469 RetValue = satoko_add_clause( pSat, pLits, 3 );
470 assert( RetValue );
471 pLits[0] = Abc_Var2Lit(VarI, 0);
472 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
473 pLits[2] = Abc_Var2Lit(VarF, 0);
474 if ( fPolarFlip )
475 {
476 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
477 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
478 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
479 }
480 RetValue = satoko_add_clause( pSat, pLits, 3 );
481 assert( RetValue );
482 pLits[0] = Abc_Var2Lit(VarI, 0);
483 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
484 pLits[2] = Abc_Var2Lit(VarF, 1);
485 if ( fPolarFlip )
486 {
487 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
488 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
489 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
490 }
491 RetValue = satoko_add_clause( pSat, pLits, 3 );
492 assert( RetValue );
493
494 // two additional clauses
495 // t' & e' -> f'
496 // t & e -> f
497
498 // t + e + f'
499 // t' + e' + f
500
501 if ( VarT == VarE )
502 {
503// assert( fCompT == !fCompE );
504 return;
505 }
506
507 pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
508 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
509 pLits[2] = Abc_Var2Lit(VarF, 1);
510 if ( fPolarFlip )
511 {
512 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
513 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
514 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
515 }
516 RetValue = satoko_add_clause( pSat, pLits, 3 );
517 assert( RetValue );
518 pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
519 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
520 pLits[2] = Abc_Var2Lit(VarF, 0);
521 if ( fPolarFlip )
522 {
523 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
524 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
525 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
526 }
527 RetValue = satoko_add_clause( pSat, pLits, 3 );
528 assert( RetValue );
529}
530void Gia_Min2AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat )
531{
532 int fPolarFlip = 0;
533 Gia_Obj_t * pFanin;
534 int * pLits, nLits, RetValue, i;
535 assert( !Gia_IsComplement(pNode) );
536 assert( Gia_ObjIsAnd( pNode ) );
537 // create storage for literals
538 nLits = Vec_PtrSize(vSuper) + 1;
539 pLits = ABC_ALLOC( int, nLits );
540 // suppose AND-gate is A & B = C
541 // add !A => !C or A + !C
542 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
543 {
544 pLits[0] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
545 pLits[1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 1);
546 if ( fPolarFlip )
547 {
548 if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
549 if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
550 }
551 RetValue = satoko_add_clause( pSat, pLits, 2 );
552 assert( RetValue );
553 }
554 // add A & B => C or !A + !B + C
555 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
556 {
557 pLits[i] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
558 if ( fPolarFlip )
559 {
560 if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] );
561 }
562 }
563 pLits[nLits-1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 0);
564 if ( fPolarFlip )
565 {
566 if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
567 }
568 RetValue = satoko_add_clause( pSat, pLits, nLits );
569 assert( RetValue );
570 ABC_FREE( pLits );
571}
572
584void Gia_Min2CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
585{
586 // if the new node is complemented or a PI, another gate begins
587 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
588 (!fFirst && Gia_ObjValue(pObj) > 1) ||
589 (fUseMuxes && pObj->fMark0) )
590 {
591 Vec_PtrPushUnique( vSuper, pObj );
592 return;
593 }
594 // go through the branches
595 Gia_Min2CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
596 Gia_Min2CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
597}
598void Gia_Min2CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
599{
600 assert( !Gia_IsComplement(pObj) );
601 assert( !Gia_ObjIsCi(pObj) );
602 Vec_PtrClear( vSuper );
603 Gia_Min2CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
604}
605void Gia_Min2ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat, Vec_Int_t * vSatVars )
606{
607 assert( !Gia_IsComplement(pObj) );
608 assert( !Gia_ObjIsConst0(pObj) );
609 if ( Gia_Min2ObjSatId(p, pObj) >= 0 )
610 return;
611 assert( Gia_Min2ObjSatId(p, pObj) == -1 );
612 Vec_IntPush( vSatVars, Gia_ObjId(p, pObj) );
613 Gia_Min2ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) );
614 if ( Gia_ObjIsAnd(pObj) )
615 Vec_PtrPush( vFrontier, pObj );
616}
617int Gia_Min2ObjGetCnfVar( Gia_Man2Min_t * p, int iObj )
618{
619 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
620 Gia_Obj_t * pNode, * pFanin;
621 int i, k, fUseMuxes = 1;
622 if ( Gia_Min2ObjSatId(p->pGia, pObj) >= 0 )
623 return Gia_Min2ObjSatId(p->pGia, pObj);
624 if ( Gia_ObjIsCi(pObj) )
625 {
626 Vec_IntPush( p->vSatVars, iObj );
627 return Gia_Min2ObjSetSatId( p->pGia, pObj, satoko_add_variable(p->pSat, 0) );
628 }
629 assert( Gia_ObjIsAnd(pObj) );
630 // start the frontier
631 Vec_PtrClear( p->vFrontier );
632 Gia_Min2ObjAddToFrontier( p->pGia, pObj, p->vFrontier, p->pSat, p->vSatVars );
633 // explore nodes in the frontier
634 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i )
635 {
636 assert( Gia_Min2ObjSatId(p->pGia,pNode) >= 0 );
637 if ( fUseMuxes && pNode->fMark0 )
638 {
639 Vec_PtrClear( p->vFanins );
640 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
641 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
642 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
643 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
644 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
645 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
646 Gia_Min2AddClausesMux( p->pGia, pNode, p->pSat );
647 }
648 else
649 {
650 Gia_Min2CollectSuper( pNode, fUseMuxes, p->vFanins );
651 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
652 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
653 Gia_Min2AddClausesSuper( p->pGia, pNode, p->vFanins, p->pSat );
654 }
655 assert( Vec_PtrSize(p->vFanins) > 1 );
656 }
657 return Gia_Min2ObjSatId(p->pGia,pObj);
658}
659
671int Gia_Min2ManSimulate( Gia_Man2Min_t * p )
672{
673 word Sim0, Sim1; int n, i, iObj;
674 p->nSims++;
675 // add random values to new CIs
676 Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p->pGia), 0 );
677 for ( i = p->nCisOld; i < Gia_ManCiNum(p->pGia); i++ )
678 Vec_WrdWriteEntry( p->vSims, Gia_ManCiIdToId(p->pGia, i), Gia_ManRandomW( 0 ) << 1 );
679 p->nCisOld = Gia_ManCiNum(p->pGia);
680 // simulate internal nodes
681 for ( n = 0; n < 2; n++ )
682 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
683 {
684 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
685 Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0p(p->pGia, pObj) );
686 Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1p(p->pGia, pObj) );
687 Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
688 Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
689 Vec_WrdWriteEntry( p->vSims, iObj, Sim0 & Sim1 );
690 }
691 Sim0 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[0]) );
692 Sim1 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[1]) );
693 Sim0 = Abc_LitIsCompl(p->iLits[0]) ? ~Sim0 : Sim0;
694 Sim1 = Abc_LitIsCompl(p->iLits[1]) ? ~Sim1 : Sim1;
695// assert( (Sim0 & Sim1) != ~0 );
696 return (Sim0 & Sim1) == 0;
697}
698
710static inline void Gia_Min2SimSetInputBit( Gia_Man2Min_t * p, int iObj, int Bit, int iPattern )
711{
712 word * pSim = Vec_WrdEntryP( p->vSims, iObj );
713 assert( iPattern > 0 && iPattern < 64 );
714 if ( Abc_InfoHasBit( (unsigned*)pSim, iPattern ) != Bit )
715 Abc_InfoXorBit( (unsigned*)pSim, iPattern );
716}
717int Gia_Min2ManSolve( Gia_Man2Min_t * p )
718{
719 int iObj0 = Abc_Lit2Var(p->iLits[0]);
720 int iObj1 = Abc_Lit2Var(p->iLits[1]);
721 int n, i, status, iVar0, iVar1, iTemp;
722 assert( iObj0 > 0 && iObj1 > 0 );
723// Vec_IntForEachEntry( &p->pGia->vCopies, iTemp, i )
724// assert( iTemp == -1 );
725 Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 );
726 Vec_IntClear( p->vSatVars );
727 assert( satoko_varnum(p->pSat) == 0 );
728 iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 );
729 iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 );
730 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) );
731 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, Abc_LitIsCompl(p->iLits[1])) );
732 status = satoko_solve( p->pSat );
733 satoko_assump_pop( p->pSat );
734 satoko_assump_pop( p->pSat );
735 if ( status == SATOKO_SAT )
736 {
737 //printf( "Disproved %d %d\n", p->iLits[0], p->iLits[1] );
738 assert( Gia_Min2ManSimulate(p) == 1 );
739 for ( n = 0; n < 2; n++ )
740 Vec_IntForEachEntry( p->vCis[n], iTemp, i )
741 Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern );
742 //assert( Gia_Min2ManSimulate(p) == 0 );
743 p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1;
744 p->nSatSat++;
745 }
746 //printf( "supp %d node %d vars %d\n",
747 // Vec_IntSize(p->vCis[0]) + Vec_IntSize(p->vCis[1]),
748 // Vec_IntSize(p->vObjs[0]) + Vec_IntSize(p->vObjs[1]),
749 // Vec_IntSize(p->vSatVars) );
750 satoko_rollback( p->pSat );
751 Vec_IntForEachEntry( p->vSatVars, iTemp, i )
752 Gia_Min2ObjCleanSatId( p->pGia, Gia_ManObj(p->pGia, iTemp) );
753 return status == SATOKO_UNSAT;
754}
755
767static inline int Gia_Min2ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs )
768{
769 int Val0, Val1;
770 Gia_Obj_t * pObj;
771 if ( Gia_ObjIsTravIdPreviousId(p, iObj) )
772 return 1;
773 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
774 return 0;
775 Gia_ObjSetTravIdCurrentId(p, iObj);
776 pObj = Gia_ManObj( p, iObj );
777 if ( Gia_ObjIsCi(pObj) )
778 {
779 Vec_IntPush( vCis, iObj );
780 return 0;
781 }
782 assert( Gia_ObjIsAnd(pObj) );
783 Val0 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs );
784 Val1 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs );
785 Vec_IntPush( vObjs, iObj );
786 return Val0 || Val1;
787}
788int Gia_Min2ManGatherSupp( Gia_Man2Min_t * p )
789{
790 int n, Overlap = 0;
791 p->nSupps++;
792 Gia_ManIncrementTravId( p->pGia );
793 for ( n = 0; n < 2; n++ )
794 {
795 Vec_IntClear( p->vCis[n] );
796 Vec_IntClear( p->vObjs[n] );
797 Gia_ManIncrementTravId( p->pGia );
798 Overlap = Gia_Min2ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] );
799 assert( n || !Overlap );
800 }
801 return Overlap;
802}
803
815int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 )
816{
817 p->nCalls++;
818 //return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
819 p->iLits[0] = iLit0;
820 p->iLits[1] = iLit1;
821 if ( iLit0 < 2 || iLit1 < 2 || Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) || Gia_ManHashLookupInt(p->pGia, iLit0, iLit1) ||
822 !Gia_Min2ManGatherSupp(p) || !Gia_Min2ManSimulate(p) || !Gia_Min2ManSolve(p) )
823 return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
824 //printf( "%d %d\n", iLit0, iLit1 );
825 p->nSatUnsat++;
826 return 0;
827}
828
840Gia_Man_t * Gia_Man2SupportAndTest( Gia_Man_t * pGia )
841{
842 Gia_Man2Min_t * pMan;
843 Gia_Man_t * pNew, * pTemp;
844 Gia_Obj_t * pObj;
845 int i;
846 Gia_ManRandomW( 1 );
847 Gia_ManFillValue( pGia );
848 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
849 pNew->pName = Abc_UtilStrsav( pGia->pName );
850 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
851 Gia_ManHashAlloc( pNew );
852 Gia_ManConst0(pGia)->Value = 0;
853 pMan = Gia_Man2SuppStart( pNew );
854 Gia_ManForEachObj1( pGia, pObj, i )
855 {
856 if ( Gia_ObjIsAnd(pObj) )
857 {
858// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
859 pObj->Value = Gia_Man2SupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
860 }
861 else if ( Gia_ObjIsCi(pObj) )
862 pObj->Value = Gia_ManAppendCi( pNew );
863 else if ( Gia_ObjIsCo(pObj) )
864 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
865 else assert( 0 );
866
867 //if ( i % 10000 == 0 )
868 // printf( "%d\n", i );
869 }
870 Gia_Man2SuppStop( pMan );
871 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
872 pNew = Gia_ManCleanup( pTemp = pNew );
873 Gia_ManStop( pTemp );
874 return pNew;
875}
876
877
878
879
883
884
885ABC_NAMESPACE_IMPL_END
886
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
ddClearFlag2
void ddClearFlag2(DdNode *f)
Definition extraBddMisc.c:1724
ddSupportStep2
void ddSupportStep2(DdNode *f, int *support)
Definition extraBddMisc.c:1693
Gia_Min2ObjGetCnfVar
int Gia_Min2ObjGetCnfVar(Gia_Man2Min_t *p, int iObj)
Definition giaSupp.c:617
Gia_ManSupportAnd
int Gia_ManSupportAnd(Gia_ManMin_t *p, int iLit0, int iLit1)
Definition giaSupp.c:280
Gia_Min2AddClausesSuper
void Gia_Min2AddClausesSuper(Gia_Man_t *p, Gia_Obj_t *pNode, Vec_Ptr_t *vSuper, satoko_t *pSat)
Definition giaSupp.c:530
Gia_Man2SuppStart
Gia_Man2Min_t * Gia_Man2SuppStart(Gia_Man_t *pGia)
Definition giaSupp.c:375
Gia_Min2ObjAddToFrontier
void Gia_Min2ObjAddToFrontier(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Ptr_t *vFrontier, satoko_t *pSat, Vec_Int_t *vSatVars)
Definition giaSupp.c:605
Gia_Min2CollectSuper_rec
void Gia_Min2CollectSuper_rec(Gia_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition giaSupp.c:584
Gia_Man2SupportAndTest
Gia_Man_t * Gia_Man2SupportAndTest(Gia_Man_t *pGia)
Definition giaSupp.c:840
Gia_Min2ManSimulate
int Gia_Min2ManSimulate(Gia_Man2Min_t *p)
Definition giaSupp.c:671
Gia_Min2ManGatherSupp
int Gia_Min2ManGatherSupp(Gia_Man2Min_t *p)
Definition giaSupp.c:788
Gia_Man2SuppStop
void Gia_Man2SuppStop(Gia_Man2Min_t *p)
Definition giaSupp.c:394
Gia_Min2AddClausesMux
void Gia_Min2AddClausesMux(Gia_Man_t *p, Gia_Obj_t *pNode, satoko_t *pSat)
Definition giaSupp.c:422
Gia_ManSupportAndTest
Gia_Man_t * Gia_ManSupportAndTest(Gia_Man_t *pGia)
Definition giaSupp.c:297
Gia_ManSuppStart
ABC_NAMESPACE_IMPL_START Gia_ManMin_t * Gia_ManSuppStart(Gia_Man_t *pGia)
DECLARATIONS ///.
Definition giaSupp.c:279
Gia_Min2CollectSuper
void Gia_Min2CollectSuper(Gia_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition giaSupp.c:598
Gia_Min2ManSolve
int Gia_Min2ManSolve(Gia_Man2Min_t *p)
Definition giaSupp.c:717
Gia_Man2SupportAnd
int Gia_Man2SupportAnd(Gia_Man2Min_t *p, int iLit0, int iLit1)
Definition giaSupp.c:815
Gia_ManSuppStop
void Gia_ManSuppStop(Gia_ManMin_t *p)
Definition giaSupp.c:281
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition giaUtil.c:1056
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition giaUtil.c:67
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_Man2Min_t
struct Gia_Man2Min_t_ Gia_Man2Min_t
Definition gia.h:1669
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManMin_t
struct Gia_ManMin_t_ Gia_ManMin_t
Definition gia.h:1665
Gia_ManHashLookupInt
int Gia_ManHashLookupInt(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:81
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition giaUtil.c:218
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
satoko_solve
int satoko_solve(satoko_t *)
Definition solver_api.c:314
SATOKO_UNSAT
@ SATOKO_UNSAT
Definition satoko.h:25
SATOKO_SAT
@ SATOKO_SAT
Definition satoko.h:24
satoko_var_polarity
char satoko_var_polarity(satoko_t *, unsigned)
Definition solver_api.c:672
satoko_varnum
int satoko_varnum(satoko_t *)
Definition solver_api.c:625
SATOKO_LIT_TRUE
@ SATOKO_LIT_TRUE
Definition satoko.h:30
satoko_add_variable
int satoko_add_variable(satoko_t *, char)
Definition solver_api.c:237
satoko_rollback
void satoko_rollback(satoko_t *)
Definition solver_api.c:508
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_assump_push
void satoko_assump_push(satoko_t *s, int)
Definition solver_api.c:298
satoko_assump_pop
void satoko_assump_pop(satoko_t *s)
Definition solver_api.c:306
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_options
satoko_opts_t * satoko_options(satoko_t *)
Definition solver_api.c:438
Gia_Man2Min_t_
Definition giaSupp.c:337
Gia_Man2Min_t_::vSims
Vec_Wrd_t * vSims
Definition giaSupp.c:346
Gia_Man2Min_t_::vFrontier
Vec_Ptr_t * vFrontier
Definition giaSupp.c:347
Gia_Man2Min_t_::pSat
satoko_t * pSat
Definition giaSupp.c:345
Gia_Man2Min_t_::vSatVars
Vec_Int_t * vSatVars
Definition giaSupp.c:349
Gia_Man2Min_t_::nSatSat
int nSatSat
Definition giaSupp.c:352
Gia_Man2Min_t_::nSims
int nSims
Definition giaSupp.c:355
Gia_Man2Min_t_::nSupps
int nSupps
Definition giaSupp.c:356
Gia_Man2Min_t_::iPattern
int iPattern
Definition giaSupp.c:351
Gia_Man2Min_t_::iLits
int iLits[2]
Definition giaSupp.c:340
Gia_Man2Min_t_::nSatUnsat
int nSatUnsat
Definition giaSupp.c:353
Gia_Man2Min_t_::pGia
Gia_Man_t * pGia
Definition giaSupp.c:339
Gia_Man2Min_t_::vFanins
Vec_Ptr_t * vFanins
Definition giaSupp.c:348
Gia_Man2Min_t_::vCis
Vec_Int_t * vCis[2]
Definition giaSupp.c:342
Gia_Man2Min_t_::nCalls
int nCalls
Definition giaSupp.c:354
Gia_Man2Min_t_::vObjs
Vec_Int_t * vObjs[2]
Definition giaSupp.c:343
Gia_Man2Min_t_::nCisOld
int nCisOld
Definition giaSupp.c:350
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
satoko_opts::learnt_ratio
float learnt_ratio
Definition satoko.h:55
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
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_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42