/**CFile**************************************************************** FileName [giaPat2.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Pattern generation.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaPat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" #include "misc/vec/vecHsh.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Min_Man_t_ Min_Man_t; struct Min_Man_t_ { int nCis; int nCos; int FirstAndLit; int FirstCoLit; Vec_Int_t vFans; Vec_Str_t vValsN; Vec_Str_t vValsL; Vec_Int_t vVis; Vec_Int_t vPat; }; static inline int Min_ManCiNum( Min_Man_t * p ) { return p->nCis; } static inline int Min_ManCoNum( Min_Man_t * p ) { return p->nCos; } static inline int Min_ManObjNum( Min_Man_t * p ) { return Vec_IntSize(&p->vFans) >> 1; } static inline int Min_ManAndNum( Min_Man_t * p ) { return Min_ManObjNum(p) - p->nCis - p->nCos - 1; } static inline int Min_ManCi( Min_Man_t * p, int i ) { return 1 + i; } static inline int Min_ManCo( Min_Man_t * p, int i ) { return Min_ManObjNum(p) - Min_ManCoNum(p) + i; } static inline int Min_ObjIsCi( Min_Man_t * p, int i ) { return i > 0 && i <= Min_ManCiNum(p); } static inline int Min_ObjIsNode( Min_Man_t * p, int i ) { return i > Min_ManCiNum(p) && i < Min_ManObjNum(p) - Min_ManCoNum(p); } static 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); } static 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); } static 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); } static inline int Min_ObjIsCo( Min_Man_t * p, int i ) { return i >= Min_ManObjNum(p) - Min_ManCoNum(p) && i < Min_ManObjNum(p); } static inline int Min_ObjLit( Min_Man_t * p, int i, int n ) { return Vec_IntEntry(&p->vFans, i + i + n); } static inline int Min_ObjLit0( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 0); } static inline int Min_ObjLit1( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 1); } static inline int Min_ObjCioId( Min_Man_t * p, int i ) { assert( i && !Min_ObjIsNode(p, i) ); return Min_ObjLit1(p, i); } static inline int Min_ObjFan0( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit0(p, i) ); } static inline int Min_ObjFan1( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit1(p, i) ); } static inline int Min_ObjFanC0( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit0(p, i) ); } static inline int Min_ObjFanC1( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit1(p, i) ); } static inline char Min_ObjValN( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsN, i); } static inline void Min_ObjSetValN( Min_Man_t * p, int i, char v ){ Vec_StrWriteEntry(&p->vValsN, i, v); } static inline char Min_LitValL( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsL, i); } static 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)); } static inline void Min_ObjCleanValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] = 0x0202; } static inline void Min_ObjMarkValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0404; } static inline void Min_ObjMark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0808; } static inline void Min_ObjUnmark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] &= 0xF7F7; } static inline int Min_LitIsCi( Min_Man_t * p, int v ) { return v > 1 && v < p->FirstAndLit; } static inline int Min_LitIsNode( Min_Man_t * p, int v ) { return v >= p->FirstAndLit && v < p->FirstCoLit; } static inline int Min_LitIsCo( Min_Man_t * p, int v ) { return v >= p->FirstCoLit; } static inline int Min_LitIsAnd( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 < v1); } static inline int Min_LitIsXor( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 > v1); } static inline int Min_LitIsBuf( int v, int v0, int v1 ) { return v0 == v1; } static inline int Min_LitFan( Min_Man_t * p, int v ) { return Vec_IntEntry(&p->vFans, v); } static inline int Min_LitFanC( Min_Man_t * p, int v ) { return Abc_LitIsCompl( Min_LitFan(p, v) ); } static 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); } static 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); } static 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; } static 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); } #define Min_ManForEachObj( p, i ) \ for ( i = 0; i < Min_ManObjNum(p); i++ ) #define Min_ManForEachCi( p, i ) \ for ( i = 1; i <= Min_ManCiNum(p); i++ ) #define Min_ManForEachCo( p, i ) \ for ( i = Min_ManObjNum(p) - Min_ManCoNum(p); i < Min_ManObjNum(p); i++ ) #define Min_ManForEachAnd( p, i ) \ for ( i = 1 + Min_ManCiNum(p); i < Min_ManObjNum(p) - Min_ManCoNum(p); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Min_Man_t * Min_ManStart( int nObjMax ) { Min_Man_t * p = ABC_CALLOC( Min_Man_t, 1 ); Vec_IntGrow( &p->vFans, nObjMax ); Vec_IntPushTwo( &p->vFans, -1, -1 ); return p; } static inline void Min_ManStop( Min_Man_t * p ) { Vec_IntErase( &p->vFans ); Vec_StrErase( &p->vValsN ); Vec_StrErase( &p->vValsL ); Vec_IntErase( &p->vVis ); Vec_IntErase( &p->vPat ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Min_ManAppendObj( Min_Man_t * p, int iLit0, int iLit1 ) { int iLit = Vec_IntSize(&p->vFans); Vec_IntPushTwo( &p->vFans, iLit0, iLit1 ); return iLit; } static inline int Min_ManAppendCi( Min_Man_t * p ) { p->nCis++; p->FirstAndLit = Vec_IntSize(&p->vFans) + 2; return Min_ManAppendObj( p, 0, p->nCis-1 ); } static inline int Min_ManAppendCo( Min_Man_t * p, int iLit0 ) { p->nCos++; if ( p->FirstCoLit == 0 ) p->FirstCoLit = Vec_IntSize(&p->vFans); return Min_ManAppendObj( p, iLit0, p->nCos-1 ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Min_ManFromGia_rec( Min_Man_t * pNew, Gia_Man_t * p, int iObj ) { Gia_Obj_t * pObj = Gia_ManObj(p, iObj); if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj) ); Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj) ); pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts ) { Gia_Obj_t * pObj; int i; Min_Man_t * pNew = Min_ManStart( Gia_ManObjNum(p) ); Gia_ManFillValue(p); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Min_ManAppendCi( pNew ); if ( vOuts == NULL ) { Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFaninLit0p(p, pObj) ); } else { Gia_ManForEachCoVec( vOuts, p, pObj, i ) Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0p(p, pObj) ); Gia_ManForEachCoVec( vOuts, p, pObj, i ) Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } return pNew; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline char Min_XsimNot( char Val ) { if ( Val < 2 ) return Val ^ 1; return 2; } static inline char Min_XsimXor( char Val0, char Val1 ) { if ( Val0 < 2 && Val1 < 2 ) return Val0 ^ Val1; return 2; } static inline char Min_XsimAnd( char Val0, char Val1 ) { if ( Val0 == 0 || Val1 == 0 ) return 0; if ( Val0 == 1 && Val1 == 1 ) return 1; return 2; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ char Min_LitVerify_rec( Min_Man_t * p, int iLit ) { char Val = Min_LitValL(p, iLit); if ( Val == 2 && Min_LitIsNode(p, iLit) ) // unassigned { int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitVerify_rec( p, iLit0 ); char Val1 = Min_LitVerify_rec( p, iLit1 ); assert( Val0 < 3 && Val1 < 3 ); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } else Vec_IntPush( &p->vVis, Abc_Lit2Var(iLit) ); Min_ObjMark2ValL( p, Abc_Lit2Var(iLit) ); } return Val&3; } char Min_LitVerify( Min_Man_t * p, int iLit, Vec_Int_t * vLits ) { int i, Entry; char Res; if ( iLit < 2 ) return 1; assert( !Min_LitIsCo(p, iLit) ); //assert( Min_ManCheckCleanValsL(p) ); assert( Vec_IntSize(&p->vVis) == 0 ); Vec_IntForEachEntry( vLits, Entry, i ) Min_LitSetValL( p, Entry, 1 ); // ms notation Res = Min_LitVerify_rec( p, iLit ); Min_ManCleanVisitedValL( p ); return Res; } void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits ) { int i, iObj, iTemp; char Res; Vec_IntClear( &p->vPat ); if ( iLit < 2 ) return; assert( !Min_LitIsCo(p, iLit) ); //assert( Min_ManCheckCleanValsL(p) ); assert( Vec_IntSize(&p->vVis) == 0 ); Vec_IntForEachEntry( vLits, iTemp, i ) Min_LitSetValL( p, iTemp, 1 ); // ms notation Res = Min_LitVerify_rec( p, iLit ); assert( Res == 1 ); Min_ObjMarkValL( p, Abc_Lit2Var(iLit) ); Vec_IntForEachEntryReverse( &p->vVis, iObj, i ) { int iLit = Abc_Var2Lit( iObj, 0 ); int Value = 7 & Min_LitValL(p, iLit); if ( Value >= 4 ) { if ( Min_LitIsCi(p, iLit) ) Vec_IntPush( &p->vPat, Abc_LitNotCond(iLit, !(Value&1)) ); else { int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL( p, iLit0 ); char Val1 = Min_LitValL( p, iLit1 ); if ( Value&1 ) // value == 1 { assert( (Val0&1) && (Val1&1) ); Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) ); Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) ); } else // value == 0 { int Zero0 = !(Val0&3); int Zero1 = !(Val1&3); assert( Zero0 || Zero1 ); if ( Zero0 && !Zero1 ) Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) ); else if ( !Zero0 && Zero1 ) Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) ); else if ( Val0 == 4 && Val1 != 4 ) Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) ); else if ( Val1 == 4 && Val0 != 4 ) Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) ); else if ( Abc_Random(0) & 1 ) Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) ); else Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) ); } } } Min_ObjCleanValL( p, Abc_Lit2Var(iLit) ); } Vec_IntClear( &p->vVis ); //Min_ManCleanVisitedValL( p ); //assert( Min_LitVerify(p, iLit, &p->vPat) == 1 ); assert( Vec_IntSize(&p->vPat) <= Vec_IntSize(vLits) ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline char Min_LitIsImplied1( Min_Man_t * p, int iLit ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } static inline char Min_LitIsImplied2( Min_Man_t * p, int iLit ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) Val0 = Min_LitIsImplied1(p, iLit0); if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) Val1 = Min_LitIsImplied1(p, iLit1); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } static inline char Min_LitIsImplied3( Min_Man_t * p, int iLit ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) Val0 = Min_LitIsImplied2(p, iLit0); if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) Val1 = Min_LitIsImplied2(p, iLit1); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } static inline char Min_LitIsImplied4( Min_Man_t * p, int iLit ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) Val0 = Min_LitIsImplied3(p, iLit0); if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) Val1 = Min_LitIsImplied3(p, iLit1); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } static inline char Min_LitIsImplied5( Min_Man_t * p, int iLit ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) Val0 = Min_LitIsImplied4(p, iLit0); if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) Val1 = Min_LitIsImplied4(p, iLit1); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } // this recursive procedure is about 10% slower char Min_LitIsImplied_rec( Min_Man_t * p, int iLit, int Depth ) { char Val = 2; int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); assert( Depth > 0 ); assert( Min_LitIsNode(p, iLit) ); // internal node assert( Min_LitValL(p, iLit) == 2 ); // unassigned if ( Depth > 1 && Val0 == 2 && Min_LitIsNode(p, iLit0) ) { Val0 = Min_LitIsImplied_rec(p, iLit0, Depth-1); Val1 = Min_LitValL(p, iLit1); } if ( Depth > 1 && Val1 == 2 && Min_LitIsNode(p, iLit1) ) { Val1 = Min_LitIsImplied_rec(p, iLit1, Depth-1); Val0 = Min_LitValL(p, iLit0); } if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else Val = Min_XsimAnd( Val0, Val1 ); if ( Val < 2 ) { Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } return Val; } int Min_LitJustify_rec( Min_Man_t * p, int iLit ) { int Res = 1, LitValue = !Abc_LitIsCompl(iLit); int Val = (int)Min_LitValL(p, iLit); if ( Val < 2 ) // assigned return Val == LitValue; // unassigned if ( Min_LitIsCi(p, iLit) ) Vec_IntPush( &p->vPat, iLit ); // ms notation else { int iLit0 = Min_LitFan(p, iLit); int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL(p, iLit0); char Val1 = Min_LitValL(p, iLit1); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) { if ( Val0 < 2 && Val1 < 2 ) Res = LitValue == (Val0 ^ Val1); else if ( Val0 < 2 ) Res = Min_LitJustify_rec(p, iLit1^Val0^!LitValue); else if ( Val1 < 2 ) Res = Min_LitJustify_rec(p, iLit0^Val1^!LitValue); else if ( Abc_Random(0) & 1 ) Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1^ LitValue); else Res = Min_LitJustify_rec(p, iLit0^1) && Min_LitJustify_rec(p, iLit1^!LitValue); assert( !Res || LitValue == Min_XsimXor(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) ); } else if ( LitValue ) // value 1 { if ( Val0 == 0 || Val1 == 0 ) Res = 0; else if ( Val0 == 1 && Val1 == 1 ) Res = 1; else if ( Val0 == 1 ) Res = Min_LitJustify_rec(p, iLit1); else if ( Val1 == 1 ) Res = Min_LitJustify_rec(p, iLit0); else Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1); assert( !Res || 1 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) ); } else // value 0 { /* int Depth = 3; if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) { Val0 = Min_LitIsImplied_rec(p, iLit0, Depth); Val1 = Min_LitValL(p, iLit1); } if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) { Val1 = Min_LitIsImplied_rec(p, iLit1, Depth); Val0 = Min_LitValL(p, iLit0); } */ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) ) { Val0 = Min_LitIsImplied3(p, iLit0); Val1 = Min_LitValL(p, iLit1); } if ( Val1 == 2 && Min_LitIsNode(p, iLit1) ) { Val1 = Min_LitIsImplied3(p, iLit1); Val0 = Min_LitValL(p, iLit0); } if ( Val0 == 0 || Val1 == 0 ) Res = 1; else if ( Val0 == 1 && Val1 == 1 ) Res = 0; else if ( Val0 == 1 ) Res = Min_LitJustify_rec(p, iLit1^1); else if ( Val1 == 1 ) Res = Min_LitJustify_rec(p, iLit0^1); else if ( Abc_Random(0) & 1 ) //else if ( (p->Random >> (iLit & 0x1F)) & 1 ) Res = Min_LitJustify_rec(p, iLit0^1); else Res = Min_LitJustify_rec(p, iLit1^1); //Val0 = Min_LitValL(p, iLit0); //Val1 = Min_LitValL(p, iLit1); assert( !Res || 0 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) ); } } if ( Res ) Min_LitSetValL( p, iLit, 1 ); return Res; } int Min_LitJustify( Min_Man_t * p, int iLit ) { int Res, fCheck = 0; Vec_IntClear( &p->vPat ); if ( iLit < 2 ) return 1; assert( !Min_LitIsCo(p, iLit) ); //assert( Min_ManCheckCleanValsL(p) ); assert( Vec_IntSize(&p->vVis) == 0 ); //p->Random = Abc_Random(0); Res = Min_LitJustify_rec( p, iLit ); Min_ManCleanVisitedValL( p ); if ( Res ) { if ( fCheck && Min_LitVerify(p, iLit, &p->vPat) != 1 ) printf( "Verification FAILED for literal %d.\n", iLit ); //else // printf( "Verification succeeded for literal %d.\n", iLit ); } //else // printf( "Could not justify literal %d.\n", iLit ); return Res; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Min_TargGenerateCexes( Min_Man_t * p, Vec_Int_t * vCoErrs, int nCexes, int nCexesStop, int * pnComputed, int fVerbose ) { abctime clk = Abc_Clock(); int t, iObj, Count = 0, CountPos = 0, CountPosSat = 0, nRuns[2] = {0}, nCountCexes[2] = {0}; Vec_Int_t * vPats = Vec_IntAlloc( 1000 ); Vec_Int_t * vPatBest = Vec_IntAlloc( Min_ManCiNum(p) ); Hsh_VecMan_t * pHash = Hsh_VecManStart( 10000 ); Min_ManForEachCo( p, iObj ) if ( Min_ObjLit0(p, iObj) > 1 ) { int nCexesGenSim0 = 0; int nCexesGenSim = 0; int nCexesGenSat = 0; if ( vCoErrs && Vec_IntEntry(vCoErrs, Min_ObjCioId(p, iObj)) >= nCexesStop ) continue; //printf( "%d ", i ); for ( t = 0; t < nCexes; t++ ) { nRuns[0]++; if ( Min_LitJustify( p, Min_ObjLit0(p, iObj) ) ) { int Before, After; assert( Vec_IntSize(&p->vPat) > 0 ); //printf( "%d ", Vec_IntSize(vPat) ); Vec_IntClear( vPatBest ); if ( 1 ) // no minimization Vec_IntAppend( vPatBest, &p->vPat ); else { /* for ( k = 0; k < 10; k++ ) { Vec_IntClear( vPat2 ); Gia_ManIncrementTravId( p ); Cexes_MinimizePattern_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), vPat2 ); assert( Vec_IntSize(vPat2) <= Vec_IntSize(vPat) ); if ( Vec_IntSize(vPatBest) == 0 || Vec_IntSize(vPatBest) > Vec_IntSize(vPat2) ) { Vec_IntClear( vPatBest ); Vec_IntAppend( vPatBest, vPat2 ); } //printf( "%d ", Vec_IntSize(vPat2) ); } */ } //Gia_CexVerify( p, Gia_ObjFaninId0p(p, pObj), !Gia_ObjFaninC0(pObj), vPatBest ); //printf( "\n" ); Before = Hsh_VecSize( pHash ); Vec_IntSort( vPatBest, 0 ); Hsh_VecManAdd( pHash, vPatBest ); After = Hsh_VecSize( pHash ); if ( Before != After ) { Vec_IntPush( vPats, Min_ObjCioId(p, iObj) ); Vec_IntPush( vPats, Vec_IntSize(vPatBest) ); Vec_IntAppend( vPats, vPatBest ); nCexesGenSim++; } nCexesGenSim0++; if ( nCexesGenSim0 > nCexesGenSim*10 ) { printf( "**** Skipping output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) ); break; } } if ( nCexesGenSim == nCexesStop ) break; } //printf( "(%d %d) ", nCexesGenSim0, nCexesGenSim ); //printf( "%d ", t/nCexesGenSim ); //printf( "The number of CEXes = %d\n", nCexesGen ); //if ( fVerbose ) // printf( "%d ", nCexesGen ); nCountCexes[0] += nCexesGenSim; nCountCexes[1] += nCexesGenSat; Count += nCexesGenSim + nCexesGenSat; CountPos++; if ( nCexesGenSim0 == 0 && t == nCexes ) printf( "#### Output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) ); } //printf( "\n" ); if ( fVerbose ) printf( "\n" ); if ( fVerbose ) printf( "Got %d unique CEXes using %d sim (%d) and %d SAT (%d) runs (ave size %.1f). PO = %d ErrPO = %d SatPO = %d ", Count, nRuns[0], nCountCexes[0], nRuns[1], nCountCexes[1], 1.0*Vec_IntSize(vPats)/Abc_MaxInt(1, Count)-2, Min_ManCoNum(p), CountPos, CountPosSat ); if ( fVerbose ) Abc_PrintTime( 0, "Time", Abc_Clock() - clk ); Hsh_VecManStop( pHash ); Vec_IntFree( vPatBest ); *pnComputed = Count; return vPats; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Min_ManTest3( Gia_Man_t * p, Vec_Int_t * vCoErrs ) { int fXor = 0; int nComputed; Vec_Int_t * vPats; Gia_Man_t * pXor = fXor ? Gia_ManDupMuxes(p, 1) : NULL; Min_Man_t * pNew = Min_ManFromGia( fXor ? pXor : p, NULL ); Gia_ManStopP( &pXor ); Min_ManStartValsL( pNew ); //Vec_IntFill( vCoErrs, Vec_IntSize(vCoErrs), 0 ); //vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 ); vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 ); Vec_IntFree( vPats ); Min_ManStop( pNew ); } void Min_ManTest4( Gia_Man_t * p ) { Vec_Int_t * vCoErrs = Vec_IntStartNatural( Gia_ManCoNum(p) ); Min_ManTest3(p, vCoErrs); Vec_IntFree( vCoErrs ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManDupCones2CollectPis_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vMap ) { Gia_Obj_t * pObj; if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) ) return; pObj = Gia_ManObj( p, iObj ); if ( Gia_ObjIsAnd(pObj) ) { Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId0(pObj, iObj), vMap ); Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId1(pObj, iObj), vMap ); } else if ( Gia_ObjIsCi(pObj) ) Vec_IntPush( vMap, iObj ); else assert( 0 ); } void Gia_ManDupCones2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsCi(pObj) || Gia_ObjUpdateTravIdCurrent(p, pObj) ) return; assert( Gia_ObjIsAnd(pObj) ); Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } Gia_Man_t * Gia_ManDupCones2( Gia_Man_t * p, int * pOuts, int nOuts, Vec_Int_t * vMap ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; Vec_IntClear( vMap ); Gia_ManIncrementTravId( p ); for ( i = 0; i < nOuts; i++ ) Gia_ManDupCones2CollectPis_rec( p, Gia_ManCoDriverId(p, pOuts[i]), vMap ); pNew = Gia_ManStart( 1000 ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObjVec( vMap, p, pObj, i ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManIncrementTravId( p ); for ( i = 0; i < nOuts; i++ ) Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(Gia_ManCo(p, pOuts[i])) ); for ( i = 0; i < nOuts; i++ ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, pOuts[i])) ); return pNew; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Min_ManRemoveItem( Vec_Wec_t * vCexes, int iItem, int iFirst, int iLimit ) { Vec_Int_t * vLevel, * vLevel0 = Vec_WecEntry(vCexes, iItem); int i; assert( iFirst <= iItem && iItem < iLimit ); Vec_WecForEachLevelReverseStartStop( vCexes, vLevel, i, iLimit, iFirst ) if ( Vec_IntSize(vLevel) > 0 ) break; assert( iFirst <= i && iItem <= i ); Vec_IntClear( vLevel0 ); if ( iItem < i ) ABC_SWAP( Vec_Int_t, *vLevel0, *vLevel ); return -1; } int Min_ManAccumulate( Vec_Wec_t * vCexes, int iFirst, int iLimit, Vec_Int_t * vCex ) { Vec_Int_t * vLevel; int i, nCommon, nDiff = 0; Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit ) { if ( Vec_IntSize(vLevel) == 0 ) { Vec_IntAppend(vLevel, vCex); return nDiff+1; } nCommon = Vec_IntTwoCountCommon( vLevel, vCex ); if ( nCommon == Vec_IntSize(vLevel) ) // ignore vCex return nDiff; if ( nCommon == Vec_IntSize(vCex) ) // remove vLevel nDiff += Min_ManRemoveItem( vCexes, i, iFirst, iLimit ); } assert( 0 ); return ABC_INFINITY; } int Min_ManCountSize( Vec_Wec_t * vCexes, int iFirst, int iLimit ) { Vec_Int_t * vLevel; int i, nTotal = 0; Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit ) nTotal += Vec_IntSize(vLevel) > 0; return nTotal; } 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 ) { int fUseSynthesis = 1; abctime clkSim = Abc_Clock(), clkSat = Abc_Clock(); Vec_Int_t * vOuts = vOuts0 ? vOuts0 : Vec_IntStartNatural( Gia_ManCoNum(p) ); Min_Man_t * pNew = Min_ManFromGia( p, vOuts ); Vec_Wec_t * vCexes = Vec_WecStart( Vec_IntSize(vOuts) * nMinCexes ); Vec_Int_t * vPatBest = Vec_IntAlloc( 100 ); Vec_Int_t * vLits = Vec_IntAlloc( 100 ); Gia_Obj_t * pObj; int i, iObj, nOuts = 0, nSimOuts = 0, nSatOuts = 0; vStats[0] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // total calls vStats[1] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // successful calls + SAT runs vStats[2] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // results Min_ManStartValsL( pNew ); Min_ManForEachCo( pNew, iObj ) { int nAllCalls = 0; int nGoodCalls = 0; int nCurrCexes = 0; if ( fUseSim && Min_ObjLit0(pNew, iObj) >= 2 ) { while ( nAllCalls++ < nMaxTries ) { if ( Min_LitJustify( pNew, Min_ObjLit0(pNew, iObj) ) ) { Vec_IntClearAppend( vLits, &pNew->vPat ); Vec_IntClearAppend( vPatBest, &pNew->vPat ); if ( 1 ) // minimization { //printf( "%d -> ", Vec_IntSize(vPatBest) ); for ( i = 0; i < 20; i++ ) { Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits ); if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) ) Vec_IntClearAppend( vPatBest, &pNew->vPat ); } //printf( "%d ", Vec_IntSize(vPatBest) ); } assert( Vec_IntSize(vPatBest) > 0 ); Vec_IntSort( vPatBest, 0 ); nCurrCexes += Min_ManAccumulate( vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes, vPatBest ); nGoodCalls++; } if ( nCurrCexes == nMinCexes || nGoodCalls > 10*nCurrCexes ) break; } nSimOuts++; } assert( nCurrCexes <= nMinCexes ); assert( nCurrCexes == Min_ManCountSize(vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes) ); Vec_IntPush( vStats[0], nAllCalls ); Vec_IntPush( vStats[1], nGoodCalls ); Vec_IntPush( vStats[2], nCurrCexes ); nOuts++; } assert( Vec_IntSize(vOuts) == nOuts ); assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[0]) ); assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[1]) ); assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[2]) ); clkSim = Abc_Clock() - clkSim; if ( fUseSat ) Gia_ManForEachCoVec( vOuts, p, pObj, i ) { if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) ) continue; { abctime clk = Abc_Clock(); int iObj = Min_ManCo(pNew, i); int Index = Gia_ObjCioId(pObj); Vec_Int_t * vMap = Vec_IntAlloc( 100 ); Gia_Man_t * pCon = Gia_ManDupCones2( p, &Index, 1, vMap ); Gia_Man_t * pCon1= fUseSynthesis ? Gia_ManAigSyn2( pCon, 0, 1, 0, 100, 0, 0, 0 ) : NULL; Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( fUseSynthesis ? pCon1 : pCon, 8, 0, 0, 0, 0 ); sat_solver* pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); int Lit = Abc_Var2Lit( 1, 0 ); int status = sat_solver_addclause( pSat, &Lit, &Lit+1 ); int nAllCalls = 0; int nCurrCexes = Vec_IntEntry(vStats[2], i); //Gia_AigerWrite( pCon, "temp_miter.aig", 0, 0, 0 ); if ( status == l_True ) { nSatOuts++; //printf( "Running SAT for output %d\n", i ); if ( Min_ObjLit0(pNew, iObj) >= 2 ) { while ( nAllCalls++ < 100 ) { int v, iVar = pCnf->nVars - Gia_ManPiNum(pCon), nVars = Gia_ManPiNum(pCon); if ( nAllCalls > 1 ) sat_solver_randomize( pSat, iVar, nVars ); status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); if ( status != l_True ) break; assert( status == l_True ); Vec_IntClear( vLits ); for ( v = 0; v < nVars; v++ ) Vec_IntPush( vLits, Abc_Var2Lit(Vec_IntEntry(vMap, v), !sat_solver_var_value(pSat, iVar + v)) ); Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits ); Vec_IntClearAppend( vPatBest, &pNew->vPat ); if ( 1 ) // minimization { //printf( "%d -> ", Vec_IntSize(vPatBest) ); for ( v = 0; v < 20; v++ ) { Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits ); if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) ) Vec_IntClearAppend( vPatBest, &pNew->vPat ); } //printf( "%d ", Vec_IntSize(vPatBest) ); } Vec_IntSort( vPatBest, 0 ); nCurrCexes += Min_ManAccumulate( vCexes, i*nMinCexes, (i+1)*nMinCexes, vPatBest ); if ( nCurrCexes == nMinCexes || nAllCalls > 10*nCurrCexes ) break; } } } Vec_IntWriteEntry( vStats[0], i, nAllCalls*nMaxTries ); Vec_IntWriteEntry( vStats[1], i, nAllCalls*nMaxTries ); Vec_IntWriteEntry( vStats[2], i, nCurrCexes ); sat_solver_delete( pSat ); Cnf_DataFree( pCnf ); Gia_ManStop( pCon ); Gia_ManStopP( &pCon1 ); Vec_IntFree( vMap ); if ( fVerbose ) { printf( "SAT solving for output %3d (cexes = %5d) : ", i, nCurrCexes ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } } } clkSat = Abc_Clock() - clkSat - clkSim; if ( fVerbose ) printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts ); if ( fVerbose ) Abc_PrintTime( 1, "Simulation time ", clkSim ); if ( fVerbose ) Abc_PrintTime( 1, "SAT solving time ", clkSat ); //Vec_WecPrint( vCexes, 0 ); if ( vOuts != vOuts0 ) Vec_IntFreeP( &vOuts ); Min_ManStop( pNew ); Vec_IntFree( vPatBest ); Vec_IntFree( vLits ); return vCexes; } /**Function************************************************************* Synopsis [Bit-packing for selected patterns.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Min_ManBitPackTry( Vec_Wrd_t * vSimsPi, int nWords, int iPat, Vec_Int_t * vLits ) { int i, Lit; assert( iPat >= 0 && iPat < 64 * nWords ); Vec_IntForEachEntry( vLits, Lit, i ) { word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId word * pCare = pInfo + Vec_WrdSize(vSimsPi); if ( Abc_InfoHasBit( (unsigned *)pCare, iPat ) && Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation return 0; } Vec_IntForEachEntry( vLits, Lit, i ) { word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId word * pCare = pInfo + Vec_WrdSize(vSimsPi); Abc_InfoSetBit( (unsigned *)pCare, iPat ); if ( Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation Abc_InfoXorBit( (unsigned *)pInfo, iPat ); } return 1; } int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * vLits ) { int iPat, nTotal = 64*nWords; for ( iPat = iPat0 + 1; iPat != iPat0; iPat = (iPat + 1) % nTotal ) if ( Min_ManBitPackTry( vSimsPi, nWords, iPat, vLits ) ) break; return iPat; } Vec_Ptr_t * Min_ReloadCexes( Vec_Wec_t * vCexes, int nMinCexes ) { Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_WecSize(vCexes) ); int i, c, nOuts = Vec_WecSize(vCexes)/nMinCexes; for ( i = 0; i < nMinCexes; i++ ) for ( c = 0; c < nOuts; c++ ) { Vec_Int_t * vLevel = Vec_WecEntry( vCexes, c*nMinCexes+i ); if ( Vec_IntSize(vLevel) ) Vec_PtrPush( vRes, vLevel ); } return vRes; } 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 ) { abctime clk = Abc_Clock(); //int fVeryVerbose = 0; Vec_Wrd_t * vSimsPi = NULL; Vec_Int_t * vLevel; int w, nBits, nTotal = 0, fFailed = ABC_INFINITY; Vec_Int_t * vOrder = NULL; Vec_Ptr_t * vReload = NULL; if ( 0 ) { vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes ); assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) ); assert( Vec_WecSize(vCexes)%nMinCexes == 0 ); Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) ); } else vReload = Min_ReloadCexes( vCexes, nMinCexes ); if ( fVerbose ) printf( "Packing: " ); for ( w = nWords0 ? nWords0 : 1; nWords0 ? w <= nWords0 : fFailed > 0; w++ ) { int i, iPatUsed, iPat = 0; //int k, iOut; Vec_WrdFreeP( &vSimsPi ); vSimsPi = fRandom ? Vec_WrdStartRandom(2 * Gia_ManCiNum(p) * w) : Vec_WrdStart(2 * Gia_ManCiNum(p) * w); Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 ); Abc_TtClear( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) ); fFailed = nTotal = 0; //Vec_IntForEachEntry( vOrder, iOut, k ) //Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes ) Vec_PtrForEachEntry( Vec_Int_t *, vReload, vLevel, i ) { //if ( fVeryVerbose && i%nMinCexes == 0 ) // printf( "\n" ); if ( Vec_IntSize(vLevel) == 0 ) continue; iPatUsed = Min_ManBitPackOne( vSimsPi, iPat, w, vLevel ); fFailed += iPatUsed == iPat; iPat = (iPatUsed + 1) % (64*(w-1) - 1); //if ( fVeryVerbose ) //printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed ); //if ( fVeryVerbose ) //Vec_IntPrint( vLevel ); nTotal++; } if ( fVerbose ) printf( "W = %d (F = %d) ", w, fFailed ); // printf( "Failed patterns = %d\n", fFailed ); } if ( fVerbose ) printf( "Total = %d\n", nTotal ); if ( fVerbose ) { nBits = Abc_TtCountOnesVec( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) ); printf( "Bit-packing is using %d words and %d bits. Density =%8.4f %%. ", Vec_WrdSize(vSimsPi)/Gia_ManCiNum(p), nBits, 100.0*nBits/64/Vec_WrdSize(vSimsPi) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } Vec_IntFreeP( &vOrder ); Vec_PtrFreeP( &vReload ); return vSimsPi; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Patt_ManOutputErrorCoverage( Vec_Wrd_t * vErrors, int nOuts ) { Vec_Int_t * vCounts = Vec_IntAlloc( nOuts ); int i, nWords = Vec_WrdSize(vErrors)/nOuts; assert( Vec_WrdSize(vErrors) == nOuts * nWords ); for ( i = 0; i < nOuts; i++ ) Vec_IntPush( vCounts, Abc_TtCountOnesVec(Vec_WrdEntryP(vErrors, nWords * i), nWords) ); return vCounts; } Vec_Wrd_t * Patt_ManTransposeErrors( Vec_Wrd_t * vErrors, int nOuts ) { extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut ); int nWordsIn = Vec_WrdSize(vErrors) / nOuts; int nWordsOut = Abc_Bit6WordNum(nOuts); Vec_Wrd_t * vSims1 = Vec_WrdStart( 64*nWordsIn*nWordsOut ); Vec_Wrd_t * vSims2 = Vec_WrdStart( 64*nWordsIn*nWordsOut ); assert( Vec_WrdSize(vErrors) == nWordsIn * nOuts ); Abc_TtCopy( Vec_WrdArray(vSims1), Vec_WrdArray(vErrors), Vec_WrdSize(vErrors), 0 ); Extra_BitMatrixTransposeP( vSims1, nWordsIn, vSims2, nWordsOut ); Vec_WrdFree( vSims1 ); return vSims2; } Vec_Int_t * Patt_ManPatternErrorCoverage( Vec_Wrd_t * vErrors, int nOuts ) { int nWords = Vec_WrdSize(vErrors)/nOuts; Vec_Wrd_t * vErrors2 = Patt_ManTransposeErrors( vErrors, nOuts ); Vec_Int_t * vPatErrs = Patt_ManOutputErrorCoverage( vErrors2, 64*nWords ); Vec_WrdFree( vErrors2 ); return vPatErrs; } #define ERR_REPT_SIZE 32 void Patt_ManProfileErrors( Vec_Int_t * vOutErrs, Vec_Int_t * vPatErrs ) { int nOuts = Vec_IntSize(vOutErrs); int nPats = Vec_IntSize(vPatErrs); int ErrOuts[ERR_REPT_SIZE+1] = {0}; int ErrPats[ERR_REPT_SIZE+1] = {0}; int i, Errs, nErrors1 = 0, nErrors2 = 0; Vec_IntForEachEntry( vOutErrs, Errs, i ) { nErrors1 += Errs; ErrOuts[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++; } Vec_IntForEachEntry( vPatErrs, Errs, i ) { nErrors2 += Errs; ErrPats[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++; } assert( nErrors1 == nErrors2 ); // errors/error_outputs/error_patterns //printf( "\nError statistics:\n" ); printf( "Errors =%6d ", nErrors1 ); printf( "ErrPOs =%5d (Ave = %5.2f) ", nOuts-ErrOuts[0], 1.0*nErrors1/Abc_MaxInt(1, nOuts-ErrOuts[0]) ); printf( "Patterns =%5d (Ave = %5.2f) ", nPats, 1.0*nErrors1/nPats ); printf( "Density =%8.4f %%\n", 100.0*nErrors1/nPats/Abc_MaxInt(1, nOuts-ErrOuts[0]) ); // how many times each output fails printf( "Outputs: " ); for ( i = 0; i <= ERR_REPT_SIZE; i++ ) if ( ErrOuts[i] ) printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrOuts[i] ); printf( "\n" ); // how many times each patterns fails an output printf( "Patterns: " ); for ( i = 0; i <= ERR_REPT_SIZE; i++ ) if ( ErrPats[i] ) printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrPats[i] ); printf( "\n" ); } int Patt_ManProfileErrorsOne( Vec_Wrd_t * vErrors, int nOuts ) { Vec_Int_t * vCoErrs = Patt_ManOutputErrorCoverage( vErrors, nOuts ); Vec_Int_t * vPatErrs = Patt_ManPatternErrorCoverage( vErrors, nOuts ); Patt_ManProfileErrors( vCoErrs, vPatErrs ); Vec_IntFree( vPatErrs ); Vec_IntFree( vCoErrs ); return 1; } Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p ) { Vec_Int_t * vRes = Vec_IntAlloc( 100 ); int i, Driver; Gia_ManForEachCoDriverId( p, Driver, i ) if ( Driver > 0 ) Vec_IntPush( vRes, i ); if ( Vec_IntSize(vRes) == 0 ) Vec_IntFreeP( &vRes ); return vRes; } Vec_Wrd_t * Min_ManRemapSims( int nInputs, Vec_Int_t * vMap, Vec_Wrd_t * vSimsPi ) { int i, iObj, nWords = Vec_WrdSize(vSimsPi)/Vec_IntSize(vMap); Vec_Wrd_t * vSimsNew = Vec_WrdStart( 2 * nInputs * nWords ); //Vec_Wrd_t * vSimsNew = Vec_WrdStartRandom( nInputs * nWords ); //Vec_WrdFillExtra( vSimsNew, 2 * nInputs * nWords, 0 ); assert( Vec_WrdSize(vSimsPi)%Vec_IntSize(vMap) == 0 ); Vec_WrdShrink( vSimsNew, Vec_WrdSize(vSimsNew)/2 ); Vec_IntForEachEntry( vMap, iObj, i ) { Abc_TtCopy( Vec_WrdArray(vSimsNew) + (iObj-1)*nWords, Vec_WrdArray(vSimsPi) + i*nWords, nWords, 0 ); Abc_TtCopy( Vec_WrdLimit(vSimsNew) + (iObj-1)*nWords, Vec_WrdLimit(vSimsPi) + i*nWords, nWords, 0 ); } return vSimsNew; } 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 ) { Vec_Int_t * vStats[3] = {0}; int i, iObj; Vec_Int_t * vMap = Vec_IntAlloc( 100 ); Gia_Man_t * pSwp2 = Gia_ManDupCones2( pSwp, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vMap ); Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose ); if ( Vec_IntSum(vStats[2]) == 0 ) { for ( i = 0; i < 3; i++ ) Vec_IntFree( vStats[i] ); Vec_IntFree( vMap ); Gia_ManStop( pSwp2 ); Vec_WecFree( vCexes ); return NULL; } else { Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose ); Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 ); Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) ); if ( fVerbose ) Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) ); if ( fVeryVerbose ) { printf( "Unsolved = %4d ", Vec_IntSize(vOuts) ); Gia_ManPrintStats( pSwp2, NULL ); Vec_IntForEachEntry( vOuts, iObj, i ) { printf( "%4d : ", i ); printf( "Out = %5d ", Vec_IntEntry(vMap, i) ); printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) ); printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) ); printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) ); printf( "Count = %5d ", Vec_IntEntry(vCounts, i) ); printf( "\n" ); if ( i == 20 ) break; } } for ( i = 0; i < 3; i++ ) Vec_IntFree( vStats[i] ); Vec_IntFree( vCounts ); Vec_WrdFree( vSimsPo ); Vec_WecFree( vCexes ); Gia_ManStop( pSwp2 ); //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) ); vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi ); Vec_WrdFree( vSimsPo ); Vec_IntFree( vMap ); return vSimsPi; } } 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 ) { abctime clk = Abc_Clock(); extern Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose ); Gia_Man_t * pSwp = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 ); abctime clkSweep = Abc_Clock() - clk; int nArgs = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n", nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0; Vec_Int_t * vOuts = Min_ManGetUnsolved( pSwp ); Vec_Wrd_t * vSimsPi = vOuts ? Gia_ManCollectSims( pSwp, 0, vOuts, nMaxTries, nMinCexes, fUseSim, fUseSat, fVerbose, fVeryVerbose ) : NULL; if ( vOuts == NULL ) printf( "There is no satisfiable outputs.\n" ); if ( fVerbose ) Abc_PrintTime( 1, "Sweep time", clkSweep ); if ( fVerbose ) Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); Vec_IntFreeP( &vOuts ); Gia_ManStop( pSwp ); nArgs = 0; return vSimsPi; } void Min_ManTest2( Gia_Man_t * p ) { Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 0, 1, 1 ); Vec_WrdFreeP( &vSimsPi ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END