ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaPat2.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/vec/vecHsh.h"
23#include "sat/cnf/cnf.h"
24#include "sat/bsat/satStore.h"
25#include "misc/util/utilTruth.h"
26
27ABC_NAMESPACE_IMPL_START
28
29
33
34typedef struct Min_Man_t_ Min_Man_t;
47
48static inline int Min_ManCiNum( Min_Man_t * p ) { return p->nCis; }
49static inline int Min_ManCoNum( Min_Man_t * p ) { return p->nCos; }
50static inline int Min_ManObjNum( Min_Man_t * p ) { return Vec_IntSize(&p->vFans) >> 1; }
51static inline int Min_ManAndNum( Min_Man_t * p ) { return Min_ManObjNum(p) - p->nCis - p->nCos - 1; }
52
53static inline int Min_ManCi( Min_Man_t * p, int i ) { return 1 + i; }
54static inline int Min_ManCo( Min_Man_t * p, int i ) { return Min_ManObjNum(p) - Min_ManCoNum(p) + i; }
55
56static inline int Min_ObjIsCi( Min_Man_t * p, int i ) { return i > 0 && i <= Min_ManCiNum(p); }
57static inline int Min_ObjIsNode( Min_Man_t * p, int i ) { return i > Min_ManCiNum(p) && i < Min_ManObjNum(p) - Min_ManCoNum(p); }
58static inline int Min_ObjIsAnd( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) < Vec_IntEntry(&p->vFans, 2*i+1); }
59static inline int Min_ObjIsXor( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) > Vec_IntEntry(&p->vFans, 2*i+1); }
60static inline int Min_ObjIsBuf( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) ==Vec_IntEntry(&p->vFans, 2*i+1); }
61static inline int Min_ObjIsCo( Min_Man_t * p, int i ) { return i >= Min_ManObjNum(p) - Min_ManCoNum(p) && i < Min_ManObjNum(p); }
62
63static inline int Min_ObjLit( Min_Man_t * p, int i, int n ) { return Vec_IntEntry(&p->vFans, i + i + n); }
64static inline int Min_ObjLit0( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 0); }
65static inline int Min_ObjLit1( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 1); }
66static inline int Min_ObjCioId( Min_Man_t * p, int i ) { assert( i && !Min_ObjIsNode(p, i) ); return Min_ObjLit1(p, i); }
67
68static inline int Min_ObjFan0( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit0(p, i) ); }
69static inline int Min_ObjFan1( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit1(p, i) ); }
70
71static inline int Min_ObjFanC0( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit0(p, i) ); }
72static inline int Min_ObjFanC1( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit1(p, i) ); }
73
74static inline char Min_ObjValN( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsN, i); }
75static inline void Min_ObjSetValN( Min_Man_t * p, int i, char v ){ Vec_StrWriteEntry(&p->vValsN, i, v); }
76
77static inline char Min_LitValL( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsL, i); }
78static inline void Min_LitSetValL( Min_Man_t * p, int i, char v ){ assert(v==0 || v==1); Vec_StrWriteEntry(&p->vValsL, i, v); Vec_StrWriteEntry(&p->vValsL, i^1, (char)!v); Vec_IntPush(&p->vVis, Abc_Lit2Var(i)); }
79static inline void Min_ObjCleanValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] = 0x0202; }
80static inline void Min_ObjMarkValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0404; }
81static inline void Min_ObjMark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0808; }
82static inline void Min_ObjUnmark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] &= 0xF7F7; }
83
84static inline int Min_LitIsCi( Min_Man_t * p, int v ) { return v > 1 && v < p->FirstAndLit; }
85static inline int Min_LitIsNode( Min_Man_t * p, int v ) { return v >= p->FirstAndLit && v < p->FirstCoLit; }
86static inline int Min_LitIsCo( Min_Man_t * p, int v ) { return v >= p->FirstCoLit; }
87
88static inline int Min_LitIsAnd( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 < v1); }
89static inline int Min_LitIsXor( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 > v1); }
90static inline int Min_LitIsBuf( int v, int v0, int v1 ) { return v0 == v1; }
91
92static inline int Min_LitFan( Min_Man_t * p, int v ) { return Vec_IntEntry(&p->vFans, v); }
93static inline int Min_LitFanC( Min_Man_t * p, int v ) { return Abc_LitIsCompl( Min_LitFan(p, v) ); }
94
95static inline void Min_ManStartValsN( Min_Man_t * p ) { Vec_StrGrow(&p->vValsN, Vec_IntCap(&p->vFans)/2); Vec_StrFill(&p->vValsN, Min_ManObjNum(p), 2); }
96static inline void Min_ManStartValsL( Min_Man_t * p ) { Vec_StrGrow(&p->vValsL, Vec_IntCap(&p->vFans)); Vec_StrFill(&p->vValsL, Vec_IntSize(&p->vFans), 2); }
97static inline int Min_ManCheckCleanValsL( Min_Man_t * p ) { int i; char c; Vec_StrForEachEntry( &p->vValsL, c, i ) if ( c != 2 ) return 0; return 1; }
98static inline void Min_ManCleanVisitedValL( Min_Man_t * p ) { int i, iObj; Vec_IntForEachEntry(&p->vVis, iObj, i) Min_ObjCleanValL(p, iObj); Vec_IntClear(&p->vVis); }
99
100
101#define Min_ManForEachObj( p, i ) \
102 for ( i = 0; i < Min_ManObjNum(p); i++ )
103#define Min_ManForEachCi( p, i ) \
104 for ( i = 1; i <= Min_ManCiNum(p); i++ )
105#define Min_ManForEachCo( p, i ) \
106 for ( i = Min_ManObjNum(p) - Min_ManCoNum(p); i < Min_ManObjNum(p); i++ )
107#define Min_ManForEachAnd( p, i ) \
108 for ( i = 1 + Min_ManCiNum(p); i < Min_ManObjNum(p) - Min_ManCoNum(p); i++ )
109
110
114
126static inline Min_Man_t * Min_ManStart( int nObjMax )
127{
128 Min_Man_t * p = ABC_CALLOC( Min_Man_t, 1 );
129 Vec_IntGrow( &p->vFans, nObjMax );
130 Vec_IntPushTwo( &p->vFans, -1, -1 );
131 return p;
132}
133static inline void Min_ManStop( Min_Man_t * p )
134{
135 Vec_IntErase( &p->vFans );
136 Vec_StrErase( &p->vValsN );
137 Vec_StrErase( &p->vValsL );
138 Vec_IntErase( &p->vVis );
139 Vec_IntErase( &p->vPat );
140 ABC_FREE( p );
141}
142
154static inline int Min_ManAppendObj( Min_Man_t * p, int iLit0, int iLit1 )
155{
156 int iLit = Vec_IntSize(&p->vFans);
157 Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
158 return iLit;
159}
160static inline int Min_ManAppendCi( Min_Man_t * p )
161{
162 p->nCis++;
163 p->FirstAndLit = Vec_IntSize(&p->vFans) + 2;
164 return Min_ManAppendObj( p, 0, p->nCis-1 );
165}
166static inline int Min_ManAppendCo( Min_Man_t * p, int iLit0 )
167{
168 p->nCos++;
169 if ( p->FirstCoLit == 0 )
170 p->FirstCoLit = Vec_IntSize(&p->vFans);
171 return Min_ManAppendObj( p, iLit0, p->nCos-1 );
172}
173
185void Min_ManFromGia_rec( Min_Man_t * pNew, Gia_Man_t * p, int iObj )
186{
187 Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int iLit0, iLit1;
188 if ( ~pObj->Value )
189 return;
190 assert( Gia_ObjIsAnd(pObj) );
191 Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj) );
192 Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj) );
193 iLit0 = Gia_ObjFanin0Copy(pObj);
194 iLit1 = Gia_ObjFanin1Copy(pObj);
195 pObj->Value = Min_ManAppendObj( pNew, Abc_MinInt(iLit0, iLit1), Abc_MaxInt(iLit0, iLit1) );
196}
197Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts )
198{
199 Gia_Obj_t * pObj; int i;
200 Min_Man_t * pNew = Min_ManStart( Gia_ManObjNum(p) );
201 Gia_ManFillValue(p);
202 Gia_ManConst0(p)->Value = 0;
203 Gia_ManForEachCi( p, pObj, i )
204 pObj->Value = Min_ManAppendCi( pNew );
205 if ( vOuts == NULL )
206 {
207 Gia_ManForEachAnd( p, pObj, i )
208 pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
209 Gia_ManForEachCo( p, pObj, i )
210 pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
211 }
212 else
213 {
214 Gia_ManForEachCoVec( vOuts, p, pObj, i )
215 Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0p(p, pObj) );
216 Gia_ManForEachCoVec( vOuts, p, pObj, i )
217 Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
218 }
219 return pNew;
220}
221
222
234static inline char Min_XsimNot( char Val )
235{
236 if ( Val < 2 )
237 return Val ^ 1;
238 return 2;
239}
240static inline char Min_XsimXor( char Val0, char Val1 )
241{
242 if ( Val0 < 2 && Val1 < 2 )
243 return Val0 ^ Val1;
244 return 2;
245}
246static inline char Min_XsimAnd( char Val0, char Val1 )
247{
248 if ( Val0 == 0 || Val1 == 0 )
249 return 0;
250 if ( Val0 == 1 && Val1 == 1 )
251 return 1;
252 return 2;
253}
254
255
256
268char Min_LitVerify_rec( Min_Man_t * p, int iLit )
269{
270 char Val = Min_LitValL(p, iLit);
271 if ( Val == 2 && Min_LitIsNode(p, iLit) ) // unassigned
272 {
273 int iLit0 = Min_LitFan(p, iLit);
274 int iLit1 = Min_LitFan(p, iLit^1);
275 char Val0 = Min_LitVerify_rec( p, iLit0 );
276 char Val1 = Min_LitVerify_rec( p, iLit1 );
277 assert( Val0 < 3 && Val1 < 3 );
278 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
279 Val = Min_XsimXor( Val0, Val1 );
280 else
281 Val = Min_XsimAnd( Val0, Val1 );
282 if ( Val < 2 )
283 {
284 Val ^= Abc_LitIsCompl(iLit);
285 Min_LitSetValL( p, iLit, Val );
286 }
287 else
288 Vec_IntPush( &p->vVis, Abc_Lit2Var(iLit) );
289 Min_ObjMark2ValL( p, Abc_Lit2Var(iLit) );
290 }
291 return Val&3;
292}
293char Min_LitVerify( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
294{
295 int i, Entry; char Res;
296 if ( iLit < 2 ) return 1;
297 assert( !Min_LitIsCo(p, iLit) );
298 //assert( Min_ManCheckCleanValsL(p) );
299 assert( Vec_IntSize(&p->vVis) == 0 );
300 Vec_IntForEachEntry( vLits, Entry, i )
301 Min_LitSetValL( p, Entry, 1 ); // ms notation
302 Res = Min_LitVerify_rec( p, iLit );
303 Min_ManCleanVisitedValL( p );
304 return Res;
305}
306
307void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
308{
309 int i, iObj, iTemp; char Res;
310 Vec_IntClear( &p->vPat );
311 if ( iLit < 2 ) return;
312 assert( !Min_LitIsCo(p, iLit) );
313 //assert( Min_ManCheckCleanValsL(p) );
314 assert( Vec_IntSize(&p->vVis) == 0 );
315 Vec_IntForEachEntry( vLits, iTemp, i )
316 Min_LitSetValL( p, iTemp, 1 ); // ms notation
317 Res = Min_LitVerify_rec( p, iLit );
318 assert( Res == 1 );
319 Min_ObjMarkValL( p, Abc_Lit2Var(iLit) );
320 Vec_IntForEachEntryReverse( &p->vVis, iObj, i )
321 {
322 int iLit = Abc_Var2Lit( iObj, 0 );
323 int Value = 7 & Min_LitValL(p, iLit);
324 if ( Value >= 4 )
325 {
326 if ( Min_LitIsCi(p, iLit) )
327 Vec_IntPush( &p->vPat, Abc_LitNotCond(iLit, !(Value&1)) );
328 else
329 {
330 int iLit0 = Min_LitFan(p, iLit);
331 int iLit1 = Min_LitFan(p, iLit^1);
332 char Val0 = Min_LitValL( p, iLit0 );
333 char Val1 = Min_LitValL( p, iLit1 );
334 if ( Value&1 ) // value == 1
335 {
336 assert( (Val0&1) && (Val1&1) );
337 Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
338 Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
339 }
340 else // value == 0
341 {
342 int Zero0 = !(Val0&3);
343 int Zero1 = !(Val1&3);
344 assert( Zero0 || Zero1 );
345 if ( Zero0 && !Zero1 )
346 Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
347 else if ( !Zero0 && Zero1 )
348 Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
349 else if ( Val0 == 4 && Val1 != 4 )
350 Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
351 else if ( Val1 == 4 && Val0 != 4 )
352 Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
353 else if ( Abc_Random(0) & 1 )
354 Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
355 else
356 Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
357 }
358 }
359 }
360 Min_ObjCleanValL( p, Abc_Lit2Var(iLit) );
361 }
362 Vec_IntClear( &p->vVis );
363 //Min_ManCleanVisitedValL( p );
364 //assert( Min_LitVerify(p, iLit, &p->vPat) == 1 );
365 assert( Vec_IntSize(&p->vPat) <= Vec_IntSize(vLits) );
366}
367
379static inline char Min_LitIsImplied1( Min_Man_t * p, int iLit )
380{
381 char Val = 2;
382 int iLit0 = Min_LitFan(p, iLit);
383 int iLit1 = Min_LitFan(p, iLit^1);
384 char Val0 = Min_LitValL(p, iLit0);
385 char Val1 = Min_LitValL(p, iLit1);
386 assert( Min_LitIsNode(p, iLit) ); // internal node
387 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
388 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
389 Val = Min_XsimXor( Val0, Val1 );
390 else
391 Val = Min_XsimAnd( Val0, Val1 );
392 if ( Val < 2 )
393 {
394 Val ^= Abc_LitIsCompl(iLit);
395 Min_LitSetValL( p, iLit, Val );
396 }
397 return Val;
398}
399static inline char Min_LitIsImplied2( Min_Man_t * p, int iLit )
400{
401 char Val = 2;
402 int iLit0 = Min_LitFan(p, iLit);
403 int iLit1 = Min_LitFan(p, iLit^1);
404 char Val0 = Min_LitValL(p, iLit0);
405 char Val1 = Min_LitValL(p, iLit1);
406 assert( Min_LitIsNode(p, iLit) ); // internal node
407 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
408 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
409 Val0 = Min_LitIsImplied1(p, iLit0);
410 Val1 = Min_LitValL(p, iLit1);
411 }
412 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
413 Val1 = Min_LitIsImplied1(p, iLit1);
414 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
415 Val = Min_XsimXor( Val0, Val1 );
416 else
417 Val = Min_XsimAnd( Val0, Val1 );
418 if ( Val < 2 )
419 {
420 Val ^= Abc_LitIsCompl(iLit);
421 Min_LitSetValL( p, iLit, Val );
422 }
423 return Val;
424}
425static inline char Min_LitIsImplied3( Min_Man_t * p, int iLit )
426{
427 char Val = 2;
428 int iLit0 = Min_LitFan(p, iLit);
429 int iLit1 = Min_LitFan(p, iLit^1);
430 char Val0 = Min_LitValL(p, iLit0);
431 char Val1 = Min_LitValL(p, iLit1);
432 assert( Min_LitIsNode(p, iLit) ); // internal node
433 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
434 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
435 Val0 = Min_LitIsImplied2(p, iLit0);
436 Val1 = Min_LitValL(p, iLit1);
437 }
438 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
439 Val1 = Min_LitIsImplied2(p, iLit1);
440 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
441 Val = Min_XsimXor( Val0, Val1 );
442 else
443 Val = Min_XsimAnd( Val0, Val1 );
444 if ( Val < 2 )
445 {
446 Val ^= Abc_LitIsCompl(iLit);
447 Min_LitSetValL( p, iLit, Val );
448 }
449 return Val;
450}
451static inline char Min_LitIsImplied4( Min_Man_t * p, int iLit )
452{
453 char Val = 2;
454 int iLit0 = Min_LitFan(p, iLit);
455 int iLit1 = Min_LitFan(p, iLit^1);
456 char Val0 = Min_LitValL(p, iLit0);
457 char Val1 = Min_LitValL(p, iLit1);
458 assert( Min_LitIsNode(p, iLit) ); // internal node
459 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
460 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
461 Val0 = Min_LitIsImplied3(p, iLit0);
462 Val1 = Min_LitValL(p, iLit1);
463 }
464 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
465 Val1 = Min_LitIsImplied3(p, iLit1);
466 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
467 Val = Min_XsimXor( Val0, Val1 );
468 else
469 Val = Min_XsimAnd( Val0, Val1 );
470 if ( Val < 2 )
471 {
472 Val ^= Abc_LitIsCompl(iLit);
473 Min_LitSetValL( p, iLit, Val );
474 }
475 return Val;
476}
477static inline char Min_LitIsImplied5( Min_Man_t * p, int iLit )
478{
479 char Val = 2;
480 int iLit0 = Min_LitFan(p, iLit);
481 int iLit1 = Min_LitFan(p, iLit^1);
482 char Val0 = Min_LitValL(p, iLit0);
483 char Val1 = Min_LitValL(p, iLit1);
484 assert( Min_LitIsNode(p, iLit) ); // internal node
485 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
486 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) {
487 Val0 = Min_LitIsImplied4(p, iLit0);
488 Val1 = Min_LitValL(p, iLit1);
489 }
490 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
491 Val1 = Min_LitIsImplied4(p, iLit1);
492 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
493 Val = Min_XsimXor( Val0, Val1 );
494 else
495 Val = Min_XsimAnd( Val0, Val1 );
496 if ( Val < 2 )
497 {
498 Val ^= Abc_LitIsCompl(iLit);
499 Min_LitSetValL( p, iLit, Val );
500 }
501 return Val;
502}
503
504// this recursive procedure is about 10% slower
505char Min_LitIsImplied_rec( Min_Man_t * p, int iLit, int Depth )
506{
507 char Val = 2;
508 int iLit0 = Min_LitFan(p, iLit);
509 int iLit1 = Min_LitFan(p, iLit^1);
510 char Val0 = Min_LitValL(p, iLit0);
511 char Val1 = Min_LitValL(p, iLit1);
512 assert( Depth > 0 );
513 assert( Min_LitIsNode(p, iLit) ); // internal node
514 assert( Min_LitValL(p, iLit) == 2 ); // unassigned
515 if ( Depth > 1 && Val0 == 2 && Min_LitIsNode(p, iLit0) )
516 {
517 Val0 = Min_LitIsImplied_rec(p, iLit0, Depth-1);
518 Val1 = Min_LitValL(p, iLit1);
519 }
520 if ( Depth > 1 && Val1 == 2 && Min_LitIsNode(p, iLit1) )
521 {
522 Val1 = Min_LitIsImplied_rec(p, iLit1, Depth-1);
523 Val0 = Min_LitValL(p, iLit0);
524 }
525 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
526 Val = Min_XsimXor( Val0, Val1 );
527 else
528 Val = Min_XsimAnd( Val0, Val1 );
529 if ( Val < 2 )
530 {
531 Val ^= Abc_LitIsCompl(iLit);
532 Min_LitSetValL( p, iLit, Val );
533 }
534 return Val;
535}
536int Min_LitJustify_rec( Min_Man_t * p, int iLit )
537{
538 int Res = 1, LitValue = !Abc_LitIsCompl(iLit);
539 int Val = (int)Min_LitValL(p, iLit);
540 if ( Val < 2 ) // assigned
541 return Val == LitValue;
542 // unassigned
543 if ( Min_LitIsCi(p, iLit) )
544 Vec_IntPush( &p->vPat, iLit ); // ms notation
545 else
546 {
547 int iLit0 = Min_LitFan(p, iLit);
548 int iLit1 = Min_LitFan(p, iLit^1);
549 char Val0 = Min_LitValL(p, iLit0);
550 char Val1 = Min_LitValL(p, iLit1);
551 if ( Min_LitIsXor(iLit, iLit0, iLit1) )
552 {
553 if ( Val0 < 2 && Val1 < 2 )
554 Res = LitValue == (Val0 ^ Val1);
555 else if ( Val0 < 2 )
556 Res = Min_LitJustify_rec(p, iLit1^Val0^!LitValue);
557 else if ( Val1 < 2 )
558 Res = Min_LitJustify_rec(p, iLit0^Val1^!LitValue);
559 else if ( Abc_Random(0) & 1 )
560 Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1^ LitValue);
561 else
562 Res = Min_LitJustify_rec(p, iLit0^1) && Min_LitJustify_rec(p, iLit1^!LitValue);
563 assert( !Res || LitValue == Min_XsimXor(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
564 }
565 else if ( LitValue ) // value 1
566 {
567 if ( Val0 == 0 || Val1 == 0 )
568 Res = 0;
569 else if ( Val0 == 1 && Val1 == 1 )
570 Res = 1;
571 else if ( Val0 == 1 )
572 Res = Min_LitJustify_rec(p, iLit1);
573 else if ( Val1 == 1 )
574 Res = Min_LitJustify_rec(p, iLit0);
575 else
576 Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1);
577 assert( !Res || 1 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
578 }
579 else // value 0
580 {
581/*
582 int Depth = 3;
583 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
584 {
585 Val0 = Min_LitIsImplied_rec(p, iLit0, Depth);
586 Val1 = Min_LitValL(p, iLit1);
587 }
588 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
589 {
590 Val1 = Min_LitIsImplied_rec(p, iLit1, Depth);
591 Val0 = Min_LitValL(p, iLit0);
592 }
593*/
594 if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
595 {
596 Val0 = Min_LitIsImplied3(p, iLit0);
597 Val1 = Min_LitValL(p, iLit1);
598 }
599 if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
600 {
601 Val1 = Min_LitIsImplied3(p, iLit1);
602 Val0 = Min_LitValL(p, iLit0);
603 }
604 if ( Val0 == 0 || Val1 == 0 )
605 Res = 1;
606 else if ( Val0 == 1 && Val1 == 1 )
607 Res = 0;
608 else if ( Val0 == 1 )
609 Res = Min_LitJustify_rec(p, iLit1^1);
610 else if ( Val1 == 1 )
611 Res = Min_LitJustify_rec(p, iLit0^1);
612 else if ( Abc_Random(0) & 1 )
613 //else if ( (p->Random >> (iLit & 0x1F)) & 1 )
614 Res = Min_LitJustify_rec(p, iLit0^1);
615 else
616 Res = Min_LitJustify_rec(p, iLit1^1);
617 //Val0 = Min_LitValL(p, iLit0);
618 //Val1 = Min_LitValL(p, iLit1);
619 assert( !Res || 0 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
620 }
621 }
622 if ( Res )
623 Min_LitSetValL( p, iLit, 1 );
624 return Res;
625}
626int Min_LitJustify( Min_Man_t * p, int iLit )
627{
628 int Res, fCheck = 0;
629 Vec_IntClear( &p->vPat );
630 if ( iLit < 2 ) return 1;
631 assert( !Min_LitIsCo(p, iLit) );
632 //assert( Min_ManCheckCleanValsL(p) );
633 assert( Vec_IntSize(&p->vVis) == 0 );
634 //p->Random = Abc_Random(0);
635 Res = Min_LitJustify_rec( p, iLit );
636 Min_ManCleanVisitedValL( p );
637 if ( Res )
638 {
639 if ( fCheck && Min_LitVerify(p, iLit, &p->vPat) != 1 )
640 printf( "Verification FAILED for literal %d.\n", iLit );
641 //else
642 // printf( "Verification succeeded for literal %d.\n", iLit );
643 }
644 //else
645 // printf( "Could not justify literal %d.\n", iLit );
646 return Res;
647}
648
649
650
662Vec_Int_t * Min_TargGenerateCexes( Min_Man_t * p, Vec_Int_t * vCoErrs, int nCexes, int nCexesStop, int * pnComputed, int fVerbose )
663{
664 abctime clk = Abc_Clock();
665 int t, iObj, Count = 0, CountPos = 0, CountPosSat = 0, nRuns[2] = {0}, nCountCexes[2] = {0};
666 Vec_Int_t * vPats = Vec_IntAlloc( 1000 );
667 Vec_Int_t * vPatBest = Vec_IntAlloc( Min_ManCiNum(p) );
668 Hsh_VecMan_t * pHash = Hsh_VecManStart( 10000 );
669 Min_ManForEachCo( p, iObj ) if ( Min_ObjLit0(p, iObj) > 1 )
670 {
671 int nCexesGenSim0 = 0;
672 int nCexesGenSim = 0;
673 int nCexesGenSat = 0;
674 if ( vCoErrs && Vec_IntEntry(vCoErrs, Min_ObjCioId(p, iObj)) >= nCexesStop )
675 continue;
676 //printf( "%d ", i );
677 for ( t = 0; t < nCexes; t++ )
678 {
679 nRuns[0]++;
680 if ( Min_LitJustify( p, Min_ObjLit0(p, iObj) ) )
681 {
682 int Before, After;
683 assert( Vec_IntSize(&p->vPat) > 0 );
684 //printf( "%d ", Vec_IntSize(vPat) );
685 Vec_IntClear( vPatBest );
686 if ( 1 ) // no minimization
687 Vec_IntAppend( vPatBest, &p->vPat );
688 else
689 {
690/*
691 for ( k = 0; k < 10; k++ )
692 {
693 Vec_IntClear( vPat2 );
694 Gia_ManIncrementTravId( p );
695 Cexes_MinimizePattern_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), vPat2 );
696 assert( Vec_IntSize(vPat2) <= Vec_IntSize(vPat) );
697 if ( Vec_IntSize(vPatBest) == 0 || Vec_IntSize(vPatBest) > Vec_IntSize(vPat2) )
698 {
699 Vec_IntClear( vPatBest );
700 Vec_IntAppend( vPatBest, vPat2 );
701 }
702 //printf( "%d ", Vec_IntSize(vPat2) );
703 }
704*/
705 }
706
707 //Gia_CexVerify( p, Gia_ObjFaninId0p(p, pObj), !Gia_ObjFaninC0(pObj), vPatBest );
708 //printf( "\n" );
709 Before = Hsh_VecSize( pHash );
710 Vec_IntSort( vPatBest, 0 );
711 Hsh_VecManAdd( pHash, vPatBest );
712 After = Hsh_VecSize( pHash );
713 if ( Before != After )
714 {
715 Vec_IntPush( vPats, Min_ObjCioId(p, iObj) );
716 Vec_IntPush( vPats, Vec_IntSize(vPatBest) );
717 Vec_IntAppend( vPats, vPatBest );
718 nCexesGenSim++;
719 }
720 nCexesGenSim0++;
721 if ( nCexesGenSim0 > nCexesGenSim*10 )
722 {
723 printf( "**** Skipping output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
724 break;
725 }
726 }
727 if ( nCexesGenSim == nCexesStop )
728 break;
729 }
730 //printf( "(%d %d) ", nCexesGenSim0, nCexesGenSim );
731 //printf( "%d ", t/nCexesGenSim );
732
733 //printf( "The number of CEXes = %d\n", nCexesGen );
734 //if ( fVerbose )
735 // printf( "%d ", nCexesGen );
736 nCountCexes[0] += nCexesGenSim;
737 nCountCexes[1] += nCexesGenSat;
738 Count += nCexesGenSim + nCexesGenSat;
739 CountPos++;
740
741 if ( nCexesGenSim0 == 0 && t == nCexes )
742 printf( "#### Output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
743 }
744 //printf( "\n" );
745 if ( fVerbose )
746 printf( "\n" );
747 if ( fVerbose )
748 printf( "Got %d unique CEXes using %d sim (%d) and %d SAT (%d) runs (ave size %.1f). PO = %d ErrPO = %d SatPO = %d ",
749 Count, nRuns[0], nCountCexes[0], nRuns[1], nCountCexes[1],
750 1.0*Vec_IntSize(vPats)/Abc_MaxInt(1, Count)-2, Min_ManCoNum(p), CountPos, CountPosSat );
751 if ( fVerbose )
752 Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
753 Hsh_VecManStop( pHash );
754 Vec_IntFree( vPatBest );
755 *pnComputed = Count;
756 return vPats;
757}
758
759
771void Min_ManTest3( Gia_Man_t * p, Vec_Int_t * vCoErrs )
772{
773 int fXor = 0;
774 int nComputed;
775 Vec_Int_t * vPats;
776 Gia_Man_t * pXor = fXor ? Gia_ManDupMuxes(p, 1) : NULL;
777 Min_Man_t * pNew = Min_ManFromGia( fXor ? pXor : p, NULL );
778 Gia_ManStopP( &pXor );
779 Min_ManStartValsL( pNew );
780 //Vec_IntFill( vCoErrs, Vec_IntSize(vCoErrs), 0 );
781 //vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
782 vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
783 Vec_IntFree( vPats );
784 Min_ManStop( pNew );
785}
786void Min_ManTest4( Gia_Man_t * p )
787{
788 Vec_Int_t * vCoErrs = Vec_IntStartNatural( Gia_ManCoNum(p) );
789 Min_ManTest3(p, vCoErrs);
790 Vec_IntFree( vCoErrs );
791}
792
793
805void Gia_ManDupCones2CollectPis_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vMap )
806{
807 Gia_Obj_t * pObj;
808 if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
809 return;
810 pObj = Gia_ManObj( p, iObj );
811 if ( Gia_ObjIsAnd(pObj) )
812 {
813 Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId0(pObj, iObj), vMap );
814 Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId1(pObj, iObj), vMap );
815 }
816 else if ( Gia_ObjIsCi(pObj) )
817 Vec_IntPush( vMap, iObj );
818 else assert( 0 );
819}
820void Gia_ManDupCones2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
821{
822 if ( Gia_ObjIsCi(pObj) || Gia_ObjUpdateTravIdCurrent(p, pObj) )
823 return;
824 assert( Gia_ObjIsAnd(pObj) );
825 Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(pObj) );
826 Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin1(pObj) );
827 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
828}
829Gia_Man_t * Gia_ManDupCones2( Gia_Man_t * p, int * pOuts, int nOuts, Vec_Int_t * vMap )
830{
831 Gia_Man_t * pNew;
832 Gia_Obj_t * pObj; int i;
833 Vec_IntClear( vMap );
834 Gia_ManIncrementTravId( p );
835 for ( i = 0; i < nOuts; i++ )
836 Gia_ManDupCones2CollectPis_rec( p, Gia_ManCoDriverId(p, pOuts[i]), vMap );
837 pNew = Gia_ManStart( 1000 );
838 pNew->pName = Abc_UtilStrsav( p->pName );
839 Gia_ManConst0(p)->Value = 0;
840 Gia_ManForEachObjVec( vMap, p, pObj, i )
841 pObj->Value = Gia_ManAppendCi( pNew );
842 Gia_ManIncrementTravId( p );
843 for ( i = 0; i < nOuts; i++ )
844 Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(Gia_ManCo(p, pOuts[i])) );
845 for ( i = 0; i < nOuts; i++ )
846 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, pOuts[i])) );
847 return pNew;
848}
849
850
862int Min_ManRemoveItem( Vec_Wec_t * vCexes, int iItem, int iFirst, int iLimit )
863{
864 Vec_Int_t * vLevel = NULL, * vLevel0 = Vec_WecEntry(vCexes, iItem); int i;
865 assert( iFirst <= iItem && iItem < iLimit );
866 Vec_WecForEachLevelReverseStartStop( vCexes, vLevel, i, iLimit, iFirst )
867 if ( Vec_IntSize(vLevel) > 0 )
868 break;
869 assert( iFirst <= i && iItem <= i );
870 Vec_IntClear( vLevel0 );
871 if ( iItem < i )
872 ABC_SWAP( Vec_Int_t, *vLevel0, *vLevel );
873 return -1;
874}
875int Min_ManAccumulate( Vec_Wec_t * vCexes, int iFirst, int iLimit, Vec_Int_t * vCex )
876{
877 Vec_Int_t * vLevel; int i, nCommon, nDiff = 0;
878 Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
879 {
880 if ( Vec_IntSize(vLevel) == 0 )
881 {
882 Vec_IntAppend(vLevel, vCex);
883 return nDiff+1;
884 }
885 nCommon = Vec_IntTwoCountCommon( vLevel, vCex );
886 if ( nCommon == Vec_IntSize(vLevel) ) // ignore vCex
887 return nDiff;
888 if ( nCommon == Vec_IntSize(vCex) ) // remove vLevel
889 nDiff += Min_ManRemoveItem( vCexes, i, iFirst, iLimit );
890 }
891 assert( 0 );
892 return ABC_INFINITY;
893}
894int Min_ManCountSize( Vec_Wec_t * vCexes, int iFirst, int iLimit )
895{
896 Vec_Int_t * vLevel; int i, nTotal = 0;
897 Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
898 nTotal += Vec_IntSize(vLevel) > 0;
899 return nTotal;
900}
901Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTries, int nMinCexes, Vec_Int_t * vStats[3], int fUseSim, int fUseSat, int fVerbose )
902{
903 int fUseSynthesis = 1;
904 abctime clkSim = Abc_Clock(), clkSat = Abc_Clock();
905 Vec_Int_t * vOuts = vOuts0 ? vOuts0 : Vec_IntStartNatural( Gia_ManCoNum(p) );
906 Min_Man_t * pNew = Min_ManFromGia( p, vOuts );
907 Vec_Wec_t * vCexes = Vec_WecStart( Vec_IntSize(vOuts) * nMinCexes );
908 Vec_Int_t * vPatBest = Vec_IntAlloc( 100 );
909 Vec_Int_t * vLits = Vec_IntAlloc( 100 );
910 Gia_Obj_t * pObj; int i, iObj, nOuts = 0, nSimOuts = 0, nSatOuts = 0;
911 vStats[0] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // total calls
912 vStats[1] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // successful calls + SAT runs
913 vStats[2] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // results
914 Min_ManStartValsL( pNew );
915 Min_ManForEachCo( pNew, iObj )
916 {
917 int nAllCalls = 0;
918 int nGoodCalls = 0;
919 int nCurrCexes = 0;
920 if ( fUseSim && Min_ObjLit0(pNew, iObj) >= 2 )
921 {
922 while ( nAllCalls++ < nMaxTries )
923 {
924 if ( Min_LitJustify( pNew, Min_ObjLit0(pNew, iObj) ) )
925 {
926 Vec_IntClearAppend( vLits, &pNew->vPat );
927 Vec_IntClearAppend( vPatBest, &pNew->vPat );
928 if ( 1 ) // minimization
929 {
930 //printf( "%d -> ", Vec_IntSize(vPatBest) );
931 for ( i = 0; i < 20; i++ )
932 {
933 Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
934 if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
935 Vec_IntClearAppend( vPatBest, &pNew->vPat );
936 }
937 //printf( "%d ", Vec_IntSize(vPatBest) );
938 }
939 assert( Vec_IntSize(vPatBest) > 0 );
940 Vec_IntSort( vPatBest, 0 );
941 nCurrCexes += Min_ManAccumulate( vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes, vPatBest );
942 nGoodCalls++;
943 }
944 if ( nCurrCexes == nMinCexes || nGoodCalls > 10*nCurrCexes )
945 break;
946 }
947 nSimOuts++;
948 }
949 assert( nCurrCexes <= nMinCexes );
950 assert( nCurrCexes == Min_ManCountSize(vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes) );
951 Vec_IntPush( vStats[0], nAllCalls );
952 Vec_IntPush( vStats[1], nGoodCalls );
953 Vec_IntPush( vStats[2], nCurrCexes );
954 nOuts++;
955 }
956 assert( Vec_IntSize(vOuts) == nOuts );
957 assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[0]) );
958 assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[1]) );
959 assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[2]) );
960 clkSim = Abc_Clock() - clkSim;
961
962 if ( fUseSat )
963 Gia_ManForEachCoVec( vOuts, p, pObj, i )
964 {
965 if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
966 continue;
967 {
968 assert( Gia_ObjIsCo(pObj) );
969 if ( Gia_ObjFaninId0p(p, pObj) == 0 ) {
970 if ( fVerbose )
971 printf( "Output %d is driven by constant %d.\n", Gia_ObjCioId(pObj), Gia_ObjFaninC0(pObj) );
972 continue;
973 }
974 abctime clk = Abc_Clock();
975 int iObj = Min_ManCo(pNew, i);
976 int Index = Gia_ObjCioId(pObj);
977 Vec_Int_t * vMap = Vec_IntAlloc( 100 );
978 Gia_Man_t * pCon = Gia_ManDupCones2( p, &Index, 1, vMap );
979 Gia_Man_t * pCon1= fUseSynthesis ? Gia_ManAigSyn2( pCon, 0, 1, 0, 100, 0, 0, 0 ) : NULL;
980 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( fUseSynthesis ? pCon1 : pCon, 8, 0, 0, 0, 0 );
981 sat_solver* pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
982 int Lit = Abc_Var2Lit( 1, 0 );
983 int status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
984 int nAllCalls = 0;
985 int nCurrCexes = Vec_IntEntry(vStats[2], i);
986 //Gia_AigerWrite( pCon, "temp_miter.aig", 0, 0, 0 );
987 if ( status == l_True )
988 {
989 nSatOuts++;
990 //printf( "Running SAT for output %d\n", i );
991 if ( Min_ObjLit0(pNew, iObj) >= 2 )
992 {
993 while ( nAllCalls++ < 100 )
994 {
995 int v, iVar = pCnf->nVars - Gia_ManPiNum(pCon), nVars = Gia_ManPiNum(pCon);
996 if ( nAllCalls > 1 )
997 sat_solver_randomize( pSat, iVar, nVars );
998 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
999 if ( status != l_True )
1000 break;
1001 assert( status == l_True );
1002 Vec_IntClear( vLits );
1003 for ( v = 0; v < nVars; v++ )
1004 Vec_IntPush( vLits, Abc_Var2Lit(Vec_IntEntry(vMap, v), !sat_solver_var_value(pSat, iVar + v)) );
1005 Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
1006 Vec_IntClearAppend( vPatBest, &pNew->vPat );
1007 if ( 1 ) // minimization
1008 {
1009 //printf( "%d -> ", Vec_IntSize(vPatBest) );
1010 for ( v = 0; v < 20; v++ )
1011 {
1012 Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
1013 if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
1014 Vec_IntClearAppend( vPatBest, &pNew->vPat );
1015 }
1016 //printf( "%d ", Vec_IntSize(vPatBest) );
1017 }
1018 Vec_IntSort( vPatBest, 0 );
1019 nCurrCexes += Min_ManAccumulate( vCexes, i*nMinCexes, (i+1)*nMinCexes, vPatBest );
1020 if ( nCurrCexes == nMinCexes || nAllCalls > 10*nCurrCexes )
1021 break;
1022 }
1023 }
1024 }
1025 Vec_IntWriteEntry( vStats[0], i, nAllCalls*nMaxTries );
1026 Vec_IntWriteEntry( vStats[1], i, nAllCalls*nMaxTries );
1027 Vec_IntWriteEntry( vStats[2], i, nCurrCexes );
1028 sat_solver_delete( pSat );
1029 Cnf_DataFree( pCnf );
1030 Gia_ManStop( pCon );
1031 Gia_ManStopP( &pCon1 );
1032 Vec_IntFree( vMap );
1033 if ( fVerbose )
1034 {
1035 printf( "SAT solving for output %3d (cexes = %5d) : ", i, nCurrCexes );
1036 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1037 }
1038 }
1039 }
1040 clkSat = Abc_Clock() - clkSat - clkSim;
1041 if ( fVerbose )
1042 printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts );
1043 if ( fVerbose )
1044 Abc_PrintTime( 1, "Simulation time ", clkSim );
1045 if ( fVerbose )
1046 Abc_PrintTime( 1, "SAT solving time ", clkSat );
1047 //Vec_WecPrint( vCexes, 0 );
1048 if ( vOuts != vOuts0 )
1049 Vec_IntFreeP( &vOuts );
1050 Min_ManStop( pNew );
1051 Vec_IntFree( vPatBest );
1052 Vec_IntFree( vLits );
1053 return vCexes;
1054}
1055
1067int Min_ManBitPackTry( Vec_Wrd_t * vSimsPi, int nWords, int iPat, Vec_Int_t * vLits )
1068{
1069 int i, Lit;
1070 assert( iPat >= 0 && iPat < 64 * nWords );
1071 Vec_IntForEachEntry( vLits, Lit, i )
1072 {
1073 word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId
1074 word * pCare = pInfo + Vec_WrdSize(vSimsPi);
1075 if ( Abc_InfoHasBit( (unsigned *)pCare, iPat ) &&
1076 Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
1077 return 0;
1078 }
1079 Vec_IntForEachEntry( vLits, Lit, i )
1080 {
1081 word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId
1082 word * pCare = pInfo + Vec_WrdSize(vSimsPi);
1083 Abc_InfoSetBit( (unsigned *)pCare, iPat );
1084 if ( Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
1085 Abc_InfoXorBit( (unsigned *)pInfo, iPat );
1086 }
1087 return 1;
1088}
1089int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * vLits )
1090{
1091 int iPat, nTotal = 64*nWords;
1092 for ( iPat = iPat0 + 1; iPat != iPat0; iPat = (iPat + 1) % nTotal )
1093 if ( Min_ManBitPackTry( vSimsPi, nWords, iPat, vLits ) )
1094 break;
1095 return iPat;
1096}
1097Vec_Ptr_t * Min_ReloadCexes( Vec_Wec_t * vCexes, int nMinCexes )
1098{
1099 Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_WecSize(vCexes) );
1100 int i, c, nOuts = Vec_WecSize(vCexes)/nMinCexes;
1101 for ( i = 0; i < nMinCexes; i++ )
1102 for ( c = 0; c < nOuts; c++ )
1103 {
1104 Vec_Int_t * vLevel = Vec_WecEntry( vCexes, c*nMinCexes+i );
1105 if ( Vec_IntSize(vLevel) )
1106 Vec_PtrPush( vRes, vLevel );
1107 }
1108 return vRes;
1109}
1110
1111Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, int nWords0, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose )
1112{
1113 abctime clk = Abc_Clock();
1114 //int fVeryVerbose = 0;
1115 Vec_Wrd_t * vSimsPi = NULL;
1116 Vec_Int_t * vLevel;
1117 int w, nBits, nTotal = 0, fFailed = ABC_INFINITY;
1118 Vec_Int_t * vOrder = NULL;
1119 Vec_Ptr_t * vReload = NULL;
1120 if ( 0 )
1121 {
1122 vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes );
1123 assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) );
1124 assert( Vec_WecSize(vCexes)%nMinCexes == 0 );
1125 Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) );
1126 }
1127 else
1128 vReload = Min_ReloadCexes( vCexes, nMinCexes );
1129 if ( fVerbose )
1130 printf( "Packing: " );
1131 for ( w = nWords0 ? nWords0 : 1; nWords0 ? w <= nWords0 : fFailed > 0; w++ )
1132 {
1133 int i, iPatUsed, iPat = 0;
1134 //int k, iOut;
1135 Vec_WrdFreeP( &vSimsPi );
1136 vSimsPi = fRandom ? Vec_WrdStartRandom(2 * Gia_ManCiNum(p) * w) : Vec_WrdStart(2 * Gia_ManCiNum(p) * w);
1137 Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
1138 Abc_TtClear( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
1139 fFailed = nTotal = 0;
1140 //Vec_IntForEachEntry( vOrder, iOut, k )
1141 //Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes )
1142 Vec_PtrForEachEntry( Vec_Int_t *, vReload, vLevel, i )
1143 {
1144 //if ( fVeryVerbose && i%nMinCexes == 0 )
1145 // printf( "\n" );
1146 if ( Vec_IntSize(vLevel) == 0 )
1147 continue;
1148 iPatUsed = Min_ManBitPackOne( vSimsPi, iPat, w, vLevel );
1149 fFailed += iPatUsed == iPat;
1150 iPat = (iPatUsed + 1) % (64*(w-1) - 1);
1151 //if ( fVeryVerbose )
1152 //printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed );
1153 //if ( fVeryVerbose )
1154 //Vec_IntPrint( vLevel );
1155 nTotal++;
1156 }
1157 if ( fVerbose )
1158 printf( "W = %d (F = %d) ", w, fFailed );
1159// printf( "Failed patterns = %d\n", fFailed );
1160 }
1161 if ( fVerbose )
1162 printf( "Total = %d\n", nTotal );
1163 if ( fVerbose )
1164 {
1165 nBits = Abc_TtCountOnesVec( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
1166 printf( "Bit-packing is using %d words and %d bits. Density =%8.4f %%. ",
1167 Vec_WrdSize(vSimsPi)/Gia_ManCiNum(p), nBits, 100.0*nBits/64/Vec_WrdSize(vSimsPi) );
1168 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1169 }
1170 Vec_IntFreeP( &vOrder );
1171 Vec_PtrFreeP( &vReload );
1172 return vSimsPi;
1173}
1174
1186Vec_Int_t * Patt_ManOutputErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
1187{
1188 Vec_Int_t * vCounts = Vec_IntAlloc( nOuts );
1189 int i, nWords = Vec_WrdSize(vErrors)/nOuts;
1190 assert( Vec_WrdSize(vErrors) == nOuts * nWords );
1191 for ( i = 0; i < nOuts; i++ )
1192 Vec_IntPush( vCounts, Abc_TtCountOnesVec(Vec_WrdEntryP(vErrors, nWords * i), nWords) );
1193 return vCounts;
1194}
1195Vec_Wrd_t * Patt_ManTransposeErrors( Vec_Wrd_t * vErrors, int nOuts )
1196{
1197 extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
1198 int nWordsIn = Vec_WrdSize(vErrors) / nOuts;
1199 int nWordsOut = Abc_Bit6WordNum(nOuts);
1200 Vec_Wrd_t * vSims1 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
1201 Vec_Wrd_t * vSims2 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
1202 assert( Vec_WrdSize(vErrors) == nWordsIn * nOuts );
1203 Abc_TtCopy( Vec_WrdArray(vSims1), Vec_WrdArray(vErrors), Vec_WrdSize(vErrors), 0 );
1204 Extra_BitMatrixTransposeP( vSims1, nWordsIn, vSims2, nWordsOut );
1205 Vec_WrdFree( vSims1 );
1206 return vSims2;
1207}
1208Vec_Int_t * Patt_ManPatternErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
1209{
1210 int nWords = Vec_WrdSize(vErrors)/nOuts;
1211 Vec_Wrd_t * vErrors2 = Patt_ManTransposeErrors( vErrors, nOuts );
1212 Vec_Int_t * vPatErrs = Patt_ManOutputErrorCoverage( vErrors2, 64*nWords );
1213 Vec_WrdFree( vErrors2 );
1214 return vPatErrs;
1215}
1216
1217#define ERR_REPT_SIZE 32
1218void Patt_ManProfileErrors( Vec_Int_t * vOutErrs, Vec_Int_t * vPatErrs )
1219{
1220 int nOuts = Vec_IntSize(vOutErrs);
1221 int nPats = Vec_IntSize(vPatErrs);
1222 int ErrOuts[ERR_REPT_SIZE+1] = {0};
1223 int ErrPats[ERR_REPT_SIZE+1] = {0};
1224 int i, Errs, nErrors1 = 0, nErrors2 = 0;
1225 Vec_IntForEachEntry( vOutErrs, Errs, i )
1226 {
1227 nErrors1 += Errs;
1228 ErrOuts[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
1229 }
1230 Vec_IntForEachEntry( vPatErrs, Errs, i )
1231 {
1232 nErrors2 += Errs;
1233 ErrPats[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
1234 }
1235 assert( nErrors1 == nErrors2 );
1236 // errors/error_outputs/error_patterns
1237 //printf( "\nError statistics:\n" );
1238 printf( "Errors =%6d ", nErrors1 );
1239 printf( "ErrPOs =%5d (Ave = %5.2f) ", nOuts-ErrOuts[0], 1.0*nErrors1/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
1240 printf( "Patterns =%5d (Ave = %5.2f) ", nPats, 1.0*nErrors1/nPats );
1241 printf( "Density =%8.4f %%\n", 100.0*nErrors1/nPats/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
1242 // how many times each output fails
1243 printf( "Outputs: " );
1244 for ( i = 0; i <= ERR_REPT_SIZE; i++ )
1245 if ( ErrOuts[i] )
1246 printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrOuts[i] );
1247 printf( "\n" );
1248 // how many times each patterns fails an output
1249 printf( "Patterns: " );
1250 for ( i = 0; i <= ERR_REPT_SIZE; i++ )
1251 if ( ErrPats[i] )
1252 printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrPats[i] );
1253 printf( "\n" );
1254}
1255int Patt_ManProfileErrorsOne( Vec_Wrd_t * vErrors, int nOuts )
1256{
1257 Vec_Int_t * vCoErrs = Patt_ManOutputErrorCoverage( vErrors, nOuts );
1258 Vec_Int_t * vPatErrs = Patt_ManPatternErrorCoverage( vErrors, nOuts );
1259 Patt_ManProfileErrors( vCoErrs, vPatErrs );
1260 Vec_IntFree( vPatErrs );
1261 Vec_IntFree( vCoErrs );
1262 return 1;
1263}
1264
1265Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p )
1266{
1267 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
1268 int i, Driver;
1269 Gia_ManForEachCoDriverId( p, Driver, i )
1270 if ( Driver > 0 )
1271 Vec_IntPush( vRes, i );
1272 if ( Vec_IntSize(vRes) == 0 )
1273 Vec_IntFreeP( &vRes );
1274 return vRes;
1275}
1276Vec_Wrd_t * Min_ManRemapSims( int nInputs, Vec_Int_t * vMap, Vec_Wrd_t * vSimsPi )
1277{
1278 int i, iObj, nWords = Vec_WrdSize(vSimsPi)/Vec_IntSize(vMap);
1279 Vec_Wrd_t * vSimsNew = Vec_WrdStart( 2 * nInputs * nWords );
1280 //Vec_Wrd_t * vSimsNew = Vec_WrdStartRandom( nInputs * nWords );
1281 //Vec_WrdFillExtra( vSimsNew, 2 * nInputs * nWords, 0 );
1282 assert( Vec_WrdSize(vSimsPi)%Vec_IntSize(vMap) == 0 );
1283 Vec_WrdShrink( vSimsNew, Vec_WrdSize(vSimsNew)/2 );
1284 Vec_IntForEachEntry( vMap, iObj, i )
1285 {
1286 Abc_TtCopy( Vec_WrdArray(vSimsNew) + (iObj-1)*nWords, Vec_WrdArray(vSimsPi) + i*nWords, nWords, 0 );
1287 Abc_TtCopy( Vec_WrdLimit(vSimsNew) + (iObj-1)*nWords, Vec_WrdLimit(vSimsPi) + i*nWords, nWords, 0 );
1288 }
1289 return vSimsNew;
1290}
1291Vec_Wrd_t * Gia_ManCollectSims( Gia_Man_t * pSwp, int nWords, Vec_Int_t * vOuts, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose )
1292{
1293 Vec_Int_t * vStats[3] = {0}; int i, iObj;
1294 Vec_Int_t * vMap = Vec_IntAlloc( 100 );
1295 Gia_Man_t * pSwp2 = Gia_ManDupCones2( pSwp, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vMap );
1296 Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
1297 if ( Vec_IntSum(vStats[2]) == 0 )
1298 {
1299 for ( i = 0; i < 3; i++ )
1300 Vec_IntFree( vStats[i] );
1301 Vec_IntFree( vMap );
1302 Gia_ManStop( pSwp2 );
1303 Vec_WecFree( vCexes );
1304 return NULL;
1305 }
1306 else
1307 {
1308 Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose );
1309 Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 );
1310 Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) );
1311 if ( fVerbose )
1312 Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) );
1313 if ( fVeryVerbose )
1314 {
1315 printf( "Unsolved = %4d ", Vec_IntSize(vOuts) );
1316 Gia_ManPrintStats( pSwp2, NULL );
1317 Vec_IntForEachEntry( vOuts, iObj, i )
1318 {
1319 printf( "%4d : ", i );
1320 printf( "Out = %5d ", Vec_IntEntry(vMap, i) );
1321 printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) );
1322 printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) );
1323 printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) );
1324 printf( "Count = %5d ", Vec_IntEntry(vCounts, i) );
1325 printf( "\n" );
1326 if ( i == 20 )
1327 break;
1328 }
1329 }
1330 for ( i = 0; i < 3; i++ )
1331 Vec_IntFree( vStats[i] );
1332 Vec_IntFree( vCounts );
1333 Vec_WrdFree( vSimsPo );
1334 Vec_WecFree( vCexes );
1335 Gia_ManStop( pSwp2 );
1336 //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) );
1337 vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi );
1338 Vec_WrdFree( vSimsPo );
1339 Vec_IntFree( vMap );
1340 return vSimsPi;
1341 }
1342}
1343Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose )
1344{
1345 abctime clk = Abc_Clock();
1346 extern Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose );
1347 Gia_Man_t * pSwp = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 );
1348 abctime clkSweep = Abc_Clock() - clk;
1349 int nArgs = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n",
1350 nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0;
1351 Vec_Int_t * vOuts = Min_ManGetUnsolved( pSwp );
1352 Vec_Wrd_t * vSimsPi = vOuts ? Gia_ManCollectSims( pSwp, 0, vOuts, nMaxTries, nMinCexes, fUseSim, fUseSat, fVerbose, fVeryVerbose ) : NULL;
1353 if ( vOuts == NULL )
1354 printf( "There is no satisfiable outputs.\n" );
1355 if ( fVerbose )
1356 Abc_PrintTime( 1, "Sweep time", clkSweep );
1357 if ( fVerbose )
1358 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
1359 Vec_IntFreeP( &vOuts );
1360 Gia_ManStop( pSwp );
1361 nArgs = 0;
1362 return vSimsPi;
1363}
1364void Min_ManTest2( Gia_Man_t * p )
1365{
1366 Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 0, 1, 1 );
1367 Vec_WrdFreeP( &vSimsPi );
1368}
1369
1381void Gia_GenerateCexesDumpBlif( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes )
1382{
1383 extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps );
1384 FILE * pFile = fopen( pFileName, "wb" );
1385 if ( pFile == NULL ) {
1386 printf( "Cannot open output file name \"%s\".\n", pFileName );
1387 return;
1388 }
1389 int fFakeIns = 0, fFakeOuts = 0;
1390 if ( p->vNamesIn == NULL )
1391 p->vNamesIn = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ), fFakeIns = 1;
1392 if ( p->vNamesOut == NULL )
1393 p->vNamesOut = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ), fFakeOuts = 1;
1394
1395 Gia_Obj_t * pObj, * pObj2;
1396 char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
1397 int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
1398 fprintf( pFile, "# Satisfying assignments for the primary outputs generated by ABC on %s\n", Gia_TimeStamp() );
1399 fprintf( pFile, ".model %s\n", p->pName );
1400 fprintf( pFile, ".inputs" );
1401 Gia_ManForEachCi( p, pObj, i )
1402 fprintf( pFile, " %s", Gia_ObjCiName(p, i) );
1403 fprintf( pFile, "\n.outputs" );
1404 Gia_ManForEachCo( p, pObj, i )
1405 fprintf( pFile, " %s", Gia_ObjCoName(p, i) );
1406 fprintf( pFile, "\n" );
1407 Gia_ManForEachCo( p, pObj, i ) {
1408 if ( Gia_ObjFaninLit0p(p, pObj) == 0 ) {
1409 fprintf( pFile, ".names %s\n", Gia_ObjCoName(p, i) );
1410 nOuts[0]++;
1411 }
1412 else if ( Gia_ObjFaninLit0p(p, pObj) == 1 ) {
1413 fprintf( pFile, ".names %s\n 1\n", Gia_ObjCiName(p, i) );
1414 nOuts[1]++;
1415 }
1416 else {
1417 fprintf( pFile, ".names" );
1418 Gia_ManForEachCi( p, pObj2, c )
1419 fprintf( pFile, " %s", Gia_ObjCiName(p, c) );
1420 fprintf( pFile, " %s\n", Gia_ObjCoName(p, i) );
1421 for ( c = 0; c < nCexes; c++ ) {
1422 Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
1423 memset(pLine, '-', Gia_ManCiNum(p) );
1424 Vec_IntForEachEntry( vPat, iLit, k )
1425 pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
1426 fprintf( pFile, "%s 1\n", pLine );
1427 }
1428 nOuts[1]++;
1429 }
1430 }
1431 fprintf( pFile, ".end\n\n" );
1432 fclose( pFile );
1433 printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into BLIF file \"%s\".\n",
1434 nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );
1435 free( pLine );
1436
1437 if ( fFakeIns ) Vec_PtrFreeFree( p->vNamesIn ), p->vNamesIn = NULL;
1438 if ( fFakeOuts ) Vec_PtrFreeFree( p->vNamesOut ), p->vNamesOut = NULL;
1439}
1440void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort )
1441{
1442 FILE * pFile = fopen( pFileName, "wb" );
1443 if ( pFile == NULL ) {
1444 printf( "Cannot open output file name \"%s\".\n", pFileName );
1445 return;
1446 }
1447 Gia_Obj_t * pObj;
1448 char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
1449 int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
1450 Gia_ManForEachCo( p, pObj, i ) {
1451 if ( Gia_ObjFaninLit0p(p, Gia_ManCo(p, i)) == 0 ) {
1452 fprintf( pFile, "%d : unsat\n", i );
1453 nOuts[0]++;
1454 }
1455 else if ( fShort ) {
1456 for ( c = 0; c < nCexes; c++ ) {
1457 Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
1458 fprintf( pFile, "%d :", i );
1459 if ( Vec_IntSize(vPat) == 0 )
1460 fprintf( pFile, " not available" );
1461 else
1462 Vec_IntForEachEntry( vPat, iLit, k )
1463 fprintf( pFile, " %d", iLit );
1464 fprintf( pFile, "\n" );
1465 }
1466 nOuts[1]++;
1467 }
1468 else {
1469 for ( c = 0; c < nCexes; c++ ) {
1470 Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
1471 memset(pLine, '-', Gia_ManCiNum(p) );
1472 Vec_IntForEachEntry( vPat, iLit, k )
1473 pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
1474 fprintf( pFile, "%d : %s\n", i, pLine );
1475 }
1476 nOuts[1]++;
1477 }
1478 }
1479 printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into file \"%s\".\n",
1480 nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );
1481 fclose( pFile );
1482 free( pLine );
1483}
1484void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose )
1485{
1486 unsigned Start = Abc_Random(1);
1487 Vec_Int_t * vStats[3] = {0}; int i;
1488 Vec_Wec_t * vCexes = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
1489 assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes );
1490 if ( fBlif )
1491 Gia_GenerateCexesDumpBlif( pFileName, p, vCexes );
1492 else
1493 Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
1494 for ( i = 0; i < 3; i++ )
1495 Vec_IntFreeP( &vStats[i] );
1496 Vec_WecFree( vCexes );
1497 Start = 0;
1498}
1499
1503
1504
1505ABC_NAMESPACE_IMPL_END
1506
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Abc_Random
unsigned Abc_Random(int fReset)
Definition utilSort.c:1004
Abc_MergeSortCost2Reverse
void Abc_MergeSortCost2Reverse(int *pInput, int nSize, int *pCost)
Definition utilSort.c:333
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
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
l_True
#define l_True
Definition bmcBmcS.c:35
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
Cec4_ManSimulateTest4
Gia_Man_t * Cec4_ManSimulateTest4(Gia_Man_t *p, int nBTLimit, int nBTLimitPo, int fVerbose)
Definition cecSatG2.c:2087
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
p
Cube * p
Definition exorList.c:222
Extra_BitMatrixTransposeP
ABC_NAMESPACE_IMPL_START void Extra_BitMatrixTransposeP(Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
DECLARATIONS ///.
Definition extraUtilMisc.c:2652
Patt_ManProfileErrors
void Patt_ManProfileErrors(Vec_Int_t *vOutErrs, Vec_Int_t *vPatErrs)
Definition giaPat2.c:1218
Min_ManBitPackOne
int Min_ManBitPackOne(Vec_Wrd_t *vSimsPi, int iPat0, int nWords, Vec_Int_t *vLits)
Definition giaPat2.c:1089
Min_ManGetUnsolved
Vec_Int_t * Min_ManGetUnsolved(Gia_Man_t *p)
Definition giaPat2.c:1265
ERR_REPT_SIZE
#define ERR_REPT_SIZE
Definition giaPat2.c:1217
Min_ManFromGia
Min_Man_t * Min_ManFromGia(Gia_Man_t *p, Vec_Int_t *vOuts)
Definition giaPat2.c:197
Min_Man_t
typedefABC_NAMESPACE_IMPL_START struct Min_Man_t_ Min_Man_t
DECLARATIONS ///.
Definition giaPat2.c:34
Min_ReloadCexes
Vec_Ptr_t * Min_ReloadCexes(Vec_Wec_t *vCexes, int nMinCexes)
Definition giaPat2.c:1097
Min_ManBitPackTry
int Min_ManBitPackTry(Vec_Wrd_t *vSimsPi, int nWords, int iPat, Vec_Int_t *vLits)
Definition giaPat2.c:1067
Min_LitVerify
char Min_LitVerify(Min_Man_t *p, int iLit, Vec_Int_t *vLits)
Definition giaPat2.c:293
Min_ManTest3
void Min_ManTest3(Gia_Man_t *p, Vec_Int_t *vCoErrs)
Definition giaPat2.c:771
Min_LitMinimize
void Min_LitMinimize(Min_Man_t *p, int iLit, Vec_Int_t *vLits)
Definition giaPat2.c:307
Patt_ManOutputErrorCoverage
Vec_Int_t * Patt_ManOutputErrorCoverage(Vec_Wrd_t *vErrors, int nOuts)
Definition giaPat2.c:1186
Min_LitJustify_rec
int Min_LitJustify_rec(Min_Man_t *p, int iLit)
Definition giaPat2.c:536
Min_ManRemapSims
Vec_Wrd_t * Min_ManRemapSims(int nInputs, Vec_Int_t *vMap, Vec_Wrd_t *vSimsPi)
Definition giaPat2.c:1276
Gia_ManDupCones2_rec
void Gia_ManDupCones2_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaPat2.c:820
Gia_ManDupCones2CollectPis_rec
void Gia_ManDupCones2CollectPis_rec(Gia_Man_t *p, int iObj, Vec_Int_t *vMap)
Definition giaPat2.c:805
Min_ManCollect
Vec_Wrd_t * Min_ManCollect(Gia_Man_t *p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose)
Definition giaPat2.c:1343
Gia_ManCollectSims
Vec_Wrd_t * Gia_ManCollectSims(Gia_Man_t *pSwp, int nWords, Vec_Int_t *vOuts, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose)
Definition giaPat2.c:1291
Gia_GenerateCexes
void Gia_GenerateCexes(char *pFileName, Gia_Man_t *p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose)
Definition giaPat2.c:1484
Min_ManAccumulate
int Min_ManAccumulate(Vec_Wec_t *vCexes, int iFirst, int iLimit, Vec_Int_t *vCex)
Definition giaPat2.c:875
Min_LitIsImplied_rec
char Min_LitIsImplied_rec(Min_Man_t *p, int iLit, int Depth)
Definition giaPat2.c:505
Min_LitJustify
int Min_LitJustify(Min_Man_t *p, int iLit)
Definition giaPat2.c:626
Gia_ManDupCones2
Gia_Man_t * Gia_ManDupCones2(Gia_Man_t *p, int *pOuts, int nOuts, Vec_Int_t *vMap)
Definition giaPat2.c:829
Min_ManFromGia_rec
void Min_ManFromGia_rec(Min_Man_t *pNew, Gia_Man_t *p, int iObj)
Definition giaPat2.c:185
Min_ManTest2
void Min_ManTest2(Gia_Man_t *p)
Definition giaPat2.c:1364
Gia_GenerateCexesDumpBlif
void Gia_GenerateCexesDumpBlif(char *pFileName, Gia_Man_t *p, Vec_Wec_t *vCexes)
Definition giaPat2.c:1381
Patt_ManPatternErrorCoverage
Vec_Int_t * Patt_ManPatternErrorCoverage(Vec_Wrd_t *vErrors, int nOuts)
Definition giaPat2.c:1208
Min_ManForEachCo
#define Min_ManForEachCo(p, i)
Definition giaPat2.c:105
Gia_GenerateCexesDumpFile
void Gia_GenerateCexesDumpFile(char *pFileName, Gia_Man_t *p, Vec_Wec_t *vCexes, int fShort)
Definition giaPat2.c:1440
Patt_ManProfileErrorsOne
int Patt_ManProfileErrorsOne(Vec_Wrd_t *vErrors, int nOuts)
Definition giaPat2.c:1255
Patt_ManTransposeErrors
Vec_Wrd_t * Patt_ManTransposeErrors(Vec_Wrd_t *vErrors, int nOuts)
Definition giaPat2.c:1195
Min_ManBitPack
Vec_Wrd_t * Min_ManBitPack(Gia_Man_t *p, int nWords0, Vec_Wec_t *vCexes, int fRandom, int nMinCexes, Vec_Int_t *vScores, int fVerbose)
Definition giaPat2.c:1111
Min_LitVerify_rec
char Min_LitVerify_rec(Min_Man_t *p, int iLit)
Definition giaPat2.c:268
Min_ManComputeCexes
Vec_Wec_t * Min_ManComputeCexes(Gia_Man_t *p, Vec_Int_t *vOuts0, int nMaxTries, int nMinCexes, Vec_Int_t *vStats[3], int fUseSim, int fUseSat, int fVerbose)
Definition giaPat2.c:901
Min_ManCountSize
int Min_ManCountSize(Vec_Wec_t *vCexes, int iFirst, int iLimit)
Definition giaPat2.c:894
Min_ManRemoveItem
int Min_ManRemoveItem(Vec_Wec_t *vCexes, int iItem, int iFirst, int iLimit)
Definition giaPat2.c:862
Min_ManTest4
void Min_ManTest4(Gia_Man_t *p)
Definition giaPat2.c:786
Min_TargGenerateCexes
Vec_Int_t * Min_TargGenerateCexes(Min_Man_t *p, Vec_Int_t *vCoErrs, int nCexes, int nCexesStop, int *pnComputed, int fVerbose)
Definition giaPat2.c:662
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManSimPatSimOut
Vec_Wrd_t * Gia_ManSimPatSimOut(Gia_Man_t *pGia, Vec_Wrd_t *vSimsPi, int fOuts)
Definition giaSimBase.c:138
Gia_ManDupMuxes
Gia_Man_t * Gia_ManDupMuxes(Gia_Man_t *p, int Limit)
Definition giaMuxes.c:98
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachCoVec
#define Gia_ManForEachCoVec(vVec, p, pObj, i)
Definition gia.h:1238
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition giaMan.c:224
Gia_ManForEachCoDriverId
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
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_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_TimeStamp
char * Gia_TimeStamp()
Definition giaUtil.c:106
Gia_ManAigSyn2
Gia_Man_t * Gia_ManAigSyn2(Gia_Man_t *p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose)
Definition giaScript.c:69
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
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_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_GetFakeNames
Vec_Ptr_t * Gia_GetFakeNames(int nNames, int fCaps)
Definition giaUtil.c:154
Mf_ManGenerateCnf
void * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
Definition giaMf.c:1877
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Min_Man_t_
Definition giaPat2.c:36
Min_Man_t_::vVis
Vec_Int_t vVis
Definition giaPat2.c:44
Min_Man_t_::vValsL
Vec_Str_t vValsL
Definition giaPat2.c:43
Min_Man_t_::FirstCoLit
int FirstCoLit
Definition giaPat2.c:40
Min_Man_t_::vFans
Vec_Int_t vFans
Definition giaPat2.c:41
Min_Man_t_::vPat
Vec_Int_t vPat
Definition giaPat2.c:45
Min_Man_t_::vValsN
Vec_Str_t vValsN
Definition giaPat2.c:42
Min_Man_t_::FirstAndLit
int FirstAndLit
Definition giaPat2.c:39
Min_Man_t_::nCis
int nCis
Definition giaPat2.c:37
Min_Man_t_::nCos
int nCos
Definition giaPat2.c:38
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
free
VOID_HACK free()
Hsh_VecMan_t
struct Hsh_VecMan_t_ Hsh_VecMan_t
Definition vecHsh.h:85
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition vecInt.h:62
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_StrForEachEntry
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecStr.h:54
Vec_WecForEachLevelReverseStartStop
#define Vec_WecForEachLevelReverseStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecWec.h:67
Vec_WecForEachLevelStartStop
#define Vec_WecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecWec.h:63
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