diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/wlc/wlcGraft.c | 149 | ||||
| -rw-r--r-- | src/proof/acec/acec2Mult.c | 630 | ||||
| -rw-r--r-- | src/proof/acec/acecMult.c | 8 |
3 files changed, 612 insertions, 175 deletions
diff --git a/src/base/wlc/wlcGraft.c b/src/base/wlc/wlcGraft.c index 8ac825fc..f7e59cf9 100644 --- a/src/base/wlc/wlcGraft.c +++ b/src/base/wlc/wlcGraft.c @@ -285,6 +285,155 @@ Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose ) return pNew; } + + + + +/**Function************************************************************* + + Synopsis [Generate simulation vectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbc_Mult( word a, word b, word r[2] ) +{ + word pL = (a & 0xFFFFFFFF) * (b & 0xFFFFFFFF); + word pM1 = (a & 0xFFFFFFFF) * (b >> 32); + word pM2 = (a >> 32) * (b & 0xFFFFFFFF); + word pH = (a >> 32) * (b >> 32); + word Car = (pM1 & 0xFFFFFFFF) + (pM2 & 0xFFFFFFFF) + (pL >> 32); + r[0] = pL; + r[1] = pH + (pM1 >> 32) + (pM2 >> 32) + (Car >> 32); +} +void Sbc_SimMult( word A[64], word B[64], word R[64][2] ) +{ + word a, b, r[2]; int i, k; + for ( i = 0; i < 64; i++ ) + A[i] = B[i] = R[0][i] = R[1][i] = 0; + Gia_ManRandom(1); + for ( i = 0; i < 64; i++ ) + { + a = Gia_ManRandom(0); + b = Gia_ManRandom(0); + Sbc_Mult( a, b, r ); + for ( k = 0; k < 64; k++ ) + { + if ( (a >> k) & 1 ) A[k] |= (1 << i); + if ( (b >> k) & 1 ) B[k] |= (1 << i); + if ( (r[0] >> k) & 1 ) R[0][k] |= (1 << i); + if ( (r[1] >> k) & 1 ) R[1][k] |= (1 << i); + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sbc_ManDetectMult( Gia_Man_t * p, Vec_Int_t * vIns ) +{ + int nWords = 1; + Vec_Int_t * vNodes = Vec_IntStart( Vec_IntSize(vIns) ); + Gia_Obj_t * pObj; int i, Entry, nIns = Vec_IntSize(vIns)/2; + word A[64], B[64], R[64][2], * pInfoObj; + + // alloc simulation info + Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 ); + Vec_MemHashAlloc( vTtMem, 10000 ); + Vec_WrdFreeP( &p->vSims ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords ); + p->nSimWords = nWords; + + // prepare simulation manager + pInfoObj = Wlc_ObjSim( p, 0 ); + Vec_MemHashInsert( vTtMem, pInfoObj ); + Gia_ObjSetTravIdCurrentId( p, 0 ); + Gia_ManForEachCi( p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + // set internal nodes + assert( Vec_IntSize(vIns) % 2 ); + Sbc_SimMult( A, B, R ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vIns, p, pObj, i ) + { + Gia_ObjSetTravIdCurrent( p, pObj ); + pInfoObj = Wlc_ObjSim( p, Gia_ObjId(p, pObj) ); + *pInfoObj = i < nIns ? A[i] : B[nIns-i]; + } + // perform simulation + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + continue; + if ( Gia_ObjIsAnd(pObj) ) + Wlc_ObjSimAnd( p, i ); + else if ( Gia_ObjIsCo(pObj) ) + Wlc_ObjSimCo( p, i ); + else assert( 0 ); + + // mark each first node + pInfoObj = Wlc_ObjSim( p, i ); + Entry = *Vec_MemHashLookup( vTtMem, pInfoObj ); + if ( Entry > 0 ) + { + if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new + Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 0) ); + continue; + } + Abc_TtNot( pInfoObj, nWords ); + Entry = *Vec_MemHashLookup( vTtMem, pInfoObj ); + Abc_TtNot( pInfoObj, nWords ); + if ( Entry > 0 ) + { + if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new + Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 1) ); + continue; + } + } + // cleanup + Vec_MemHashFree( vTtMem ); + Vec_MemFreeP( &vTtMem ); + Vec_WrdFreeP( &p->vSims ); + p->nSimWords = 0; + return vNodes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbc_ManDetectMultTest( Gia_Man_t * p ) +{ + extern Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia ); + + Vec_Int_t * vIns = Sdb_StoComputeCutsDetect( p ); + Vec_Int_t * vNodes = Sbc_ManDetectMult( p, vIns ); + + Vec_IntPrint( vNodes ); + + Vec_IntFree( vNodes ); + Vec_IntFree( vIns ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/acec/acec2Mult.c b/src/proof/acec/acec2Mult.c index 62fd1279..d54ed007 100644 --- a/src/proof/acec/acec2Mult.c +++ b/src/proof/acec/acec2Mult.c @@ -24,7 +24,128 @@ ABC_NAMESPACE_IMPL_START -static unsigned s_FuncTruths[1920] = { + +static int s_nFuncTruths4a = 192; // 0xACC0 -- F(a=0) <== useful +static unsigned s_FuncTruths4a[192] = { +0xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860, +0x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8, +0xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06, +0x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E, +0xCA0C, 0xAC0A, 0xE230, 0xB822, 0xD844, 0xE450, 0xC0AC, 0xA0CA, 0xE320, 0xB282, 0xD484, 0xE540, +0xCB08, 0x8E82, 0xC0B8, 0x88E2, 0xD940, 0xD490, 0x8E84, 0xAD08, 0xB290, 0xB920, 0x88E4, 0xA0D8, +0xC50C, 0xA30A, 0xD130, 0x8B22, 0x8D44, 0xB150, 0xC05C, 0xA03A, 0xD310, 0x82B2, 0x84D4, 0xB510, +0xC704, 0x828E, 0xC074, 0x882E, 0x9D04, 0x90D4, 0x848E, 0xA702, 0x90B2, 0x9B02, 0x884E, 0xA072, +0xC5FC, 0xA3FA, 0xD1FC, 0x8BEE, 0x8DEE, 0xB1FA, 0xCF5C, 0xAF3A, 0xDF1C, 0x8EBE, 0x8EDE, 0xBF1A, +0xF734, 0xB2BE, 0xF374, 0xBB2E, 0xBF26, 0xB2F6, 0xD4DE, 0xF752, 0xD4F6, 0xDF46, 0xDD4E, 0xF572, +0xCAFC, 0xACFA, 0xE2FC, 0xB8EE, 0xD8EE, 0xE4FA, 0xCFAC, 0xAFCA, 0xEF2C, 0xBE8E, 0xDE8E, 0xEF4A, +0xFB38, 0xBEB2, 0xF3B8, 0xBBE2, 0xFB62, 0xF6B2, 0xDED4, 0xFD58, 0xF6D4, 0xFD64, 0xDDE4, 0xF5D8, +0x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160, +0xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E, +0x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706, +0xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8 +}; + + +/* +static int s_nFuncTruths4 = 192; // 0xF335 -- F(a=1) +static unsigned s_FuncTruths4[192] = { +0x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160, +0xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E, +0x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706, +0xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8, +0xC0AC, 0xA0CA, 0xC0B8, 0x88E2, 0x88E4, 0xA0D8, 0xCA0C, 0xAC0A, 0xCB08, 0x8E82, 0x8E84, 0xAD08, +0xE320, 0xB282, 0xE230, 0xB822, 0xB920, 0xB290, 0xD484, 0xE540, 0xD490, 0xD940, 0xD844, 0xE450, +0xC05C, 0xA03A, 0xC074, 0x882E, 0x884E, 0xA072, 0xC50C, 0xA30A, 0xC704, 0x828E, 0x848E, 0xA702, +0xD310, 0x82B2, 0xD130, 0x8B22, 0x9B02, 0x90B2, 0x84D4, 0xB510, 0x90D4, 0x9D04, 0x8D44, 0xB150, +0xCF5C, 0xAF3A, 0xF374, 0xBB2E, 0xDD4E, 0xF572, 0xC5FC, 0xA3FA, 0xF734, 0xB2BE, 0xD4DE, 0xF752, +0xDF1C, 0x8EBE, 0xD1FC, 0x8BEE, 0xDF46, 0xD4F6, 0x8EDE, 0xBF1A, 0xB2F6, 0xBF26, 0x8DEE, 0xB1FA, +0xCFAC, 0xAFCA, 0xF3B8, 0xBBE2, 0xDDE4, 0xF5D8, 0xCAFC, 0xACFA, 0xFB38, 0xBEB2, 0xDED4, 0xFD58, +0xEF2C, 0xBE8E, 0xE2FC, 0xB8EE, 0xFD64, 0xF6D4, 0xDE8E, 0xEF4A, 0xF6B2, 0xFB62, 0xD8EE, 0xE4FA, +0xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860, +0x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8, +0xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06, +0x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E +}; +*/ + +static int s_nFuncTruths4b = 48; // 0xF3C0 -- F(a=b) <== useful +static unsigned s_FuncTruths4b[48] = { +0xF3C0, 0xF5A0, 0xCFC0, 0xDD88, 0xBB88, 0xAFA0, 0xFC30, 0xFA50, 0xCCF0, 0xD8D8, 0xB8B8, 0xAAF0, +0xF0CC, 0xE4E4, 0xFC0C, 0xEE44, 0xAACC, 0xACAC, 0xE2E2, 0xF0AA, 0xCACA, 0xCCAA, 0xEE22, 0xFA0A, +0x3F0C, 0x5F0A, 0x3F30, 0x7722, 0x7744, 0x5F50, 0x30FC, 0x50FA, 0x33F0, 0x7272, 0x7474, 0x55F0, +0x0FCC, 0x4E4E, 0x0CFC, 0x44EE, 0x55CC, 0x5C5C, 0x2E2E, 0x0FAA, 0x3A3A, 0x33AA, 0x22EE, 0x0AFA +}; + +/* +static int s_nFuncTruths4 = 12; // 0x35AC -- F(a!=b) +static unsigned s_FuncTruths4[12] = { +0x35AC, 0x53CA, 0x1DB8, 0x47E2, 0x27E4, 0x1BD8, 0x3A5C, 0x5C3A, 0x4E72, 0x2E74, 0x724E, 0x742E +}; +*/ + +static int s_nFuncTruths4 = 384; // 0x35C0 -- F(b=0, c=0) <== useful +static unsigned s_FuncTruths4[384] = { +0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0, +0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22, +0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0, +0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88, +0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A, +0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522, +0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A, +0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588, +0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570, +0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A, +0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0, +0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A, +0xA3FC, 0xC5FA, 0x8BFC, 0xD1EE, 0xB1EE, 0x8DFA, 0xAF3C, 0xCF5A, 0x8FBC, 0xDE1E, 0xBE1E, 0x8FDA, +0xB3BC, 0xF636, 0xBB3C, 0xF366, 0xB3E6, 0xBE36, 0xF656, 0xD5DA, 0xDE56, 0xD5E6, 0xF566, 0xDD5A, +0x53FC, 0x35FA, 0x47FC, 0x1DEE, 0x1BEE, 0x27FA, 0x5F3C, 0x3F5A, 0x4F7C, 0x1EDE, 0x1EBE, 0x2F7A, +0x737C, 0x36F6, 0x773C, 0x3F66, 0x3B6E, 0x36BE, 0x56F6, 0x757A, 0x56DE, 0x5D6E, 0x5F66, 0x775A, +0x3FCA, 0x5FAC, 0x3FE2, 0x77B8, 0x77D8, 0x5FE4, 0x3CFA, 0x5AFC, 0x3EF2, 0x7B78, 0x7D78, 0x5EF4, +0x3ECE, 0x6F6C, 0x3CEE, 0x66FC, 0x76DC, 0x7D6C, 0x6F6A, 0x5EAE, 0x7B6A, 0x76BA, 0x66FA, 0x5AEE, +0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E, +0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544, +0xCF3A, 0xAF5C, 0xF32E, 0xBB74, 0xDD72, 0xF54E, 0xC3FA, 0xA5FC, 0xF23E, 0xB7B4, 0xD7D2, 0xF45E, +0xCE3E, 0x9F9C, 0xC3EE, 0x99FC, 0xDC76, 0xD7C6, 0x9F9A, 0xAE5E, 0xB7A6, 0xBA76, 0x99FA, 0xA5EE, +0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4, +0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44, +0xF3AC, 0xF5CA, 0xCFB8, 0xDDE2, 0xBBE4, 0xAFD8, 0xFA3C, 0xFC5A, 0xCBF8, 0xDED2, 0xBEB4, 0xADF8, +0xE3EC, 0xF6C6, 0xEE3C, 0xFC66, 0xB9EC, 0xBE9C, 0xF6A6, 0xE5EA, 0xDE9A, 0xD9EA, 0xFA66, 0xEE5A, +0xF35C, 0xF53A, 0xCF74, 0xDD2E, 0xBB4E, 0xAF72, 0xF53C, 0xF35A, 0xC7F4, 0xD2DE, 0xB4BE, 0xA7F2, +0xD3DC, 0xC6F6, 0xDD3C, 0xCF66, 0x9BCE, 0x9CBE, 0xA6F6, 0xB5BA, 0x9ADE, 0x9DAE, 0xAF66, 0xBB5A, +0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752, +0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A, +0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58, +0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A +}; + +/* +static int s_nFuncTruths4 = 96; // 0xFD80 -- F(d=0) +static unsigned s_FuncTruths4[96] = { +0xFD80, 0xFB80, 0xEF80, 0xF8D0, 0xF8B0, 0xE8F0, 0xECC4, 0xE8CC, 0xEC8C, 0xE8AA, 0xEAA2, 0xEA8A, +0xFE40, 0xFE20, 0xFE08, 0xF4E0, 0xF2E0, 0xF0E8, 0xDCC8, 0xCCE8, 0xCEC8, 0xAAE8, 0xBAA8, 0xAEA8, +0xF720, 0xF740, 0xDF08, 0xDF40, 0xBF20, 0xBF08, 0xF270, 0xF470, 0xD0F8, 0xD4F0, 0xB2F0, 0xB0F8, +0xC4EC, 0xD4CC, 0xCE4C, 0xDC4C, 0x8CEC, 0x8ECC, 0xB2AA, 0xA2EA, 0x8EAA, 0x8AEA, 0xBA2A, 0xAE2A, +0xFB10, 0xFD10, 0xEF04, 0xFD04, 0xFB02, 0xEF02, 0xF1B0, 0xF1D0, 0xE0F4, 0xF0D4, 0xF0B2, 0xE0F2, +0xC8DC, 0xCCD4, 0xCD8C, 0xCDC4, 0xC8CE, 0xCC8E, 0xAAB2, 0xA8BA, 0xAA8E, 0xA8AE, 0xABA2, 0xAB8A, +0x7F02, 0x7F04, 0x7F10, 0x70F2, 0x70F4, 0x71F0, 0x4CCE, 0x4DCC, 0x4CDC, 0x2BAA, 0x2AAE, 0x2ABA, +0x40FE, 0x20FE, 0x08FE, 0x4F0E, 0x2F0E, 0x0F8E, 0x7332, 0x33B2, 0x3B32, 0x55D4, 0x7554, 0x5D54, +}; +*/ + +/* +static int s_nFuncTruths4 = 48; // 0xD728 -- F(e=0) +static unsigned s_FuncTruths4[48] = { +0xD728, 0xB748, 0x9F60, 0xD278, 0xB478, 0x96F0, 0xC66C, 0x96CC, 0x9C6C, 0x96AA, 0xA66A, 0x9A6A, +0xEB14, 0xED12, 0xF906, 0xE1B4, 0xE1D2, 0xF096, 0xC99C, 0xCC96, 0xC9C6, 0xAA96, 0xA99A, 0xA9A6, +0x7D82, 0x7B84, 0x6F90, 0x78D2, 0x78B4, 0x69F0, 0x6CC6, 0x69CC, 0x6C9C, 0x69AA, 0x6AA6, 0x6A9A, +0x41BE, 0x21DE, 0x09F6, 0x4B1E, 0x2D1E, 0x0F96, 0x6336, 0x3396, 0x3936, 0x5596, 0x6556, 0x5956 +}; +*/ + + +static int s_nFuncTruths5 = 960; // 0xF335ACC0 +static unsigned s_FuncTruths5[960] = { 0xF335ACC0, 0xF553CAA0, 0xCF1DB8C0, 0xDD47E288, 0xBB27E488, 0xAF1BD8A0, 0xC1FDBC80, 0xD4D7E828, 0xB2B7E848, 0xA1FBDA80, 0x89EFE680, 0x8E9FE860, 0xF3AC35C0, 0xF5CA53A0, 0xCFB81DC0, 0xDDE24788, 0xBBE42788, 0xAFD81BA0, 0xC1BCFD80, 0xD4E8D728, 0xB2E8B748, 0xA1DAFB80, 0x89E6EF80, 0x8EE89F60, @@ -32,29 +153,14 @@ static unsigned s_FuncTruths[1920] = { 0xBEB42878, 0xADF81AB0, 0x8EE896F0, 0x8E96E8F0, 0xE334ECC4, 0xF660C66C, 0xEE3C3C44, 0xFC66660C, 0xB926EC8C, 0xBE289C6C, 0xE3EC34C4, 0xF6C6606C, 0xB296E8CC, 0xB2E896CC, 0xB9EC268C, 0xBE9C286C, 0xF660A66A, 0xE552EAA2, 0xDE489A6A, 0xD946EA8A, 0xFA66660A, 0xEE5A5A22, 0xD4E896AA, 0xD496E8AA, -0xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0x0CCA533F, 0x0AAC355F, 0x30E2473F, 0x22B81D77, -0x44D81B77, 0x50E4275F, 0x3E02437F, 0x2B2817D7, 0x4D4817B7, 0x5E04257F, 0x7610197F, 0x7160179F, -0x0C53CA3F, 0x0A35AC5F, 0x3047E23F, 0x221DB877, 0x441BD877, 0x5027E45F, 0x3E43027F, 0x2B1728D7, -0x4D1748B7, 0x5E25047F, 0x7619107F, 0x7117609F, 0x05C3C3AF, 0x03A5A5CF, 0x34E3072F, 0x21B72D87, -0x41D74B87, 0x52E5074F, 0x3407E32F, 0x212DB787, 0x414BD787, 0x5207E54F, 0x7117690F, 0x7169170F, -0x1CCB133B, 0x099F3993, 0x11C3C3BB, 0x039999F3, 0x46D91373, 0x41D76393, 0x1C13CB3B, 0x09399F93, -0x4D691733, 0x4D176933, 0x4613D973, 0x4163D793, 0x099F5995, 0x1AAD155D, 0x21B76595, 0x26B91575, -0x059999F5, 0x11A5A5DD, 0x2B176955, 0x2B691755, 0x09599F95, 0x1A15AD5D, 0x2615B975, 0x2165B795, -0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88, 0xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8, -0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8, 0xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488, -0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8, 0xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8, -0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48, 0xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848, -0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8, 0xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0, -0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60, 0x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28, -0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8, 0xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8, -0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48, 0x0CC5A33F, 0x0AA3C55F, 0x30D18B3F, 0x228BD177, -0x448DB177, 0x50B18D5F, 0x3D0183BF, 0x282BD717, 0x484DB717, 0x5B0185DF, 0x670191F7, 0x60719F17, -0x0CA3C53F, 0x0AC5A35F, 0x308BD13F, 0x22D18B77, 0x44B18D77, 0x508DB15F, 0x3D8301BF, 0x28D72B17, -0x48B74D17, 0x5B8501DF, 0x679101F7, 0x609F7117, 0x0AC3C35F, 0x0CA5A53F, 0x38D30B1F, 0x2D8721B7, -0x4B8741D7, 0x58B50D1F, 0x380BD31F, 0x2D2187B7, 0x4B4187D7, 0x580DB51F, 0x690F7117, 0x69710F17, -0x2CC72337, 0x3993099F, 0x22C3C377, 0x3099993F, 0x649D3137, 0x639341D7, 0x2C23C737, 0x3909939F, -0x694D3317, 0x69334D17, 0x64319D37, 0x634193D7, 0x5995099F, 0x4AA74557, 0x659521B7, 0x629B5157, -0x5099995F, 0x44A5A577, 0x69552B17, 0x692B5517, 0x5909959F, 0x4A45A757, 0x62519B57, 0x652195B7, +0xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88, +0xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8, 0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8, +0xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488, 0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8, +0xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8, 0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48, +0xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848, 0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8, +0xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0, 0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60, +0x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28, 0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8, +0xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8, 0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48, 0xFCC5A330, 0xFAA3C550, 0xFCD18B0C, 0xEE8BD144, 0xEE8DB122, 0xFAB18D0A, 0xFDC180BC, 0xE8EBD414, 0xE8EDB212, 0xFBA180DA, 0xEF8980E6, 0xE8F98E06, 0xFCA3C530, 0xFAC5A350, 0xFC8BD10C, 0xEED18B44, 0xEEB18D22, 0xFA8DB10A, 0xFD80C1BC, 0xE8D4EB14, 0xE8B2ED12, 0xFB80A1DA, 0xEF8089E6, 0xE88EF906, @@ -62,29 +168,14 @@ static unsigned s_FuncTruths[1920] = { 0xEBE182D2, 0xF8ADB01A, 0xE88EF096, 0xE8F08E96, 0xECC4E334, 0xF990C99C, 0xEEC3C344, 0xFC99990C, 0xEC8CB926, 0xEB82C9C6, 0xECE3C434, 0xF9C9909C, 0xE8CCB296, 0xE8B2CC96, 0xECB98C26, 0xEBC982C6, 0xF990A99A, 0xEAA2E552, 0xED84A9A6, 0xEA8AD946, 0xFA99990A, 0xEEA5A522, 0xE8D4AA96, 0xE8AAD496, -0xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0x033A5CCF, 0x055C3AAF, 0x032E74F3, 0x11742EBB, -0x11724EDD, 0x054E72F5, 0x023E7F43, 0x17142BEB, 0x17124DED, 0x045E7F25, 0x10767F19, 0x170671F9, -0x035C3ACF, 0x053A5CAF, 0x03742EF3, 0x112E74BB, 0x114E72DD, 0x05724EF5, 0x027F3E43, 0x172B14EB, -0x174D12ED, 0x047F5E25, 0x107F7619, 0x177106F9, 0x053C3CAF, 0x035A5ACF, 0x072F34E3, 0x127B1E4B, -0x147D1E2D, 0x074F52E5, 0x07342FE3, 0x121E7B4B, 0x141E7D2D, 0x07524FE5, 0x17710F69, 0x170F7169, -0x133B1CCB, 0x066F3663, 0x113C3CBB, 0x036666F3, 0x137346D9, 0x147D3639, 0x131C3BCB, 0x06366F63, -0x17334D69, 0x174D3369, 0x134673D9, 0x14367D39, 0x066F5665, 0x155D1AAD, 0x127B5659, 0x157526B9, -0x056666F5, 0x115A5ADD, 0x172B5569, 0x17552B69, 0x06566F65, 0x151A5DAD, 0x152675B9, 0x12567B59, -0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44, 0xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4, -0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E, 0xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844, -0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4, 0xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E, -0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84, 0xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484, -0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E, 0xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0, -0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90, 0xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682, -0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64, 0xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4, -0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684, 0x0335ACCF, 0x0553CAAF, 0x031DB8F3, 0x1147E2BB, -0x1127E4DD, 0x051BD8F5, 0x013DBF83, 0x1417EB2B, 0x1217ED4D, 0x015BDF85, 0x0167F791, 0x0617F971, -0x03AC35CF, 0x05CA53AF, 0x03B81DF3, 0x11E247BB, 0x11E427DD, 0x05D81BF5, 0x01BF3D83, 0x14EB172B, -0x12ED174D, 0x01DF5B85, 0x01F76791, 0x06F91771, 0x0A3C3C5F, 0x0C5A5A3F, 0x0B1F38D3, 0x1E4B127B, -0x1E2D147D, 0x0D1F58B5, 0x0B381FD3, 0x1E124B7B, 0x1E142D7D, 0x0D581FB5, 0x0F691771, 0x0F176971, -0x23372CC7, 0x3663066F, 0x223C3C77, 0x3066663F, 0x3137649D, 0x3639147D, 0x232C37C7, 0x3606636F, -0x3317694D, 0x3369174D, 0x3164379D, 0x3614397D, 0x5665066F, 0x45574AA7, 0x5659127B, 0x5157629B, -0x5066665F, 0x445A5A77, 0x5569172B, 0x5517692B, 0x5606656F, 0x454A57A7, 0x5162579B, 0x5612597B, +0xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44, +0xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4, 0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E, +0xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844, 0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4, +0xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E, 0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84, +0xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484, 0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E, +0xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0, 0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90, +0xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682, 0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64, +0xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4, 0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684, 0x3F53CA0C, 0x5F35AC0A, 0x3F47E230, 0x771DB822, 0x771BD844, 0x5F27E450, 0x35F3C0AC, 0x53F5A0CA, 0x34F7E320, 0x717DB282, 0x717BD484, 0x52F7E540, 0x1CDFCB08, 0x4D7D8E82, 0x1DCFC0B8, 0x47DD88E2, 0x46DFD940, 0x4D6FD490, 0x2B7B8E84, 0x1ABFAD08, 0x2B6FB290, 0x26BFB920, 0x27BB88E4, 0x1BAFA0D8, @@ -100,21 +191,6 @@ static unsigned s_FuncTruths[1920] = { 0x6F066AA6, 0x5E25AE2A, 0x7B126A9A, 0x7619BA2A, 0x660AFA66, 0x5A22EE5A, 0x60F66AA6, 0x52E5A2EA, 0x71B269AA, 0x7169B2AA, 0x606AF6A6, 0x52A2E5EA, 0x4D8E69AA, 0x4D698EAA, 0x48DE6A9A, 0x46D98AEA, 0x468AD9EA, 0x486ADE9A, 0x6F6A06A6, 0x5EAE252A, 0x7B6A129A, 0x76BA192A, 0x66FA0A66, 0x5AEE225A, -0xC0AC35F3, 0xA0CA53F5, 0xC0B81DCF, 0x88E247DD, 0x88E427BB, 0xA0D81BAF, 0xCA0C3F53, 0xAC0A5F35, -0xCB081CDF, 0x8E824D7D, 0x8E842B7B, 0xAD081ABF, 0xE32034F7, 0xB282717D, 0xE2303F47, 0xB822771D, -0xB92026BF, 0xB2902B6F, 0xD484717B, 0xE54052F7, 0xD4904D6F, 0xD94046DF, 0xD844771B, 0xE4505F27, -0xC035ACF3, 0xA053CAF5, 0xC01DB8CF, 0x8847E2DD, 0x8827E4BB, 0xA01BD8AF, 0xCA3F0C53, 0xAC5F0A35, -0xCB1C08DF, 0x8E4D827D, 0x8E2B847B, 0xAD1A08BF, 0xE33420F7, 0xB271827D, 0xE23F3047, 0xB877221D, -0xB92620BF, 0xB22B906F, 0xD471847B, 0xE55240F7, 0xD44D906F, 0xD94640DF, 0xD877441B, 0xE45F5027, -0xC3AF05C3, 0xA5CF03A5, 0xC1BC0D8F, 0x84ED872D, 0x82EB874B, 0xA1DA0B8F, 0xC305AFC3, 0xA503CFA5, -0xC10DBC8F, 0x8487ED2D, 0x8287EB4B, 0xA10BDA8F, 0xE32F3407, 0xB787212D, 0xE3342F07, 0xB721872D, -0xB22B960F, 0xB2962B0F, 0xD787414B, 0xE54F5207, 0xD4964D0F, 0xD44D960F, 0xD741874B, 0xE5524F07, -0xC1BC31B3, 0x90F99339, 0xC3BB11C3, 0x99F30399, 0x89E623B3, 0x82EB9363, 0xCB1C3B13, 0x9F099339, -0xCB3B1C13, 0x9F930939, 0x8E962B33, 0x8E2B9633, 0xC131BCB3, 0x9093F939, 0xC311BBC3, 0x9903F399, -0x8923E6B3, 0x8293EB63, 0xD4967133, 0xD4719633, 0xD7934163, 0xD9734613, 0xD9467313, 0xD7419363, -0x90F99559, 0xA1DA51D5, 0x84ED9565, 0x89E645D5, 0x99F50599, 0xA5DD11A5, 0x9F099559, 0xAD1A5D15, -0x8E4D9655, 0x8E964D55, 0x9F950959, 0xAD5D1A15, 0xB2719655, 0xB2967155, 0xB7219565, 0xB9267515, -0xB9752615, 0xB7952165, 0x9095F959, 0xA151DAD5, 0x8495ED65, 0x8945E6D5, 0x9905F599, 0xA511DDA5, 0x3FA3C50C, 0x5FC5A30A, 0x3F8BD130, 0x77D18B22, 0x77B18D44, 0x5F8DB150, 0x3AF3C05C, 0x5CF5A03A, 0x38FBD310, 0x7D7182B2, 0x7B7184D4, 0x58FDB510, 0x2CEFC704, 0x7D4D828E, 0x2ECFC074, 0x74DD882E, 0x64FD9D04, 0x6F4D90D4, 0x7B2B848E, 0x4AEFA702, 0x6F2B90B2, 0x62FB9B02, 0x72BB884E, 0x4EAFA072, @@ -130,36 +206,6 @@ static unsigned s_FuncTruths[1920] = { 0x6AA66F06, 0x5B85AB8A, 0x6A9A7B12, 0x6791ABA2, 0x66A0AF66, 0x5A88BB5A, 0x6AA660F6, 0x58B5A8BA, 0x69AA71B2, 0x6971AAB2, 0x6A60A6F6, 0x58A8B5BA, 0x69AA4D8E, 0x694DAA8E, 0x6A9A48DE, 0x649DA8AE, 0x64A89DAE, 0x6A489ADE, 0x6A6FA606, 0x5BAB858A, 0x6A7B9A12, 0x67AB91A2, 0x66AFA066, 0x5ABB885A, -0xC05C3AF3, 0xA03A5CF5, 0xC0742ECF, 0x882E74DD, 0x884E72BB, 0xA0724EAF, 0xC50C3FA3, 0xA30A5FC5, -0xC7042CEF, 0x828E7D4D, 0x848E7B2B, 0xA7024AEF, 0xD31038FB, 0x82B27D71, 0xD1303F8B, 0x8B2277D1, -0x9B0262FB, 0x90B26F2B, 0x84D47B71, 0xB51058FD, 0x90D46F4D, 0x9D0464FD, 0x8D4477B1, 0xB1505F8D, -0xC03A5CF3, 0xA05C3AF5, 0xC02E74CF, 0x88742EDD, 0x88724EBB, 0xA04E72AF, 0xC53F0CA3, 0xA35F0AC5, -0xC72C04EF, 0x827D8E4D, 0x847B8E2B, 0xA74A02EF, 0xD33810FB, 0x827DB271, 0xD13F308B, 0x8B7722D1, -0x9B6202FB, 0x906FB22B, 0x847BD471, 0xB55810FD, 0x906FD44D, 0x9D6404FD, 0x8D7744B1, 0xB15F508D, -0xC35F0AC3, 0xA53F0CA5, 0xC27C0E4F, 0x872D84ED, 0x874B82EB, 0xA47A0E2F, 0xC30A5FC3, 0xA50C3FA5, -0xC20E7C4F, 0x87842DED, 0x87824BEB, 0xA40E7A2F, 0xD31F380B, 0x87B72D21, 0xD3381F0B, 0x872DB721, -0x960FB22B, 0x96B20F2B, 0x87D74B41, 0xB51F580D, 0x96D40F4D, 0x960FD44D, 0x874BD741, 0xB5581F0D, -0xC27C3273, 0x933990F9, 0xC37722C3, 0x993F3099, 0x986E323B, 0x936382EB, 0xC72C3723, 0x93399F09, -0xC7372C23, 0x939F3909, 0x968E332B, 0x96338E2B, 0xC2327C73, 0x939039F9, 0xC32277C3, 0x99303F99, -0x98326E3B, 0x938263EB, 0x96D43371, 0x9633D471, 0x93D76341, 0x9D376431, 0x9D643731, 0x9363D741, -0x955990F9, 0xA47A5475, 0x956584ED, 0x986E545D, 0x995F5099, 0xA57744A5, 0x95599F09, 0xA74A5745, -0x96558E4D, 0x968E554D, 0x959F5909, 0xA7574A45, 0x9655B271, 0x96B25571, 0x9565B721, 0x9B625751, -0x9B576251, 0x95B76521, 0x959059F9, 0xA4547A75, 0x958465ED, 0x98546E5D, 0x99505F99, 0xA54477A5, -0xCF5C3A03, 0xAF3A5C05, 0xF3742E03, 0xBB2E7411, 0xDD4E7211, 0xF5724E05, 0xC5FC30A3, 0xA3FA50C5, -0xF73420E3, 0xB2BE7141, 0xD4DE7121, 0xF75240E5, 0xDF1C08CB, 0x8EBE4D41, 0xD1FC0C8B, 0x8BEE44D1, -0xDF4640D9, 0xD4F64D09, 0x8EDE2B21, 0xBF1A08AD, 0xB2F62B09, 0xBF2620B9, 0x8DEE22B1, 0xB1FA0A8D, -0xCF3A5C03, 0xAF5C3A05, 0xF32E7403, 0xBB742E11, 0xDD724E11, 0xF54E7205, 0xC530FCA3, 0xA350FAC5, -0xF72034E3, 0xB271BE41, 0xD471DE21, 0xF74052E5, 0xDF081CCB, 0x8E4DBE41, 0xD10CFC8B, 0x8B44EED1, -0xDF4046D9, 0xD44DF609, 0x8E2BDE21, 0xBF081AAD, 0xB22BF609, 0xBF2026B9, 0x8D22EEB1, 0xB10AFA8D, -0xC350FAC3, 0xA530FCA5, 0xF2703E43, 0xB721B4E1, 0xD741D2E1, 0xF4705E25, 0xC3FA50C3, 0xA5FC30A5, -0xF23E7043, 0xB7B421E1, 0xD7D241E1, 0xF45E7025, 0xD01CF8CB, 0x84B4EDE1, 0xD0F81CCB, 0x84EDB4E1, -0xD44DF069, 0xD4F04D69, 0x82D2EBE1, 0xB01AF8AD, 0xB2F02B69, 0xB22BF069, 0x82EBD2E1, 0xB0F81AAD, -0xCE4C3E43, 0x9F099CC9, 0xC344EEC3, 0x990CFC99, 0xDC4C7619, 0xD741C6C9, 0xC4EC34E3, 0x90F99CC9, -0xC434ECE3, 0x909CF9C9, 0xD4CC7169, 0xD471CC69, 0xCE3E4C43, 0x9F9C09C9, 0xC3EE44C3, 0x99FC0C99, -0xDC764C19, 0xD7C641C9, 0x8ECC2B69, 0x8E2BCC69, 0x82C6EBC9, 0x8C26ECB9, 0x8CEC26B9, 0x82EBC6C9, -0x9F099AA9, 0xAE2A5E25, 0xB721A6A9, 0xBA2A7619, 0x990AFA99, 0xA522EEA5, 0x90F99AA9, 0xA2EA52E5, -0xB271AA69, 0xB2AA7169, 0x909AF9A9, 0xA252EAE5, 0x8E4DAA69, 0x8EAA4D69, 0x84EDA6A9, 0x8AEA46D9, -0x8A46EAD9, 0x84A6EDA9, 0x9F9A09A9, 0xAE5E2A25, 0xB7A621A9, 0xBA762A19, 0x99FA0A99, 0xA5EE22A5, 0x30A3C5FC, 0x50C5A3FA, 0x0C8BD1FC, 0x44D18BEE, 0x22B18DEE, 0x0A8DB1FA, 0x3A03CF5C, 0x5C05AF3A, 0x08CBDF1C, 0x4D418EBE, 0x2B218EDE, 0x08ADBF1A, 0x20E3F734, 0x7141B2BE, 0x2E03F374, 0x7411BB2E, 0x20B9BF26, 0x2B09B2F6, 0x7121D4DE, 0x40E5F752, 0x4D09D4F6, 0x40D9DF46, 0x7211DD4E, 0x4E05F572, @@ -175,21 +221,6 @@ static unsigned s_FuncTruths[1920] = { 0x60F66556, 0x51D5A1DA, 0x48DE5956, 0x45D589E6, 0x66F50566, 0x5ADD115A, 0x6F066556, 0x5D15AD1A, 0x4D8E5596, 0x4D558E96, 0x6F650656, 0x5DAD151A, 0x71B25596, 0x7155B296, 0x7B125956, 0x7515B926, 0x75B91526, 0x7B591256, 0x6065F656, 0x51A1D5DA, 0x4859DE56, 0x4589D5E6, 0x6605F566, 0x5A11DD5A, -0xCFAC3503, 0xAFCA5305, 0xF3B81D03, 0xBBE24711, 0xDDE42711, 0xF5D81B05, 0xCAFC3053, 0xACFA5035, -0xFB3810D3, 0xBEB24171, 0xDED42171, 0xFD5810B5, 0xEF2C04C7, 0xBE8E414D, 0xE2FC0C47, 0xB8EE441D, -0xFD64049D, 0xF6D4094D, 0xDE8E212B, 0xEF4A02A7, 0xF6B2092B, 0xFB62029B, 0xD8EE221B, 0xE4FA0A27, -0xCF35AC03, 0xAF53CA05, 0xF31DB803, 0xBB47E211, 0xDD27E411, 0xF51BD805, 0xCA30FC53, 0xAC50FA35, -0xFB1038D3, 0xBE41B271, 0xDE21D471, 0xFD1058B5, 0xEF042CC7, 0xBE418E4D, 0xE20CFC47, 0xB844EE1D, -0xFD04649D, 0xF609D44D, 0xDE218E2B, 0xEF024AA7, 0xF609B22B, 0xFB02629B, 0xD822EE1B, 0xE40AFA27, -0xC3A0F5C3, 0xA5C0F3A5, 0xF1B03D83, 0xB4E1B721, 0xD2E1D741, 0xF1D05B85, 0xC3F5A0C3, 0xA5F3C0A5, -0xF13DB083, 0xB4B7E121, 0xD2D7E141, 0xF15BD085, 0xE02CF4C7, 0xB484E1ED, 0xE0F42CC7, 0xB4E184ED, -0xF069D44D, 0xF0D4694D, 0xD282E1EB, 0xE04AF2A7, 0xF0B2692B, 0xF069B22B, 0xD2E182EB, 0xE0F24AA7, -0xCD8C3D83, 0x9CC99F09, 0xC388DDC3, 0x99C0CF99, 0xCDC46791, 0xC6C9D741, 0xC8DC38D3, 0x9CC990F9, -0xC838DCD3, 0x9C90C9F9, 0xCCD46971, 0xCC69D471, 0xCD3D8C83, 0x9C9FC909, 0xC3DD88C3, 0x99CFC099, -0xCD67C491, 0xC6D7C941, 0xCC8E692B, 0xCC698E2B, 0xC682C9EB, 0xC862CE9B, 0xC8CE629B, 0xC6C982EB, -0x9AA99F09, 0xAB8A5B85, 0xA6A9B721, 0xABA26791, 0x99A0AF99, 0xA588BBA5, 0x9AA990F9, 0xA8BA58B5, -0xAA69B271, 0xAAB26971, 0x9A90A9F9, 0xA858BAB5, 0xAA698E4D, 0xAA8E694D, 0xA6A984ED, 0xA8AE649D, -0xA864AE9D, 0xA684A9ED, 0x9A9FA909, 0xAB5B8A85, 0xA6B7A921, 0xAB67A291, 0x99AFA099, 0xA5BB88A5, 0x3053CAFC, 0x5035ACFA, 0x0C47E2FC, 0x441DB8EE, 0x221BD8EE, 0x0A27E4FA, 0x3503CFAC, 0x5305AFCA, 0x04C7EF2C, 0x414DBE8E, 0x212BDE8E, 0x02A7EF4A, 0x10D3FB38, 0x4171BEB2, 0x1D03F3B8, 0x4711BBE2, 0x029BFB62, 0x092BF6B2, 0x2171DED4, 0x10B5FD58, 0x094DF6D4, 0x049DFD64, 0x2711DDE4, 0x1B05F5D8, @@ -212,22 +243,7 @@ static unsigned s_FuncTruths[1920] = { 0x14B47D78, 0x25705EF4, 0x177196F0, 0x179671F0, 0x433E4CCE, 0x066FC66C, 0x443C3CEE, 0x0C6666FC, 0x19764CDC, 0x147D9C6C, 0x434C3ECE, 0x06C66F6C, 0x17964DCC, 0x174D96CC, 0x194C76DC, 0x149C7D6C, 0x066FA66A, 0x255E2AAE, 0x127B9A6A, 0x19762ABA, 0x0A6666FA, 0x225A5AEE, 0x172B96AA, 0x17962BAA, -0x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0xACC0F335, 0xCAA0F553, 0xB8C0CF1D, 0xE288DD47, -0xE488BB27, 0xD8A0AF1B, 0xBC80C1FD, 0xE828D4D7, 0xE848B2B7, 0xDA80A1FB, 0xE68089EF, 0xE8608E9F, -0xACF3C035, 0xCAF5A053, 0xB8CFC01D, 0xE2DD8847, 0xE4BB8827, 0xD8AFA01B, 0xBCC180FD, 0xE8D428D7, -0xE8B248B7, 0xDAA180FB, 0xE68980EF, 0xE88E609F, 0xAFC3C305, 0xCFA5A503, 0xBCC18F0D, 0xED842D87, -0xEB824B87, 0xDAA18F0B, 0xBC8FC10D, 0xED2D8487, 0xEB4B8287, 0xDA8FA10B, 0xE88E690F, 0xE8698E0F, -0xBCC1B331, 0xF9903993, 0xBBC3C311, 0xF3999903, 0xE689B323, 0xEB826393, 0xBCB3C131, 0xF9399093, -0xE869B233, 0xE8B26933, 0xE6B38923, 0xEB638293, 0xF9905995, 0xDAA1D551, 0xED846595, 0xE689D545, -0xF5999905, 0xDDA5A511, 0xE8D46955, 0xE869D455, 0xF9599095, 0xDAD5A151, 0xE6D58945, 0xED658495, -0xA33F0CC5, 0xC55F0AA3, 0x8B3F30D1, 0xD177228B, 0xB177448D, 0x8D5F50B1, 0x83BF3D01, 0xD717282B, -0xB717484D, 0x85DF5B01, 0x91F76701, 0x9F176071, 0xA30C3FC5, 0xC50A5FA3, 0x8B303FD1, 0xD122778B, -0xB144778D, 0x8D505FB1, 0x833DBF01, 0xD728172B, 0xB748174D, 0x855BDF01, 0x9167F701, 0x9F601771, -0xA03C3CF5, 0xC05A5AF3, 0x833DB0F1, 0xD278127B, 0xB478147D, 0x855BD0F1, 0x83B03DF1, 0xD212787B, -0xB414787D, 0x85D05BF1, 0x96F01771, 0x9617F071, 0x833D8CCD, 0xC66C066F, 0x883C3CDD, 0xC06666CF, -0x9167C4CD, 0x9C6C147D, 0x838C3DCD, 0xC6066C6F, 0x9617CC4D, 0x96CC174D, 0x91C467CD, 0x9C146C7D, -0xA66A066F, 0x855B8AAB, 0x9A6A127B, 0x9167A2AB, 0xA06666AF, 0x885A5ABB, 0x96AA172B, 0x9617AA2B, -0xA6066A6F, 0x858A5BAB, 0x91A267AB, 0x9A126A7B, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74, +0x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74, 0x4E88BB72, 0x72A0AF4E, 0x7C40C2FE, 0x28E8D7D4, 0x48E8B7B2, 0x7A20A4FE, 0x6E0898FE, 0x60E89F8E, 0x5CF3C03A, 0x3AF5A05C, 0x74CFC02E, 0x2EDD8874, 0x4EBB8872, 0x72AFA04E, 0x7CC240FE, 0x28D7E8D4, 0x48B7E8B2, 0x7AA420FE, 0x6E9808FE, 0x609FE88E, 0x5FC3C30A, 0x3FA5A50C, 0x7CC24F0E, 0x2D87ED84, @@ -242,22 +258,7 @@ static unsigned s_FuncTruths[1920] = { 0x41E1D7D2, 0x7025F45E, 0x7117F096, 0x71F01796, 0x4CCE433E, 0x099FC99C, 0x44C3C3EE, 0x0C9999FC, 0x4CDC1976, 0x41D7C9C6, 0x4C43CE3E, 0x09C99F9C, 0x4DCC1796, 0x4D17CC96, 0x4C19DC76, 0x41C9D7C6, 0x099FA99A, 0x2AAE255E, 0x21B7A9A6, 0x2ABA1976, 0x0A9999FA, 0x22A5A5EE, 0x2B17AA96, 0x2BAA1796, -0x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0xA330FCC5, 0xC550FAA3, 0x8B0CFCD1, 0xD144EE8B, -0xB122EE8D, 0x8D0AFAB1, 0x80BCFDC1, 0xD414E8EB, 0xB212E8ED, 0x80DAFBA1, 0x80E6EF89, 0x8E06E8F9, -0xA3FC30C5, 0xC5FA50A3, 0x8BFC0CD1, 0xD1EE448B, 0xB1EE228D, 0x8DFA0AB1, 0x80FDBCC1, 0xD4E814EB, -0xB2E812ED, 0x80FBDAA1, 0x80EFE689, 0x8EE806F9, 0xAF3C3C05, 0xCF5A5A03, 0x8F0DBCC1, 0xDE481E4B, -0xBE281E2D, 0x8F0BDAA1, 0x8FBC0DC1, 0xDE1E484B, 0xBE1E282D, 0x8FDA0BA1, 0x8EE80F69, 0x8E0FE869, -0xB331BCC1, 0xF6603663, 0xBB3C3C11, 0xF3666603, 0xB323E689, 0xBE283639, 0xB3BC31C1, 0xF6366063, -0xB233E869, 0xB2E83369, 0xB3E62389, 0xBE362839, 0xF6605665, 0xD551DAA1, 0xDE485659, 0xD545E689, -0xF5666605, 0xDD5A5A11, 0xD4E85569, 0xD455E869, 0xF6566065, 0xD5DA51A1, 0xD5E64589, 0xDE564859, -0xACCF0335, 0xCAAF0553, 0xB8F3031D, 0xE2BB1147, 0xE4DD1127, 0xD8F5051B, 0xBF83013D, 0xEB2B1417, -0xED4D1217, 0xDF85015B, 0xF7910167, 0xF9710617, 0xAC03CF35, 0xCA05AF53, 0xB803F31D, 0xE211BB47, -0xE411DD27, 0xD805F51B, 0xBF01833D, 0xEB142B17, 0xED124D17, 0xDF01855B, 0xF7019167, 0xF9067117, -0xA0C3C3F5, 0xC0A5A5F3, 0xB0F1833D, 0xE1B421B7, 0xE1D241D7, 0xD0F1855B, 0xB083F13D, 0xE121B4B7, -0xE141D2D7, 0xD085F15B, 0xF0967117, 0xF0719617, 0x8CCD833D, 0xC99C099F, 0x88C3C3DD, 0xC09999CF, -0xC4CD9167, 0xC9C641D7, 0x8C83CD3D, 0xC9099C9F, 0xCC4D9617, 0xCC964D17, 0xC491CD67, 0xC941C6D7, -0xA99A099F, 0x8AAB855B, 0xA9A621B7, 0xA2AB9167, 0xA09999AF, 0x88A5A5BB, 0xAA962B17, 0xAA2B9617, -0xA9099A9F, 0x8A85AB5B, 0xA291AB67, 0xA921A6B7, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8, +0x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8, 0x1B22EED8, 0x270AFAE4, 0x407CFEC2, 0x14D4EBE8, 0x12B2EDE8, 0x207AFEA4, 0x086EFE98, 0x068EF9E8, 0x53FC30CA, 0x35FA50AC, 0x47FC0CE2, 0x1DEE44B8, 0x1BEE22D8, 0x27FA0AE4, 0x40FE7CC2, 0x14EBD4E8, 0x12EDB2E8, 0x20FE7AA4, 0x08FE6E98, 0x06F98EE8, 0x5F3C3C0A, 0x3F5A5A0C, 0x4F0E7CC2, 0x1E4BDE48, @@ -295,6 +296,7 @@ struct Sdb_Sto_t_ int nCutSize; int nCutNum; int fCutMin; + int fTruthMin; int fVerbose; Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes) Vec_Int_t * vRefs; // refs for each node @@ -591,7 +593,8 @@ static inline int Sdb_CutComputeTruth6( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cu t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves ); t = fIsXor ? t0 ^ t1 : t0 & t1; if ( (fCompl = (int)(t & 1)) ) t = ~t; - pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves ); + if ( p->fTruthMin ) + pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves ); assert( (int)(t & 1) == 0 ); truthId = Vec_MemHashInsert(p->vTtMem, &t); pCutR->iFunc = Abc_Var2Lit( truthId, fCompl ); @@ -617,7 +620,8 @@ static inline int Sdb_CutComputeTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) ); else Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) ); - pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize ); + if ( p->fTruthMin ) + pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize ); assert( (uTruth[0] & 1) == 0 ); //Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" ); truthId = Vec_MemHashInsert(p->vTtMem, uTruth); @@ -774,6 +778,167 @@ void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj ) Sdb_CutAddUnit( p, iObj ); } + + +/**Function************************************************************* + + Synopsis [Cut comparison.] + + Description [Find out if there is a cut in vCuts such that pCut + has only one extra input. If so, return this input.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sdb_StoDiffExactlyOne( Vec_Wec_t * vCuts, int Limit, int * pCut ) +{ + Vec_Int_t * vCut; + int i, k, iNew; + // check if it is fully contained in any one + Vec_WecForEachLevel( vCuts, vCut, i ) + { + for ( k = 1; k <= pCut[0]; k++ ) + if ( Vec_IntFind(vCut, pCut[k]) == -1 ) + break; + if ( k == pCut[0] + 1 ) + return -1; + } + // check if there is one different + Vec_WecForEachLevel( vCuts, vCut, i ) + { + if ( i == Limit ) + break; + for ( iNew = -1, k = 1; k <= pCut[0]; k++ ) + { + if ( Vec_IntFind(vCut, pCut[k]) >= 0 ) + continue; + if ( iNew == -1 ) + iNew = pCut[k]; + else + break; + } + if ( k == pCut[0] + 1 && iNew != -1 ) + return iNew; + } + return -1; +} +int Sdb_StoDiffExactlyOne3( Vec_Wec_t * vCuts, int Limit, int * pCut, int * pCount ) +{ + Vec_Int_t * vCut; + int i, iNewAll = -1, Count = 0; + Vec_WecForEachLevel( vCuts, vCut, i ) + { + int k, iNew = -1; + if ( i == Limit ) + break; + for ( k = 1; k <= pCut[0]; k++ ) + { + if ( Vec_IntFind(vCut, pCut[k]) >= 0 ) + continue; + if ( iNew == -1 ) + iNew = pCut[k]; + else + break; + } + if ( k == pCut[0] + 1 && iNew != -1 ) + { + if ( iNewAll == -1 ) + iNewAll = iNew; + if ( iNewAll == iNew ) + Count++; + } + } + *pCount = Count; + return iNewAll; +} +Vec_Int_t * Sdb_StoFindAll( Vec_Wec_t * vCuts ) +{ + int i, k, Entry, iNew = -1; + Vec_Int_t * vCut, * vAll = Vec_IntAlloc( 100 ); + Vec_WecForEachLevel( vCuts, vCut, i ) + Vec_IntForEachEntry( vCut, Entry, k ) + Vec_IntPushUnique( vAll, Entry ); + return vAll; +} +int Sdb_StoDiffExactlyOne2( Vec_Int_t * vAll, int * pCut ) +{ + int k, iNew = -1; + for ( k = 1; k <= pCut[0]; k++ ) + { + if ( Vec_IntFind(vAll, pCut[k]) >= 0 ) + continue; + if ( iNew == -1 ) + iNew = pCut[k]; + else + break; + } + if ( k == pCut[0] + 1 && iNew != -1 ) + return iNew; + return -1; +} +Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front ) +{ + int fVerbose = 1; + Vec_Int_t * vCut, * vCounts; + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_Int_t * vResA = Vec_IntAlloc( 100 ); + Vec_Int_t * vResB = Vec_IntAlloc( 100 ); + int i, k, Entry, Max = 0, Min, MinValue; + // find MAX value + Vec_WecForEachLevel( vCuts, vCut, i ) + Vec_IntForEachEntry( vCut, Entry, k ) + Max = Abc_MaxInt( Max, Entry ); + // count how many times each value appears + vCounts = Vec_IntStart( Max + 1 ); + Vec_WecForEachLevel( vCuts, vCut, i ) + Vec_IntForEachEntry( vCut, Entry, k ) + Vec_IntAddToEntry( vCounts, Entry, 1 ); + Vec_IntWriteEntry( vCounts, 0, 0 ); + // print out + if ( fVerbose ) + Vec_IntForEachEntry( vCounts, Entry, k ) + if ( Entry ) + printf( "%5d %5d\n", k, Entry ); + // collect first part + MinValue = ABC_INFINITY; + Vec_IntForEachEntry( vCounts, Entry, k ) + if ( Entry ) + MinValue = Abc_MinInt( MinValue, Entry ); + Min = Vec_IntFind( vCounts, MinValue ); + Vec_IntPush( vResA, Min ); + Vec_IntWriteEntry( vCounts, Min, 0 ); + Vec_IntForEachEntry( vCounts, Entry, k ) + if ( Entry == MinValue || Entry == 2*MinValue ) + { + Vec_IntPush( vResA, k ); + Vec_IntWriteEntry( vCounts, k, 0 ); + } + // collect second parts + MinValue = Vec_IntEntry( vCounts, Front ); + Min = Front; + Vec_IntPush( vResB, Min ); + Vec_IntWriteEntry( vCounts, Min, 0 ); + Vec_IntForEachEntry( vCounts, Entry, k ) + if ( Entry == MinValue || Entry == 2*MinValue ) + { + Vec_IntPush( vResB, k ); + Vec_IntWriteEntry( vCounts, k, 0 ); + } + Vec_IntFree( vCounts ); + Vec_IntPrint( vResA ); + Vec_IntPrint( vResB ); + // here we need to order the inputs + + // append + Vec_IntAppend( vRes, vResA ); + Vec_IntAppend( vRes, vResB ); + Vec_IntFree( vResA ); + Vec_IntFree( vResB ); + return vRes; +} + /**Function************************************************************* Synopsis [Iterate through the cuts.] @@ -785,41 +950,152 @@ void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj ) SeeAlso [] ***********************************************************************/ -int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj ) +int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj, int CutSize, int ** ppCut ) { - int fVerbose = 1; + int fVerbose = 0; Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj ); int i, k, * pCut, * pList = Vec_IntArray( vThis ); word * pTruth; Sdb_ForEachCut( pList, pCut, i ) { - if ( pCut[0] != 5 ) + if ( pCut[0] != CutSize ) continue; - pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1])); - for ( k = 0; k < 1920; k++ ) - if ( s_FuncTruths[k] == (unsigned)*pTruth ) - break; - if ( k < 1920 ) + if ( pCut[0] == 5 ) { - if ( fVerbose ) + pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1])); + for ( k = 0; k < s_nFuncTruths5; k++ ) + if ( s_FuncTruths5[k] == (unsigned)*pTruth ) + break; + if ( k < s_nFuncTruths5 ) { - printf( "Object %d has 5-input cut: ", iObj ); - for ( k = 1; k <= pCut[0]; k++ ) - printf( "%d ", pCut[k] ); - printf( "\n" ); + if ( fVerbose ) + { + printf( "Object %d has %d-input cut: ", iObj, pCut[0] ); + for ( k = 1; k <= pCut[0]; k++ ) + printf( "%d ", pCut[k] ); + printf( "\n" ); + } + *ppCut = pCut; + return 1; // five-input + } + } + if ( pCut[0] == 4 ) + { + pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1])); + for ( k = 0; k < s_nFuncTruths4; k++ ) + if ( s_FuncTruths4[k] == (0xFFFF & (unsigned)*pTruth) ) + break; + if ( k < s_nFuncTruths4 ) + { + if ( fVerbose ) + { + printf( "Object %d has %d-input cut: ", iObj, pCut[0] ); + for ( k = 1; k <= pCut[0]; k++ ) + printf( "%d ", pCut[k] ); + printf( "\n" ); + } + *ppCut = pCut; + return 2; // front + } + } + if ( pCut[0] == 4 ) + { + pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1])); + for ( k = 0; k < s_nFuncTruths4a; k++ ) + if ( s_FuncTruths4a[k] == (0xFFFF & (unsigned)*pTruth) ) + break; + if ( k < s_nFuncTruths4a ) + { + if ( fVerbose ) + { + printf( "Object %d has %d-input cut: ", iObj, pCut[0] ); + for ( k = 1; k <= pCut[0]; k++ ) + printf( "%d ", pCut[k] ); + printf( "\n" ); + } + *ppCut = pCut; + return 3; // back unsigned + } + } + if ( pCut[0] == 4 ) + { + pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1])); + for ( k = 0; k < s_nFuncTruths4b; k++ ) + if ( s_FuncTruths4b[k] == (0xFFFF & (unsigned)*pTruth) ) + break; + if ( k < s_nFuncTruths4b ) + { + if ( fVerbose ) + { + printf( "Object %d has %d-input cut: ", iObj, pCut[0] ); + for ( k = 1; k <= pCut[0]; k++ ) + printf( "%d ", pCut[k] ); + printf( "\n" ); + } + *ppCut = pCut; + return 4; // back signed } - return 1; } } return 0; } -void Sdb_StoIterCuts( Sdb_Sto_t * p ) +Vec_Int_t * Sdb_StoIterCuts( Sdb_Sto_t * p ) { + Vec_Wec_t * v5Cuts = Vec_WecAlloc( 100 ); + Vec_Int_t * v5Cut, * vAll, * vRes; Gia_Obj_t * pObj; - int iObj, Count = 0; + int k, iObj, * pCut, Limit, iNew, iNewFront = -1, iNewBack = -1, iSigned = 0; + Gia_ManForEachAnd( p->pGia, pObj, iObj ) + { + int RetValue = Sdb_StoIterCutsOne( p, iObj, 5, &pCut ); + if ( RetValue == 0 ) + continue; + assert( RetValue == 1 ); + assert( pCut[0] == 5 ); + v5Cut = Vec_WecPushLevel( v5Cuts ); + for ( k = 1; k <= pCut[0]; k++ ) + Vec_IntPush( v5Cut, pCut[k] ); + } + Limit = Vec_WecSize( v5Cuts ); + printf( "Detected %d 5-cuts.\n", Vec_WecSize(v5Cuts) ); + vAll = Sdb_StoFindAll( v5Cuts ); Gia_ManForEachAnd( p->pGia, pObj, iObj ) - Count += Sdb_StoIterCutsOne( p, iObj ); - printf( "Detected %d cuts.\n", Count ); + { + int RetValue = Sdb_StoIterCutsOne( p, iObj, 4, &pCut ); + if ( RetValue == 0 ) + continue; + assert( RetValue >= 2 && RetValue <= 4 ); + assert( pCut[0] == 4 ); + // find cut, which differs in exactly one input + iNew = Sdb_StoDiffExactlyOne( v5Cuts, Limit, pCut ); + if ( iNew == -1 ) + continue; + if ( RetValue == 2 ) + iNewFront = iNew; + else + iNewBack = iNew; + if ( RetValue == 4 ) + iSigned = 1; + // save in the second cut + v5Cut = Vec_WecPushLevel( v5Cuts ); + Vec_IntPush( v5Cut, 0 ); + for ( k = 1; k <= pCut[0]; k++ ) + Vec_IntPush( v5Cut, pCut[k] ); + } + Vec_IntFree( vAll ); + Vec_WecPrint( v5Cuts, 0 ); + + if ( iNewFront ) + printf( "Front = %d\n", iNewFront ); + if ( iNewBack ) + printf( "Back = %d\n", iNewBack ); + if ( iSigned ) + printf( "Sign = %d\n", iSigned ); + + vRes = Sdb_StoFindInputs( v5Cuts, iNewFront ); + + Vec_WecFree( v5Cuts ); + return vRes; } /**Function************************************************************* @@ -833,22 +1109,23 @@ void Sdb_StoIterCuts( Sdb_Sto_t * p ) SeeAlso [] ***********************************************************************/ -Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fVerbose ) +Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fTruthMin, int fVerbose ) { Sdb_Sto_t * p; assert( nCutSize < SDB_CUT_NO_LEAF ); assert( nCutSize > 1 && nCutSize <= SDB_MAX_CUTSIZE ); assert( nCutNum > 1 && nCutNum < SDB_MAX_CUTNUM ); p = ABC_CALLOC( Sdb_Sto_t, 1 ); - p->clkStart = Abc_Clock(); - p->nCutSize = nCutSize; - p->nCutNum = nCutNum; - p->fCutMin = fCutMin; - p->fVerbose = fVerbose; - p->pGia = pGia; - p->vRefs = Vec_IntAlloc( Gia_ManObjNum(pGia) ); - p->vCuts = Vec_WecStart( Gia_ManObjNum(pGia) ); - p->vTtMem = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL; + p->clkStart = Abc_Clock(); + p->nCutSize = nCutSize; + p->nCutNum = nCutNum; + p->fCutMin = fCutMin; + p->fTruthMin = fTruthMin; + p->fVerbose = fVerbose; + p->pGia = pGia; + p->vRefs = Vec_IntAlloc( Gia_ManObjNum(pGia) ); + p->vCuts = Vec_WecStart( Gia_ManObjNum(pGia) ); + p->vTtMem = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL; return p; } void Sdb_StoFree( Sdb_Sto_t * p ) @@ -886,9 +1163,10 @@ void Sdb_StoRefObj( Sdb_Sto_t * p, int iObj ) else if ( Gia_ObjIsCo(pObj) ) Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 ); } -void Sdb_StoComputeCutsTest( Gia_Man_t * pGia ) +Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia ) { - Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 6, 20, 1, 1 ); + Vec_Int_t * vRes = NULL; + Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 5, 20, 1, 0, 1 ); Gia_Obj_t * pObj; int i, iObj; // prepare references @@ -912,11 +1190,15 @@ void Sdb_StoComputeCutsTest( Gia_Man_t * pGia ) printf( "Over = %4d ", p->nCutsOver ); Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart ); } - Sdb_StoIterCuts( p ); + vRes = Sdb_StoIterCuts( p ); Sdb_StoFree( p ); + return vRes; +} +void Sdb_StoComputeCutsTest( Gia_Man_t * pGia ) +{ + Vec_Int_t * vRes = Sdb_StoComputeCutsDetect( pGia ); + Vec_IntFree( vRes ); } - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c index c63fdde2..66ee2fb7 100644 --- a/src/proof/acec/acecMult.c +++ b/src/proof/acec/acecMult.c @@ -189,6 +189,7 @@ unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes ) for ( k = 0; k < nPerms; k++ ) { uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 ); + if ( !(uPerm & 1) ) Vec_IntPushUnique( vRes, uPerm ); if ( uTruthMin > uPerm ) uTruthMin = uPerm; @@ -197,6 +198,7 @@ unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes ) for ( k = 0; k < nPerms; k++ ) { uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 ); + if ( !(uPerm & 1) ) Vec_IntPushUnique( vRes, uPerm ); if ( uTruthMin > uPerm ) uTruthMin = uPerm; @@ -233,8 +235,12 @@ void Acec_MultFuncTest4() Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); int i, Entry; - unsigned Truth = 0x35C0; + unsigned Truth = 0xF3C0; +// unsigned Truth = 0xF335; +// unsigned Truth = 0xFD80; //unsigned Truth = 0xD728; + //unsigned Truth = 0x35C0; + //unsigned Truth = 0xACC0; unsigned Canon = Extra_TruthCanonNPN2( Truth, 4, vRes ); Extra_PrintHex( stdout, (unsigned*)&Truth, 4 ); printf( "\n" ); |