| /**CFile**************************************************************** |
| |
| FileName [mpmPre.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Configurable technology mapper.] |
| |
| Synopsis [DSD-related precomputations.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 1, 2013.] |
| |
| Revision [$Id: mpmPre.c,v 1.00 2013/06/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include <stdio.h> |
| #include <stdlib.h> |
| #include <string.h> |
| #include <assert.h> |
| |
| #include "misc/vec/vec.h" |
| #include "misc/vec/vecHsh.h" |
| #include "misc/extra/extra.h" |
| #include "bool/kit/kit.h" |
| #include "misc/util/utilTruth.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Ifd_Obj_t_ Ifd_Obj_t; |
| struct Ifd_Obj_t_ |
| { |
| unsigned nFreq : 18; // frequency |
| unsigned nAnds : 6; // number of AND gates |
| unsigned nSupp : 5; // support size |
| unsigned Type : 2; // type |
| unsigned fWay : 1; // transparent edge |
| unsigned pFans[3]; // fanins |
| }; |
| |
| typedef struct Ifd_Man_t_ Ifd_Man_t; |
| struct Ifd_Man_t_ |
| { |
| Ifd_Obj_t * pObjs; |
| int nObjs; |
| int nObjsAlloc; |
| // hashing operations |
| Vec_Int_t * vArgs; // iDsd1 op iDsdC |
| Vec_Int_t * vRes; // result of operation |
| Hsh_IntMan_t * vHash; // hash table |
| Vec_Int_t * vMarks; // marks where given N begins |
| Vec_Wrd_t * vTruths; // truth tables |
| Vec_Int_t * vClauses; // truth tables |
| // other data |
| Vec_Int_t * vSuper; |
| |
| }; |
| |
| static inline int Ifd_ObjIsVar( Ifd_Obj_t * p ) { return p->Type == 0; } |
| static inline int Ifd_ObjIsAnd( Ifd_Obj_t * p ) { return p->Type == 1; } |
| static inline int Ifd_ObjIsXor( Ifd_Obj_t * p ) { return p->Type == 2; } |
| static inline int Ifd_ObjIsMux( Ifd_Obj_t * p ) { return p->Type == 3; } |
| |
| static inline Ifd_Obj_t * Ifd_ManObj( Ifd_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return p->pObjs + i; } |
| static inline Ifd_Obj_t * Ifd_ManObjFromLit( Ifd_Man_t * p, int iLit ) { return Ifd_ManObj( p, Abc_Lit2Var(iLit) ); } |
| static inline int Ifd_ObjId( Ifd_Man_t * p, Ifd_Obj_t * pObj ) { assert( pObj - p->pObjs >= 0 && pObj - p->pObjs < p->nObjs ); return pObj - p->pObjs; } |
| static inline int Ifd_LitSuppSize( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nSupp : 0; } |
| static inline int Ifd_LitNumAnds( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nAnds : 0; } |
| |
| #define Ifd_ManForEachNodeWithSupp( p, nVars, pLeaf, i ) \ |
| for ( i = Vec_IntEntry(p->vMarks, nVars); (i < Vec_IntEntry(p->vMarks, nVars+1)) && (pLeaf = Ifd_ManObj(p, i)); i++ ) |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ifd_Man_t * Ifd_ManStart() |
| { |
| Ifd_Man_t * p; |
| p = ABC_CALLOC( Ifd_Man_t, 1 ); |
| p->nObjsAlloc = Abc_PrimeCudd( 50000000 ); |
| p->nObjs = 2; |
| p->pObjs = ABC_CALLOC( Ifd_Obj_t, p->nObjsAlloc ); |
| memset( p->pObjs, 0xFF, sizeof(Ifd_Obj_t) ); // const node |
| (p->pObjs + 1)->nSupp = 1; // variable |
| (p->pObjs + 1)->fWay = 1; // variable |
| // hashing operations |
| p->vArgs = Vec_IntAlloc( 4000 ); |
| p->vRes = Vec_IntAlloc( 1000 ); |
| p->vHash = Hsh_IntManStart( p->vArgs, 4, 1000 ); |
| p->vMarks = Vec_IntAlloc( 100 ); |
| Vec_IntPush( p->vMarks, 0 ); |
| Vec_IntPush( p->vMarks, 1 ); |
| Vec_IntPush( p->vMarks, p->nObjs ); |
| // other data |
| p->vSuper = Vec_IntAlloc( 1000 ); |
| p->vTruths = Vec_WrdAlloc( 1000 ); |
| p->vClauses = Vec_IntAlloc( 1000 ); |
| return p; |
| } |
| void Ifd_ManStop( Ifd_Man_t * p ) |
| { |
| int i, This, Prev = 0; |
| Vec_IntForEachEntryStart( p->vMarks, This, i, 1 ) |
| { |
| printf( "%d(%d:%d) ", i-1, This, This - Prev ); |
| Prev = This; |
| } |
| printf( "\n" ); |
| |
| Vec_IntFreeP( &p->vArgs ); |
| Vec_IntFreeP( &p->vRes ); |
| Vec_WrdFreeP( &p->vTruths ); |
| Vec_IntFreeP( &p->vClauses ); |
| Vec_IntFreeP( &p->vMarks ); |
| Hsh_IntManStop( p->vHash ); |
| Vec_IntFreeP( &p->vSuper ); |
| ABC_FREE( p->pObjs ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Printing structures.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ifd_ObjPrint_rec( Ifd_Man_t * p, int iLit, int * pCounter, int DiffType ) |
| { |
| char Symb[2][4] = { {'?','(','[','<'}, {'?',')',']','>'} }; |
| Ifd_Obj_t * pDsd; |
| if ( Abc_LitIsCompl(iLit) ) |
| printf( "!" ), iLit = Abc_LitNot(iLit); |
| if ( iLit == 2 ) |
| { printf( "%c", 'a' + (*pCounter)++ ); return; } |
| pDsd = Ifd_ManObjFromLit( p, iLit ); |
| if ( DiffType ) |
| printf( "%c", Symb[0][pDsd->Type] ); |
| Ifd_ObjPrint_rec( p, pDsd->pFans[0], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[0]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[0])->Type ); |
| Ifd_ObjPrint_rec( p, pDsd->pFans[1], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[1]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[1])->Type ); |
| if ( pDsd->pFans[2] != -1 ) |
| Ifd_ObjPrint_rec( p, pDsd->pFans[2], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[2]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[2])->Type ); |
| if ( DiffType ) |
| printf( "%c", Symb[1][pDsd->Type] ); |
| } |
| void Ifd_ObjPrint( Ifd_Man_t * p, int iLit ) |
| { |
| int Counter = 0; |
| if ( iLit == 0 ) |
| { printf( "0" ); return; } |
| if ( iLit == 1 ) |
| { printf( "1" ); return; } |
| Ifd_ObjPrint_rec( p, iLit, &Counter, 1 ); |
| } |
| void Ifd_ManPrint2( Ifd_Man_t * p ) |
| { |
| int i; |
| for ( i = 0; i < p->nObjs; i++ ) |
| { |
| printf( "%4d : ", i ); |
| Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) ); |
| printf( "\n" ); |
| } |
| } |
| void Ifd_ManPrint( Ifd_Man_t * p ) |
| { |
| int i; |
| for ( i = 0; i < p->nObjs; i++ ) |
| { |
| word Fun = Vec_WrdEntry( p->vTruths, i ); |
| printf( " { " ); |
| printf( "%d, ", Extra_TruthSupportSize((unsigned *)&Fun, 6) ); |
| printf( "%2d, ", Ifd_LitNumAnds(p, Abc_Var2Lit(i, 0)) ); |
| printf( "%2d, ", Vec_IntEntry(p->vClauses, i) ); |
| printf( "ABC_CONST(" ); |
| Extra_PrintHex( stdout, (unsigned *)&Fun, 6 ); |
| printf( "), \"" ); |
| Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) ); |
| printf( "\" }, // %4d \n", i ); |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computing truth tables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| word Ifd_ObjTruth_rec( Ifd_Man_t * p, int iLit, int * pCounter ) |
| { |
| static word s_Truths6[6] = { |
| ABC_CONST(0xAAAAAAAAAAAAAAAA), |
| ABC_CONST(0xCCCCCCCCCCCCCCCC), |
| ABC_CONST(0xF0F0F0F0F0F0F0F0), |
| ABC_CONST(0xFF00FF00FF00FF00), |
| ABC_CONST(0xFFFF0000FFFF0000), |
| ABC_CONST(0xFFFFFFFF00000000) |
| }; |
| Ifd_Obj_t * pDsd; |
| word Fun0, Fun1, Fun2 = 0; |
| assert( !Abc_LitIsCompl(iLit) ); |
| if ( iLit == 2 ) |
| return s_Truths6[(*pCounter)++]; |
| pDsd = Ifd_ManObjFromLit( p, iLit ); |
| |
| Fun0 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[0]), pCounter ); |
| Fun1 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[1]), pCounter ); |
| if ( pDsd->pFans[2] != -1 ) |
| Fun2 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[2]), pCounter ); |
| |
| Fun0 = Abc_LitIsCompl(pDsd->pFans[0]) ? ~Fun0 : Fun0; |
| Fun1 = Abc_LitIsCompl(pDsd->pFans[1]) ? ~Fun1 : Fun1; |
| if ( pDsd->pFans[2] != -1 ) |
| Fun2 = Abc_LitIsCompl(pDsd->pFans[2]) ? ~Fun2 : Fun2; |
| |
| if ( pDsd->Type == 1 ) |
| return Fun0 & Fun1; |
| if ( pDsd->Type == 2 ) |
| return Fun0 ^ Fun1; |
| if ( pDsd->Type == 3 ) |
| return (Fun2 & Fun1) | (~Fun2 & Fun0); |
| assert( 0 ); |
| return -1; |
| } |
| word Ifd_ObjTruth( Ifd_Man_t * p, int iLit ) |
| { |
| word Fun; |
| int Counter = 0; |
| if ( iLit == 0 ) |
| return 0; |
| if ( iLit == 1 ) |
| return ~(word)0; |
| Fun = Ifd_ObjTruth_rec( p, Abc_LitRegular(iLit), &Counter ); |
| return Abc_LitIsCompl(iLit) ? ~Fun : Fun; |
| } |
| void Ifd_ManTruthAll( Ifd_Man_t * p ) |
| { |
| word Fun; |
| int i; |
| assert( Vec_WrdSize(p->vTruths) == 0 ); |
| for ( i = 0; i < p->nObjs; i++ ) |
| { |
| Fun = Ifd_ObjTruth( p, Abc_Var2Lit( i, 0 ) ); |
| Vec_WrdPush( p->vTruths, Fun ); |
| // Extra_PrintHex( stdout, (unsigned *)&Fun, 6 ); printf( " " ); |
| // Kit_DsdPrintFromTruth( (unsigned *)&Fun, 6 ); printf( "\n" ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Mpm_ComputeCnfSizeOne( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) |
| { |
| Vec_StrClear( vCnf ); |
| if ( Truth == 0 || ~Truth == 0 ) |
| { |
| // assert( nVars == 0 ); |
| Vec_StrPush( vCnf, (char)(Truth == 0) ); |
| Vec_StrPush( vCnf, (char)-1 ); |
| return 1; |
| } |
| else |
| { |
| int i, k, c, RetValue, Literal, Cube, nCubes = 0; |
| assert( nVars > 0 ); |
| for ( c = 0; c < 2; c ++ ) |
| { |
| Truth = c ? ~Truth : Truth; |
| RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); |
| assert( RetValue == 0 ); |
| nCubes += Vec_IntSize( vCover ); |
| Vec_IntForEachEntry( vCover, Cube, i ) |
| { |
| for ( k = 0; k < nVars; k++ ) |
| { |
| Literal = 3 & (Cube >> (k << 1)); |
| if ( Literal == 1 ) // '0' -> pos lit |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) ); |
| else if ( Literal == 2 ) // '1' -> neg lit |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) ); |
| else if ( Literal != 0 ) |
| assert( 0 ); |
| } |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) ); |
| Vec_StrPush( vCnf, (char)-1 ); |
| } |
| } |
| return nCubes; |
| } |
| } |
| void Mpm_ComputeCnfSizeAll( Ifd_Man_t * p ) |
| { |
| Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 ); |
| Vec_Str_t * vCnf = Vec_StrAlloc( 1000 ); |
| word Truth; |
| int i; |
| assert( Vec_IntSize(p->vClauses) == 0 ); |
| Vec_WrdForEachEntry( p->vTruths, Truth, i ) |
| Vec_IntPush( p->vClauses, Mpm_ComputeCnfSizeOne(Truth, 6, vCover, vCnf) ); |
| Vec_IntFree( vCover ); |
| Vec_StrFree( vCnf ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Canonicizing DSD structures.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ifd_ManHashLookup( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type ) |
| { |
| int pData[4]; |
| assert( iDsdC != -1 || iDsd0 >= iDsd1 ); |
| assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) ); |
| pData[0] = iDsd0; |
| pData[1] = iDsd1; |
| pData[2] = iDsdC; |
| pData[3] = Type; |
| return *Hsh_IntManLookup( p->vHash, (unsigned *)pData ); |
| } |
| void Ifd_ManHashInsert( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type, int Res ) |
| { |
| int iObj; |
| assert( iDsdC != -1 || iDsd0 >= iDsd1 ); |
| assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) ); |
| Vec_IntPush( p->vArgs, iDsd0 ); |
| Vec_IntPush( p->vArgs, iDsd1 ); |
| Vec_IntPush( p->vArgs, iDsdC ); |
| Vec_IntPush( p->vArgs, Type ); |
| iObj = Hsh_IntManAdd( p->vHash, Vec_IntSize(p->vRes) ); |
| assert( iObj == Vec_IntSize(p->vRes) ); |
| Vec_IntPush( p->vRes, Res ); |
| assert( 4 * Vec_IntSize(p->vRes) == Vec_IntSize(p->vArgs) ); |
| } |
| int Ifd_ManHashFindOrAdd( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type ) |
| { |
| Ifd_Obj_t * pObj; |
| int iObj, Value; |
| assert( iDsdC != -1 || iDsd0 >= iDsd1 ); |
| assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) ); |
| Vec_IntPush( p->vArgs, iDsd0 ); |
| Vec_IntPush( p->vArgs, iDsd1 ); |
| Vec_IntPush( p->vArgs, iDsdC ); |
| Vec_IntPush( p->vArgs, Type ); |
| Value = Hsh_IntManAdd( p->vHash, Vec_IntSize(p->vRes) ); |
| if ( Value < Vec_IntSize(p->vRes) ) |
| { |
| iObj = Vec_IntEntry(p->vRes, Value); |
| Vec_IntShrink( p->vArgs, Vec_IntSize(p->vArgs) - 4 ); |
| pObj = Ifd_ManObj( p, iObj ); |
| // pObj->nFreq++; |
| assert( (int)pObj->Type == Type ); |
| assert( (int)pObj->nSupp == Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC) ); |
| } |
| else |
| { |
| if ( p->nObjs == p->nObjsAlloc ) |
| printf( "The number of nodes is more than %d\n", p->nObjs ); |
| assert( p->nObjs < p->nObjsAlloc ); |
| iObj = p->nObjs; |
| pObj = Ifd_ManObj( p, p->nObjs++ ); |
| // pObj->nFreq = 1; |
| pObj->nSupp = Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC); |
| pObj->nAnds = Ifd_LitNumAnds(p, iDsd0) + Ifd_LitNumAnds(p, iDsd1) + Ifd_LitNumAnds(p, iDsdC) + ((Type == 1) ? 1 : 3); |
| pObj->Type = Type; |
| if ( Type == 1 ) |
| pObj->fWay = 0; |
| else if ( Type == 2 ) |
| pObj->fWay = Ifd_ManObjFromLit(p, iDsd0)->fWay || Ifd_ManObjFromLit(p, iDsd1)->fWay; |
| else if ( Type == 3 ) |
| // pObj->fWay = (Ifd_ManObjFromLit(p, iDsd0)->fWay && Ifd_ManObjFromLit(p, iDsd1)->fWay) || (Abc_Lit2Var(iDsd0) == Abc_Lit2Var(iDsd1) && Ifd_ManObjFromLit(p, iDsdC)->fWay); |
| pObj->fWay = (Ifd_ManObjFromLit(p, iDsd0)->fWay && Ifd_ManObjFromLit(p, iDsd1)->fWay) || (iDsd0 == Abc_LitNot(iDsd1) && Ifd_ManObjFromLit(p, iDsdC)->fWay); |
| else assert( 0 ); |
| pObj->pFans[0] = iDsd0; |
| pObj->pFans[1] = iDsd1; |
| pObj->pFans[2] = iDsdC; |
| Vec_IntPush( p->vRes, iObj ); |
| } |
| assert( 4 * Vec_IntSize(p->vRes) == Vec_IntSize(p->vArgs) ); |
| return iObj; |
| } |
| void Ifd_ManOperSuper_rec( Ifd_Man_t * p, int iLit, int Type, Vec_Int_t * vObjs ) |
| { |
| Ifd_Obj_t * pDsd = Ifd_ManObjFromLit( p, iLit ); |
| if ( Abc_LitIsCompl(iLit) || (int)pDsd->Type != Type ) |
| Vec_IntPush( vObjs, iLit ); |
| else |
| { |
| Ifd_ManOperSuper_rec( p, pDsd->pFans[0], Type, vObjs ); |
| Ifd_ManOperSuper_rec( p, pDsd->pFans[1], Type, vObjs ); |
| } |
| } |
| int Ifd_ManOper( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type ) |
| { |
| int i, iLit0, iLit1, iThis, fCompl = 0; |
| if ( Type == 1 ) // AND |
| { |
| if ( iDsd0 == 0 || iDsd1 == 0 ) |
| return 0; |
| if ( iDsd0 == 1 || iDsd1 == 1 ) |
| return (iDsd0 == 1) ? iDsd1 : iDsd0; |
| } |
| else if ( Type == 2 ) // XOR |
| { |
| if ( iDsd0 < 2 ) |
| return Abc_LitNotCond( iDsd1, iDsd0 ); |
| if ( iDsd1 < 2 ) |
| return Abc_LitNotCond( iDsd0, iDsd1 ); |
| if ( Abc_LitIsCompl(iDsd0) ) |
| fCompl ^= 1, iDsd0 = Abc_LitNot(iDsd0); |
| if ( Abc_LitIsCompl(iDsd1) ) |
| fCompl ^= 1, iDsd1 = Abc_LitNot(iDsd1); |
| } |
| else if ( Type == 3 ) |
| { |
| if ( Abc_LitIsCompl(iDsdC) ) |
| { |
| ABC_SWAP( int, iDsd0, iDsd1 ); |
| iDsdC = Abc_LitNot(iDsdC); |
| } |
| if ( Abc_LitIsCompl(iDsd1) ) |
| fCompl ^= 1, iDsd0 = Abc_LitNot(iDsd0), iDsd1 = Abc_LitNot(iDsd1); |
| } |
| assert( iDsd0 > 1 && iDsd1 > 1 && Type >= 1 && Type <= 3 ); |
| /* |
| // check cache |
| iThis = Ifd_ManHashLookup( p, iDsd0, iDsd1, iDsdC, Type ); |
| if ( iThis != -1 ) |
| return Abc_Var2Lit( iThis, fCompl ); |
| */ |
| // create new entry |
| if ( Type == 3 ) |
| { |
| iThis = Ifd_ManHashFindOrAdd( p, iDsd0, iDsd1, iDsdC, Type ); |
| return Abc_Var2Lit( iThis, fCompl ); |
| } |
| assert( iDsdC == -1 ); |
| Vec_IntClear( p->vSuper ); |
| Ifd_ManOperSuper_rec( p, iDsd0, Type, p->vSuper ); |
| Ifd_ManOperSuper_rec( p, iDsd1, Type, p->vSuper ); |
| Vec_IntSort( p->vSuper, 1 ); |
| iLit0 = Vec_IntEntry( p->vSuper, 0 ); |
| Vec_IntForEachEntryStart( p->vSuper, iLit1, i, 1 ) |
| iLit0 = Abc_Var2Lit( Ifd_ManHashFindOrAdd(p, iLit0, iLit1, -1, Type), 0 ); |
| assert( !Abc_LitIsCompl(iLit0) ); |
| // insert into cache |
| // if ( Vec_IntSize(p->vSuper) > 2 ) |
| // Ifd_ManHashInsert( p, iDsd0, iDsd1, iDsdC, Type, iLit0 ); |
| return Abc_LitNotCond( iLit0, fCompl ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ifd_ManFindDsd_rec( Ifd_Man_t * pMan, char * pStr, char ** p, int * pMatches ) |
| { |
| int fCompl = 0; |
| if ( **p == '!' ) |
| (*p)++, fCompl = 1; |
| if ( **p >= 'a' && **p <= 'f' ) // var |
| { |
| assert( **p - 'a' >= 0 && **p - 'a' < 6 ); |
| return Abc_Var2Lit( 1, fCompl ); |
| } |
| if ( **p == '(' ) // and/or |
| { |
| char * q = pStr + pMatches[ *p - pStr ]; |
| int Lit, Res = 1; |
| assert( **p == '(' && *q == ')' ); |
| for ( (*p)++; *p < q; (*p)++ ) |
| { |
| Lit = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches ); |
| Res = Ifd_ManOper( pMan, Res, Lit, 0, 1 ); |
| } |
| assert( *p == q ); |
| return Abc_LitNotCond( Res, fCompl ); |
| } |
| if ( **p == '[' ) // xor |
| { |
| char * q = pStr + pMatches[ *p - pStr ]; |
| int Lit, Res = 0; |
| assert( **p == '[' && *q == ']' ); |
| for ( (*p)++; *p < q; (*p)++ ) |
| { |
| Lit = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches ); |
| Res = Ifd_ManOper( pMan, Res, Lit, 0, 2 ); |
| } |
| assert( *p == q ); |
| return Abc_LitNotCond( Res, fCompl ); |
| } |
| if ( **p == '<' ) // mux |
| { |
| int Temp[3], * pTemp = Temp, Res; |
| char * q = pStr + pMatches[ *p - pStr ]; |
| assert( **p == '<' && *q == '>' ); |
| // derive MAX components |
| for ( (*p)++; *p < q; (*p)++ ) |
| *pTemp++ = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches ); |
| assert( pTemp == Temp + 3 ); |
| assert( *p == q ); |
| // Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]); |
| Res = Ifd_ManOper( pMan, Temp[2], Temp[1], Temp[0], 3 ); |
| return Abc_LitNotCond( Res, fCompl ); |
| } |
| assert( 0 ); |
| return 0; |
| } |
| #define IFM_MAX_STR 100 |
| #define IFM_MAX_VAR 16 |
| int * Ifd_ManComputeMatches( char * p ) |
| { |
| static int pMatches[IFM_MAX_STR]; |
| int pNested[IFM_MAX_VAR]; |
| int v, nNested = 0; |
| for ( v = 0; p[v]; v++ ) |
| { |
| assert( v < IFM_MAX_STR ); |
| pMatches[v] = 0; |
| if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' ) |
| pNested[nNested++] = v; |
| else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' ) |
| pMatches[pNested[--nNested]] = v; |
| assert( nNested < IFM_MAX_VAR ); |
| } |
| assert( nNested == 0 ); |
| return pMatches; |
| } |
| int Ifd_ManFindDsd( Ifd_Man_t * pMan, char * p ) |
| { |
| int Res; |
| if ( *p == '0' && *(p+1) == 0 ) |
| Res = 0; |
| else if ( *p == '1' && *(p+1) == 0 ) |
| Res = 1; |
| else |
| Res = Ifd_ManFindDsd_rec( pMan, p, &p, Ifd_ManComputeMatches(p) ); |
| assert( *++p == 0 ); |
| return Res; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ifd_ManDsdTest2() |
| { |
| char * p = "(abc)"; |
| // char * q = "(a[bc])"; |
| // char * r = "[<abc>(def)]"; |
| Ifd_Man_t * pMan = Ifd_ManStart(); |
| int iLit = Ifd_ManFindDsd( pMan, p ); |
| Ifd_ObjPrint( pMan, iLit ); |
| Ifd_ManStop( pMan ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Wrd_t * Ifd_ManDsdTruths( int nVars ) |
| { |
| int fUseMux = 1; |
| Vec_Wrd_t * vTruths; |
| Ifd_Man_t * pMan = Ifd_ManStart(); |
| Ifd_Obj_t * pLeaf0, * pLeaf1, * pLeaf2; |
| int v, i, j, k, c0, c1, c2; |
| for ( v = 2; v <= nVars; v++ ) |
| { |
| // create ANDs/XORs |
| for ( i = 1; i < v; i++ ) |
| for ( j = 1; j < v; j++ ) |
| if ( i + j == v ) |
| { |
| Ifd_ManForEachNodeWithSupp( pMan, i, pLeaf0, c0 ) |
| Ifd_ManForEachNodeWithSupp( pMan, j, pLeaf1, c1 ) |
| { |
| assert( (int)pLeaf0->nSupp == i ); |
| assert( (int)pLeaf1->nSupp == j ); |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), -1, 1 ); |
| if ( !pLeaf1->fWay ) |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 1), -1, 1 ); |
| if ( !pLeaf0->fWay ) |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 0), -1, 1 ); |
| if ( !pLeaf0->fWay && !pLeaf1->fWay ) |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 1), -1, 1 ); |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), -1, 2 ); |
| } |
| } |
| // create MUX |
| if ( fUseMux ) |
| for ( i = 1; i < v-1; i++ ) |
| for ( j = 1; j < v-1; j++ ) |
| for ( k = 1; k < v-1; k++ ) |
| if ( i + j + k == v ) |
| { |
| Ifd_ManForEachNodeWithSupp( pMan, i, pLeaf0, c0 ) |
| Ifd_ManForEachNodeWithSupp( pMan, j, pLeaf1, c1 ) |
| Ifd_ManForEachNodeWithSupp( pMan, k, pLeaf2, c2 ) |
| { |
| assert( (int)pLeaf0->nSupp == i ); |
| assert( (int)pLeaf1->nSupp == j ); |
| assert( (int)pLeaf2->nSupp == k ); |
| //printf( "%d %d %d ", i, j, k ); |
| //printf( "%d %d %d\n", Ifd_ObjId(pMan, pLeaf0), Ifd_ObjId(pMan, pLeaf1), Ifd_ObjId(pMan, pLeaf2) ); |
| if ( pLeaf2->fWay && c0 < c1 ) |
| continue; |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), Abc_Var2Lit(c2, 0), 3 ); |
| if ( !pLeaf0->fWay && !pLeaf1->fWay ) |
| Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 0), Abc_Var2Lit(c2, 0), 3 ); |
| } |
| } |
| // bookmark |
| Vec_IntPush( pMan->vMarks, pMan->nObjs ); |
| } |
| Ifd_ManTruthAll( pMan ); |
| Mpm_ComputeCnfSizeAll( pMan ); |
| // Ifd_ManPrint( pMan ); |
| vTruths = pMan->vTruths; pMan->vTruths = NULL; |
| Ifd_ManStop( pMan ); |
| return vTruths; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generating the guided array for minimal permutations.] |
| |
| Description [http://icodesnip.com/search/johnson%20trotter/] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ifd_ManDsdPermPrint( int * perm, int size ) |
| { |
| int i; |
| for ( i = 0; i < size; i++ ) |
| printf( "%d", perm[i] ); |
| printf( "\n" ); |
| } |
| Vec_Int_t * Ifd_ManDsdPermJT( int n ) |
| { |
| Vec_Int_t * vGuide = Vec_IntAlloc( 100 ); |
| int *array, *dir, tmp, tmp2, i, max; |
| array = (int*)malloc(sizeof(int) * n); |
| dir = (int*)calloc(n, sizeof(int)); |
| for (i = 0; i < n; i++) |
| array[i] = i; |
| max = n - 1; |
| if (n != 1) |
| do |
| { |
| // Ifd_ManDsdPermPrint(array, n); |
| tmp = array[max]; |
| tmp2 = dir[max]; |
| i = !dir[max] ? max - 1 : max + 1; |
| array[max] = array[i]; |
| array[i] = tmp; |
| Vec_IntPush( vGuide, Abc_MinInt(max, i) ); |
| dir[max] = dir[i]; |
| dir[i] = tmp2; |
| for (i = 0; i < n; i++) |
| if (array[i] > tmp) |
| dir[i] = !dir[i]; |
| max = n; |
| for (i = 0; i < n; i++) |
| if (((!dir[i] && i != 0 && array[i] > array[i-1]) || (dir[i] && i != n-1 && array[i] > array[i+1])) && (array[i] > array[max] || max == n)) |
| max = i; |
| } |
| while (max < n); |
| // Ifd_ManDsdPermPrint(array,n); |
| Vec_IntPush( vGuide, 0 ); |
| free(dir); |
| free(array); |
| return vGuide; |
| } |
| int Ifd_ManDsdTest4() |
| { |
| int pPerm[6] = { 0, 1, 2, 3, 4, 5 }; |
| Vec_Int_t * vGuide = Ifd_ManDsdPermJT( 6 ); |
| int i, Entry; |
| Vec_IntForEachEntry( vGuide, Entry, i ) |
| { |
| ABC_SWAP( int, pPerm[Entry], pPerm[Entry+1] ); |
| Ifd_ManDsdPermPrint( pPerm, 6 ); |
| } |
| Vec_IntFree( vGuide ); |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline word Extra_Truth6SwapAdjacent( word t, int iVar ) |
| { |
| // variable swapping code |
| static word PMasks[5][3] = { |
| { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) }, |
| { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) }, |
| { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) }, |
| { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) }, |
| { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) } |
| }; |
| assert( iVar < 5 ); |
| return (t & PMasks[iVar][0]) | ((t & PMasks[iVar][1]) << (1 << iVar)) | ((t & PMasks[iVar][2]) >> (1 << iVar)); |
| } |
| static inline word Extra_Truth6ChangePhase( word t, int iVar) |
| { |
| // elementary truth tables |
| static word Truth6[6] = { |
| ABC_CONST(0xAAAAAAAAAAAAAAAA), |
| ABC_CONST(0xCCCCCCCCCCCCCCCC), |
| ABC_CONST(0xF0F0F0F0F0F0F0F0), |
| ABC_CONST(0xFF00FF00FF00FF00), |
| ABC_CONST(0xFFFF0000FFFF0000), |
| ABC_CONST(0xFFFFFFFF00000000) |
| }; |
| assert( iVar < 6 ); |
| return ((t & ~Truth6[iVar]) << (1 << iVar)) | ((t & Truth6[iVar]) >> (1 << iVar)); |
| } |
| Vec_Wrd_t * Extra_Truth6AllConfigs2( word t, int * pComp, int * pPerm, int nVars ) |
| { |
| int nPerms = Extra_Factorial( nVars ); |
| int nSwaps = (1 << nVars); |
| Vec_Wrd_t * vTruths = Vec_WrdStart( nPerms * (1 << (nVars+1)) ); |
| word tCur, tTemp1, tTemp2; |
| int i, p, c; |
| for ( i = 0; i < 2; i++ ) |
| { |
| tCur = i ? t : ~t; |
| tTemp1 = tCur; |
| for ( p = 0; p < nPerms; p++ ) |
| { |
| tTemp2 = tCur; |
| for ( c = 0; c < nSwaps; c++ ) |
| { |
| Vec_WrdWriteEntry( vTruths, (p << (nVars+1))|(i << nVars)|c, tCur ); |
| tCur = Extra_Truth6ChangePhase( tCur, pComp[c] ); |
| } |
| assert( tTemp2 == tCur ); |
| tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] ); |
| } |
| assert( tTemp1 == tCur ); |
| } |
| if ( t ) |
| { |
| int i; |
| word Truth; |
| Vec_WrdForEachEntry( vTruths, Truth, i ) |
| assert( Truth ); |
| } |
| return vTruths; |
| } |
| Vec_Wrd_t * Extra_Truth6AllConfigs( word t, int * pComp, int * pPerm, int nVars ) |
| { |
| int nPerms = Extra_Factorial( nVars ); |
| int nSwaps = (1 << nVars); |
| Vec_Wrd_t * vTruths = Vec_WrdStart( nPerms * nSwaps ); |
| word tCur = t, tTemp1, tTemp2; |
| int p, c, Config; |
| |
| tTemp1 = tCur; |
| for ( p = 0; p < nPerms; p++ ) |
| { |
| tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] ); |
| Config = 0; |
| tTemp2 = tCur; |
| for ( c = 0; c < nSwaps; c++ ) |
| { |
| Vec_WrdWriteEntry( vTruths, (p << nVars)|Config, tCur ); |
| tCur = Extra_Truth6ChangePhase( tCur, pComp[c] ); |
| Config ^= (1 << pComp[c]); |
| } |
| assert( Config == 0 ); |
| assert( tTemp2 == tCur ); |
| } |
| assert( tTemp1 == tCur ); |
| |
| if ( t ) |
| { |
| int i; |
| word Truth; |
| Vec_WrdForEachEntry( vTruths, Truth, i ) |
| assert( Truth ); |
| } |
| return vTruths; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ifd_ComputeSignature( word uTruth, int pCounts[6] ) |
| { |
| int v, Pos, Neg, Xor; |
| for ( v = 0; v < 6; v++ ) |
| { |
| Neg = Abc_TtCountOnes( Abc_Tt6Cofactor0(uTruth, v) ) / 2; |
| Pos = Abc_TtCountOnes( Abc_Tt6Cofactor1(uTruth, v) ) / 2; |
| Xor = Abc_TtCountOnes( Abc_Tt6Cofactor0(uTruth, v) ^ Abc_Tt6Cofactor1(uTruth, v) ) / 2; |
| if ( Pos <= Neg ) |
| pCounts[v] = (Pos << 20) | (Neg << 10) | Xor; |
| else |
| pCounts[v] = (Neg << 20) | (Pos << 10) | Xor; |
| } |
| Vec_IntSelectSort( pCounts, 6 ); |
| } |
| int Ifd_ManDsdTest33() |
| { |
| int nVars = 6; |
| Vec_Wrd_t * vTruths = Ifd_ManDsdTruths( nVars ); |
| int i, v, pCounts[6]; |
| word uTruth; |
| Vec_WrdForEachEntry( vTruths, uTruth, i ) |
| { |
| Ifd_ComputeSignature( uTruth, pCounts ); |
| // print |
| printf( "%5d : ", i ); |
| for ( v = 0; v < 6; v++ ) |
| printf( "%2d %2d %2d ", (pCounts[v] >> 20) & 0xFF, (pCounts[v] >> 10) & 0xFF, (pCounts[v] >> 0) & 0xFF ); |
| printf( " " ); |
| Kit_DsdPrintFromTruth( (unsigned *)&uTruth, nVars ); |
| printf( "\n" ); |
| } |
| Vec_WrdFree( vTruths ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ifd_ManDsdTest() |
| { |
| int nVars = 6; |
| FILE * pFile; |
| char pFileName[32]; |
| Vec_Wrd_t * vTruths = Ifd_ManDsdTruths( nVars ); |
| Vec_Wrd_t * vVariants; |
| Vec_Int_t * vUniques; |
| Vec_Int_t * vCompls; |
| Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( 4000000 ); |
| Vec_Int_t * vConfgRes = Vec_IntAlloc( 4000000 ); |
| int * pComp, * pPerm; |
| word Truth, Variant; |
| int i, k, Uniq, Runner, Counter = 0; |
| assert( nVars >= 3 && nVars <= 6 ); |
| assert( Vec_WrdSize(vTruths) < (1<<10) ); |
| vCompls = Vec_IntAlloc( 720 * 64 ); |
| pComp = Extra_GreyCodeSchedule( nVars ); |
| pPerm = Extra_PermSchedule( nVars ); |
| Vec_WrdForEachEntry( vTruths, Truth, i ) |
| { |
| vVariants = Extra_Truth6AllConfigs( Truth, pComp, pPerm, nVars ); |
| // save compl bits |
| Vec_IntClear( vCompls ); |
| Vec_WrdForEachEntry( vVariants, Variant, k ) |
| { |
| Vec_IntPush( vCompls, (int)(Variant & 1) ); |
| Vec_WrdWriteEntry( vVariants, k, Variant & 1 ? ~Variant : Variant ); |
| } |
| // uniqify |
| vUniques = Hsh_WrdManHashArray( vVariants, 1 ); |
| Runner = 0; |
| Vec_IntForEachEntry( vUniques, Uniq, k ) |
| if ( Runner == Uniq ) |
| { |
| Variant = Vec_WrdEntry(vVariants, k); |
| assert( (Variant & 1) == 0 ); |
| Vec_WrdPush( vTruthRes, Variant ); |
| Vec_IntPush( vConfgRes, (i << 17)|(Vec_IntEntry(vCompls, k) << 16)|k ); |
| Runner++; |
| } |
| Vec_IntUniqify( vUniques ); |
| assert( Runner == Vec_IntSize(vUniques) ); |
| Counter += Vec_IntSize(vUniques); |
| //printf( "%5d : ", i ); Kit_DsdPrintFromTruth( &Truth, nVars ), printf( " " ), Vec_IntPrint( vUniques ), printf( "\n" ); |
| Vec_IntFree( vUniques ); |
| Vec_WrdFree( vVariants ); |
| } |
| Vec_IntFree( vCompls ); |
| Vec_WrdFree( vTruths ); |
| ABC_FREE( pPerm ); |
| ABC_FREE( pComp ); |
| printf( "Total = %d.\n", Counter ); |
| assert( Vec_WrdSize(vTruthRes) == Counter ); |
| // write the data into a file |
| sprintf( pFileName, "dsdfuncs%d.dat", nVars ); |
| pFile = fopen( pFileName, "wb" ); |
| fwrite( Vec_WrdArray(vTruthRes), sizeof(word), Vec_WrdSize(vTruthRes), pFile ); |
| fwrite( Vec_IntArray(vConfgRes), sizeof(int), Vec_IntSize(vConfgRes), pFile ); |
| fclose( pFile ); |
| printf( "File \"%s\" with %d 6-input functions has been written out.\n", pFileName, Vec_IntSize(vConfgRes) ); |
| Vec_WrdFree( vTruthRes ); |
| Vec_IntFree( vConfgRes ); |
| return 1; |
| } |
| |
| int Ifd_ManDsdTest55() |
| { |
| abctime clk = Abc_Clock(); |
| FILE * pFile; |
| char * pFileName = "dsdfuncs6.dat"; |
| int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420 |
| Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size + 1 ); |
| Vec_Int_t * vConfgRes = Vec_IntAlloc( size ); |
| Hsh_IntMan_t * pHash; |
| |
| pFile = fopen( pFileName, "rb" ); |
| RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile ); |
| RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile ); |
| vTruthRes->nSize = size; |
| vConfgRes->nSize = size; |
| // create hash table |
| pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 ); |
| // experiment with functions |
| |
| // cleanup |
| Hsh_IntManStop( pHash ); |
| Vec_WrdFree( vTruthRes ); |
| Vec_IntFree( vConfgRes ); |
| Abc_PrintTime( 1, "Reading file", Abc_Clock() - clk ); |
| return 1; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
