diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaPat2.c | 1273 | ||||
| -rw-r--r-- | src/aig/gia/giaSimBase.c | 100 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/misc/vec/vecWec.h | 77 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 18 |
7 files changed, 1475 insertions, 0 deletions
@@ -5095,6 +5095,10 @@ SOURCE=.\src\aig\gia\giaPat.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaPat2.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaPf.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 66ac9e13..fb924ce5 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -622,6 +622,8 @@ static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * p static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } +static inline int Gia_ObjUpdateTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return 1; Gia_ObjSetTravIdCurrent(p, pObj); return 0; } +static inline int Gia_ObjUpdateTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsTravIdPrevious(p, pObj) ) return 1; Gia_ObjSetTravIdPrevious(p, pObj); return 0; } static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; } static inline void Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1; } static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); } diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c new file mode 100644 index 00000000..3151ed22 --- /dev/null +++ b/src/aig/gia/giaPat2.c @@ -0,0 +1,1273 @@ +/**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 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( Min_LitIsNode(p, iLit) ); // internal node + 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; +} +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 = 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 == 5 ) // 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 && Val1 != 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 = 1; + 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 ) + { + Vec_IntSort( &p->vPat, 0 ); + 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 ) +{ + 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 < 10; 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 ); + 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]) ); + + 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; + { + 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 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( 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); + sat_solver_randomize( pSat, iVar, nVars ); + status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + 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 ); + Vec_IntFree( vMap ); + } + } + if ( fVerbose ) + printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts ); + //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_Wrd_t * Min_ManBitPack( Gia_Man_t * p, 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 = 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) ); + if ( fVerbose ) + printf( "Packing: " ); + //for ( w = 1; fFailed > 100; w++ ) + for ( w = 1; fFailed > 0; w++ ) + { + int i, k, iOut, iPatUsed, iPat = 0; + 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 ) + { + 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); + 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 ); + } + 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_IntFree( vOrder ); + 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 ); + return vRes; +} +Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Vec_Int_t * vStats[3] = {0}; int i, iObj; + 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 ); + Gia_Man_t * pSwp2 = Gia_ManDupSelectedOutputs( pSwp, vOuts ); + Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose ); + Vec_Wrd_t * vSimsPi = Min_ManBitPack( p, 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) ); + Abc_PrintTime( 1, "Sweep time", clkSweep ); + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + } + if ( 0 ) + { + printf( "Unsolved = %4d ", Vec_IntSize(vOuts) ); + Gia_ManPrintStats( pSwp2, NULL ); + Vec_IntForEachEntry( vOuts, iObj, i ) + { + printf( "%4d : ", i ); + printf( "Out = %5d ", iObj ); + 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 ); + Vec_IntFree( vOuts ); + Gia_ManStop( pSwp ); + Gia_ManStop( pSwp2 ); + nArgs = 0; + return vSimsPi; +} +void Min_ManTest2( Gia_Man_t * p ) +{ + Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 1, 0 ); + Vec_WrdFreeP( &vSimsPi ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index bfafdcfd..a9706742 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -2522,6 +2522,106 @@ int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int return RetValue; } +/**Function************************************************************* + + Synopsis [Serialization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSim2ArrayOne( Vec_Wrd_t * vSimsPi, Vec_Int_t * vRes ) +{ + word * pInfo = Vec_WrdArray(vSimsPi); int w, i; + word * pCare = pInfo + Vec_WrdSize(vSimsPi); + Vec_IntClear( vRes ); + for ( w = 0; w < Vec_WrdSize(vSimsPi); w++ ) + if ( pCare[w] ) + for ( i = 0; i < 64; i++ ) + if ( Abc_TtGetBit(pCare, w*64+i) ) + Vec_IntPush( vRes, Abc_Var2Lit(w*64+i, Abc_TtGetBit(pInfo, w*64+i)) ); + Vec_IntPush( vRes, Vec_WrdSize(vSimsPi) ); +} +Vec_Wec_t * Gia_ManSim2Array( Vec_Ptr_t * vSims ) +{ + Vec_Wec_t * vRes = Vec_WecStart( Vec_PtrSize(vSims) ); + Vec_Int_t * vLevel; int i; + Vec_WecForEachLevel( vRes, vLevel, i ) + Gia_ManSim2ArrayOne( (Vec_Wrd_t *)Vec_PtrEntry(vSims, i), vLevel ); + return vRes; +} + +Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes ) +{ + int i, iLit, nWords = Vec_IntEntryLast(vRes); + Vec_Wrd_t * vSimsPi = Vec_WrdStart( 2*nWords ); + word * pInfo = Vec_WrdArray(vSimsPi); + word * pCare = pInfo + nWords; + Vec_IntPop( vRes ); + Vec_IntForEachEntry( vRes, iLit, i ) + { + Abc_TtXorBit( pCare, Abc_Lit2Var(iLit) ); + if ( Abc_LitIsCompl(iLit) ) + Abc_TtXorBit( pInfo, Abc_Lit2Var(iLit) ); + } + Vec_IntPush( vRes, nWords ); + Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 ); + return vSimsPi; +} +Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes ) +{ + Vec_Ptr_t * vSims = Vec_PtrAlloc( Vec_WecSize(vRes) ); + Vec_Int_t * vLevel; int i; + Vec_WecForEachLevel( vRes, vLevel, i ) + Vec_PtrPush( vSims, Gia_ManArray2SimOne(vLevel) ); + return vSims; +} + +void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi ) +{ + Vec_Ptr_t * vTemp = Vec_PtrAlloc( 2 ); + Vec_PtrPushTwo( vTemp, vSimsPi, vSimsPi ); + { + Vec_Wec_t * vRes = Gia_ManSim2Array( vTemp ); + Vec_WecDumpBin( "temp.sims", vRes, 1 ); + { + Vec_Wec_t * vRes = Vec_WecReadBin( "temp.sims", 1 ); + Vec_Ptr_t * vTemp2 = Gia_ManArray2Sim( vRes ); + Vec_Wrd_t * vSimsPi2 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 0 ); + Vec_Wrd_t * vSimsPi3 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 1 ); + + Abc_TtAnd( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi)+Vec_WrdSize(vSimsPi), Vec_WrdSize(vSimsPi), 0 ); + + vSimsPi->nSize *= 2; + vSimsPi2->nSize *= 2; + vSimsPi3->nSize *= 2; + Vec_WrdDumpHex( "test1.hex", vSimsPi, 1, 1 ); + Vec_WrdDumpHex( "test2.hex", vSimsPi2, 1, 1 ); + Vec_WrdDumpHex( "test3.hex", vSimsPi3, 1, 1 ); + vSimsPi->nSize /= 2; + vSimsPi2->nSize /= 2; + vSimsPi3->nSize /= 2; + + if ( Vec_WrdEqual( vSimsPi, vSimsPi2 ) ) + printf( "Success.\n" ); + else + printf( "Failure.\n" ); + if ( Vec_WrdEqual( vSimsPi, vSimsPi3 ) ) + printf( "Success.\n" ); + else + printf( "Failure.\n" ); + Vec_WrdFree( vSimsPi2 ); + Vec_WrdFree( vSimsPi3 ); + Vec_PtrFree( vTemp2 ); + Vec_WecFree( vRes ); + } + Vec_WecFree( vRes ); + } + Vec_PtrFree( vTemp ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 8cbcaa25..d801a243 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -60,6 +60,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaOf.c \ src/aig/gia/giaPack.c \ src/aig/gia/giaPat.c \ + src/aig/gia/giaPat2.c \ src/aig/gia/giaPf.c \ src/aig/gia/giaQbf.c \ src/aig/gia/giaReshape1.c \ diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h index a97f1ceb..cd463e01 100644 --- a/src/misc/vec/vecWec.h +++ b/src/misc/vec/vecWec.h @@ -791,6 +791,83 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes ) } +/**Function************************************************************* + + Synopsis [File interface.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecDumpBin( char * pFileName, Vec_Wec_t * p, int fVerbose ) +{ + Vec_Int_t * vLevel; + int i, nSize, RetValue; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + nSize = Vec_WecSize(p); + RetValue = fwrite( &nSize, 1, sizeof(int), pFile ); + Vec_WecForEachLevel( p, vLevel, i ) + { + nSize = Vec_IntSize(vLevel); + RetValue += fwrite( &nSize, 1, sizeof(int), pFile ); + RetValue += fwrite( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile ); + } + fclose( pFile ); + if ( RetValue != (int)sizeof(int)*(Vec_WecSizeSize(p)+Vec_WecSize(p)+1) ) + printf( "Error writing data into file.\n" ); + if ( fVerbose ) + printf( "Written %d integer arrays into file \"%s\".\n", Vec_WecSize(p), pFileName ); +} +static inline Vec_Wec_t * Vec_WecReadBin( char * pFileName, int fVerbose ) +{ + Vec_Wec_t * p = NULL; Vec_Int_t * vLevel; int i, nSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + fseek( pFile, 0, SEEK_END ); + nSize = ftell( pFile ); + if ( nSize == 0 ) + { + printf( "The input file is empty.\n" ); + fclose( pFile ); + return NULL; + } + if ( nSize % sizeof(int) > 0 ) + { + printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", (int)(nSize % sizeof(int)) ); + fclose( pFile ); + return NULL; + } + rewind( pFile ); + RetValue = fread( &nSize, 1, sizeof(int), pFile ); + assert( RetValue == 4 ); + p = Vec_WecStart( nSize ); + Vec_WecForEachLevel( p, vLevel, i ) + { + RetValue = fread( &nSize, 1, sizeof(int), pFile ); + assert( RetValue == 4 ); + Vec_IntFill( vLevel, nSize, 0 ); + RetValue = fread( Vec_IntArray(vLevel), 1, sizeof(int)*nSize, pFile ); + assert( RetValue == 4*nSize ); + } + fclose( pFile ); + if ( fVerbose ) + printf( "Read %d integer arrays from file \"%s\".\n", Vec_WecSize(p), pFileName ); + return p; +} + + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f4126567..53f3ebe2 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -292,6 +292,24 @@ static inline int sat_solver_final(sat_solver* s, int ** ppArray) return s->conf_final.size; } +static inline void sat_solver_randomize( sat_solver * pSat, int iVar, int nVars ) +{ + int i, nPols = 0, * pVars = ABC_ALLOC( int, nVars ); + for ( i = 0; i < nVars; i++ ) + if ( Abc_Random(0) & 1 ) + pVars[nPols++] = iVar + i; + sat_solver_set_polarity( pSat, pVars, nPols ); + for ( i = 0; i < nVars; i++ ) + pVars[i] = iVar + i; + for ( i = 0; i < nVars; i++ ) + { + int j = Abc_Random(0) % nVars; + ABC_SWAP( int, pVars[i], pVars[j] ); + } + sat_solver_set_var_activity( pSat, pVars, nVars ); + ABC_FREE( pVars ); +} + static inline abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit) { abctime nRuntimeLimit = s->nRuntimeLimit; |