From 27b8cce3feae55216049fcf8667d1ce6ef3794f2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 18 Dec 2022 20:06:07 -0800 Subject: [PATCH] Experiments with precomputation. --- src/aig/miniaig/miniaig.h | 6 ++ src/base/abci/abc.c | 1 + src/misc/util/utilTruth.h | 59 ++++++++++++++++ src/sat/bmc/bmcMaj.c | 141 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 207 insertions(+) diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 9aa41b119..6aa105643 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -103,6 +103,12 @@ static int Mini_AigNodeFanin1( Mini_Aig_t * p, int Id ) assert( p->pArray[2*Id+1] == MINI_AIG_NULL || p->pArray[2*Id+1] < 2*Id ); return p->pArray[2*Id+1]; } +static void Mini_AigFlipLastPo( Mini_Aig_t * p ) +{ + assert( p->pArray[p->nSize-1] == MINI_AIG_NULL ); + assert( p->pArray[p->nSize-2] != MINI_AIG_NULL ); + p->pArray[p->nSize-2] ^= 1; +} // working with variables and literals static int Mini_AigVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 36367a204..14f168703 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -14103,6 +14103,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder ); //Mnist_ExperimentWithScaling( nDecMax ); //Gyx_ProblemSolveTest(); + Exa_ManExactSynthesis4Vars(); { extern Abc_Ntk_t * Abc_NtkFromArray(); Abc_Ntk_t * pNtkRes = Abc_NtkFromArray(); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 1a771afa2..e7b83b255 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -664,6 +664,65 @@ static inline void Abc_TtIthVar( word * pOut, int iVar, int nVars ) pOut[k] = 0; } } +static inline void Abc_TtTruth2( word * pOut, word * pIn0, word * pIn1, int Truth, int nWords ) +{ + int w; + assert( Truth >= 0 && Truth <= 0xF ); + switch ( Truth ) + { + case 0x0 : for ( w = 0; w < nWords; w++ ) pOut[w] = 0; break; // 0000 + case 0x1 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & ~pIn0[w]; break; // 0001 + case 0x2 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & pIn0[w]; break; // 0010 + case 0x3 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] ; break; // 0011 + case 0x4 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & ~pIn0[w]; break; // 0100 + case 0x5 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn0[w]; break; // 0101 + case 0x6 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ pIn0[w]; break; // 0110 + case 0x7 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | ~pIn0[w]; break; // 0111 + case 0x8 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & pIn0[w]; break; // 1000 + case 0x9 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ ~pIn0[w]; break; // 1001 + case 0xA : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn0[w]; break; // 1010 + case 0xB : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | pIn0[w]; break; // 1011 + case 0xC : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ; break; // 1100 + case 0xD : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | ~pIn0[w]; break; // 1101 + case 0xE : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | pIn0[w]; break; // 1110 + case 0xF : for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0; break; // 1111 + default : assert( 0 ); + } +} +static inline void Abc_TtTruth4( word Entry, word ** pNodes, word * pOut, int nWords, int fCompl ) +{ + unsigned First = (unsigned)Entry; + unsigned Second = (unsigned)(Entry >> 32); + int i, k = 5; + for ( i = 0; i < 4; i++ ) + { + int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF; + if ( Pair == 0 ) + break; + Lit0 = Pair & 0xF; + Lit1 = Pair >> 4; + assert( Lit0 != Lit1 ); + if ( Lit0 < Lit1 ) + Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords ); + else + Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) ); + } + for ( i = 0; i < 3; i++ ) + { + int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF; + if ( Pair == 0 ) + break; + Lit0 = Pair & 0x1F; + Lit1 = Pair >> 5; + assert( Lit0 != Lit1 ); + if ( Lit0 < Lit1 ) + Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords ); + else + Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) ); + } + assert( k > 5 ); + Abc_TtCopy( pOut, pNodes[k-1], nWords, (int)(Entry >> 62) ^ fCompl ); +} /**Function************************************************************* diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 2525f943c..0f0838a31 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -2721,6 +2721,147 @@ void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars ) Vec_WrdFree( vSimsOut ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mini_AigPrintArray( FILE * pFile, Mini_Aig_t * p ) +{ + int i, Count = 0; + fprintf( pFile, " { " ); + Mini_AigForEachAnd( p, i ) + fprintf( pFile, "%2d,%2d, ", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin1(p, i) ), Count++; + Mini_AigForEachPo( p, i ) + fprintf( pFile, "%2d,%2d", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin0(p, i) ), Count++; + for ( i = Count; i < 8; i++ ) + fprintf( pFile, ", %2d,%2d", 0, 0 ); + fprintf( pFile, " }" ); +} +word Mini_AigWriteEntry( Mini_Aig_t * p ) +{ + word Res = 0; int i, k = 0; + Mini_AigForEachAnd( p, i ) + { + int iLit0 = Mini_AigNodeFanin0(p, i); + int iLit1 = Mini_AigNodeFanin1(p, i); + int Pair; + if ( k < 4 ) + { + assert( (iLit1 & 0xF) != (iLit0 & 0xF) ); + Pair = ((iLit1 & 0xF) << 4) | (iLit0 & 0xF); + Res |= (word)Pair << (k*8); + } + else + { + assert( (iLit1 & 0x1F) != (iLit0 & 0x1F) ); + Pair = ((iLit1 & 0x1F) << 5) | (iLit0 & 0x1F); + Res |= (word)Pair << (32 + (k-4)*10); + } + k++; + } + Mini_AigForEachPo( p, i ) + if ( Mini_AigNodeFanin0(p, i) & 1 ) + Res |= (word)1 << 62; + return Res; +} +word Abc_TtConvertEntry( word Res ) +{ + unsigned First = (unsigned)Res; + unsigned Second = (unsigned)(Res >> 32); + word Fun0, Fun1, Nodes[16] = {0}; int i, k = 5; + for ( i = 0; i < 4; i++ ) + Nodes[i+1] = s_Truths6[i]; + for ( i = 0; i < 4; i++ ) + { + int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF; + if ( Pair == 0 ) + break; + Lit0 = Pair & 0xF; + Lit1 = Pair >> 4; + assert( Lit0 != Lit1 ); + Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1]; + Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1]; + Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1; + } + for ( i = 0; i < 3; i++ ) + { + int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF; + if ( Pair == 0 ) + break; + Lit0 = Pair & 0x1F; + Lit1 = Pair >> 5; + assert( Lit0 != Lit1 ); + Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1]; + Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1]; + Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1; + } + return (Res >> 62) ? ~Nodes[k-1] : Nodes[k-1]; +} +word Exa_ManExactSynthesis4VarsOne( int Index, int Truth, int nNodes ) +{ + Mini_Aig_t * pMini = NULL; + int i, m, nMints = 16, fCompl = 0; + Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); + Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints ); + word pTruth[16] = { Abc_Tt6Stretch((word)Truth, 4) }; + if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, 1 ); } + for ( m = 0; m < nMints; m++ ) + { + Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) ); + for ( i = 0; i < 4; i++ ) + if ( (m >> i) & 1 ) + Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i ); + } + assert( Vec_WrdSize(vSimsIn) == 16 ); + pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, 4, 5, 1, nNodes, 0, 0, 0, 0, 0, 0 ); + if ( pMini && fCompl ) Mini_AigFlipLastPo( pMini ); + Vec_WrdFree( vSimsIn ); + Vec_WrdFree( vSimsOut ); + if ( pMini ) + { + /* + FILE * pTable = fopen( "min_xaig4.txt", "a+" ); + Mini_AigPrintArray( pTable, pMini ); + fprintf( pTable, ", // %d : 0x%04x (%d)\n", Index, Truth, nNodes ); + fclose( pTable ); + */ + word Res = Mini_AigWriteEntry( pMini ); + int uTruth = 0xFFFF & (int)Abc_TtConvertEntry( Res ); + if ( uTruth == Truth ) + printf( "Check ok.\n" ); + else + printf( "Check NOT ok!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\n" ); + Mini_AigStop( pMini ); + return Res; + } + return 0; +} +void Exa_ManExactSynthesis4Vars() +{ + int i, k, nFuncs = 1 << 15; + Vec_Wrd_t * vRes = Vec_WrdAlloc( nFuncs ); + Vec_WrdPush( vRes, 0 ); + for ( i = 1; i < nFuncs; i++ ) + { + word Res = 0; + printf( "\nFunction %d:\n", i ); + for ( k = 1; k < 8; k++ ) + if ( (Res = Exa_ManExactSynthesis4VarsOne( i, i, k )) ) + break; + assert( Res ); + Vec_WrdPush( vRes, Res ); + } + Vec_WrdDumpBin( "minxaig4.data", vRes, 1 ); + Vec_WrdFree( vRes ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////