From ddb22f3bed7cb457576b4b80e55d47eabf3a1308 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2022 14:21:47 -0700 Subject: Various changes. --- src/aig/gia/gia.h | 4 ++++ src/aig/gia/giaResub2.c | 2 +- src/aig/gia/giaSatSyn.c | 60 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + src/aig/miniaig/miniaig.h | 19 +++++++++++++++ 5 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 src/aig/gia/giaSatSyn.c (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 488f12cf..7487b8f3 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -527,18 +527,22 @@ static inline int Gia_ObjDiff1( Gia_Obj_t * pObj ) { static inline int Gia_ObjFaninC0( Gia_Obj_t * pObj ) { return pObj->fCompl0; } static inline int Gia_ObjFaninC1( Gia_Obj_t * pObj ) { return pObj->fCompl1; } static inline int Gia_ObjFaninC2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes && Abc_LitIsCompl(p->pMuxes[Gia_ObjId(p, pObj)]); } +static inline int Gia_ObjFaninC( Gia_Obj_t * pObj, int n ) { return n ? Gia_ObjFaninC1(pObj) : Gia_ObjFaninC0(pObj); } static inline Gia_Obj_t * Gia_ObjFanin0( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff0; } static inline Gia_Obj_t * Gia_ObjFanin1( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff1; } static inline Gia_Obj_t * Gia_ObjFanin2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes ? Gia_ManObj(p, Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)])) : NULL; } +static inline Gia_Obj_t * Gia_ObjFanin( Gia_Obj_t * pObj, int n ) { return n ? Gia_ObjFanin1(pObj) : Gia_ObjFanin0(pObj); } static inline Gia_Obj_t * Gia_ObjChild0( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); } static inline Gia_Obj_t * Gia_ObjChild1( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); } static inline Gia_Obj_t * Gia_ObjChild2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin2(p, pObj), Gia_ObjFaninC2(p, pObj) ); } static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff0; } static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; } static inline int Gia_ObjFaninId2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? Abc_Lit2Var(p->pMuxes[ObjId]) : -1; } +static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int ObjId, int n ){ return n ? Gia_ObjFaninId1(pObj, ObjId) : Gia_ObjFaninId0(pObj, ObjId); } static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); } static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); } static inline int Gia_ObjFaninId2p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)]) : -1; } +static inline int Gia_ObjFaninIdp( Gia_Man_t * p, Gia_Obj_t * pObj, int n){ return n ? Gia_ObjFaninId1p(p, pObj) : Gia_ObjFaninId0p(p, pObj); } static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1; } diff --git a/src/aig/gia/giaResub2.c b/src/aig/gia/giaResub2.c index 1219526f..10c5a9e0 100644 --- a/src/aig/gia/giaResub2.c +++ b/src/aig/gia/giaResub2.c @@ -733,7 +733,7 @@ void Gia_RsbCiWindowTest( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n ) { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj); } +//static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n ) { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj); } static inline int Gia_ObjTravIsTopTwo( Gia_Man_t * p, int iNodeA ) { return (p->pTravIds[iNodeA] >= p->nTravIds - 1); } static inline int Gia_ObjTravIsSame( Gia_Man_t * p, int iNodeA, int iNodeB ) { return (p->pTravIds[iNodeA] == p->pTravIds[iNodeB]); } diff --git a/src/aig/gia/giaSatSyn.c b/src/aig/gia/giaSatSyn.c new file mode 100644 index 00000000..15829f79 --- /dev/null +++ b/src/aig/gia/giaSatSyn.c @@ -0,0 +1,60 @@ +/**CFile**************************************************************** + + FileName [giaSyn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [High-effort synthesis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSyn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/util/utilTruth.h" +#include "sat/glucose/AbcGlucose.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int nTimeLimit, int fUseXor, int fFancy, int fVerbose ) +{ + Gia_Man_t * pNew = NULL; + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 171d8be3..cd2e0afe 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -77,6 +77,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaSatLut.c \ src/aig/gia/giaSatMap.c \ src/aig/gia/giaSatoko.c \ + src/aig/gia/giaSatSyn.c \ src/aig/gia/giaSat3.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaScript.c \ diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 0365b946..274048b9 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -648,6 +648,25 @@ int main( int argc, char ** argv ) } */ +/* +#include "aig/miniaig/miniaig.h" + +// this procedure creates a MiniAIG for function F = a*b + ~c and writes it into a file "test.aig" +void Mini_AigTest() +{ + Mini_Aig_t * p = Mini_AigStart(); // create empty AIG manager (contains only const0 node) + int litApos = Mini_AigCreatePi( p ); // create input A (returns pos lit of A) + int litBpos = Mini_AigCreatePi( p ); // create input B (returns pos lit of B) + int litCpos = Mini_AigCreatePi( p ); // create input C (returns pos lit of C) + int litCneg = Mini_AigLitNot( litCpos ); // neg lit of C + int litAnd = Mini_AigAnd( p, litApos, litBpos ); // lit for a*b + int litOr = Mini_AigOr( p, litAnd, litCneg ); // lit for a*b + ~c + Mini_AigCreatePo( p, litOr ); // create primary output + Mini_AigerWrite( "test.aig", p, 1 ); // write the result into a file + Mini_AigStop( p ); // deallocate MiniAIG +} +*/ + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3 From 66449e803339350c2ede36e78ce562b50d12007b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2022 20:38:33 -0700 Subject: Constructing boolean relation. --- src/aig/gia/giaSimBase.c | 156 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 156 insertions(+) (limited to 'src/aig') diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 002f6bc2..923e5735 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -2777,6 +2777,162 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Gia_ManRelTfos( Gia_Man_t * p, Vec_Int_t * vObjs ) +{ + Gia_Obj_t * pObj; + Vec_Wec_t * vNodes = Vec_WecStart( Vec_IntSize(vObjs)+1 ); + Vec_Int_t * vSigns = Vec_IntStart( Gia_ManObjNum(p) ); + int n, k, i, iObj, * pSigns = Vec_IntArray(vSigns); + assert( Vec_IntSize(vObjs) < 32 ); + Vec_IntForEachEntry( vObjs, iObj, i ) + pSigns[iObj] |= 1 << i; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( pSigns[i] == 0 ) + for ( n = 0; n < 2; n++ ) + pSigns[i] |= pSigns[Gia_ObjFaninId(pObj, i, n)]; + if ( pSigns[i] == 0 ) + continue; + Vec_WecPush( vNodes, Vec_IntSize(vObjs), i ); + for ( k = 0; k < Vec_IntSize(vObjs); k++ ) + if ( (pSigns[i] >> k) & 1 ) + Vec_WecPush( vNodes, k, i ); + } + Vec_IntFree( vSigns ); + return vNodes; +} +Vec_Wrd_t * Gia_ManRelDerive( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims ) +{ + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj; + int i, m, iVar, iMint = 0, nMints = 1 << Vec_IntSize(vObjs); + Vec_Wrd_t * vCopy = Vec_WrdDup(vSims); Vec_Int_t * vLevel; + Vec_Wrd_t * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints ); + Vec_Wec_t * vNodes = Gia_ManRelTfos( p, vObjs ); + Vec_WecPrint( vNodes, 0 ); + Gia_ManForEachAnd( p, pObj, i ) + assert( pObj->fPhase == 0 ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 1; + vLevel = Vec_WecEntry( vNodes, Vec_IntSize(vObjs) ); + Gia_ManForEachObjVec( vLevel, p, pObj, i ) + if ( pObj->fPhase ) + Abc_TtClear( Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords), nWords ); + else + Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy ); + for ( m = 0; m < nMints; m++ ) + { + Gia_ManForEachCo( p, pObj, i ) + { + word * pSimO = Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords); + word * pSimF = Vec_WrdEntryP(vCopy, Gia_ObjFaninId0p(p, pObj)*nWords); + word * pSimR = Vec_WrdEntryP(vRel, (iMint*Gia_ManCoNum(p) + i)*nWords); + Abc_TtXor( pSimR, pSimF, pSimO, nWords, Gia_ObjFaninC0(pObj) ); + } + if ( m == nMints-1 ) + break; + iVar = Abc_TtSuppFindFirst( (m+1) ^ ((m+1) >> 1) ^ (m) ^ ((m) >> 1) ); + vLevel = Vec_WecEntry( vNodes, iVar ); + assert( Vec_IntEntry(vLevel, 0) == Vec_IntEntry(vObjs, iVar) ); + Abc_TtNot( Vec_WrdEntryP(vCopy, Vec_IntEntry(vObjs, iVar)*nWords), nWords ); + Gia_ManForEachObjVec( vLevel, p, pObj, i ) + if ( !pObj->fPhase ) + Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy ); + iMint ^= 1 << iVar; + } + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 0; + Vec_WrdFree( vCopy ); + Vec_WecFree( vNodes ); + return vRel; +} +Vec_Wrd_t * Gia_ManRelDerive2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims ) +{ + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj; + int i, Id, m, Index, iMint = 0, nMints = 1 << Vec_IntSize(vObjs); + Vec_Wrd_t * vPos, * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints ); + for ( m = 0; m < nMints; m++ ) + { + Gia_Man_t * pNew = Gia_ManDup( p ); + Gia_ManForEachAnd( pNew, pObj, i ) + { + if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId0(pObj, i))) >= 0 ) + pObj->iDiff0 = i, pObj->fCompl0 ^= (m >> Index) & 1; + if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId1(pObj, i))) >= 0 ) + pObj->iDiff1 = i, pObj->fCompl1 ^= (m >> Index) & 1; + } + vPos = Gia_ManSimPatSimOut( pNew, p->vSimsPi, 1 ); + Gia_ManForEachCoId( p, Id, i ) + Abc_TtXor( Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p) + i)*nWords), Vec_WrdEntryP(vPos, i*nWords), Vec_WrdEntryP(vSims, Id*nWords), nWords, 0 ); + Vec_WrdFree( vPos ); + Gia_ManStop( pNew ); + } + return vRel; +} +void Gia_ManRelPrint( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel ) +{ + int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + int i, Id, m, nMints = 1 << Vec_IntSize(vObjs); + printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) ); + for ( w = 0; w < 64*nWords; w++ ) + { + Gia_ManForEachCiId( p, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + printf( " " ); + Vec_IntForEachEntry( vObjs, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + printf( " " ); + Gia_ManForEachCoId( p, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + printf( " " ); + for ( m = 0; m < nMints; m++ ) + { + printf( " " ); + for ( i = 0; i < Vec_IntSize(vObjs); i++ ) + printf( "%d", (m >> i) & 1 ); + printf( "=" ); + Gia_ManForEachCoId( p, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w) ); + } + printf( "\n" ); + } +} +Vec_Int_t * Gia_ManRelInitObjs() +{ + Vec_Int_t * vRes = Vec_IntAlloc( 3 ); + Vec_IntPush( vRes, 41 ); + Vec_IntPush( vRes, 46 ); + Vec_IntPush( vRes, 53 ); + return vRes; +} +void Gia_ManRelDeriveTest( Gia_Man_t * p ) +{ + Vec_Int_t * vObjs = Gia_ManRelInitObjs(); + Vec_Wrd_t * vSims, * vRel, * vRel2; int nWords; + Vec_WrdFreeP( &p->vSimsPi ); + p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + vSims = Gia_ManSimPatSim( p ); + vRel = Gia_ManRelDerive( p, vObjs, vSims ); + vRel2 = Gia_ManRelDerive2( p, vObjs, vSims ); + assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) ); + Gia_ManRelPrint( p, vObjs, vSims, vRel ); + Vec_WrdFree( vRel2 ); + Vec_WrdFree( vRel ); + Vec_WrdFree( vSims ); + Vec_IntFree( vObjs ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3 From a9237f50ea01efdd62f86d334a38ffbe80a3d141 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 31 Jul 2022 19:12:55 -0700 Subject: New switch in command &st for adding buffers. --- src/aig/gia/giaDup.c | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'src/aig') diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index cc501562..c9af8a32 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -860,6 +860,27 @@ Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap ) Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; } +Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCiNum(p) + Gia_ManCoNum(p) ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendBuf( pNew, pObj->Value ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + Gia_ManHashStop( pNew ); + return pNew; +} /**Function************************************************************* -- cgit v1.2.3 From 132b8939219553341a8a45bae58dc777993bd807 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 3 Aug 2022 10:09:44 -0700 Subject: Investigating complex miters. --- src/aig/gia/giaSimBase.c | 88 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 86 insertions(+), 2 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 923e5735..3d103574 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -2706,6 +2706,81 @@ Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose ) return p; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManProcessBuffs( Gia_Man_t * pHie, Vec_Wrd_t * vSimsH, int nWords, Vec_Mem_t * vStore, Vec_Int_t * vLabels ) +{ + Vec_Int_t * vPoSigs = Vec_IntAlloc( Gia_ManBufNum(pHie) ); + Vec_Int_t * vMap; + Vec_Wec_t * vNodes = Vec_WecStart( Gia_ManBufNum(pHie) ); + Gia_Obj_t * pObj; int i, Sig, Value; + Gia_ManForEachBuf( pHie, pObj, i ) + { + word * pSim = Vec_WrdEntryP(vSimsH, Gia_ObjId(pHie, pObj)*nWords); + int fCompl = pSim[0] & 1; + if ( fCompl ) + Abc_TtNot( pSim, nWords ); + Vec_IntPush( vPoSigs, Vec_MemHashInsert(vStore, pSim) ); + if ( fCompl ) + Abc_TtNot( pSim, nWords ); + } + Vec_IntPrint( vPoSigs ); + vMap = Vec_IntStartFull( Vec_MemEntryNum(vStore) ); + Vec_IntForEachEntry( vPoSigs, Sig, i ) + { + assert( Vec_IntEntry(vMap, Sig) == -1 ); + Vec_IntWriteEntry( vMap, Sig, i ); + } + Vec_IntForEachEntry( vLabels, Sig, i ) + { + if ( Sig < 0 ) + continue; + Value = Vec_IntEntry(vMap, Sig); + if ( Value == -1 ) + continue; + assert( Value >= 0 && Value < Gia_ManBufNum(pHie) ); + Vec_WecPush( vNodes, Value, i ); + } + Vec_WecPrint( vNodes, 0 ); + Vec_WecFree( vNodes ); + Vec_IntFree( vMap ); + Vec_IntFree( vPoSigs ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld ) +{ + Gia_Obj_t * pObj; int i; + Gia_ManSetPhase( pNew ); + Gia_ManSetPhase( pOld ); + Gia_ManForEachCo( pNew, pObj, i ) + if ( pObj->fPhase ^ Gia_ManCo(pOld, i)->fPhase ) + { + printf( "Updating out %d.\n", i ); + Gia_ObjFlipFaninC0( pObj ); + } +} + /**Function************************************************************* Synopsis [] @@ -2723,7 +2798,8 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV Vec_Wrd_t * vSims = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords ); Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat ); Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie ); - Gia_Obj_t * pObj; int * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0; + Vec_Int_t * vLabels = Vec_IntStartFull( Gia_ManObjNum(pFlat) ); + Gia_Obj_t * pObj; int fCompl, Value, * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0; Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page pFlat->vSimsPi = NULL; pHie->vSimsPi = NULL; @@ -2739,7 +2815,13 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV word * pSim = Vec_WrdEntryP(vSims0, i*nWords); nC0s += Abc_TtIsConst0(pSim, nWords); nC1s += Abc_TtIsConst1(pSim, nWords); - Vec_MemHashInsert( vStore, pSim ); + fCompl = pSim[0] & 1; + if ( fCompl ) + Abc_TtNot( pSim, nWords ); + Value = Vec_MemHashInsert( vStore, pSim ); + if ( fCompl ) + Abc_TtNot( pSim, nWords ); + Vec_IntWriteEntry( vLabels, i, Value ); } nUnique = Vec_MemEntryNum( vStore ); printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n", @@ -2765,10 +2847,12 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV //if ( Gia_ObjIsBuf(pObj) ) // printf( "%d(%d) ", i, nBoundary-1 ); } + Gia_ManProcessBuffs( pHie, vSims1, nWords, vStore, vLabels ); Vec_MemHashFree( vStore ); Vec_MemFree( vStore ); Vec_WrdFree( vSims0 ); Vec_WrdFree( vSims1 ); + Vec_IntFree( vLabels ); printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary. ", nMatched, 100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)), -- cgit v1.2.3 From 1368a920b9ba4903bc0891c981c8450249e1767f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 8 Aug 2022 16:41:32 -0700 Subject: Improvements to command 'twoexact'. --- src/aig/miniaig/miniaig.h | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'src/aig') diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 274048b9..9aa41b11 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -144,6 +144,18 @@ static Mini_Aig_t * Mini_AigStart() Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL ); return p; } +static Mini_Aig_t * Mini_AigStartSupport( int nIns, int nObjsAlloc ) +{ + Mini_Aig_t * p; int i; + assert( 1+nIns < nObjsAlloc ); + p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); + p->nCap = 2*nObjsAlloc; + p->nSize = 2*(1+nIns); + p->pArray = MINI_AIG_ALLOC( int, p->nCap ); + for ( i = 0; i < p->nSize; i++ ) + p->pArray[i] = MINI_AIG_NULL; + return p; +} static void Mini_AigStop( Mini_Aig_t * p ) { MINI_AIG_FREE( p->pArray ); @@ -170,6 +182,31 @@ static int Mini_AigAndNum( Mini_Aig_t * p ) nNodes++; return nNodes; } +static int Mini_AigXorNum( Mini_Aig_t * p ) +{ + int i, nNodes = 0; + Mini_AigForEachAnd( p, i ) + nNodes += p->pArray[2*i] > p->pArray[2*i+1]; + return nNodes; +} +static int Mini_AigLevelNum( Mini_Aig_t * p ) +{ + int i, Level = 0; + int * pLevels = MINI_AIG_CALLOC( int, Mini_AigNodeNum(p) ); + Mini_AigForEachAnd( p, i ) + { + int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))]; + int Lel1 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin1(p, i))]; + pLevels[i] = 1 + (Lel0 > Lel1 ? Lel0 : Lel1); + } + Mini_AigForEachPo( p, i ) + { + int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))]; + Level = Level > Lel0 ? Level : Lel0; + } + MINI_AIG_FREE( pLevels ); + return Level; +} static void Mini_AigPrintStats( Mini_Aig_t * p ) { printf( "MiniAIG stats: PI = %d PO = %d FF = %d AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) ); -- cgit v1.2.3 From 1b0439d128be83914825ed097f4b42201d531213 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 11 Aug 2022 20:19:37 -0700 Subject: Changing 2:1 MUX fanin order to be (ctrl, data0, data1). --- src/aig/miniaig/ndr.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h index 68c2779c..19373063 100644 --- a/src/aig/miniaig/ndr.h +++ b/src/aig/miniaig/ndr.h @@ -506,7 +506,7 @@ static inline void Ndr_WriteVerilogModule( FILE * pFile, void * pDesign, int Mod else if ( nArray == 3 && Type == ABC_OPER_ARI_ADD ) fprintf( pFile, "%s + %s + %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] ); else if ( Type == ABC_OPER_BIT_MUX ) - fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] ); + fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[2]], pNames[pArray[1]] ); else fprintf( pFile, ";\n", Abc_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) ); } -- cgit v1.2.3 From c3c643820e714cf1ad392a2a84276c7c168cffda Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 30 Aug 2022 12:00:33 -0700 Subject: Various changes. --- src/aig/gia/giaCut.c | 215 ++++++++++++++++++++++++++++++++++++++- src/aig/gia/giaSimBase.c | 257 +++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 464 insertions(+), 8 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c index 7ee795b6..19e2d8fc 100644 --- a/src/aig/gia/giaCut.c +++ b/src/aig/gia/giaCut.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/util/utilTruth.h" +#include "misc/vec/vecHsh.h" ABC_NAMESPACE_IMPL_START @@ -29,7 +30,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// #define GIA_MAX_CUTSIZE 8 -#define GIA_MAX_CUTNUM 51 +#define GIA_MAX_CUTNUM 65 #define GIA_MAX_TT_WORDS ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1) #define GIA_CUT_NO_LEAF 0xF @@ -778,6 +779,218 @@ void Gia_ManExtractTest( Gia_Man_t * pGia ) Abc_PrintTime( 0, "Creating windows", Abc_Clock() - clk ); } +/**Function************************************************************* + + Synopsis [Extract a given number of cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_StoCutPrint( int * pCut ) +{ + int v; + printf( "{" ); + for ( v = 1; v <= pCut[0]; v++ ) + printf( " %d", pCut[v] ); + printf( " }\n" ); +} +void Gia_StoPrintCuts( Vec_Int_t * vThis, int iObj, int nCutSize ) +{ + int i, * pCut; + printf( "Cuts of node %d (size = %d):\n", iObj, nCutSize ); + Sdb_ForEachCut( Vec_IntArray(vThis), pCut, i ) + if ( !nCutSize || pCut[0] == nCutSize ) + Gia_StoCutPrint( pCut ); +} +Vec_Wec_t * Gia_ManFilterCuts( Gia_Man_t * pGia, Vec_Wec_t * vStore, int nCutSize, int nCuts ) +{ + abctime clkStart = Abc_Clock(); + Vec_Wec_t * vCutsSel = Vec_WecAlloc( nCuts ); + Vec_Int_t * vLevel, * vCut = Vec_IntAlloc( 10 ); + Vec_Wec_t * vCuts = Vec_WecAlloc( 1000 ); + Hsh_VecMan_t * p = Hsh_VecManStart( 1000 ); int i, s; + Vec_WecForEachLevel( vStore, vLevel, i ) if ( Vec_IntSize(vLevel) ) + { + int v, k, * pCut, Value; + Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) + { + if ( pCut[0] < 2 ) + continue; + + for ( v = 1; v <= pCut[0]; v++ ) + if ( pCut[v] < 9 ) + break; + if ( v <= pCut[0] ) + continue; + + Vec_IntClear( vCut ); + Vec_IntPushArray( vCut, pCut+1, pCut[0] ); + Value = Hsh_VecManAdd( p, vCut ); + if ( Value == Vec_WecSize(vCuts) ) + { + Vec_Int_t * vTemp = Vec_WecPushLevel(vCuts); + Vec_IntPush( vTemp, 0 ); + Vec_IntAppend( vTemp, vCut ); + } + Vec_IntAddToEntry( Vec_WecEntry(vCuts, Value), 0, 1 ); + } + } + printf( "Collected cuts = %d.\n", Vec_WecSize(vCuts) ); + for ( s = 3; s <= nCutSize; s++ ) + Vec_WecForEachLevel( vCuts, vLevel, i ) + if ( Vec_IntSize(vLevel) - 1 == s ) + { + int * pCut = Vec_IntEntryP(vLevel, 1); + int u, v, Value; + for ( u = 0; u < s; u++ ) + { + Vec_IntClear( vCut ); + for ( v = 0; v < s; v++ ) if ( v != u ) + Vec_IntPush( vCut, pCut[v] ); + assert( Vec_IntSize(vCut) == s-1 ); + Value = Hsh_VecManAdd( p, vCut ); + if ( Value < Vec_WecSize(vCuts) ) + Vec_IntAddToEntry( vLevel, 0, Vec_IntEntry(Vec_WecEntry(vCuts, Value), 0) ); + } + } + Hsh_VecManStop( p ); + Vec_IntFree( vCut ); + // collect + Vec_WecSortByFirstInt( vCuts, 1 ); + Vec_WecForEachLevelStop( vCuts, vLevel, i, Abc_MinInt(Vec_WecSize(vCuts), nCuts) ) + Vec_IntAppend( Vec_WecPushLevel(vCutsSel), vLevel ); + Abc_PrintTime( 0, "Cut filtering time", Abc_Clock() - clkStart ); + return vCutsSel; +} +int Gia_ManCountRefs( Gia_Man_t * pGia, Vec_Int_t * vLevel ) +{ + int i, iObj, nRefs = 0; + Vec_IntForEachEntry( vLevel, iObj, i ) + nRefs += Gia_ObjRefNumId(pGia, iObj); + return nRefs; +} +Vec_Wrd_t * Gia_ManGenSims( Gia_Man_t * pGia ) +{ + Vec_Wrd_t * vSims; + Vec_WrdFreeP( &pGia->vSimsPi ); + pGia->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pGia) ); + vSims = Gia_ManSimPatSim( pGia ); + return vSims; +} +int Gia_ManFindSatDcs( Gia_Man_t * pGia, Vec_Wrd_t * vSims, Vec_Int_t * vLevel ) +{ + int nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); + int i, w, iObj, Res = 0, Pres[256] = {0}, nMints = 1 << Vec_IntSize(vLevel); + for ( w = 0; w < 64*nWords; w++ ) + { + int iInMint = 0; + Vec_IntForEachEntry( vLevel, iObj, i ) + if ( Abc_TtGetBit( Vec_WrdEntryP(vSims, iObj*nWords), w ) ) + iInMint |= 1 << i; + Pres[iInMint]++; + } + for ( i = 0; i < nMints; i++ ) + Res += Pres[i] == 0; + return Res; +} + + +int Gia_ManCollectCutDivs( Gia_Man_t * p, Vec_Int_t * vIns ) +{ + Gia_Obj_t * pObj; int i, Res = 0; + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_IntSort( vIns, 0 ); + + Vec_IntPush( vRes, 0 ); + Vec_IntAppend( vRes, vIns ); + + Gia_ManIncrementTravId( p ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vIns, p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + continue; + else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) ) + { + if ( !Gia_ObjIsTravIdPrevious(p, pObj) ) + Vec_IntPush( vRes, i ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } +// printf( "Divisors: " ); +// Vec_IntPrint( vRes ); + Res = Vec_IntSize(vRes); + Vec_IntFree( vRes ); + return Res; +} + +void Gia_ManConsiderCuts( Gia_Man_t * pGia, Vec_Wec_t * vCuts ) +{ + Vec_Wrd_t * vSims = Gia_ManGenSims( pGia ); + Vec_Int_t * vLevel; int i; + Gia_ManCreateRefs( pGia ); + Vec_WecForEachLevel( vCuts, vLevel, i ) + { + printf( "Cut %3d ", i ); + printf( "Ref = %3d : ", Vec_IntEntry(vLevel, 0) ); + + Vec_IntShift( vLevel, 1 ); + printf( "Ref = %3d : ", Gia_ManCountRefs(pGia, vLevel) ); + printf( "SDC = %3d : ", Gia_ManFindSatDcs(pGia, vSims, vLevel) ); + printf( "Div = %3d : ", Gia_ManCollectCutDivs(pGia, vLevel) ); + Vec_IntPrint( vLevel ); + Vec_IntShift( vLevel, -1 ); + } + Vec_WrdFree( vSims ); +} + + +Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 ) +{ + int nCutSize = nCutSize0; + int nCutNum = 64; + int fCutMin = 0; + int fTruthMin = 0; + int fVerbose = fVerbose0; + Vec_Wec_t * vCutsSel; + Gia_Sto_t * p = Gia_StoAlloc( pGia, nCutSize, nCutNum, fCutMin, fTruthMin, fVerbose ); + Gia_Obj_t * pObj; int i, iObj; + assert( nCutSize <= GIA_MAX_CUTSIZE ); + assert( nCutNum < GIA_MAX_CUTNUM ); + // prepare references + Gia_ManForEachObj( p->pGia, pObj, iObj ) + Gia_StoRefObj( p, iObj ); + // compute cuts + Gia_StoComputeCutsConst0( p, 0 ); + Gia_ManForEachCiId( p->pGia, iObj, i ) + Gia_StoComputeCutsCi( p, iObj ); + Gia_ManForEachAnd( p->pGia, pObj, iObj ) + Gia_StoComputeCutsNode( p, iObj ); + if ( p->fVerbose ) + { + printf( "Running cut computation with CutSize = %d CutNum = %d CutMin = %s TruthMin = %s\n", + p->nCutSize, p->nCutNum, p->fCutMin ? "yes":"no", p->fTruthMin ? "yes":"no" ); + printf( "CutPair = %.0f ", p->CutCount[0] ); + printf( "Merge = %.0f (%.2f %%) ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] ); + printf( "Eval = %.0f (%.2f %%) ", p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] ); + printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] ); + printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) ); + printf( "\n" ); + printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ", + p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) ); + Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart ); + } + vCutsSel = Gia_ManFilterCuts( pGia, p->vCuts, nCutSize0, nCuts0 ); + Gia_ManConsiderCuts( pGia, vCutsSel ); + Gia_StoFree( p ); + return vCutsSel; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 3d103574..6f825549 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -2943,7 +2943,7 @@ Vec_Wrd_t * Gia_ManRelDerive( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSim Vec_Wrd_t * Gia_ManRelDerive2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims ) { int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj; - int i, Id, m, Index, iMint = 0, nMints = 1 << Vec_IntSize(vObjs); + int i, Id, m, Index, nMints = 1 << Vec_IntSize(vObjs); Vec_Wrd_t * vPos, * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints ); for ( m = 0; m < nMints; m++ ) { @@ -2991,15 +2991,83 @@ void Gia_ManRelPrint( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_W printf( "\n" ); } } +void Gia_ManRelPrint2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel ) +{ + int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + int i, Id, m, nMints = 1 << Vec_IntSize(vObjs); + int nWordsM = Abc_Truth6WordNum(Vec_IntSize(vObjs)); + Vec_Wrd_t * vRes = Vec_WrdStart( 64*nWords * nWordsM ); + printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) ); + for ( w = 0; w < 64*nWords; w++ ) + { + int iMint = 0; + int nValid = 0; + Gia_ManForEachCiId( p, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + printf( " " ); + Vec_IntForEachEntry( vObjs, Id, i ) + { + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ) + iMint |= 1 << i; + } + printf( " " ); + Gia_ManForEachCoId( p, Id, i ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) ); + printf( " " ); + for ( m = 0; m < nMints; m++ ) + { + int Count = 0; + Gia_ManForEachCoId( p, Id, i ) + Count += Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w); + printf( "%d", Count == 0 ); + nValid += Count > 0; + if ( Count == 0 ) + Abc_TtSetBit( Vec_WrdEntryP(vRes, w*nWordsM), m ); + } + printf( " " ); + for ( m = 0; m < nMints; m++ ) + printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), m) ); + printf( " " ); + assert( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint) ); + for ( i = 0; i < Vec_IntSize(vObjs); i++ ) + if ( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint ^ (1 << i)) ) + printf( "-" ); + else + printf( "%d", (iMint >> i) & 1 ); + printf( " %d", nMints-nValid ); + printf( "\n" ); + } + Vec_WrdFree( vRes ); +} Vec_Int_t * Gia_ManRelInitObjs() { - Vec_Int_t * vRes = Vec_IntAlloc( 3 ); - Vec_IntPush( vRes, 41 ); - Vec_IntPush( vRes, 46 ); + Vec_Int_t * vRes = Vec_IntAlloc( 10 ); + /* + Vec_IntPush( vRes, 33 ); + Vec_IntPush( vRes, 52 ); Vec_IntPush( vRes, 53 ); + Vec_IntPush( vRes, 65 ); + Vec_IntPush( vRes, 79 ); + Vec_IntPush( vRes, 81 ); + */ + /* + Vec_IntPush( vRes, 60 ); + Vec_IntPush( vRes, 61 ); + Vec_IntPush( vRes, 71 ); + Vec_IntPush( vRes, 72 ); + */ + /* + Vec_IntPush( vRes, 65 ); + Vec_IntPush( vRes, 79 ); + Vec_IntPush( vRes, 81 ); + */ + Vec_IntPush( vRes, 52 ); + Vec_IntPush( vRes, 54 ); + Vec_IntPrint( vRes ); return vRes; } -void Gia_ManRelDeriveTest( Gia_Man_t * p ) +void Gia_ManRelDeriveTest2( Gia_Man_t * p ) { Vec_Int_t * vObjs = Gia_ManRelInitObjs(); Vec_Wrd_t * vSims, * vRel, * vRel2; int nWords; @@ -3009,14 +3077,189 @@ void Gia_ManRelDeriveTest( Gia_Man_t * p ) vSims = Gia_ManSimPatSim( p ); vRel = Gia_ManRelDerive( p, vObjs, vSims ); vRel2 = Gia_ManRelDerive2( p, vObjs, vSims ); - assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) ); - Gia_ManRelPrint( p, vObjs, vSims, vRel ); + //assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) ); + Gia_ManRelPrint2( p, vObjs, vSims, vRel ); Vec_WrdFree( vRel2 ); Vec_WrdFree( vRel ); Vec_WrdFree( vSims ); Vec_IntFree( vObjs ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManRelInitIns() +{ + Vec_Int_t * vRes = Vec_IntAlloc( 10 ); + Vec_IntPush( vRes, 12 ); + Vec_IntPush( vRes, 18 ); + Vec_IntPush( vRes, 21 ); + Vec_IntPush( vRes, 34 ); + Vec_IntPush( vRes, 45 ); + Vec_IntPush( vRes, 59 ); + return vRes; +} +Vec_Int_t * Gia_ManRelInitOuts() +{ + Vec_Int_t * vRes = Vec_IntAlloc( 10 ); + Vec_IntPush( vRes, 65 ); + Vec_IntPush( vRes, 66 ); + return vRes; +} +Vec_Int_t * Gia_ManRelInitMffc( Gia_Man_t * p, Vec_Int_t * vOuts ) +{ + Gia_Obj_t * pObj; int i; + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_IntSort( vOuts, 0 ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vOuts, p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachCo( p, pObj, i ) + if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) ) + Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachAndReverse( p, pObj, i ) + if ( Gia_ObjIsTravIdPrevious(p, pObj) ) + continue; + else if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + { + if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) ) + Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) ); + if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin1(pObj)) ) + Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin1(pObj) ); + } + Gia_ManForEachAnd( p, pObj, i ) + if ( !Gia_ObjIsTravIdCurrent(p, pObj) ) + Vec_IntPush( vRes, i ); + printf( "MFFC: " ); + Vec_IntPrint( vRes ); + return vRes; +} +Vec_Int_t * Gia_ManRelInitDivs( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vOuts ) +{ + Gia_Obj_t * pObj; int i; + Vec_Int_t * vMffc = Gia_ManRelInitMffc( p, vOuts ); + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_IntSort( vIns, 0 ); + + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vMffc, p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + Vec_IntFree( vMffc ); + + Vec_IntPush( vRes, 0 ); + Vec_IntAppend( vRes, vIns ); + + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vIns, p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + continue; + else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) ) + { + if ( !Gia_ObjIsTravIdPrevious(p, pObj) ) + Vec_IntPush( vRes, i ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + printf( "Divisors: " ); + Vec_IntPrint( vRes ); + return vRes; +} + +Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts ) +{ + Vec_Int_t * vRes = Vec_IntStartFull( 1 << Vec_IntSize(vIns) ); + int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + for ( w = 0; w < 64*nWords; w++ ) + { + int i, iObj, iMint = 0, iMint2 = 0; + Vec_IntForEachEntry( vIns, iObj, i ) + if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) ) + iMint |= 1 << i; + if ( Vec_IntEntry(vRes, iMint) >= 0 ) + continue; + Vec_IntForEachEntry( vOuts, iObj, i ) + if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) ) + iMint2 |= 1 << i; + Vec_IntWriteEntry( vRes, iMint, iMint2 ); + } + return vRes; +} + +void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) +{ + extern void Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fVerbose ); + + int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); + Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); + Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints ); + int Entry0 = Vec_IntEntry( vRel, 0 ); + + word Value, Phase = 0; + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + Vec_IntForEachEntry( vDivs, iObj, i ) + if ( Vec_WrdEntry(vSims, iObj*nWords) & 1 ) + Phase |= 1 << i; + + assert( Entry0 >= 0 ); + printf( "Entry0 = %d\n", Entry0 ); + Entry0 ^= 1; +// for ( m = 0; m < nMints; m++ ) + Vec_IntForEachEntry( vRel, Entry, m ) + { + if ( Entry == -1 ) + continue; + Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, iMint), Entry0 ^ Entry ); + + Value = 0; + Vec_IntForEachEntry( vDivs, iObj, i ) + if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), m) ) + Abc_TtSetBit( &Value, i ); + Vec_WrdEntryP(vSimsOut, iMint)[0] = Value ^ Phase; + + iMint++; + } + assert( iMint == nMints ); + printf( "Created %d minterms.\n", iMint ); + Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 1 ); + Vec_WrdFree( vSimsIn ); + Vec_WrdFree( vSimsOut ); +} +void Gia_ManRelDeriveTest( Gia_Man_t * p ) +{ + Vec_Int_t * vIns = Gia_ManRelInitIns(); + Vec_Int_t * vOuts = Gia_ManRelInitOuts(); + Vec_Wrd_t * vSims; Vec_Int_t * vRel, * vDivs; int nWords; + Vec_WrdFreeP( &p->vSimsPi ); + p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + vSims = Gia_ManSimPatSim( p ); + vRel = Gia_ManRelDeriveSimple( p, vSims, vIns, vOuts ); + vDivs = Gia_ManRelInitDivs( p, vIns, vOuts ); + //printf( "Neg = %d\n", Vec_IntCountEntry(vRel, -1) ); + + Gia_ManRelSolve( p, vSims, vIns, vOuts, vRel, vDivs ); + + Vec_IntFree( vDivs ); + Vec_IntPrint( vRel ); + Vec_IntFree( vRel ); + Vec_WrdFree( vSims ); + Vec_IntFree( vIns ); + Vec_IntFree( vOuts ); +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3 From 34d571a562dffbec17c97c788bcfaede5b8734f8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 30 Aug 2022 12:30:15 -0700 Subject: Various changes. --- src/aig/gia/giaSimBase.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 6f825549..c8e25f85 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -22,6 +22,7 @@ #include "misc/util/utilTruth.h" #include "misc/extra/extra.h" //#include +#include "aig/miniaig/miniaig.h" ABC_NAMESPACE_IMPL_START @@ -3198,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) { - extern void Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fVerbose ); + extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fVerbose ); int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); -- cgit v1.2.3 From 138c381f76bcc1106a2fd3dcd40fcaee89c84e81 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 30 Aug 2022 13:19:14 -0700 Subject: Testing utility code. --- src/aig/gia/giaUtil.c | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'src/aig') diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index d8130550..dfddc693 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -3130,6 +3130,37 @@ void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName ) } } + +/**Function************************************************************* + + Synopsis [Transform flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintArray( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int i, nSize = Gia_ManObjNum(p); + printf( "static int s_ArraySize = %d;\n", nSize ); + printf( "static int s_ArrayData[%d] = {\n", 2*nSize ); + printf( " 0, 0," ); + printf( "\n " ); + Gia_ManForEachCi( p, pObj, i ) + printf( "0, 0, " ); + printf( "\n " ); + Gia_ManForEachAnd( p, pObj, i ) + printf( "%d, %d, ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit1p(p, pObj) ); + printf( "\n " ); + Gia_ManForEachCo( p, pObj, i ) + printf( "%d, %d, ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) ); + printf( "\n" ); + printf( "};\n" ); + +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3 From 0ed81b34f1048a10aa1b6785c2fb65b526c77b5a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 30 Aug 2022 13:28:59 -0700 Subject: Compiler warnings. --- src/aig/gia/giaSimBase.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index c8e25f85..75a6d653 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) { - extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fVerbose ); + extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose ); int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); @@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In } assert( iMint == nMints ); printf( "Created %d minterms.\n", iMint ); - Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 1 ); + Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); } -- cgit v1.2.3 From 96b9ef2ce5347f380c1a07e1de1887a177f7e37e Mon Sep 17 00:00:00 2001 From: Yukio Miyasaka Date: Sat, 17 Sep 2022 15:42:36 -0700 Subject: import ttopt --- src/aig/gia/giaTtopt.cpp | 1207 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + 2 files changed, 1208 insertions(+) create mode 100644 src/aig/gia/giaTtopt.cpp (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp new file mode 100644 index 00000000..eca0989d --- /dev/null +++ b/src/aig/gia/giaTtopt.cpp @@ -0,0 +1,1207 @@ +// Author : Yukio Miyasaka +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "gia.h" + +ABC_NAMESPACE_IMPL_START + +namespace Ttopt { + +struct PairHasher { + std::size_t operator()(const std::pair & k) const { + std::hash hasher; + std::size_t seed = hasher(k.first) + 0x9e3779b9; + seed = hasher(k.second) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + return seed; + } +}; + +class TruthTable { +public: + const int ww = 64; // word width + const int lww = 6; // log word width + typedef std::bitset<64> bsw; + + int nInputs; + int nSize; + int nTotalSize; + int nOutputs; + std::vector t; + + std::vector > vvIndices; + std::vector > vvRedundantIndices; + std::vector vLevels; + + std::vector > savedt; + std::vector > > vvIndicesSaved; + std::vector > > vvRedundantIndicesSaved; + std::vector > vLevelsSaved; + + std::mt19937 rng; + static const word ones[]; + static const word swapmask[]; + + TruthTable(int nInputs, int nOutputs): nInputs(nInputs), nOutputs(nOutputs) { + if(nInputs >= lww) { + nSize = 1 << (nInputs - lww); + nTotalSize = nSize * nOutputs; + t.resize(nTotalSize); + } else { + nSize = 0; + nTotalSize = ((1 << nInputs) * nOutputs + ww - 1) / ww; + t.resize(nTotalSize); + } + vLevels.resize(nInputs); + std::iota(vLevels.begin(), vLevels.end(), 0); + } + + std::string BinaryToString(int bin, int size) { + std::string str; + for(int i = 0; i < size; i++) { + str += (bin & 1) + '0'; + bin = bin >> 1; + } + return str; + } + void GeneratePla(std::string filename) { + std::ofstream f(filename); + f << ".i " << nInputs << std::endl; + f << ".o " << nOutputs << std::endl; + if(nSize) { + for(int index = 0; index < nSize; index++) { + for(int pos = 0; pos < ww; pos++) { + int pat = (index << lww) + pos; + f << BinaryToString(pat, nInputs) << " "; + for(int i = 0; i < nOutputs; i++) { + f << ((t[nSize * i + index] >> pos) & 1); + } + f << std::endl; + } + } + } else { + for(int pos = 0; pos < (1 << nInputs); pos++) { + f << BinaryToString(pos, nInputs) << " "; + for(int i = 0; i < nOutputs; i++) { + int padding = i * (1 << nInputs); + f << ((t[padding / ww] >> (pos + padding % ww)) & 1); + } + f << std::endl; + } + } + } + + virtual void Save(uint i) { + if(savedt.size() < i + 1) { + savedt.resize(i + 1); + vLevelsSaved.resize(i + 1); + } + savedt[i] = t; + vLevelsSaved[i] = vLevels; + } + + virtual void Load(uint i) { + assert(i < savedt.size()); + t = savedt[i]; + vLevels = vLevelsSaved[i]; + } + + virtual void SaveIndices(uint i) { + if(vvIndicesSaved.size() < i + 1) { + vvIndicesSaved.resize(i + 1); + vvRedundantIndicesSaved.resize(i + 1); + } + vvIndicesSaved[i] = vvIndices; + vvRedundantIndicesSaved[i] = vvRedundantIndices; + } + + virtual void LoadIndices(uint i) { + vvIndices = vvIndicesSaved[i]; + vvRedundantIndices = vvRedundantIndicesSaved[i]; + } + + word GetValue(int index_lev, int lev) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + return (t[index] >> pos) & ones[logwidth]; + } + + int IsEq(int index1, int index2, int lev, bool fCompl = false) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + bool fEq = true; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + fEq &= t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i]; + fCompl &= t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i]; + } + } else { + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + fEq &= !value; + fCompl &= !(value ^ ones[logwidth]); + } + return 2 * fCompl + fEq; + } + + bool Imply(int index1, int index2, int lev) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + if(t[nScopeSize * index1 + i] & ~t[nScopeSize * index2 + i]) { + return false; + } + } + return true; + } + return !(GetValue(index1, lev) & (GetValue(index2, lev) ^ ones[logwidth])); + } + + int BDDNodeCountLevel(int lev) { + return vvIndices[lev].size() - vvRedundantIndices[lev].size(); + } + + int BDDNodeCount() { + int count = 1; // const node + for(int i = 0; i < nInputs; i++) { + count += BDDNodeCountLevel(i); + } + return count; + } + + int BDDFind(int index, int lev) { + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + bool fZero = true; + bool fOne = true; + for(int i = 0; i < nScopeSize && (fZero || fOne); i++) { + word value = t[nScopeSize * index + i]; + fZero &= !value; + fOne &= !(~value); + } + if(fZero || fOne) { + return -2 ^ fOne; + } + for(uint j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; + bool fEq = true; + bool fCompl = true; + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + fEq &= t[nScopeSize * index + i] == t[nScopeSize * index2 + i]; + fCompl &= t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i]; + } + if(fEq || fCompl) { + return (j << 1) ^ fCompl; + } + } + } else { + word value = GetValue(index, lev); + if(!value) { + return -2; + } + if(!(value ^ ones[logwidth])) { + return -1; + } + for(uint j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; + word value2 = value ^ GetValue(index2, lev); + if(!(value2)) { + return j << 1; + } + if(!(value2 ^ ones[logwidth])) { + return (j << 1) ^ 1; + } + } + } + return -3; + } + + virtual int BDDBuildOne(int index, int lev) { + int r = BDDFind(index, lev); + if(r >= -2) { + return r; + } + vvIndices[lev].push_back(index); + return (vvIndices[lev].size() - 1) << 1; + } + + virtual void BDDBuildStartup() { + vvIndices.clear(); + vvIndices.resize(nInputs); + vvRedundantIndices.clear(); + vvRedundantIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + BDDBuildOne(i, 0); + } + } + + virtual void BDDBuildLevel(int lev) { + for(int index: vvIndices[lev-1]) { + int cof0 = BDDBuildOne(index << 1, lev); + int cof1 = BDDBuildOne((index << 1) ^ 1, lev); + if(cof0 == cof1) { + vvRedundantIndices[lev-1].push_back(index); + } + } + } + + virtual int BDDBuild() { + BDDBuildStartup(); + for(int i = 1; i < nInputs; i++) { + BDDBuildLevel(i); + } + return BDDNodeCount(); + } + + virtual int BDDRebuild(int lev) { + vvIndices[lev].clear(); + vvIndices[lev+1].clear(); + for(int i = lev; i < lev + 2; i++) { + if(!i) { + for(int j = 0; j < nOutputs; j++) { + BDDBuildOne(j, 0); + } + } else { + vvRedundantIndices[i-1].clear(); + BDDBuildLevel(i); + } + } + if(lev < nInputs - 2) { + vvRedundantIndices[lev+1].clear(); + for(int index: vvIndices[lev+1]) { + if(IsEq(index << 1, (index << 1) ^ 1, lev + 2)) { + vvRedundantIndices[lev+1].push_back(index); + } + } + } + return BDDNodeCount(); + } + + virtual void Swap(int lev) { + assert(lev < nInputs - 1); + auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); + auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::swap(*it0, *it1); + if(nInputs - lev - 1 > lww) { + int nScopeSize = 1 << (nInputs - lev - 2 - lww); + for(int i = nScopeSize; i < nTotalSize; i += (nScopeSize << 2)) { + for(int j = 0; j < nScopeSize; j++) { + std::swap(t[i + j], t[i + nScopeSize + j]); + } + } + } else if(nInputs - lev - 1 == lww) { + for(int i = 0; i < nTotalSize; i += 2) { + t[i+1] ^= t[i] >> (ww / 2); + t[i] ^= t[i+1] << (ww / 2); + t[i+1] ^= t[i] >> (ww / 2); + } + } else { + for(int i = 0; i < nTotalSize; i++) { + int d = nInputs - lev - 2; + int shamt = 1 << d; + t[i] ^= (t[i] >> shamt) & swapmask[d]; + t[i] ^= (t[i] & swapmask[d]) << shamt; + t[i] ^= (t[i] >> shamt) & swapmask[d]; + } + } + } + + void SwapIndex(int &index, int d) { + if((index >> d) % 4 == 1) { + index += 1 << d; + } else if((index >> d) % 4 == 2) { + index -= 1 << d; + } + } + + virtual int BDDSwap(int lev) { + Swap(lev); + for(int i = lev + 2; i < nInputs; i++) { + for(uint j = 0; j < vvIndices[i].size(); j++) { + SwapIndex(vvIndices[i][j], i - (lev + 2)); + } + } + // swapping vvRedundantIndices is unnecessary for node counting + return BDDRebuild(lev); + } + + int SiftReo() { + int best = BDDBuild(); + Save(0); + SaveIndices(0); + std::vector vars(nInputs); + std::iota(vars.begin(), vars.end(), 0); + std::sort(vars.begin(), vars.end(), [&](int i1, int i2) {return BDDNodeCountLevel(vLevels[i1]) > BDDNodeCountLevel(vLevels[i2]);}); + bool turn = true; + for(int var: vars) { + bool updated = false; + int lev = vLevels[var]; + for(int i = lev; i < nInputs - 1; i++) { + int count = BDDSwap(i); + if(best > count) { + best = count; + updated = true; + Save(turn); + SaveIndices(turn); + } + } + if(lev) { + Load(!turn); + LoadIndices(!turn); + for(int i = lev - 1; i >= 0; i--) { + int count = BDDSwap(i); + if(best > count) { + best = count; + updated = true; + Save(turn); + SaveIndices(turn); + } + } + } + turn ^= updated; + Load(!turn); + LoadIndices(!turn); + } + return best; + } + + void Reo(std::vector vLevelsNew) { + for(int i = 0; i < nInputs; i++) { + int var = std::find(vLevelsNew.begin(), vLevelsNew.end(), i) - vLevelsNew.begin(); + int lev = vLevels[var]; + if(lev < i) { + for(int j = lev; j < i; j++) { + Swap(j); + } + } else if(lev > i) { + for(int j = lev - 1; j >= i; j--) { + Swap(j); + } + } + } + assert(vLevels == vLevelsNew); + } + + int RandomSiftReo(int nRound) { + int best = SiftReo(); + Save(2); + for(int i = 0; i < nRound; i++) { + std::vector vLevelsNew(nInputs); + std::iota(vLevelsNew.begin(), vLevelsNew.end(), 0); + std::shuffle(vLevelsNew.begin(), vLevelsNew.end(), rng); + Reo(vLevelsNew); + int r = SiftReo(); + if(best > r) { + best = r; + Save(2); + } + } + Load(2); + return best; + } + + int BDDGenerateAigRec(Gia_Man_t *pNew, std::vector const &vInputs, std::vector > &vvNodes, int index, int lev) { + int r = BDDFind(index, lev); + if(r >= 0) { + return vvNodes[lev][r >> 1] ^ (r & 1); + } + if(r >= -2) { + return r + 2; + } + int cof0 = BDDGenerateAigRec(pNew, vInputs, vvNodes, index << 1, lev + 1); + int cof1 = BDDGenerateAigRec(pNew, vInputs, vvNodes, (index << 1) ^ 1, lev + 1); + if(cof0 == cof1) { + return cof0; + } + int node; + if(Imply(index << 1, (index << 1) ^ 1, lev + 1)) { + node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev], cof1), cof0); + } else if(Imply((index << 1) ^ 1, index << 1, lev + 1)) { + node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev] ^ 1, cof0), cof1); + } else { + node = Gia_ManHashMux(pNew, vInputs[lev], cof1, cof0); + } + vvIndices[lev].push_back(index); + vvNodes[lev].push_back(node); + return node; + } + + virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) { + vvIndices.clear(); + vvIndices.resize(nInputs); + std::vector > vvNodes(nInputs); + std::vector vInputs(nInputs); + for(int i = 0; i < nInputs; i++) { + vInputs[vLevels[i]] = Vec_IntEntry(vSupp, nInputs - i - 1) << 1; + } + for(int i = 0; i < nOutputs; i++) { + int node = BDDGenerateAigRec(pNew, vInputs, vvNodes, i, 0); + Gia_ManAppendCo(pNew, node); + } + } +}; + +const word TruthTable::ones[7] = {ABC_CONST(0x0000000000000001), + ABC_CONST(0x0000000000000003), + ABC_CONST(0x000000000000000f), + ABC_CONST(0x00000000000000ff), + ABC_CONST(0x000000000000ffff), + ABC_CONST(0x00000000ffffffff), + ABC_CONST(0xffffffffffffffff)}; + +const word TruthTable::swapmask[5] = {ABC_CONST(0x2222222222222222), + ABC_CONST(0x0c0c0c0c0c0c0c0c), + ABC_CONST(0x00f000f000f000f0), + ABC_CONST(0x0000ff000000ff00), + ABC_CONST(0x00000000ffff0000)}; + +class TruthTableReo : public TruthTable { +public: + bool fBuilt = false; + std::vector > vvChildren; + std::vector > > vvChildrenSaved; + + TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {} + + void Save(uint i) override { + if(vLevelsSaved.size() < i + 1) { + vLevelsSaved.resize(i + 1); + } + vLevelsSaved[i] = vLevels; + } + + void Load(uint i) override { + assert(i < vLevelsSaved.size()); + vLevels = vLevelsSaved[i]; + } + + void SaveIndices(uint i) override { + TruthTable::SaveIndices(i); + if(vvChildrenSaved.size() < i + 1) { + vvChildrenSaved.resize(i + 1); + } + vvChildrenSaved[i] = vvChildren; + } + + void LoadIndices(uint i) override { + TruthTable::LoadIndices(i); + vvChildren = vvChildrenSaved[i]; + } + + void BDDBuildStartup() override { + vvChildren.clear(); + vvChildren.resize(nInputs); + TruthTable::BDDBuildStartup(); + } + + void BDDBuildLevel(int lev) override { + for(int index: vvIndices[lev-1]) { + int cof0 = BDDBuildOne(index << 1, lev); + int cof1 = BDDBuildOne((index << 1) ^ 1, lev); + vvChildren[lev-1].push_back(cof0); + vvChildren[lev-1].push_back(cof1); + if(cof0 == cof1) { + vvRedundantIndices[lev-1].push_back(index); + } + } + } + + int BDDBuild() override { + if(fBuilt) { + return BDDNodeCount(); + } + fBuilt = true; + BDDBuildStartup(); + for(int i = 1; i < nInputs + 1; i++) { + BDDBuildLevel(i); + } + return BDDNodeCount(); + } + + int BDDRebuildOne(int index, int cof0, int cof1, int lev, std::unordered_map, int, PairHasher> &unique, std::vector &vChildrenLow) { + if(cof0 < 0 && cof0 == cof1) { + return cof0; + } + bool fCompl = cof0 & 1; + if(fCompl) { + cof0 ^= 1; + cof1 ^= 1; + } + if(unique.count({cof0, cof1})) { + return (unique[{cof0, cof1}] << 1) ^ fCompl; + } + vvIndices[lev].push_back(index); + unique[{cof0, cof1}] = vvIndices[lev].size() - 1; + vChildrenLow.push_back(cof0); + vChildrenLow.push_back(cof1); + if(cof0 == cof1) { + vvRedundantIndices[lev].push_back(index); + } + return ((vvIndices[lev].size() - 1) << 1) ^ fCompl; + } + + int BDDRebuild(int lev) override { + vvRedundantIndices[lev].clear(); + vvRedundantIndices[lev+1].clear(); + std::vector vChildrenHigh; + std::vector vChildrenLow; + std::unordered_map, int, PairHasher> unique; + unique.reserve(2 * vvIndices[lev+1].size()); + vvIndices[lev+1].clear(); + for(uint i = 0; i < vvIndices[lev].size(); i++) { + int index = vvIndices[lev][i]; + int cof0index = vvChildren[lev][i+i] >> 1; + int cof1index = vvChildren[lev][i+i+1] >> 1; + bool cof0c = vvChildren[lev][i+i] & 1; + bool cof1c = vvChildren[lev][i+i+1] & 1; + int cof00, cof01, cof10, cof11; + if(cof0index < 0) { + cof00 = -2 ^ cof0c; + cof01 = -2 ^ cof0c; + } else { + cof00 = vvChildren[lev+1][cof0index+cof0index] ^ cof0c; + cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ cof0c; + } + if(cof1index < 0) { + cof10 = -2 ^ cof1c; + cof11 = -2 ^ cof1c; + } else { + cof10 = vvChildren[lev+1][cof1index+cof1index] ^ cof1c; + cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ cof1c; + } + int newcof0 = BDDRebuildOne(index << 1, cof00, cof10, lev + 1, unique, vChildrenLow); + int newcof1 = BDDRebuildOne((index << 1) ^ 1, cof01, cof11, lev + 1, unique, vChildrenLow); + vChildrenHigh.push_back(newcof0); + vChildrenHigh.push_back(newcof1); + if(newcof0 == newcof1) { + vvRedundantIndices[lev].push_back(index); + } + } + vvChildren[lev] = vChildrenHigh; + vvChildren[lev+1] = vChildrenLow; + return BDDNodeCount(); + } + + void Swap(int lev) override { + assert(lev < nInputs - 1); + auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); + auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::swap(*it0, *it1); + BDDRebuild(lev); + } + + int BDDSwap(int lev) override { + Swap(lev); + return BDDNodeCount(); + } + + virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) override { + abort(); + } +}; + +class TruthTableRewrite : public TruthTable { +public: + TruthTableRewrite(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {} + + void SetValue(int index_lev, int lev, word value) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + t[index] &= ~(ones[logwidth] << pos); + t[index] ^= value << pos; + } + + void CopyFunc(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + if(!fCompl) { + if(index2 < 0) { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = 0; + } + } else { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = t[nScopeSize * index2 + i]; + } + } + } else { + if(index2 < 0) { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = ones[lww]; + } + } else { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = ~t[nScopeSize * index2 + i]; + } + } + } + } else { + word value = 0; + if(index2 >= 0) { + value = GetValue(index2, lev); + } + if(fCompl) { + value ^= ones[logwidth]; + } + SetValue(index1, lev, value); + } + } + + void ShiftToMajority(int index, int lev) { + assert(index >= 0); + int logwidth = nInputs - lev; + int count = 0; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + count += bsw(t[nScopeSize * index + i]).count(); + } + } else { + count = bsw(GetValue(index, lev)).count(); + } + bool majority = count > (1 << (logwidth - 1)); + CopyFunc(index, -1, lev, majority); + } +}; + +class TruthTableCare : public TruthTableRewrite { +public: + std::vector originalt; + std::vector caret; + std::vector care; + + std::vector > > vvMergedIndices; + + std::vector > savedcare; + std::vector > > > vvMergedIndicesSaved; + + TruthTableCare(int nInputs, int nOutputs): TruthTableRewrite(nInputs, nOutputs) { + if(nSize) { + care.resize(nSize); + } else { + care.resize(1); + } + } + + void Save(uint i) override { + TruthTable::Save(i); + if(savedcare.size() < i + 1) { + savedcare.resize(i + 1); + } + savedcare[i] = care; + } + + void Load(uint i) override { + TruthTable::Load(i); + care = savedcare[i]; + } + + void SaveIndices(uint i) override { + TruthTable::SaveIndices(i); + if(vvMergedIndicesSaved.size() < i + 1) { + vvMergedIndicesSaved.resize(i + 1); + } + vvMergedIndicesSaved[i] = vvMergedIndices; + } + + void LoadIndices(uint i) override { + TruthTable::LoadIndices(i); + vvMergedIndices = vvMergedIndicesSaved[i]; + } + + void Swap(int lev) override { + TruthTable::Swap(lev); + if(nInputs - lev - 1 > lww) { + int nScopeSize = 1 << (nInputs - lev - 2 - lww); + for(int i = nScopeSize; i < nSize; i += (nScopeSize << 2)) { + for(int j = 0; j < nScopeSize; j++) { + std::swap(care[i + j], care[i + nScopeSize + j]); + } + } + } else if(nInputs - lev - 1 == lww) { + for(int i = 0; i < nSize; i += 2) { + care[i+1] ^= care[i] >> (ww / 2); + care[i] ^= care[i+1] << (ww / 2); + care[i+1] ^= care[i] >> (ww / 2); + } + } else { + for(int i = 0; i < nSize || (i == 0 && !nSize); i++) { + int d = nInputs - lev - 2; + int shamt = 1 << d; + care[i] ^= (care[i] >> shamt) & swapmask[d]; + care[i] ^= (care[i] & swapmask[d]) << shamt; + care[i] ^= (care[i] >> shamt) & swapmask[d]; + } + } + } + + void RestoreCare() { + caret.clear(); + if(nSize) { + for(int i = 0; i < nOutputs; i++) { + caret.insert(caret.end(), care.begin(), care.end()); + } + } else { + caret.resize(nTotalSize); + for(int i = 0; i < nOutputs; i++) { + int padding = i * (1 << nInputs); + caret[padding / ww] |= care[0] << (padding % ww); + } + } + } + + word GetCare(int index_lev, int lev) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + return (caret[index] >> pos) & ones[logwidth]; + } + + void CopyFuncMasked(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + word value = t[nScopeSize * index2 + i]; + if(fCompl) { + value = ~value; + } + word cvalue = caret[nScopeSize * index2 + i]; + t[nScopeSize * index1 + i] &= ~cvalue; + t[nScopeSize * index1 + i] |= cvalue & value; + } + } else { + word one = ones[logwidth]; + word value1 = GetValue(index1, lev); + word value2 = GetValue(index2, lev); + if(fCompl) { + value2 ^= one; + } + word cvalue = GetCare(index2, lev); + value1 &= cvalue ^ one; + value1 |= cvalue & value2; + SetValue(index1, lev, value1); + } + } + + bool IsDC(int index, int lev) { + if(nInputs - lev > lww) { + int nScopeSize = 1 << (nInputs - lev - lww); + for(int i = 0; i < nScopeSize; i++) { + if(caret[nScopeSize * index + i]) { + return false; + } + } + } else if(GetCare(index, lev)) { + return false; + } + return true; + } + + int Include(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + bool fEq = true; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word cvalue = caret[nScopeSize * index2 + i]; + if(~caret[nScopeSize * index1 + i] & cvalue) { + return 0; + } + word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + } else { + word cvalue = GetCare(index2, lev); + if((GetCare(index1, lev) ^ ones[logwidth]) & cvalue) { + return 0; + } + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + fEq &= !(value & cvalue); + fCompl &= !((value ^ ones[logwidth]) & cvalue); + } + return 2 * fCompl + fEq; + } + + int Intersect(int index1, int index2, int lev, bool fCompl, bool fEq = true) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i]; + word cvalue = caret[nScopeSize * index1 + i] & caret[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + } else { + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + word cvalue = GetCare(index1, lev) & GetCare(index2, lev); + fEq &= !(value & cvalue); + fCompl &= !((value ^ ones[logwidth]) & cvalue); + } + return 2 * fCompl + fEq; + } + + void MergeCare(int index1, int index2, int lev) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + caret[nScopeSize * index1 + i] |= caret[nScopeSize * index2 + i]; + } + } else { + word value = GetCare(index2, lev); + int index = index1 >> (lww - logwidth); + int pos = (index1 % (1 << (lww - logwidth))) << logwidth; + caret[index] |= value << pos; + } + } + + void Merge(int index1, int index2, int lev, bool fCompl) { + MergeCare(index1, index2, lev); + vvMergedIndices[lev].push_back({(index1 << 1) ^ fCompl, index2}); + } + + int BDDBuildOne(int index, int lev) override { + int r = BDDFind(index, lev); + if(r >= -2) { + if(r >= 0) { + Merge(vvIndices[lev][r >> 1], index, lev, r & 1); + } + return r; + } + vvIndices[lev].push_back(index); + return (vvIndices[lev].size() - 1) << 1; + } + + void CompleteMerge() { + for(int i = nInputs - 1; i >= 0; i--) { + for(auto it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) { + CopyFunc((*it).second, (*it).first >> 1, i, (*it).first & 1); + } + } + } + + void BDDBuildStartup() override { + RestoreCare(); + vvIndices.clear(); + vvIndices.resize(nInputs); + vvRedundantIndices.clear(); + vvRedundantIndices.resize(nInputs); + vvMergedIndices.clear(); + vvMergedIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + if(!IsDC(i, 0)) { + BDDBuildOne(i, 0); + } + } + } + + virtual void BDDRebuildByMerge(int lev) { + for(auto &p: vvMergedIndices[lev]) { + MergeCare(p.first >> 1, p.second, lev); + } + } + + int BDDRebuild(int lev) override { + RestoreCare(); + for(int i = lev; i < nInputs; i++) { + vvIndices[i].clear(); + vvMergedIndices[i].clear(); + if(i) { + vvRedundantIndices[i-1].clear(); + } + } + for(int i = 0; i < lev; i++) { + BDDRebuildByMerge(i); + } + for(int i = lev; i < nInputs; i++) { + if(!i) { + for(int j = 0; j < nOutputs; j++) { + if(!IsDC(j, 0)) { + BDDBuildOne(j, 0); + } + } + } else { + BDDBuildLevel(i); + } + } + return BDDNodeCount(); + } + + int BDDSwap(int lev) override { + Swap(lev); + return BDDRebuild(lev); + } + + void OptimizationStartup() { + originalt = t; + RestoreCare(); + vvIndices.clear(); + vvIndices.resize(nInputs); + vvMergedIndices.clear(); + vvMergedIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + if(!IsDC(i, 0)) { + BDDBuildOne(i, 0); + } else { + ShiftToMajority(i, 0); + } + } + } + + virtual void Optimize() { + OptimizationStartup(); + for(int i = 1; i < nInputs; i++) { + for(int index: vvIndices[i-1]) { + BDDBuildOne(index << 1, i); + BDDBuildOne((index << 1) ^ 1, i); + } + } + CompleteMerge(); + } +}; + +class TruthTableLevelTSM : public TruthTableCare { +public: + TruthTableLevelTSM(int nInputs, int nOutputs): TruthTableCare(nInputs, nOutputs) {} + + int BDDFindTSM(int index, int lev) { + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + bool fZero = true; + bool fOne = true; + for(int i = 0; i < nScopeSize && (fZero || fOne); i++) { + word value = t[nScopeSize * index + i]; + word cvalue = caret[nScopeSize * index + i]; + fZero &= !(value & cvalue); + fOne &= !(~value & cvalue); + } + if(fZero || fOne) { + return -2 ^ fOne; + } + for(int index2: vvIndices[lev]) { + bool fEq = true; + bool fCompl = true; + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word value = t[nScopeSize * index + i] ^ t[nScopeSize * index2 + i]; + word cvalue = caret[nScopeSize * index + i] & caret[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + if(fEq || fCompl) { + return (index2 << 1) ^ !fEq; + } + } + } else { + word one = ones[logwidth]; + word value = GetValue(index, lev); + word cvalue = GetCare(index, lev); + if(!(value & cvalue)) { + return -2; + } + if(!((value ^ one) & cvalue)) { + return -1; + } + for(int index2: vvIndices[lev]) { + word value2 = value ^ GetValue(index2, lev); + word cvalue2 = cvalue & GetCare(index2, lev); + if(!(value2 & cvalue2)) { + return index2 << 1; + } + if(!((value2 ^ one) & cvalue2)) { + return (index2 << 1) ^ 1; + } + } + } + return -3; + } + + int BDDBuildOne(int index, int lev) override { + int r = BDDFindTSM(index, lev); + if(r >= -2) { + if(r >= 0) { + CopyFuncMasked(r >> 1, index, lev, r & 1); + Merge(r >> 1, index, lev, r & 1); + } else { + vvMergedIndices[lev].push_back({r, index}); + } + return r; + } + vvIndices[lev].push_back(index); + return index << 1; + } + + int BDDBuild() override { + TruthTable::Save(3); + int r = TruthTable::BDDBuild(); + TruthTable::Load(3); + return r; + } + + void BDDRebuildByMerge(int lev) override { + for(auto &p: vvMergedIndices[lev]) { + if(p.first >= 0) { + CopyFuncMasked(p.first >> 1, p.second, lev, p.first & 1); + MergeCare(p.first >> 1, p.second, lev); + } + } + } + + int BDDRebuild(int lev) override { + TruthTable::Save(3); + int r = TruthTableCare::BDDRebuild(lev); + TruthTable::Load(3); + return r; + } +}; + +} + +extern "C" +Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts ); + +extern "C" +Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vSupp; + word v; + word * pTruth; + int i, g, k, nInputs; + Gia_ManLevelNum( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManForEachCi( p, pObj, k ) + Gia_ManAppendCi( pNew ); + Gia_ObjComputeTruthTableStart( p, nIns ); + Gia_ManHashStart( pNew ); + for ( g = 0; g < Gia_ManCoNum(p); g += nOuts ) + { + vSupp = Gia_ManCollectSuppNew( p, g, nOuts ); + nInputs = Vec_IntSize( vSupp ); + Ttopt::TruthTableReo tt( nInputs, nOuts ); + for ( k = 0; k < nOuts; k++ ) + { + pObj = Gia_ManCo( p, g+k ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp ); + if ( nInputs >= 6 ) + for ( i = 0; i < tt.nSize; i++ ) + tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i]; + else + { + i = k * (1 << nInputs); + v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs]; + tt.t[i / tt.ww] |= v << (i % tt.ww); + } + } + tt.RandomSiftReo( nRounds ); + Ttopt::TruthTable tt2( nInputs, nOuts ); + tt2.t = tt.t; + tt2.Reo( tt.vLevels ); + tt2.BDDGenerateAig( pNew, vSupp ); + Vec_IntFree( vSupp ); + } + Gia_ObjComputeTruthTableStop( p ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +extern "C" +word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare ); + +extern "C" +Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) +{ + int fVerbose = 0; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vSupp; + word v; + word * pTruth, * pCare; + int i, g, k, nInputs; + Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileName, fVerbose ); + Gia_ManLevelNum( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManForEachCi( p, pObj, k ) + Gia_ManAppendCi( pNew ); + Gia_ObjComputeTruthTableStart( p, nIns ); + Gia_ManHashStart( pNew ); + for ( g = 0; g < Gia_ManCoNum(p); g += nOuts ) + { + vSupp = Gia_ManCollectSuppNew( p, g, nOuts ); + nInputs = Vec_IntSize( vSupp ); + Ttopt::TruthTableLevelTSM tt( nInputs, nOuts ); + for ( k = 0; k < nOuts; k++ ) + { + pObj = Gia_ManCo( p, g+k ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp ); + if ( nInputs >= 6 ) + for ( i = 0; i < tt.nSize; i++ ) + tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i]; + else + { + i = k * (1 << nInputs); + v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs]; + tt.t[i / tt.ww] |= v << (i % tt.ww); + } + } + i = 1 << Vec_IntSize( vSupp ); + pCare = Gia_ManCountFraction( p, vSimI, vSupp, nRarity, fVerbose, &i ); + tt.care[0] = pCare[0]; + for ( i = 1; i < tt.nSize; i++ ) + tt.care[i] = pCare[i]; + ABC_FREE( pCare ); + tt.RandomSiftReo( nRounds ); + tt.Optimize(); + tt.BDDGenerateAig( pNew, vSupp ); + Vec_IntFree( vSupp ); + } + Gia_ObjComputeTruthTableStop( p ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Vec_WrdFreeP( &vSimI ); + return pNew; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index cd2e0afe..870da208 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -105,5 +105,6 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTis.c \ src/aig/gia/giaTruth.c \ src/aig/gia/giaTsim.c \ + src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ src/aig/gia/giaUtil.c -- cgit v1.2.3 From 2df7443317be7655713cf9e5abb0b5aa87f643af Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 12:33:45 -0700 Subject: Temporarily disabling new code. --- src/aig/gia/giaTtopt.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index eca0989d..99594afc 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1,4 +1,6 @@ // Author : Yukio Miyasaka +#if 0 + #include #include #include @@ -12,10 +14,14 @@ #include #include +#endif + #include "gia.h" ABC_NAMESPACE_IMPL_START +#if 0 + namespace Ttopt { struct PairHasher { @@ -1203,5 +1209,17 @@ Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, c Vec_WrdFreeP( &vSimI ); return pNew; } +#endif + +Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) +{ + return NULL; +} + +Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) +{ + return NULL; +} ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3 From 6c8c6aafc505afa9a10ea51d5d47aa898a2d8489 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 12:41:19 -0700 Subject: Temporarily disabling new code. --- src/aig/gia/giaTtopt.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index 99594afc..e5dff231 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1211,11 +1211,13 @@ Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, c } #endif +extern "C" Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) { return NULL; } +extern "C" Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) { return NULL; -- cgit v1.2.3 From 124e750e9a236d782a701debab466d564128c538 Mon Sep 17 00:00:00 2001 From: Yukio Miyasaka Date: Mon, 19 Sep 2022 14:51:34 -0700 Subject: fix compile errors and warnings --- src/aig/gia/giaTtopt.cpp | 232 ++++++++++++++++++++--------------------------- 1 file changed, 98 insertions(+), 134 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index e5dff231..8939a87b 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1,42 +1,20 @@ // Author : Yukio Miyasaka -#if 0 - -#include -#include -#include #include -#include #include -#include -#include #include -#include #include -#include - -#endif #include "gia.h" +#include "misc/vec/vecHash.h" ABC_NAMESPACE_IMPL_START -#if 0 - namespace Ttopt { -struct PairHasher { - std::size_t operator()(const std::pair & k) const { - std::hash hasher; - std::size_t seed = hasher(k.first) + 0x9e3779b9; - seed = hasher(k.second) + 0x9e3779b9 + (seed << 6) + (seed >> 2); - return seed; - } -}; - class TruthTable { public: - const int ww = 64; // word width - const int lww = 6; // log word width + static const int ww; // word width + static const int lww; // log word width typedef std::bitset<64> bsw; int nInputs; @@ -54,11 +32,11 @@ public: std::vector > > vvRedundantIndicesSaved; std::vector > vLevelsSaved; - std::mt19937 rng; static const word ones[]; static const word swapmask[]; TruthTable(int nInputs, int nOutputs): nInputs(nInputs), nOutputs(nOutputs) { + srand(0xABC); if(nInputs >= lww) { nSize = 1 << (nInputs - lww); nTotalSize = nSize * nOutputs; @@ -69,45 +47,12 @@ public: t.resize(nTotalSize); } vLevels.resize(nInputs); - std::iota(vLevels.begin(), vLevels.end(), 0); - } - - std::string BinaryToString(int bin, int size) { - std::string str; - for(int i = 0; i < size; i++) { - str += (bin & 1) + '0'; - bin = bin >> 1; - } - return str; - } - void GeneratePla(std::string filename) { - std::ofstream f(filename); - f << ".i " << nInputs << std::endl; - f << ".o " << nOutputs << std::endl; - if(nSize) { - for(int index = 0; index < nSize; index++) { - for(int pos = 0; pos < ww; pos++) { - int pat = (index << lww) + pos; - f << BinaryToString(pat, nInputs) << " "; - for(int i = 0; i < nOutputs; i++) { - f << ((t[nSize * i + index] >> pos) & 1); - } - f << std::endl; - } - } - } else { - for(int pos = 0; pos < (1 << nInputs); pos++) { - f << BinaryToString(pos, nInputs) << " "; - for(int i = 0; i < nOutputs; i++) { - int padding = i * (1 << nInputs); - f << ((t[padding / ww] >> (pos + padding % ww)) & 1); - } - f << std::endl; - } + for(int i = 0; i < nInputs; i++) { + vLevels[i] = i; } } - virtual void Save(uint i) { + virtual void Save(unsigned i) { if(savedt.size() < i + 1) { savedt.resize(i + 1); vLevelsSaved.resize(i + 1); @@ -116,13 +61,13 @@ public: vLevelsSaved[i] = vLevels; } - virtual void Load(uint i) { + virtual void Load(unsigned i) { assert(i < savedt.size()); t = savedt[i]; vLevels = vLevelsSaved[i]; } - virtual void SaveIndices(uint i) { + virtual void SaveIndices(unsigned i) { if(vvIndicesSaved.size() < i + 1) { vvIndicesSaved.resize(i + 1); vvRedundantIndicesSaved.resize(i + 1); @@ -131,7 +76,7 @@ public: vvRedundantIndicesSaved[i] = vvRedundantIndices; } - virtual void LoadIndices(uint i) { + virtual void LoadIndices(unsigned i) { vvIndices = vvIndicesSaved[i]; vvRedundantIndices = vvRedundantIndicesSaved[i]; } @@ -206,7 +151,7 @@ public: if(fZero || fOne) { return -2 ^ fOne; } - for(uint j = 0; j < vvIndices[lev].size(); j++) { + for(unsigned j = 0; j < vvIndices[lev].size(); j++) { int index2 = vvIndices[lev][j]; bool fEq = true; bool fCompl = true; @@ -226,7 +171,7 @@ public: if(!(value ^ ones[logwidth])) { return -1; } - for(uint j = 0; j < vvIndices[lev].size(); j++) { + for(unsigned j = 0; j < vvIndices[lev].size(); j++) { int index2 = vvIndices[lev][j]; word value2 = value ^ GetValue(index2, lev); if(!(value2)) { @@ -260,7 +205,8 @@ public: } virtual void BDDBuildLevel(int lev) { - for(int index: vvIndices[lev-1]) { + for(unsigned i = 0; i < vvIndices[lev-1].size(); i++) { + int index = vvIndices[lev-1][i]; int cof0 = BDDBuildOne(index << 1, lev); int cof1 = BDDBuildOne((index << 1) ^ 1, lev); if(cof0 == cof1) { @@ -292,7 +238,8 @@ public: } if(lev < nInputs - 2) { vvRedundantIndices[lev+1].clear(); - for(int index: vvIndices[lev+1]) { + for(unsigned i = 0; i < vvIndices[lev+1].size(); i++) { + int index = vvIndices[lev+1][i]; if(IsEq(index << 1, (index << 1) ^ 1, lev + 2)) { vvRedundantIndices[lev+1].push_back(index); } @@ -303,8 +250,8 @@ public: virtual void Swap(int lev) { assert(lev < nInputs - 1); - auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); - auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::vector::iterator it0 = std::find(vLevels.begin(), vLevels.end(), lev); + std::vector::iterator it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); std::swap(*it0, *it1); if(nInputs - lev - 1 > lww) { int nScopeSize = 1 << (nInputs - lev - 2 - lww); @@ -341,7 +288,7 @@ public: virtual int BDDSwap(int lev) { Swap(lev); for(int i = lev + 2; i < nInputs; i++) { - for(uint j = 0; j < vvIndices[i].size(); j++) { + for(unsigned j = 0; j < vvIndices[i].size(); j++) { SwapIndex(vvIndices[i][j], i - (lev + 2)); } } @@ -354,10 +301,23 @@ public: Save(0); SaveIndices(0); std::vector vars(nInputs); - std::iota(vars.begin(), vars.end(), 0); - std::sort(vars.begin(), vars.end(), [&](int i1, int i2) {return BDDNodeCountLevel(vLevels[i1]) > BDDNodeCountLevel(vLevels[i2]);}); + for(int i = 0; i < nInputs; i++) { + vars[i] = i; + } + std::vector vCounts(nInputs); + for(int i = 0; i < nInputs; i++) { + vCounts[i] = BDDNodeCountLevel(vLevels[i]); + } + for(int i = 1; i < nInputs; i++) { + int j = i; + while(j > 0 && vCounts[vars[j-1]] < vCounts[vars[j]]) { + std::swap(vars[j], vars[j-1]); + j--; + } + } bool turn = true; - for(int var: vars) { + for(unsigned j = 0; j < vars.size(); j++) { + int var = vars[j]; bool updated = false; int lev = vLevels[var]; for(int i = lev; i < nInputs - 1; i++) { @@ -411,8 +371,13 @@ public: Save(2); for(int i = 0; i < nRound; i++) { std::vector vLevelsNew(nInputs); - std::iota(vLevelsNew.begin(), vLevelsNew.end(), 0); - std::shuffle(vLevelsNew.begin(), vLevelsNew.end(), rng); + for(int j = 0; j < nInputs; j++) { + vLevelsNew[j] = j; + } + for(int j = nInputs - 1; j > 0; j--) { + int d = rand() % j; + std::swap(vLevelsNew[j], vLevelsNew[d]); + } Reo(vLevelsNew); int r = SiftReo(); if(best > r) { @@ -465,6 +430,9 @@ public: } }; +const int TruthTable::ww = 64; +const int TruthTable::lww = 6; + const word TruthTable::ones[7] = {ABC_CONST(0x0000000000000001), ABC_CONST(0x0000000000000003), ABC_CONST(0x000000000000000f), @@ -481,25 +449,27 @@ const word TruthTable::swapmask[5] = {ABC_CONST(0x2222222222222222), class TruthTableReo : public TruthTable { public: - bool fBuilt = false; + bool fBuilt; std::vector > vvChildren; std::vector > > vvChildrenSaved; - TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {} + TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) { + fBuilt = false; + } - void Save(uint i) override { + void Save(unsigned i) { if(vLevelsSaved.size() < i + 1) { vLevelsSaved.resize(i + 1); } vLevelsSaved[i] = vLevels; } - void Load(uint i) override { + void Load(unsigned i) { assert(i < vLevelsSaved.size()); vLevels = vLevelsSaved[i]; } - void SaveIndices(uint i) override { + void SaveIndices(unsigned i) { TruthTable::SaveIndices(i); if(vvChildrenSaved.size() < i + 1) { vvChildrenSaved.resize(i + 1); @@ -507,19 +477,20 @@ public: vvChildrenSaved[i] = vvChildren; } - void LoadIndices(uint i) override { + void LoadIndices(unsigned i) { TruthTable::LoadIndices(i); vvChildren = vvChildrenSaved[i]; } - void BDDBuildStartup() override { + void BDDBuildStartup() { vvChildren.clear(); vvChildren.resize(nInputs); TruthTable::BDDBuildStartup(); } - void BDDBuildLevel(int lev) override { - for(int index: vvIndices[lev-1]) { + void BDDBuildLevel(int lev) { + for(unsigned i = 0; i < vvIndices[lev-1].size(); i++) { + int index = vvIndices[lev-1][i]; int cof0 = BDDBuildOne(index << 1, lev); int cof1 = BDDBuildOne((index << 1) ^ 1, lev); vvChildren[lev-1].push_back(cof0); @@ -530,7 +501,7 @@ public: } } - int BDDBuild() override { + int BDDBuild() { if(fBuilt) { return BDDNodeCount(); } @@ -542,7 +513,7 @@ public: return BDDNodeCount(); } - int BDDRebuildOne(int index, int cof0, int cof1, int lev, std::unordered_map, int, PairHasher> &unique, std::vector &vChildrenLow) { + int BDDRebuildOne(int index, int cof0, int cof1, int lev, Hash_IntMan_t *unique, std::vector &vChildrenLow) { if(cof0 < 0 && cof0 == cof1) { return cof0; } @@ -551,11 +522,12 @@ public: cof0 ^= 1; cof1 ^= 1; } - if(unique.count({cof0, cof1})) { - return (unique[{cof0, cof1}] << 1) ^ fCompl; + int *place = Hash_Int2ManLookup(unique, cof0, cof1); + if(*place) { + return (Hash_IntObjData2(unique, *place) << 1) ^ fCompl; } vvIndices[lev].push_back(index); - unique[{cof0, cof1}] = vvIndices[lev].size() - 1; + Hash_Int2ManInsert(unique, cof0, cof1, vvIndices[lev].size() - 1); vChildrenLow.push_back(cof0); vChildrenLow.push_back(cof1); if(cof0 == cof1) { @@ -564,15 +536,14 @@ public: return ((vvIndices[lev].size() - 1) << 1) ^ fCompl; } - int BDDRebuild(int lev) override { + int BDDRebuild(int lev) { vvRedundantIndices[lev].clear(); vvRedundantIndices[lev+1].clear(); std::vector vChildrenHigh; std::vector vChildrenLow; - std::unordered_map, int, PairHasher> unique; - unique.reserve(2 * vvIndices[lev+1].size()); + Hash_IntMan_t *unique = Hash_IntManStart(2 * vvIndices[lev+1].size()); vvIndices[lev+1].clear(); - for(uint i = 0; i < vvIndices[lev].size(); i++) { + for(unsigned i = 0; i < vvIndices[lev].size(); i++) { int index = vvIndices[lev][i]; int cof0index = vvChildren[lev][i+i] >> 1; int cof1index = vvChildren[lev][i+i+1] >> 1; @@ -601,25 +572,26 @@ public: vvRedundantIndices[lev].push_back(index); } } + Hash_IntManStop(unique); vvChildren[lev] = vChildrenHigh; vvChildren[lev+1] = vChildrenLow; return BDDNodeCount(); } - void Swap(int lev) override { + void Swap(int lev) { assert(lev < nInputs - 1); - auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); - auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::vector::iterator it0 = std::find(vLevels.begin(), vLevels.end(), lev); + std::vector::iterator it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); std::swap(*it0, *it1); BDDRebuild(lev); } - int BDDSwap(int lev) override { + int BDDSwap(int lev) { Swap(lev); return BDDNodeCount(); } - virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) override { + virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) { abort(); } }; @@ -712,7 +684,7 @@ public: } } - void Save(uint i) override { + void Save(unsigned i) { TruthTable::Save(i); if(savedcare.size() < i + 1) { savedcare.resize(i + 1); @@ -720,12 +692,12 @@ public: savedcare[i] = care; } - void Load(uint i) override { + void Load(unsigned i) { TruthTable::Load(i); care = savedcare[i]; } - void SaveIndices(uint i) override { + void SaveIndices(unsigned i) { TruthTable::SaveIndices(i); if(vvMergedIndicesSaved.size() < i + 1) { vvMergedIndicesSaved.resize(i + 1); @@ -733,12 +705,12 @@ public: vvMergedIndicesSaved[i] = vvMergedIndices; } - void LoadIndices(uint i) override { + void LoadIndices(unsigned i) { TruthTable::LoadIndices(i); vvMergedIndices = vvMergedIndicesSaved[i]; } - void Swap(int lev) override { + void Swap(int lev) { TruthTable::Swap(lev); if(nInputs - lev - 1 > lww) { int nScopeSize = 1 << (nInputs - lev - 2 - lww); @@ -899,10 +871,10 @@ public: void Merge(int index1, int index2, int lev, bool fCompl) { MergeCare(index1, index2, lev); - vvMergedIndices[lev].push_back({(index1 << 1) ^ fCompl, index2}); + vvMergedIndices[lev].push_back(std::make_pair((index1 << 1) ^ fCompl, index2)); } - int BDDBuildOne(int index, int lev) override { + int BDDBuildOne(int index, int lev) { int r = BDDFind(index, lev); if(r >= -2) { if(r >= 0) { @@ -916,13 +888,13 @@ public: void CompleteMerge() { for(int i = nInputs - 1; i >= 0; i--) { - for(auto it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) { + for(std::vector >::reverse_iterator it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) { CopyFunc((*it).second, (*it).first >> 1, i, (*it).first & 1); } } } - void BDDBuildStartup() override { + void BDDBuildStartup() { RestoreCare(); vvIndices.clear(); vvIndices.resize(nInputs); @@ -938,12 +910,13 @@ public: } virtual void BDDRebuildByMerge(int lev) { - for(auto &p: vvMergedIndices[lev]) { + for(unsigned i = 0; i < vvMergedIndices[lev].size(); i++) { + std::pair &p = vvMergedIndices[lev][i]; MergeCare(p.first >> 1, p.second, lev); } } - int BDDRebuild(int lev) override { + int BDDRebuild(int lev) { RestoreCare(); for(int i = lev; i < nInputs; i++) { vvIndices[i].clear(); @@ -969,7 +942,7 @@ public: return BDDNodeCount(); } - int BDDSwap(int lev) override { + int BDDSwap(int lev) { Swap(lev); return BDDRebuild(lev); } @@ -993,7 +966,8 @@ public: virtual void Optimize() { OptimizationStartup(); for(int i = 1; i < nInputs; i++) { - for(int index: vvIndices[i-1]) { + for(unsigned j = 0; j < vvIndices[i-1].size(); j++) { + int index = vvIndices[i-1][j]; BDDBuildOne(index << 1, i); BDDBuildOne((index << 1) ^ 1, i); } @@ -1021,7 +995,8 @@ public: if(fZero || fOne) { return -2 ^ fOne; } - for(int index2: vvIndices[lev]) { + for(unsigned j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; bool fEq = true; bool fCompl = true; for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { @@ -1044,7 +1019,8 @@ public: if(!((value ^ one) & cvalue)) { return -1; } - for(int index2: vvIndices[lev]) { + for(unsigned j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; word value2 = value ^ GetValue(index2, lev); word cvalue2 = cvalue & GetCare(index2, lev); if(!(value2 & cvalue2)) { @@ -1058,14 +1034,14 @@ public: return -3; } - int BDDBuildOne(int index, int lev) override { + int BDDBuildOne(int index, int lev) { int r = BDDFindTSM(index, lev); if(r >= -2) { if(r >= 0) { CopyFuncMasked(r >> 1, index, lev, r & 1); Merge(r >> 1, index, lev, r & 1); } else { - vvMergedIndices[lev].push_back({r, index}); + vvMergedIndices[lev].push_back(std::make_pair(r, index)); } return r; } @@ -1073,15 +1049,16 @@ public: return index << 1; } - int BDDBuild() override { + int BDDBuild() { TruthTable::Save(3); int r = TruthTable::BDDBuild(); TruthTable::Load(3); return r; } - void BDDRebuildByMerge(int lev) override { - for(auto &p: vvMergedIndices[lev]) { + void BDDRebuildByMerge(int lev) { + for(unsigned i = 0; i < vvMergedIndices[lev].size(); i++) { + std::pair &p = vvMergedIndices[lev][i]; if(p.first >= 0) { CopyFuncMasked(p.first >> 1, p.second, lev, p.first & 1); MergeCare(p.first >> 1, p.second, lev); @@ -1089,7 +1066,7 @@ public: } } - int BDDRebuild(int lev) override { + int BDDRebuild(int lev) { TruthTable::Save(3); int r = TruthTableCare::BDDRebuild(lev); TruthTable::Load(3); @@ -1209,19 +1186,6 @@ Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, c Vec_WrdFreeP( &vSimI ); return pNew; } -#endif - -extern "C" -Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) -{ - return NULL; -} - -extern "C" -Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) -{ - return NULL; -} ABC_NAMESPACE_IMPL_END -- cgit v1.2.3 From 47c153629f78073bcfda223b8e9885e2280d4108 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 15:57:48 -0700 Subject: Compiler warnings. --- src/aig/gia/giaTtopt.cpp | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index 8939a87b..398bc7ff 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1,4 +1,11 @@ // Author : Yukio Miyasaka + +#ifdef _WIN32 +#ifndef __MINGW32__ +#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information +#endif +#endif + #include #include #include @@ -301,14 +308,15 @@ public: Save(0); SaveIndices(0); std::vector vars(nInputs); - for(int i = 0; i < nInputs; i++) { + int i; + for(i = 0; i < nInputs; i++) { vars[i] = i; } std::vector vCounts(nInputs); - for(int i = 0; i < nInputs; i++) { + for(i = 0; i < nInputs; i++) { vCounts[i] = BDDNodeCountLevel(vLevels[i]); } - for(int i = 1; i < nInputs; i++) { + for(i = 1; i < nInputs; i++) { int j = i; while(j > 0 && vCounts[vars[j-1]] < vCounts[vars[j]]) { std::swap(vars[j], vars[j-1]); @@ -316,7 +324,8 @@ public: } } bool turn = true; - for(unsigned j = 0; j < vars.size(); j++) { + unsigned j; + for(j = 0; j < vars.size(); j++) { int var = vars[j]; bool updated = false; int lev = vLevels[var]; @@ -371,10 +380,11 @@ public: Save(2); for(int i = 0; i < nRound; i++) { std::vector vLevelsNew(nInputs); - for(int j = 0; j < nInputs; j++) { + int j; + for(j = 0; j < nInputs; j++) { vLevelsNew[j] = j; } - for(int j = nInputs - 1; j > 0; j--) { + for(j = nInputs - 1; j > 0; j--) { int d = rand() % j; std::swap(vLevelsNew[j], vLevelsNew[d]); } @@ -420,10 +430,11 @@ public: vvIndices.resize(nInputs); std::vector > vvNodes(nInputs); std::vector vInputs(nInputs); - for(int i = 0; i < nInputs; i++) { + int i; + for(i = 0; i < nInputs; i++) { vInputs[vLevels[i]] = Vec_IntEntry(vSupp, nInputs - i - 1) << 1; } - for(int i = 0; i < nOutputs; i++) { + for(i = 0; i < nOutputs; i++) { int node = BDDGenerateAigRec(pNew, vInputs, vvNodes, i, 0); Gia_ManAppendCo(pNew, node); } @@ -918,17 +929,18 @@ public: int BDDRebuild(int lev) { RestoreCare(); - for(int i = lev; i < nInputs; i++) { + int i; + for(i = lev; i < nInputs; i++) { vvIndices[i].clear(); vvMergedIndices[i].clear(); if(i) { vvRedundantIndices[i-1].clear(); } } - for(int i = 0; i < lev; i++) { + for(i = 0; i < lev; i++) { BDDRebuildByMerge(i); } - for(int i = lev; i < nInputs; i++) { + for(i = lev; i < nInputs; i++) { if(!i) { for(int j = 0; j < nOutputs; j++) { if(!IsDC(j, 0)) { -- cgit v1.2.3 From 4d183efe48dfef9b992ff46c2636973b36ccb7f4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 16:07:29 -0700 Subject: Compiler warnings. --- src/aig/gia/gia.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 7487b8f3..1f4b7ee7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1758,6 +1758,10 @@ extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p ); extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p ); extern Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose ); +/*=== giaTtopt.c ===========================================================*/ +extern Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ); +extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ); + /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); @@ -1767,7 +1771,6 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); - ABC_NAMESPACE_HEADER_END -- cgit v1.2.3 From 6325e41681a259cf63de3aabe10b4b0930e77e56 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 16:13:54 -0700 Subject: Compiler warnings. --- src/aig/gia/giaTtopt.cpp | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index 398bc7ff..7d507152 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1,4 +1,22 @@ -// Author : Yukio Miyasaka +/**CFile**************************************************************** + + FileName [giaTtopt.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Truth-table-based logic synthesis.] + + Author [Yukio Miyasaka] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaTtopt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ #ifdef _WIN32 #ifndef __MINGW32__ @@ -1091,7 +1109,7 @@ public: extern "C" Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts ); -extern "C" +//extern "C" Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) { Gia_Man_t * pNew; @@ -1143,7 +1161,7 @@ Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) extern "C" word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare ); -extern "C" +//extern "C" Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) { int fVerbose = 0; -- cgit v1.2.3 From 1bd7550378752ba3957ffe4a2af58a74de8c7c51 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 16:30:52 -0700 Subject: Compiler warnings. --- src/aig/gia/gia.h | 3 +++ src/aig/gia/giaTtopt.cpp | 8 -------- 2 files changed, 3 insertions(+), 8 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1f4b7ee7..942c9eb7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1548,6 +1548,9 @@ extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName, int fGiaSimple extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName ); extern Gia_Man_t * Gia_ManReadMiniLut( char * pFileName ); extern void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName ); +/*=== giaMinLut.c ===========================================================*/ +extern word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare ); +extern Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts ); /*=== giaMuxes.c ===========================================================*/ extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors ); extern void Gia_ManPrintMuxStats( Gia_Man_t * p ); diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index 7d507152..61d07441 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1106,10 +1106,6 @@ public: } -extern "C" -Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts ); - -//extern "C" Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) { Gia_Man_t * pNew; @@ -1158,10 +1154,6 @@ Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) return pNew; } -extern "C" -word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare ); - -//extern "C" Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) { int fVerbose = 0; -- cgit v1.2.3 From fdd565659987ffc45e54f1f101496d00e2c820c9 Mon Sep 17 00:00:00 2001 From: Yukio Miyasaka Date: Mon, 19 Sep 2022 18:25:00 -0700 Subject: fix compile warnings --- src/aig/gia/giaTtopt.cpp | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index 61d07441..a765633f 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -123,8 +123,8 @@ public: if(logwidth > lww) { int nScopeSize = 1 << (logwidth - lww); for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { - fEq &= t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i]; - fCompl &= t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i]; + fEq &= (t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i]); + fCompl &= (t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i]); } } else { word value = GetValue(index1, lev) ^ GetValue(index2, lev); @@ -174,18 +174,18 @@ public: fOne &= !(~value); } if(fZero || fOne) { - return -2 ^ fOne; + return -2 ^ (int)fOne; } for(unsigned j = 0; j < vvIndices[lev].size(); j++) { int index2 = vvIndices[lev][j]; bool fEq = true; bool fCompl = true; for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { - fEq &= t[nScopeSize * index + i] == t[nScopeSize * index2 + i]; - fCompl &= t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i]; + fEq &= (t[nScopeSize * index + i] == t[nScopeSize * index2 + i]); + fCompl &= (t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i]); } if(fEq || fCompl) { - return (j << 1) ^ fCompl; + return (j << 1) ^ (int)fCompl; } } } else { @@ -553,7 +553,7 @@ public: } int *place = Hash_Int2ManLookup(unique, cof0, cof1); if(*place) { - return (Hash_IntObjData2(unique, *place) << 1) ^ fCompl; + return (Hash_IntObjData2(unique, *place) << 1) ^ (int)fCompl; } vvIndices[lev].push_back(index); Hash_Int2ManInsert(unique, cof0, cof1, vvIndices[lev].size() - 1); @@ -562,7 +562,7 @@ public: if(cof0 == cof1) { vvRedundantIndices[lev].push_back(index); } - return ((vvIndices[lev].size() - 1) << 1) ^ fCompl; + return ((vvIndices[lev].size() - 1) << 1) ^ (int)fCompl; } int BDDRebuild(int lev) { @@ -580,18 +580,18 @@ public: bool cof1c = vvChildren[lev][i+i+1] & 1; int cof00, cof01, cof10, cof11; if(cof0index < 0) { - cof00 = -2 ^ cof0c; - cof01 = -2 ^ cof0c; + cof00 = -2 ^ (int)cof0c; + cof01 = -2 ^ (int)cof0c; } else { - cof00 = vvChildren[lev+1][cof0index+cof0index] ^ cof0c; - cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ cof0c; + cof00 = vvChildren[lev+1][cof0index+cof0index] ^ (int)cof0c; + cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ (int)cof0c; } if(cof1index < 0) { - cof10 = -2 ^ cof1c; - cof11 = -2 ^ cof1c; + cof10 = -2 ^ (int)cof1c; + cof11 = -2 ^ (int)cof1c; } else { - cof10 = vvChildren[lev+1][cof1index+cof1index] ^ cof1c; - cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ cof1c; + cof10 = vvChildren[lev+1][cof1index+cof1index] ^ (int)cof1c; + cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ (int)cof1c; } int newcof0 = BDDRebuildOne(index << 1, cof00, cof10, lev + 1, unique, vChildrenLow); int newcof1 = BDDRebuildOne((index << 1) ^ 1, cof01, cof11, lev + 1, unique, vChildrenLow); @@ -900,7 +900,7 @@ public: void Merge(int index1, int index2, int lev, bool fCompl) { MergeCare(index1, index2, lev); - vvMergedIndices[lev].push_back(std::make_pair((index1 << 1) ^ fCompl, index2)); + vvMergedIndices[lev].push_back(std::make_pair((index1 << 1) ^ (int)fCompl, index2)); } int BDDBuildOne(int index, int lev) { @@ -1023,7 +1023,7 @@ public: fOne &= !(~value & cvalue); } if(fZero || fOne) { - return -2 ^ fOne; + return -2 ^ (int)fOne; } for(unsigned j = 0; j < vvIndices[lev].size(); j++) { int index2 = vvIndices[lev][j]; @@ -1036,7 +1036,7 @@ public: fCompl &= !(~value & cvalue); } if(fEq || fCompl) { - return (index2 << 1) ^ !fEq; + return (index2 << 1) ^ (int)!fEq; } } } else { -- cgit v1.2.3 From 813a0f1ff1ae7512cb7947f54cd3f2ab252848c8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Oct 2022 23:51:40 -0700 Subject: Updating features of &if mapper. --- src/aig/gia/giaIf.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index ae87277a..8b4e5b12 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1891,7 +1891,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) if ( !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize && !pIfMan->pPars->fEnableCheck75 && !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && - !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars ) + !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars && !pIfMan->pPars->fUseCheck1 && !pIfMan->pPars->fUseCheck2 ) If_CutRotatePins( pIfMan, pCutBest ); // collect leaves of the best cut Vec_IntClear( vLeaves ); -- cgit v1.2.3 From 70cb339f869e485802159d7f2b886130793556c4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 19 Oct 2022 05:05:56 -0700 Subject: Bug fix in &dch -x. --- src/aig/gia/giaEquiv.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 5c82b260..030eaa60 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1869,7 +1869,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb Gia_Obj_t * pRepr, * pReprNew, * pObjNew; if ( ~pObj->Value ) return; - if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) && !Gia_ObjFailed(p,Gia_ObjId(p,pObj)) ) { if ( Gia_ObjIsConst0(pRepr) ) { -- cgit v1.2.3