ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acec2Mult.c
Go to the documentation of this file.
1
20
21#include "acecInt.h"
22#include "misc/vec/vecMem.h"
23#include "misc/util/utilTruth.h"
24
25ABC_NAMESPACE_IMPL_START
26
27
28static int s_nFuncTruths4a = 192; // 0xACC0 -- F(a=0) <== useful
29static unsigned s_FuncTruths4a[192] = {
300xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860,
310x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8,
320xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06,
330x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E,
340xCA0C, 0xAC0A, 0xE230, 0xB822, 0xD844, 0xE450, 0xC0AC, 0xA0CA, 0xE320, 0xB282, 0xD484, 0xE540,
350xCB08, 0x8E82, 0xC0B8, 0x88E2, 0xD940, 0xD490, 0x8E84, 0xAD08, 0xB290, 0xB920, 0x88E4, 0xA0D8,
360xC50C, 0xA30A, 0xD130, 0x8B22, 0x8D44, 0xB150, 0xC05C, 0xA03A, 0xD310, 0x82B2, 0x84D4, 0xB510,
370xC704, 0x828E, 0xC074, 0x882E, 0x9D04, 0x90D4, 0x848E, 0xA702, 0x90B2, 0x9B02, 0x884E, 0xA072,
380xC5FC, 0xA3FA, 0xD1FC, 0x8BEE, 0x8DEE, 0xB1FA, 0xCF5C, 0xAF3A, 0xDF1C, 0x8EBE, 0x8EDE, 0xBF1A,
390xF734, 0xB2BE, 0xF374, 0xBB2E, 0xBF26, 0xB2F6, 0xD4DE, 0xF752, 0xD4F6, 0xDF46, 0xDD4E, 0xF572,
400xCAFC, 0xACFA, 0xE2FC, 0xB8EE, 0xD8EE, 0xE4FA, 0xCFAC, 0xAFCA, 0xEF2C, 0xBE8E, 0xDE8E, 0xEF4A,
410xFB38, 0xBEB2, 0xF3B8, 0xBBE2, 0xFB62, 0xF6B2, 0xDED4, 0xFD58, 0xF6D4, 0xFD64, 0xDDE4, 0xF5D8,
420x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160,
430xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E,
440x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706,
450xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8
46};
47
48
49/*
50static int s_nFuncTruths4 = 192; // 0xF335 -- F(a=1)
51static unsigned s_FuncTruths4[192] = {
520x0CCA, 0x0AAC, 0x30E2, 0x22B8, 0x44D8, 0x50E4, 0x3E02, 0x2B28, 0x4D48, 0x5E04, 0x7610, 0x7160,
530xF33A, 0xF55C, 0xCF2E, 0xDD74, 0xBB72, 0xAF4E, 0xC2FE, 0xD7D4, 0xB7B2, 0xA4FE, 0x98FE, 0x9F8E,
540x033A, 0x055C, 0x032E, 0x1174, 0x1172, 0x054E, 0x023E, 0x1714, 0x1712, 0x045E, 0x1076, 0x1706,
550xFCCA, 0xFAAC, 0xFCE2, 0xEEB8, 0xEED8, 0xFAE4, 0xFEC2, 0xEBE8, 0xEDE8, 0xFEA4, 0xFE98, 0xF9E8,
560xC0AC, 0xA0CA, 0xC0B8, 0x88E2, 0x88E4, 0xA0D8, 0xCA0C, 0xAC0A, 0xCB08, 0x8E82, 0x8E84, 0xAD08,
570xE320, 0xB282, 0xE230, 0xB822, 0xB920, 0xB290, 0xD484, 0xE540, 0xD490, 0xD940, 0xD844, 0xE450,
580xC05C, 0xA03A, 0xC074, 0x882E, 0x884E, 0xA072, 0xC50C, 0xA30A, 0xC704, 0x828E, 0x848E, 0xA702,
590xD310, 0x82B2, 0xD130, 0x8B22, 0x9B02, 0x90B2, 0x84D4, 0xB510, 0x90D4, 0x9D04, 0x8D44, 0xB150,
600xCF5C, 0xAF3A, 0xF374, 0xBB2E, 0xDD4E, 0xF572, 0xC5FC, 0xA3FA, 0xF734, 0xB2BE, 0xD4DE, 0xF752,
610xDF1C, 0x8EBE, 0xD1FC, 0x8BEE, 0xDF46, 0xD4F6, 0x8EDE, 0xBF1A, 0xB2F6, 0xBF26, 0x8DEE, 0xB1FA,
620xCFAC, 0xAFCA, 0xF3B8, 0xBBE2, 0xDDE4, 0xF5D8, 0xCAFC, 0xACFA, 0xFB38, 0xBEB2, 0xDED4, 0xFD58,
630xEF2C, 0xBE8E, 0xE2FC, 0xB8EE, 0xFD64, 0xF6D4, 0xDE8E, 0xEF4A, 0xF6B2, 0xFB62, 0xD8EE, 0xE4FA,
640xACC0, 0xCAA0, 0xB8C0, 0xE288, 0xE488, 0xD8A0, 0xBC80, 0xE828, 0xE848, 0xDA80, 0xE680, 0xE860,
650x5CC0, 0x3AA0, 0x74C0, 0x2E88, 0x4E88, 0x72A0, 0x7C40, 0x28E8, 0x48E8, 0x7A20, 0x6E08, 0x60E8,
660xA330, 0xC550, 0x8B0C, 0xD144, 0xB122, 0x8D0A, 0x80BC, 0xD414, 0xB212, 0x80DA, 0x80E6, 0x8E06,
670x5330, 0x3550, 0x470C, 0x1D44, 0x1B22, 0x270A, 0x407C, 0x14D4, 0x12B2, 0x207A, 0x086E, 0x068E
68};
69*/
70
71static int s_nFuncTruths4b = 48; // 0xF3C0 -- F(a=b) <== useful
72static unsigned s_FuncTruths4b[48] = {
730xF3C0, 0xF5A0, 0xCFC0, 0xDD88, 0xBB88, 0xAFA0, 0xFC30, 0xFA50, 0xCCF0, 0xD8D8, 0xB8B8, 0xAAF0,
740xF0CC, 0xE4E4, 0xFC0C, 0xEE44, 0xAACC, 0xACAC, 0xE2E2, 0xF0AA, 0xCACA, 0xCCAA, 0xEE22, 0xFA0A,
750x3F0C, 0x5F0A, 0x3F30, 0x7722, 0x7744, 0x5F50, 0x30FC, 0x50FA, 0x33F0, 0x7272, 0x7474, 0x55F0,
760x0FCC, 0x4E4E, 0x0CFC, 0x44EE, 0x55CC, 0x5C5C, 0x2E2E, 0x0FAA, 0x3A3A, 0x33AA, 0x22EE, 0x0AFA
77};
78
79/*
80static int s_nFuncTruths4 = 12; // 0x35AC -- F(a!=b)
81static unsigned s_FuncTruths4[12] = {
820x35AC, 0x53CA, 0x1DB8, 0x47E2, 0x27E4, 0x1BD8, 0x3A5C, 0x5C3A, 0x4E72, 0x2E74, 0x724E, 0x742E
83};
84*/
85
86static int s_nFuncTruths4 = 384; // 0x35C0 -- F(b=0, c=0) <== useful
87static unsigned s_FuncTruths4[384] = {
880x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
890x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
900x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
910x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
920xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
930xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
940xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
950xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
960x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
970x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
980xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
990x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
1000xA3FC, 0xC5FA, 0x8BFC, 0xD1EE, 0xB1EE, 0x8DFA, 0xAF3C, 0xCF5A, 0x8FBC, 0xDE1E, 0xBE1E, 0x8FDA,
1010xB3BC, 0xF636, 0xBB3C, 0xF366, 0xB3E6, 0xBE36, 0xF656, 0xD5DA, 0xDE56, 0xD5E6, 0xF566, 0xDD5A,
1020x53FC, 0x35FA, 0x47FC, 0x1DEE, 0x1BEE, 0x27FA, 0x5F3C, 0x3F5A, 0x4F7C, 0x1EDE, 0x1EBE, 0x2F7A,
1030x737C, 0x36F6, 0x773C, 0x3F66, 0x3B6E, 0x36BE, 0x56F6, 0x757A, 0x56DE, 0x5D6E, 0x5F66, 0x775A,
1040x3FCA, 0x5FAC, 0x3FE2, 0x77B8, 0x77D8, 0x5FE4, 0x3CFA, 0x5AFC, 0x3EF2, 0x7B78, 0x7D78, 0x5EF4,
1050x3ECE, 0x6F6C, 0x3CEE, 0x66FC, 0x76DC, 0x7D6C, 0x6F6A, 0x5EAE, 0x7B6A, 0x76BA, 0x66FA, 0x5AEE,
1060xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
1070xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
1080xCF3A, 0xAF5C, 0xF32E, 0xBB74, 0xDD72, 0xF54E, 0xC3FA, 0xA5FC, 0xF23E, 0xB7B4, 0xD7D2, 0xF45E,
1090xCE3E, 0x9F9C, 0xC3EE, 0x99FC, 0xDC76, 0xD7C6, 0x9F9A, 0xAE5E, 0xB7A6, 0xBA76, 0x99FA, 0xA5EE,
1100x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
1110x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
1120xF3AC, 0xF5CA, 0xCFB8, 0xDDE2, 0xBBE4, 0xAFD8, 0xFA3C, 0xFC5A, 0xCBF8, 0xDED2, 0xBEB4, 0xADF8,
1130xE3EC, 0xF6C6, 0xEE3C, 0xFC66, 0xB9EC, 0xBE9C, 0xF6A6, 0xE5EA, 0xDE9A, 0xD9EA, 0xFA66, 0xEE5A,
1140xF35C, 0xF53A, 0xCF74, 0xDD2E, 0xBB4E, 0xAF72, 0xF53C, 0xF35A, 0xC7F4, 0xD2DE, 0xB4BE, 0xA7F2,
1150xD3DC, 0xC6F6, 0xDD3C, 0xCF66, 0x9BCE, 0x9CBE, 0xA6F6, 0xB5BA, 0x9ADE, 0x9DAE, 0xAF66, 0xBB5A,
1160x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
1170x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
1180x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
1190x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A
120};
121
122/*
123static int s_nFuncTruths4 = 96; // 0xFD80 -- F(d=0)
124static unsigned s_FuncTruths4[96] = {
1250xFD80, 0xFB80, 0xEF80, 0xF8D0, 0xF8B0, 0xE8F0, 0xECC4, 0xE8CC, 0xEC8C, 0xE8AA, 0xEAA2, 0xEA8A,
1260xFE40, 0xFE20, 0xFE08, 0xF4E0, 0xF2E0, 0xF0E8, 0xDCC8, 0xCCE8, 0xCEC8, 0xAAE8, 0xBAA8, 0xAEA8,
1270xF720, 0xF740, 0xDF08, 0xDF40, 0xBF20, 0xBF08, 0xF270, 0xF470, 0xD0F8, 0xD4F0, 0xB2F0, 0xB0F8,
1280xC4EC, 0xD4CC, 0xCE4C, 0xDC4C, 0x8CEC, 0x8ECC, 0xB2AA, 0xA2EA, 0x8EAA, 0x8AEA, 0xBA2A, 0xAE2A,
1290xFB10, 0xFD10, 0xEF04, 0xFD04, 0xFB02, 0xEF02, 0xF1B0, 0xF1D0, 0xE0F4, 0xF0D4, 0xF0B2, 0xE0F2,
1300xC8DC, 0xCCD4, 0xCD8C, 0xCDC4, 0xC8CE, 0xCC8E, 0xAAB2, 0xA8BA, 0xAA8E, 0xA8AE, 0xABA2, 0xAB8A,
1310x7F02, 0x7F04, 0x7F10, 0x70F2, 0x70F4, 0x71F0, 0x4CCE, 0x4DCC, 0x4CDC, 0x2BAA, 0x2AAE, 0x2ABA,
1320x40FE, 0x20FE, 0x08FE, 0x4F0E, 0x2F0E, 0x0F8E, 0x7332, 0x33B2, 0x3B32, 0x55D4, 0x7554, 0x5D54,
133};
134*/
135
136/*
137static int s_nFuncTruths4 = 48; // 0xD728 -- F(e=0)
138static unsigned s_FuncTruths4[48] = {
1390xD728, 0xB748, 0x9F60, 0xD278, 0xB478, 0x96F0, 0xC66C, 0x96CC, 0x9C6C, 0x96AA, 0xA66A, 0x9A6A,
1400xEB14, 0xED12, 0xF906, 0xE1B4, 0xE1D2, 0xF096, 0xC99C, 0xCC96, 0xC9C6, 0xAA96, 0xA99A, 0xA9A6,
1410x7D82, 0x7B84, 0x6F90, 0x78D2, 0x78B4, 0x69F0, 0x6CC6, 0x69CC, 0x6C9C, 0x69AA, 0x6AA6, 0x6A9A,
1420x41BE, 0x21DE, 0x09F6, 0x4B1E, 0x2D1E, 0x0F96, 0x6336, 0x3396, 0x3936, 0x5596, 0x6556, 0x5956
143};
144*/
145
146
147static int s_nFuncTruths5 = 960; // 0xF335ACC0
148static unsigned s_FuncTruths5[960] = {
1490xF335ACC0, 0xF553CAA0, 0xCF1DB8C0, 0xDD47E288, 0xBB27E488, 0xAF1BD8A0, 0xC1FDBC80, 0xD4D7E828,
1500xB2B7E848, 0xA1FBDA80, 0x89EFE680, 0x8E9FE860, 0xF3AC35C0, 0xF5CA53A0, 0xCFB81DC0, 0xDDE24788,
1510xBBE42788, 0xAFD81BA0, 0xC1BCFD80, 0xD4E8D728, 0xB2E8B748, 0xA1DAFB80, 0x89E6EF80, 0x8EE89F60,
1520xFA3C3C50, 0xFC5A5A30, 0xCB1CF8D0, 0xDE48D278, 0xBE28B478, 0xAD1AF8B0, 0xCBF81CD0, 0xDED24878,
1530xBEB42878, 0xADF81AB0, 0x8EE896F0, 0x8E96E8F0, 0xE334ECC4, 0xF660C66C, 0xEE3C3C44, 0xFC66660C,
1540xB926EC8C, 0xBE289C6C, 0xE3EC34C4, 0xF6C6606C, 0xB296E8CC, 0xB2E896CC, 0xB9EC268C, 0xBE9C286C,
1550xF660A66A, 0xE552EAA2, 0xDE489A6A, 0xD946EA8A, 0xFA66660A, 0xEE5A5A22, 0xD4E896AA, 0xD496E8AA,
1560xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88,
1570xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8, 0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8,
1580xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488, 0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8,
1590xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8, 0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48,
1600xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848, 0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8,
1610xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0, 0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60,
1620x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28, 0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8,
1630xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8, 0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48,
1640xFCC5A330, 0xFAA3C550, 0xFCD18B0C, 0xEE8BD144, 0xEE8DB122, 0xFAB18D0A, 0xFDC180BC, 0xE8EBD414,
1650xE8EDB212, 0xFBA180DA, 0xEF8980E6, 0xE8F98E06, 0xFCA3C530, 0xFAC5A350, 0xFC8BD10C, 0xEED18B44,
1660xEEB18D22, 0xFA8DB10A, 0xFD80C1BC, 0xE8D4EB14, 0xE8B2ED12, 0xFB80A1DA, 0xEF8089E6, 0xE88EF906,
1670xFAC3C350, 0xFCA5A530, 0xF8D0CB1C, 0xED84E1B4, 0xEB82E1D2, 0xF8B0AD1A, 0xF8CBD01C, 0xEDE184B4,
1680xEBE182D2, 0xF8ADB01A, 0xE88EF096, 0xE8F08E96, 0xECC4E334, 0xF990C99C, 0xEEC3C344, 0xFC99990C,
1690xEC8CB926, 0xEB82C9C6, 0xECE3C434, 0xF9C9909C, 0xE8CCB296, 0xE8B2CC96, 0xECB98C26, 0xEBC982C6,
1700xF990A99A, 0xEAA2E552, 0xED84A9A6, 0xEA8AD946, 0xFA99990A, 0xEEA5A522, 0xE8D4AA96, 0xE8AAD496,
1710xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44,
1720xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4, 0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E,
1730xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844, 0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4,
1740xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E, 0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84,
1750xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484, 0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E,
1760xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0, 0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90,
1770xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682, 0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64,
1780xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4, 0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684,
1790x3F53CA0C, 0x5F35AC0A, 0x3F47E230, 0x771DB822, 0x771BD844, 0x5F27E450, 0x35F3C0AC, 0x53F5A0CA,
1800x34F7E320, 0x717DB282, 0x717BD484, 0x52F7E540, 0x1CDFCB08, 0x4D7D8E82, 0x1DCFC0B8, 0x47DD88E2,
1810x46DFD940, 0x4D6FD490, 0x2B7B8E84, 0x1ABFAD08, 0x2B6FB290, 0x26BFB920, 0x27BB88E4, 0x1BAFA0D8,
1820x3FCA530C, 0x5FAC350A, 0x3FE24730, 0x77B81D22, 0x77D81B44, 0x5FE42750, 0x35C0F3AC, 0x53A0F5CA,
1830x34E3F720, 0x71B27D82, 0x71D47B84, 0x52E5F740, 0x1CCBDF08, 0x4D8E7D82, 0x1DC0CFB8, 0x4788DDE2,
1840x46D9DF40, 0x4DD46F90, 0x2B8E7B84, 0x1AADBF08, 0x2BB26F90, 0x26B9BF20, 0x2788BBE4, 0x1BA0AFD8,
1850x3C50FA3C, 0x5A30FC5A, 0x3E43F270, 0x7B1278D2, 0x7D1478B4, 0x5E25F470, 0x3CFA503C, 0x5AFC305A,
1860x3EF24370, 0x7B7812D2, 0x7D7814B4, 0x5EF42570, 0x1CD0CBF8, 0x4878DED2, 0x1CCBD0F8, 0x48DE78D2,
1870x4DD469F0, 0x4D69D4F0, 0x2878BEB4, 0x1AB0ADF8, 0x2B69B2F0, 0x2BB269F0, 0x28BE78B4, 0x1AADB0F8,
1880x3E43CE4C, 0x6F066CC6, 0x3C44EE3C, 0x660CFC66, 0x7619DC4C, 0x7D146C9C, 0x34E3C4EC, 0x60F66CC6,
1890x34C4E3EC, 0x606CF6C6, 0x7169D4CC, 0x71D469CC, 0x3ECE434C, 0x6F6C06C6, 0x3CEE443C, 0x66FC0C66,
1900x76DC194C, 0x7D6C149C, 0x2B698ECC, 0x2B8E69CC, 0x286CBE9C, 0x268CB9EC, 0x26B98CEC, 0x28BE6C9C,
1910x6F066AA6, 0x5E25AE2A, 0x7B126A9A, 0x7619BA2A, 0x660AFA66, 0x5A22EE5A, 0x60F66AA6, 0x52E5A2EA,
1920x71B269AA, 0x7169B2AA, 0x606AF6A6, 0x52A2E5EA, 0x4D8E69AA, 0x4D698EAA, 0x48DE6A9A, 0x46D98AEA,
1930x468AD9EA, 0x486ADE9A, 0x6F6A06A6, 0x5EAE252A, 0x7B6A129A, 0x76BA192A, 0x66FA0A66, 0x5AEE225A,
1940x3FA3C50C, 0x5FC5A30A, 0x3F8BD130, 0x77D18B22, 0x77B18D44, 0x5F8DB150, 0x3AF3C05C, 0x5CF5A03A,
1950x38FBD310, 0x7D7182B2, 0x7B7184D4, 0x58FDB510, 0x2CEFC704, 0x7D4D828E, 0x2ECFC074, 0x74DD882E,
1960x64FD9D04, 0x6F4D90D4, 0x7B2B848E, 0x4AEFA702, 0x6F2B90B2, 0x62FB9B02, 0x72BB884E, 0x4EAFA072,
1970x3FC5A30C, 0x5FA3C50A, 0x3FD18B30, 0x778BD122, 0x778DB144, 0x5FB18D50, 0x3AC0F35C, 0x5CA0F53A,
1980x38D3FB10, 0x7D8271B2, 0x7B8471D4, 0x58B5FD10, 0x2CC7EF04, 0x7D824D8E, 0x2EC0CF74, 0x7488DD2E,
1990x649DFD04, 0x6F904DD4, 0x7B842B8E, 0x4AA7EF02, 0x6F902BB2, 0x629BFB02, 0x7288BB4E, 0x4EA0AF72,
2000x3CA0F53C, 0x5AC0F35A, 0x3D83F1B0, 0x78D27B12, 0x78B47D14, 0x5B85F1D0, 0x3CF5A03C, 0x5AF3C05A,
2010x3DF183B0, 0x787BD212, 0x787DB414, 0x5BF185D0, 0x2CE0C7F4, 0x7848D2DE, 0x2CC7E0F4, 0x78D248DE,
2020x69F04DD4, 0x694DF0D4, 0x7828B4BE, 0x4AE0A7F2, 0x692BF0B2, 0x69F02BB2, 0x78B428BE, 0x4AA7E0F2,
2030x3D83CD8C, 0x6CC66F06, 0x3C88DD3C, 0x66C0CF66, 0x6791CDC4, 0x6C9C7D14, 0x38D3C8DC, 0x6CC660F6,
2040x38C8D3DC, 0x6C60C6F6, 0x6971CCD4, 0x69CC71D4, 0x3DCD838C, 0x6C6FC606, 0x3CDD883C, 0x66CFC066,
2050x67CD91C4, 0x6C7D9C14, 0x692BCC8E, 0x69CC2B8E, 0x6C289CBE, 0x62C89BCE, 0x629BC8CE, 0x6C9C28BE,
2060x6AA66F06, 0x5B85AB8A, 0x6A9A7B12, 0x6791ABA2, 0x66A0AF66, 0x5A88BB5A, 0x6AA660F6, 0x58B5A8BA,
2070x69AA71B2, 0x6971AAB2, 0x6A60A6F6, 0x58A8B5BA, 0x69AA4D8E, 0x694DAA8E, 0x6A9A48DE, 0x649DA8AE,
2080x64A89DAE, 0x6A489ADE, 0x6A6FA606, 0x5BAB858A, 0x6A7B9A12, 0x67AB91A2, 0x66AFA066, 0x5ABB885A,
2090x30A3C5FC, 0x50C5A3FA, 0x0C8BD1FC, 0x44D18BEE, 0x22B18DEE, 0x0A8DB1FA, 0x3A03CF5C, 0x5C05AF3A,
2100x08CBDF1C, 0x4D418EBE, 0x2B218EDE, 0x08ADBF1A, 0x20E3F734, 0x7141B2BE, 0x2E03F374, 0x7411BB2E,
2110x20B9BF26, 0x2B09B2F6, 0x7121D4DE, 0x40E5F752, 0x4D09D4F6, 0x40D9DF46, 0x7211DD4E, 0x4E05F572,
2120x30C5A3FC, 0x50A3C5FA, 0x0CD18BFC, 0x448BD1EE, 0x228DB1EE, 0x0AB18DFA, 0x3ACF035C, 0x5CAF053A,
2130x08DFCB1C, 0x4D8E41BE, 0x2B8E21DE, 0x08BFAD1A, 0x20F7E334, 0x71B241BE, 0x2EF30374, 0x74BB112E,
2140x20BFB926, 0x2BB209F6, 0x71D421DE, 0x40F7E552, 0x4DD409F6, 0x40DFD946, 0x72DD114E, 0x4EF50572,
2150x3CAF053C, 0x5ACF035A, 0x0D8FC1BC, 0x48DE4B1E, 0x28BE2D1E, 0x0B8FA1DA, 0x3C05AF3C, 0x5A03CF5A,
2160x0DC18FBC, 0x484BDE1E, 0x282DBE1E, 0x0BA18FDA, 0x2FE30734, 0x7B4B121E, 0x2F07E334, 0x7B124B1E,
2170x2BB20F96, 0x2B0FB296, 0x7D2D141E, 0x4FE50752, 0x4D0FD496, 0x4DD40F96, 0x7D142D1E, 0x4F07E552,
2180x31B3C1BC, 0x60F66336, 0x3CBB113C, 0x66F30366, 0x23B389E6, 0x28BE3936, 0x3B13CB1C, 0x6F066336,
2190x3BCB131C, 0x6F630636, 0x2B338E96, 0x2B8E3396, 0x31C1B3BC, 0x6063F636, 0x3C11BB3C, 0x6603F366,
2200x2389B3E6, 0x2839BE36, 0x7133D496, 0x71D43396, 0x7D391436, 0x73D91346, 0x7313D946, 0x7D143936,
2210x60F66556, 0x51D5A1DA, 0x48DE5956, 0x45D589E6, 0x66F50566, 0x5ADD115A, 0x6F066556, 0x5D15AD1A,
2220x4D8E5596, 0x4D558E96, 0x6F650656, 0x5DAD151A, 0x71B25596, 0x7155B296, 0x7B125956, 0x7515B926,
2230x75B91526, 0x7B591256, 0x6065F656, 0x51A1D5DA, 0x4859DE56, 0x4589D5E6, 0x6605F566, 0x5A11DD5A,
2240x3053CAFC, 0x5035ACFA, 0x0C47E2FC, 0x441DB8EE, 0x221BD8EE, 0x0A27E4FA, 0x3503CFAC, 0x5305AFCA,
2250x04C7EF2C, 0x414DBE8E, 0x212BDE8E, 0x02A7EF4A, 0x10D3FB38, 0x4171BEB2, 0x1D03F3B8, 0x4711BBE2,
2260x029BFB62, 0x092BF6B2, 0x2171DED4, 0x10B5FD58, 0x094DF6D4, 0x049DFD64, 0x2711DDE4, 0x1B05F5D8,
2270x30CA53FC, 0x50AC35FA, 0x0CE247FC, 0x44B81DEE, 0x22D81BEE, 0x0AE427FA, 0x35CF03AC, 0x53AF05CA,
2280x04EFC72C, 0x41BE4D8E, 0x21DE2B8E, 0x02EFA74A, 0x10FBD338, 0x41BE71B2, 0x1DF303B8, 0x47BB11E2,
2290x02FB9B62, 0x09F62BB2, 0x21DE71D4, 0x10FDB558, 0x09F64DD4, 0x04FD9D64, 0x27DD11E4, 0x1BF505D8,
2300x3C5F0A3C, 0x5A3F0C5A, 0x0E4FC27C, 0x4B1E48DE, 0x2D1E28BE, 0x0E2FA47A, 0x3C0A5F3C, 0x5A0C3F5A,
2310x0EC24F7C, 0x4B481EDE, 0x2D281EBE, 0x0EA42F7A, 0x1FD30B38, 0x4B7B1E12, 0x1F0BD338, 0x4B1E7B12,
2320x0F962BB2, 0x0F2B96B2, 0x2D7D1E14, 0x1FB50D58, 0x0F4D96D4, 0x0F964DD4, 0x2D1E7D14, 0x1F0DB558,
2330x3273C27C, 0x633660F6, 0x3C77223C, 0x663F3066, 0x323B986E, 0x393628BE, 0x3723C72C, 0x63366F06,
2340x37C7232C, 0x636F3606, 0x332B968E, 0x33962B8E, 0x32C2737C, 0x636036F6, 0x3C22773C, 0x66303F66,
2350x32983B6E, 0x392836BE, 0x337196D4, 0x339671D4, 0x397D3614, 0x379D3164, 0x37319D64, 0x39367D14,
2360x655660F6, 0x5475A47A, 0x595648DE, 0x545D986E, 0x665F5066, 0x5A77445A, 0x65566F06, 0x5745A74A,
2370x55964D8E, 0x554D968E, 0x656F5606, 0x57A7454A, 0x559671B2, 0x557196B2, 0x59567B12, 0x57519B62,
2380x579B5162, 0x597B5612, 0x656056F6, 0x54A4757A, 0x594856DE, 0x54985D6E, 0x66505F66, 0x5A44775A,
2390x533F0CCA, 0x355F0AAC, 0x473F30E2, 0x1D7722B8, 0x1B7744D8, 0x275F50E4, 0x437F3E02, 0x17D72B28,
2400x17B74D48, 0x257F5E04, 0x197F7610, 0x179F7160, 0x530C3FCA, 0x350A5FAC, 0x47303FE2, 0x1D2277B8,
2410x1B4477D8, 0x27505FE4, 0x433E7F02, 0x172BD728, 0x174DB748, 0x255E7F04, 0x19767F10, 0x17719F60,
2420x503C3CFA, 0x305A5AFC, 0x433E70F2, 0x127BD278, 0x147DB478, 0x255E70F4, 0x43703EF2, 0x12D27B78,
2430x14B47D78, 0x25705EF4, 0x177196F0, 0x179671F0, 0x433E4CCE, 0x066FC66C, 0x443C3CEE, 0x0C6666FC,
2440x19764CDC, 0x147D9C6C, 0x434C3ECE, 0x06C66F6C, 0x17964DCC, 0x174D96CC, 0x194C76DC, 0x149C7D6C,
2450x066FA66A, 0x255E2AAE, 0x127B9A6A, 0x19762ABA, 0x0A6666FA, 0x225A5AEE, 0x172B96AA, 0x17962BAA,
2460x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74,
2470x4E88BB72, 0x72A0AF4E, 0x7C40C2FE, 0x28E8D7D4, 0x48E8B7B2, 0x7A20A4FE, 0x6E0898FE, 0x60E89F8E,
2480x5CF3C03A, 0x3AF5A05C, 0x74CFC02E, 0x2EDD8874, 0x4EBB8872, 0x72AFA04E, 0x7CC240FE, 0x28D7E8D4,
2490x48B7E8B2, 0x7AA420FE, 0x6E9808FE, 0x609FE88E, 0x5FC3C30A, 0x3FA5A50C, 0x7CC24F0E, 0x2D87ED84,
2500x4B87EB82, 0x7AA42F0E, 0x7C4FC20E, 0x2DED8784, 0x4BEB8782, 0x7A2FA40E, 0x690FE88E, 0x69E80F8E,
2510x7CC27332, 0x3993F990, 0x77C3C322, 0x3F999930, 0x6E983B32, 0x6393EB82, 0x7C73C232, 0x39F99390,
2520x69E833B2, 0x6933E8B2, 0x6E3B9832, 0x63EB9382, 0x5995F990, 0x7AA47554, 0x6595ED84, 0x6E985D54,
2530x5F999950, 0x77A5A544, 0x6955E8D4, 0x69E855D4, 0x59F99590, 0x7A75A454, 0x6E5D9854, 0x65ED9584,
2540x5CCF033A, 0x3AAF055C, 0x74F3032E, 0x2EBB1174, 0x4EDD1172, 0x72F5054E, 0x7F43023E, 0x2BEB1714,
2550x4DED1712, 0x7F25045E, 0x7F191076, 0x71F91706, 0x5C03CF3A, 0x3A05AF5C, 0x7403F32E, 0x2E11BB74,
2560x4E11DD72, 0x7205F54E, 0x7F02433E, 0x2B17EB14, 0x4D17ED12, 0x7F04255E, 0x7F101976, 0x7117F906,
2570x50C3C3FA, 0x30A5A5FC, 0x70F2433E, 0x21B7E1B4, 0x41D7E1D2, 0x70F4255E, 0x7043F23E, 0x21E1B7B4,
2580x41E1D7D2, 0x7025F45E, 0x7117F096, 0x71F01796, 0x4CCE433E, 0x099FC99C, 0x44C3C3EE, 0x0C9999FC,
2590x4CDC1976, 0x41D7C9C6, 0x4C43CE3E, 0x09C99F9C, 0x4DCC1796, 0x4D17CC96, 0x4C19DC76, 0x41C9D7C6,
2600x099FA99A, 0x2AAE255E, 0x21B7A9A6, 0x2ABA1976, 0x0A9999FA, 0x22A5A5EE, 0x2B17AA96, 0x2BAA1796,
2610x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8,
2620x1B22EED8, 0x270AFAE4, 0x407CFEC2, 0x14D4EBE8, 0x12B2EDE8, 0x207AFEA4, 0x086EFE98, 0x068EF9E8,
2630x53FC30CA, 0x35FA50AC, 0x47FC0CE2, 0x1DEE44B8, 0x1BEE22D8, 0x27FA0AE4, 0x40FE7CC2, 0x14EBD4E8,
2640x12EDB2E8, 0x20FE7AA4, 0x08FE6E98, 0x06F98EE8, 0x5F3C3C0A, 0x3F5A5A0C, 0x4F0E7CC2, 0x1E4BDE48,
2650x1E2DBE28, 0x2F0E7AA4, 0x4F7C0EC2, 0x1EDE4B48, 0x1EBE2D28, 0x2F7A0EA4, 0x0F698EE8, 0x0F8E69E8,
2660x73327CC2, 0x3663F660, 0x773C3C22, 0x3F666630, 0x3B326E98, 0x3639BE28, 0x737C32C2, 0x36F66360,
2670x33B269E8, 0x3369B2E8, 0x3B6E3298, 0x36BE3928, 0x5665F660, 0x75547AA4, 0x5659DE48, 0x5D546E98,
2680x5F666650, 0x775A5A44, 0x5569D4E8, 0x55D469E8, 0x56F66560, 0x757A54A4, 0x5D6E5498, 0x56DE5948
269};
270
274
275#define SDB_MAX_CUTSIZE 6
276#define SDB_MAX_CUTNUM 51
277#define SDB_MAX_TT_WORDS ((SDB_MAX_CUTSIZE > 6) ? 1 << (SDB_MAX_CUTSIZE-6) : 1)
278
279#define SDB_CUT_NO_LEAF 0xF
280
281typedef struct Sdb_Cut_t_ Sdb_Cut_t;
282struct Sdb_Cut_t_
283{
284 word Sign; // signature
285 int iFunc; // functionality
286 int Cost; // cut cost
287 int CostLev; // cut cost
288 unsigned nTreeLeaves : 28; // tree leaves
289 unsigned nLeaves : 4; // leaf count
290 int pLeaves[SDB_MAX_CUTSIZE]; // leaves
291};
292
293typedef struct Sdb_Sto_t_ Sdb_Sto_t;
294struct Sdb_Sto_t_
295{
296 int nCutSize;
297 int nCutNum;
298 int fCutMin;
299 int fTruthMin;
300 int fVerbose;
301 Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
302 Vec_Int_t * vRefs; // refs for each node
303 Vec_Wec_t * vCuts; // cuts for each node
304 Vec_Mem_t * vTtMem; // truth tables
305 Sdb_Cut_t pCuts[3][SDB_MAX_CUTNUM]; // temporary cuts
306 Sdb_Cut_t * ppCuts[SDB_MAX_CUTNUM]; // temporary cut pointers
307 int nCutsR; // the number of cuts
308 int Pivot; // current object
309 int iCutBest; // best-delay cut
310 int nCutsOver; // overflow cuts
311 double CutCount[4]; // cut counters
312 abctime clkStart; // starting time
313};
314
315static inline word * Sdb_CutTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut ) { return Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc)); }
316
317#define Sdb_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 2 )
318
322
334static inline word Sdb_CutGetSign( Sdb_Cut_t * pCut )
335{
336 word Sign = 0; int i;
337 for ( i = 0; i < (int)pCut->nLeaves; i++ )
338 Sign |= ((word)1) << (pCut->pLeaves[i] & 0x3F);
339 return Sign;
340}
341static inline int Sdb_CutCheck( Sdb_Cut_t * pBase, Sdb_Cut_t * pCut ) // check if pCut is contained in pBase
342{
343 int nSizeB = pBase->nLeaves;
344 int nSizeC = pCut->nLeaves;
345 int i, * pB = pBase->pLeaves;
346 int k, * pC = pCut->pLeaves;
347 for ( i = 0; i < nSizeC; i++ )
348 {
349 for ( k = 0; k < nSizeB; k++ )
350 if ( pC[i] == pB[k] )
351 break;
352 if ( k == nSizeB )
353 return 0;
354 }
355 return 1;
356}
357static inline int Sdb_CutSetCheckArray( Sdb_Cut_t ** ppCuts, int nCuts )
358{
359 Sdb_Cut_t * pCut0, * pCut1;
360 int i, k, m, n, Value;
361 assert( nCuts > 0 );
362 for ( i = 0; i < nCuts; i++ )
363 {
364 pCut0 = ppCuts[i];
365 assert( pCut0->nLeaves <= SDB_MAX_CUTSIZE );
366 assert( pCut0->Sign == Sdb_CutGetSign(pCut0) );
367 // check duplicates
368 for ( m = 0; m < (int)pCut0->nLeaves; m++ )
369 for ( n = m + 1; n < (int)pCut0->nLeaves; n++ )
370 assert( pCut0->pLeaves[m] < pCut0->pLeaves[n] );
371 // check pairs
372 for ( k = 0; k < nCuts; k++ )
373 {
374 pCut1 = ppCuts[k];
375 if ( pCut0 == pCut1 )
376 continue;
377 // check containments
378 Value = Sdb_CutCheck( pCut0, pCut1 );
379 assert( Value == 0 );
380 }
381 }
382 return 1;
383}
384
385
397static inline int Sdb_CutMergeOrder( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, Sdb_Cut_t * pCut, int nCutSize )
398{
399 int nSize0 = pCut0->nLeaves;
400 int nSize1 = pCut1->nLeaves;
401 int i, * pC0 = pCut0->pLeaves;
402 int k, * pC1 = pCut1->pLeaves;
403 int c, * pC = pCut->pLeaves;
404 // the case of the largest cut sizes
405 if ( nSize0 == nCutSize && nSize1 == nCutSize )
406 {
407 for ( i = 0; i < nSize0; i++ )
408 {
409 if ( pC0[i] != pC1[i] ) return 0;
410 pC[i] = pC0[i];
411 }
412 pCut->nLeaves = nCutSize;
413 pCut->iFunc = -1;
414 pCut->Sign = pCut0->Sign | pCut1->Sign;
415 return 1;
416 }
417 // compare two cuts with different numbers
418 i = k = c = 0;
419 if ( nSize0 == 0 ) goto FlushCut1;
420 if ( nSize1 == 0 ) goto FlushCut0;
421 while ( 1 )
422 {
423 if ( c == nCutSize ) return 0;
424 if ( pC0[i] < pC1[k] )
425 {
426 pC[c++] = pC0[i++];
427 if ( i >= nSize0 ) goto FlushCut1;
428 }
429 else if ( pC0[i] > pC1[k] )
430 {
431 pC[c++] = pC1[k++];
432 if ( k >= nSize1 ) goto FlushCut0;
433 }
434 else
435 {
436 pC[c++] = pC0[i++]; k++;
437 if ( i >= nSize0 ) goto FlushCut1;
438 if ( k >= nSize1 ) goto FlushCut0;
439 }
440 }
441
442FlushCut0:
443 if ( c + nSize0 > nCutSize + i ) return 0;
444 while ( i < nSize0 )
445 pC[c++] = pC0[i++];
446 pCut->nLeaves = c;
447 pCut->iFunc = -1;
448 pCut->Sign = pCut0->Sign | pCut1->Sign;
449 return 1;
450
451FlushCut1:
452 if ( c + nSize1 > nCutSize + k ) return 0;
453 while ( k < nSize1 )
454 pC[c++] = pC1[k++];
455 pCut->nLeaves = c;
456 pCut->iFunc = -1;
457 pCut->Sign = pCut0->Sign | pCut1->Sign;
458 return 1;
459}
460static inline int Sdb_CutMergeOrder2( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, Sdb_Cut_t * pCut, int nCutSize )
461{
462 int x0, i0 = 0, nSize0 = pCut0->nLeaves, * pC0 = pCut0->pLeaves;
463 int x1, i1 = 0, nSize1 = pCut1->nLeaves, * pC1 = pCut1->pLeaves;
464 int xMin, c = 0, * pC = pCut->pLeaves;
465 while ( 1 )
466 {
467 x0 = (i0 == nSize0) ? ABC_INFINITY : pC0[i0];
468 x1 = (i1 == nSize1) ? ABC_INFINITY : pC1[i1];
469 xMin = Abc_MinInt(x0, x1);
470 if ( xMin == ABC_INFINITY ) break;
471 if ( c == nCutSize ) return 0;
472 pC[c++] = xMin;
473 if (x0 == xMin) i0++;
474 if (x1 == xMin) i1++;
475 }
476 pCut->nLeaves = c;
477 pCut->iFunc = -1;
478 pCut->Sign = pCut0->Sign | pCut1->Sign;
479 return 1;
480}
481static inline int Sdb_CutSetCutIsContainedOrder( Sdb_Cut_t * pBase, Sdb_Cut_t * pCut ) // check if pCut is contained in pBase
482{
483 int i, nSizeB = pBase->nLeaves;
484 int k, nSizeC = pCut->nLeaves;
485 if ( nSizeB == nSizeC )
486 {
487 for ( i = 0; i < nSizeB; i++ )
488 if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
489 return 0;
490 return 1;
491 }
492 assert( nSizeB > nSizeC );
493 if ( nSizeC == 0 )
494 return 1;
495 for ( i = k = 0; i < nSizeB; i++ )
496 {
497 if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
498 return 0;
499 if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
500 {
501 if ( ++k == nSizeC )
502 return 1;
503 }
504 }
505 return 0;
506}
507static inline int Sdb_CutSetLastCutIsContained( Sdb_Cut_t ** pCuts, int nCuts )
508{
509 int i;
510 for ( i = 0; i < nCuts; i++ )
511 if ( pCuts[i]->nLeaves <= pCuts[nCuts]->nLeaves && (pCuts[i]->Sign & pCuts[nCuts]->Sign) == pCuts[i]->Sign && Sdb_CutSetCutIsContainedOrder(pCuts[nCuts], pCuts[i]) )
512 return 1;
513 return 0;
514}
515
527static inline int Sdb_CutCompare( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1 )
528{
529 if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1;
530 if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1;
531 if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
532 if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
533 return 0;
534}
535static inline int Sdb_CutSetLastCutContains( Sdb_Cut_t ** pCuts, int nCuts )
536{
537 int i, k, fChanges = 0;
538 for ( i = 0; i < nCuts; i++ )
539 if ( pCuts[nCuts]->nLeaves < pCuts[i]->nLeaves && (pCuts[nCuts]->Sign & pCuts[i]->Sign) == pCuts[nCuts]->Sign && Sdb_CutSetCutIsContainedOrder(pCuts[i], pCuts[nCuts]) )
540 pCuts[i]->nLeaves = SDB_CUT_NO_LEAF, fChanges = 1;
541 if ( !fChanges )
542 return nCuts;
543 for ( i = k = 0; i <= nCuts; i++ )
544 {
545 if ( pCuts[i]->nLeaves == SDB_CUT_NO_LEAF )
546 continue;
547 if ( k < i )
548 ABC_SWAP( Sdb_Cut_t *, pCuts[k], pCuts[i] );
549 k++;
550 }
551 return k - 1;
552}
553static inline void Sdb_CutSetSortByCost( Sdb_Cut_t ** pCuts, int nCuts )
554{
555 int i;
556 for ( i = nCuts; i > 0; i-- )
557 {
558 if ( Sdb_CutCompare(pCuts[i - 1], pCuts[i]) < 0 )
559 return;
560 ABC_SWAP( Sdb_Cut_t *, pCuts[i - 1], pCuts[i] );
561 }
562}
563static inline int Sdb_CutSetAddCut( Sdb_Cut_t ** pCuts, int nCuts, int nCutNum )
564{
565 if ( nCuts == 0 )
566 return 1;
567 nCuts = Sdb_CutSetLastCutContains(pCuts, nCuts);
568 assert( nCuts >= 0 );
569 Sdb_CutSetSortByCost( pCuts, nCuts );
570 // add new cut if there is room
571 return Abc_MinInt( nCuts + 1, nCutNum - 1 );
572}
573
585static inline int Sdb_CutComputeTruth6( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, int fCompl0, int fCompl1, Sdb_Cut_t * pCutR, int fIsXor )
586{
587 int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t;
588 word t0 = *Sdb_CutTruth(p, pCut0);
589 word t1 = *Sdb_CutTruth(p, pCut1);
590 if ( Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 ) t0 = ~t0;
591 if ( Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 ) t1 = ~t1;
592 t0 = Abc_Tt6Expand( t0, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
593 t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
594 t = fIsXor ? t0 ^ t1 : t0 & t1;
595 if ( (fCompl = (int)(t & 1)) ) t = ~t;
596 if ( p->fTruthMin )
597 pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
598 assert( (int)(t & 1) == 0 );
599 truthId = Vec_MemHashInsert(p->vTtMem, &t);
600 pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
601 assert( (int)pCutR->nLeaves <= nOldSupp );
602 return (int)pCutR->nLeaves < nOldSupp;
603}
604static inline int Sdb_CutComputeTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, int fCompl0, int fCompl1, Sdb_Cut_t * pCutR, int fIsXor )
605{
606 if ( p->nCutSize <= 6 )
607 return Sdb_CutComputeTruth6( p, pCut0, pCut1, fCompl0, fCompl1, pCutR, fIsXor );
608 {
609 word uTruth[SDB_MAX_TT_WORDS], uTruth0[SDB_MAX_TT_WORDS], uTruth1[SDB_MAX_TT_WORDS];
610 int nOldSupp = pCutR->nLeaves, truthId;
611 int nCutSize = p->nCutSize, fCompl;
612 int nWords = Abc_Truth6WordNum(nCutSize);
613 word * pTruth0 = Sdb_CutTruth(p, pCut0);
614 word * pTruth1 = Sdb_CutTruth(p, pCut1);
615 Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 );
616 Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 );
617 Abc_TtExpand( uTruth0, nCutSize, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
618 Abc_TtExpand( uTruth1, nCutSize, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
619 if ( fIsXor )
620 Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) );
621 else
622 Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) );
623 if ( p->fTruthMin )
624 pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
625 assert( (uTruth[0] & 1) == 0 );
626//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
627 truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
628 pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
629 assert( (int)pCutR->nLeaves <= nOldSupp );
630 return (int)pCutR->nLeaves < nOldSupp;
631 }
632}
633
645static inline int Sdb_CutCountBits( word i )
646{
647 i = i - ((i >> 1) & 0x5555555555555555);
648 i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
649 i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
650 return (i*(0x0101010101010101))>>56;
651}
652static inline void Sdb_CutAddUnit( Sdb_Sto_t * p, int iObj )
653{
654 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
655 if ( Vec_IntSize(vThis) == 0 )
656 Vec_IntPush( vThis, 1 );
657 else
658 Vec_IntAddToEntry( vThis, 0, 1 );
659 Vec_IntPush( vThis, 1 );
660 Vec_IntPush( vThis, iObj );
661 Vec_IntPush( vThis, 2 );
662}
663static inline void Sdb_CutAddZero( Sdb_Sto_t * p, int iObj )
664{
665 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
666 assert( Vec_IntSize(vThis) == 0 );
667 Vec_IntPush( vThis, 1 );
668 Vec_IntPush( vThis, 0 );
669 Vec_IntPush( vThis, 0 );
670}
671static inline int Sdb_CutTreeLeaves( Sdb_Sto_t * p, Sdb_Cut_t * pCut )
672{
673 int i, Cost = 0;
674 for ( i = 0; i < (int)pCut->nLeaves; i++ )
675 Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
676 return Cost;
677}
678static inline int Sdb_StoPrepareSet( Sdb_Sto_t * p, int iObj, int Index )
679{
680 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
681 int i, v, * pCut, * pList = Vec_IntArray( vThis );
682 Sdb_ForEachCut( pList, pCut, i )
683 {
684 Sdb_Cut_t * pCutTemp = &p->pCuts[Index][i];
685 pCutTemp->nLeaves = pCut[0];
686 for ( v = 1; v <= pCut[0]; v++ )
687 pCutTemp->pLeaves[v-1] = pCut[v];
688 pCutTemp->iFunc = pCut[pCut[0]+1];
689 pCutTemp->Sign = Sdb_CutGetSign( pCutTemp );
690 pCutTemp->nTreeLeaves = Sdb_CutTreeLeaves( p, pCutTemp );
691 }
692 return pList[0];
693}
694static inline void Sdb_StoInitResult( Sdb_Sto_t * p )
695{
696 int i;
697 for ( i = 0; i < SDB_MAX_CUTNUM; i++ )
698 p->ppCuts[i] = &p->pCuts[2][i];
699}
700static inline void Sdb_StoStoreResult( Sdb_Sto_t * p, int iObj, Sdb_Cut_t ** pCuts, int nCuts )
701{
702 int i, v;
703 Vec_Int_t * vList = Vec_WecEntry( p->vCuts, iObj );
704 Vec_IntPush( vList, nCuts );
705 for ( i = 0; i < nCuts; i++ )
706 {
707 Vec_IntPush( vList, pCuts[i]->nLeaves );
708 for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
709 Vec_IntPush( vList, pCuts[i]->pLeaves[v] );
710 Vec_IntPush( vList, pCuts[i]->iFunc );
711 }
712}
713static inline void Sdb_CutPrint( Sdb_Sto_t * p, int iObj, Sdb_Cut_t * pCut )
714{
715 int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia));
716 if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
717 printf( "%d {", pCut->nLeaves );
718 for ( i = 0; i < (int)pCut->nLeaves; i++ )
719 printf( " %*d", nDigits, pCut->pLeaves[i] );
720 for ( ; i < (int)p->nCutSize; i++ )
721 printf( " %*s", nDigits, " " );
722 printf( " } Cost = %3d CostL = %3d Tree = %d ",
723 pCut->Cost, pCut->CostLev, pCut->nTreeLeaves );
724 printf( "\n" );
725}
726void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj )
727{
728 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
729 int fIsXor = Gia_ObjIsXor(pObj);
730 int nCutSize = p->nCutSize;
731 int nCutNum = p->nCutNum;
732 int fComp0 = Gia_ObjFaninC0(pObj);
733 int fComp1 = Gia_ObjFaninC1(pObj);
734 int Fan0 = Gia_ObjFaninId0(pObj, iObj);
735 int Fan1 = Gia_ObjFaninId1(pObj, iObj);
736 int nCuts0 = Sdb_StoPrepareSet( p, Fan0, 0 );
737 int nCuts1 = Sdb_StoPrepareSet( p, Fan1, 1 );
738 int i, k, nCutsR = 0;
739 Sdb_Cut_t * pCut0, * pCut1, ** pCutsR = p->ppCuts;
740 assert( !Gia_ObjIsBuf(pObj) );
741 assert( !Gia_ObjIsMux(p->pGia, pObj) );
742 Sdb_StoInitResult( p );
743 p->CutCount[0] += nCuts0 * nCuts1;
744 for ( i = 0, pCut0 = p->pCuts[0]; i < nCuts0; i++, pCut0++ )
745 for ( k = 0, pCut1 = p->pCuts[1]; k < nCuts1; k++, pCut1++ )
746 {
747 if ( (int)(pCut0->nLeaves + pCut1->nLeaves) > nCutSize && Sdb_CutCountBits(pCut0->Sign | pCut1->Sign) > nCutSize )
748 continue;
749 p->CutCount[1]++;
750 if ( !Sdb_CutMergeOrder(pCut0, pCut1, pCutsR[nCutsR], nCutSize) )
751 continue;
752 if ( Sdb_CutSetLastCutIsContained(pCutsR, nCutsR) )
753 continue;
754 p->CutCount[2]++;
755 if ( p->fCutMin && Sdb_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) )
756 pCutsR[nCutsR]->Sign = Sdb_CutGetSign(pCutsR[nCutsR]);
757 pCutsR[nCutsR]->nTreeLeaves = Sdb_CutTreeLeaves( p, pCutsR[nCutsR] );
758 nCutsR = Sdb_CutSetAddCut( pCutsR, nCutsR, nCutNum );
759 }
760 p->CutCount[3] += nCutsR;
761 p->nCutsOver += nCutsR == nCutNum-1;
762 p->nCutsR = nCutsR;
763 p->Pivot = iObj;
764 // debug printout
765 if ( 0 )
766 {
767 printf( "*** Obj = %4d NumCuts = %4d\n", iObj, nCutsR );
768 for ( i = 0; i < nCutsR; i++ )
769 Sdb_CutPrint( p, iObj, pCutsR[i] );
770 printf( "\n" );
771 }
772 // verify
773 assert( nCutsR > 0 && nCutsR < nCutNum );
774 assert( Sdb_CutSetCheckArray(pCutsR, nCutsR) );
775 // store the cutset
776 Sdb_StoStoreResult( p, iObj, pCutsR, nCutsR );
777 if ( nCutsR > 1 || pCutsR[0]->nLeaves > 1 )
778 Sdb_CutAddUnit( p, iObj );
779}
780
781
782
795int Sdb_StoDiffExactlyOne( Vec_Wec_t * vCuts, int Limit, int * pCut )
796{
797 Vec_Int_t * vCut;
798 int i, k, iNew;
799 // check if it is fully contained in any one
800 Vec_WecForEachLevel( vCuts, vCut, i )
801 {
802 for ( k = 1; k <= pCut[0]; k++ )
803 if ( Vec_IntFind(vCut, pCut[k]) == -1 )
804 break;
805 if ( k == pCut[0] + 1 )
806 return -1;
807 }
808 // check if there is one different
809 Vec_WecForEachLevel( vCuts, vCut, i )
810 {
811 if ( i == Limit )
812 break;
813 for ( iNew = -1, k = 1; k <= pCut[0]; k++ )
814 {
815 if ( Vec_IntFind(vCut, pCut[k]) >= 0 )
816 continue;
817 if ( iNew == -1 )
818 iNew = pCut[k];
819 else
820 break;
821 }
822 if ( k == pCut[0] + 1 && iNew != -1 )
823 return iNew;
824 }
825 return -1;
826}
827int Sdb_StoDiffExactlyOne3( Vec_Wec_t * vCuts, int Limit, int * pCut, int * pCount )
828{
829 Vec_Int_t * vCut;
830 int i, iNewAll = -1, Count = 0;
831 Vec_WecForEachLevel( vCuts, vCut, i )
832 {
833 int k, iNew = -1;
834 if ( i == Limit )
835 break;
836 for ( k = 1; k <= pCut[0]; k++ )
837 {
838 if ( Vec_IntFind(vCut, pCut[k]) >= 0 )
839 continue;
840 if ( iNew == -1 )
841 iNew = pCut[k];
842 else
843 break;
844 }
845 if ( k == pCut[0] + 1 && iNew != -1 )
846 {
847 if ( iNewAll == -1 )
848 iNewAll = iNew;
849 if ( iNewAll == iNew )
850 Count++;
851 }
852 }
853 *pCount = Count;
854 return iNewAll;
855}
856Vec_Int_t * Sdb_StoFindAll( Vec_Wec_t * vCuts )
857{
858 int i, k, Entry;
859 Vec_Int_t * vCut, * vAll = Vec_IntAlloc( 100 );
860 Vec_WecForEachLevel( vCuts, vCut, i )
861 Vec_IntForEachEntry( vCut, Entry, k )
862 Vec_IntPushUnique( vAll, Entry );
863 return vAll;
864}
865int Sdb_StoDiffExactlyOne2( Vec_Int_t * vAll, int * pCut )
866{
867 int k, iNew = -1;
868 for ( k = 1; k <= pCut[0]; k++ )
869 {
870 if ( Vec_IntFind(vAll, pCut[k]) >= 0 )
871 continue;
872 if ( iNew == -1 )
873 iNew = pCut[k];
874 else
875 break;
876 }
877 if ( k == pCut[0] + 1 && iNew != -1 )
878 return iNew;
879 return -1;
880}
881Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
882{
883 int fVerbose = 0;
884 Vec_Int_t * vCut, * vCounts;
885 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
886 Vec_Int_t * vResA = Vec_IntAlloc( 100 );
887 Vec_Int_t * vResB = Vec_IntAlloc( 100 );
888 int i, k, Entry, Max = 0, Min, MinValue;
889 // find MAX value
890 Vec_WecForEachLevel( vCuts, vCut, i )
891 Vec_IntForEachEntry( vCut, Entry, k )
892 Max = Abc_MaxInt( Max, Entry );
893 // count how many times each value appears
894 vCounts = Vec_IntStart( Max + 1 );
895 Vec_WecForEachLevel( vCuts, vCut, i )
896 Vec_IntForEachEntry( vCut, Entry, k )
897 Vec_IntAddToEntry( vCounts, Entry, 1 );
898 Vec_IntWriteEntry( vCounts, 0, 0 );
899 // print out
900 if ( fVerbose )
901 Vec_IntForEachEntry( vCounts, Entry, k )
902 if ( Entry )
903 printf( "%5d %5d\n", k, Entry );
904 // collect first part
905 MinValue = ABC_INFINITY;
906 Vec_IntForEachEntry( vCounts, Entry, k )
907 if ( Entry )
908 MinValue = Abc_MinInt( MinValue, Entry );
909 if ( MinValue == ABC_INFINITY )
910 return vRes;
911 Min = Vec_IntFind( vCounts, MinValue );
912 Vec_IntPush( vResA, Min );
913 Vec_IntWriteEntry( vCounts, Min, 0 );
914 Vec_IntForEachEntry( vCounts, Entry, k )
915 if ( Entry == MinValue || Entry == 2*MinValue )
916 {
917 Vec_IntPush( vResA, k );
918 Vec_IntWriteEntry( vCounts, k, 0 );
919 }
920 // collect second parts
921 MinValue = Vec_IntEntry( vCounts, Front );
922 Min = Front;
923 Vec_IntPush( vResB, Min );
924 Vec_IntWriteEntry( vCounts, Min, 0 );
925 Vec_IntForEachEntry( vCounts, Entry, k )
926 if ( Entry == MinValue || Entry == 2*MinValue )
927 {
928 Vec_IntPush( vResB, k );
929 Vec_IntWriteEntry( vCounts, k, 0 );
930 }
931 Vec_IntFree( vCounts );
932 Vec_IntPrint( vResA );
933 Vec_IntPrint( vResB );
934 // here we need to order the inputs
935
936 // append
937 Vec_IntAppend( vRes, vResA );
938 Vec_IntAppend( vRes, vResB );
939 Vec_IntFree( vResA );
940 Vec_IntFree( vResB );
941 return vRes;
942}
943
955int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj, int CutSize, int ** ppCut )
956{
957 int fVerbose = 0;
958 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
959 int i, k, * pCut, * pList = Vec_IntArray( vThis );
960 word * pTruth;
961 Sdb_ForEachCut( pList, pCut, i )
962 {
963 if ( pCut[0] != CutSize )
964 continue;
965 if ( pCut[0] == 5 )
966 {
967 pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
968 for ( k = 0; k < s_nFuncTruths5; k++ )
969 if ( s_FuncTruths5[k] == (unsigned)*pTruth )
970 break;
971 if ( k < s_nFuncTruths5 )
972 {
973 if ( fVerbose )
974 {
975 printf( "Object %d has %d-input cut: ", iObj, pCut[0] );
976 for ( k = 1; k <= pCut[0]; k++ )
977 printf( "%d ", pCut[k] );
978 printf( "\n" );
979 }
980 *ppCut = pCut;
981 return 1; // five-input
982 }
983 }
984 if ( pCut[0] == 4 )
985 {
986 pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
987 for ( k = 0; k < s_nFuncTruths4; k++ )
988 if ( s_FuncTruths4[k] == (0xFFFF & (unsigned)*pTruth) )
989 break;
990 if ( k < s_nFuncTruths4 )
991 {
992 if ( fVerbose )
993 {
994 printf( "Object %d has %d-input cut: ", iObj, pCut[0] );
995 for ( k = 1; k <= pCut[0]; k++ )
996 printf( "%d ", pCut[k] );
997 printf( "\n" );
998 }
999 *ppCut = pCut;
1000 return 2; // front
1001 }
1002 }
1003 if ( pCut[0] == 4 )
1004 {
1005 pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
1006 for ( k = 0; k < s_nFuncTruths4a; k++ )
1007 if ( s_FuncTruths4a[k] == (0xFFFF & (unsigned)*pTruth) )
1008 break;
1009 if ( k < s_nFuncTruths4a )
1010 {
1011 if ( fVerbose )
1012 {
1013 printf( "Object %d has %d-input cut: ", iObj, pCut[0] );
1014 for ( k = 1; k <= pCut[0]; k++ )
1015 printf( "%d ", pCut[k] );
1016 printf( "\n" );
1017 }
1018 *ppCut = pCut;
1019 return 3; // back unsigned
1020 }
1021 }
1022 if ( pCut[0] == 4 )
1023 {
1024 pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
1025 for ( k = 0; k < s_nFuncTruths4b; k++ )
1026 if ( s_FuncTruths4b[k] == (0xFFFF & (unsigned)*pTruth) )
1027 break;
1028 if ( k < s_nFuncTruths4b )
1029 {
1030 if ( fVerbose )
1031 {
1032 printf( "Object %d has %d-input cut: ", iObj, pCut[0] );
1033 for ( k = 1; k <= pCut[0]; k++ )
1034 printf( "%d ", pCut[k] );
1035 printf( "\n" );
1036 }
1037 *ppCut = pCut;
1038 return 4; // back signed
1039 }
1040 }
1041 }
1042 return 0;
1043}
1044Vec_Int_t * Sdb_StoIterCuts( Sdb_Sto_t * p )
1045{
1046 Vec_Wec_t * v5Cuts = Vec_WecAlloc( 100 );
1047 Vec_Int_t * v5Cut, * vAll, * vRes;
1048 Gia_Obj_t * pObj;
1049 int k, iObj, * pCut, Limit, iNew, iNewFront = -1, iNewBack = -1, iSigned = 0;
1050 Gia_ManForEachAnd( p->pGia, pObj, iObj )
1051 {
1052 int RetValue = Sdb_StoIterCutsOne( p, iObj, 5, &pCut );
1053 if ( RetValue == 0 )
1054 continue;
1055 assert( RetValue == 1 );
1056 assert( pCut[0] == 5 );
1057 v5Cut = Vec_WecPushLevel( v5Cuts );
1058 for ( k = 1; k <= pCut[0]; k++ )
1059 Vec_IntPush( v5Cut, pCut[k] );
1060 }
1061 Limit = Vec_WecSize( v5Cuts );
1062 printf( "Detected %d 5-cuts.\n", Vec_WecSize(v5Cuts) );
1063 vAll = Sdb_StoFindAll( v5Cuts );
1064 Gia_ManForEachAnd( p->pGia, pObj, iObj )
1065 {
1066 int RetValue = Sdb_StoIterCutsOne( p, iObj, 4, &pCut );
1067 if ( RetValue == 0 )
1068 continue;
1069 assert( RetValue >= 2 && RetValue <= 4 );
1070 assert( pCut[0] == 4 );
1071 // find cut, which differs in exactly one input
1072 iNew = Sdb_StoDiffExactlyOne( v5Cuts, Limit, pCut );
1073 if ( iNew == -1 )
1074 continue;
1075 if ( RetValue == 2 )
1076 iNewFront = iNew;
1077 else
1078 iNewBack = iNew;
1079 if ( RetValue == 4 )
1080 iSigned = 1;
1081 // save in the second cut
1082 v5Cut = Vec_WecPushLevel( v5Cuts );
1083 Vec_IntPush( v5Cut, 0 );
1084 for ( k = 1; k <= pCut[0]; k++ )
1085 Vec_IntPush( v5Cut, pCut[k] );
1086 }
1087 Vec_IntFree( vAll );
1088 Vec_WecPrint( v5Cuts, 0 );
1089
1090 if ( iNewFront )
1091 printf( "Front = %d\n", iNewFront );
1092 if ( iNewBack )
1093 printf( "Back = %d\n", iNewBack );
1094 if ( iSigned )
1095 printf( "Sign = %d\n", iSigned );
1096
1097 vRes = Sdb_StoFindInputs( v5Cuts, iNewFront );
1098
1099 Vec_WecFree( v5Cuts );
1100 return vRes;
1101}
1102
1114Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fTruthMin, int fVerbose )
1115{
1116 Sdb_Sto_t * p;
1117 assert( nCutSize < SDB_CUT_NO_LEAF );
1118 assert( nCutSize > 1 && nCutSize <= SDB_MAX_CUTSIZE );
1119 assert( nCutNum > 1 && nCutNum < SDB_MAX_CUTNUM );
1120 p = ABC_CALLOC( Sdb_Sto_t, 1 );
1121 p->clkStart = Abc_Clock();
1122 p->nCutSize = nCutSize;
1123 p->nCutNum = nCutNum;
1124 p->fCutMin = fCutMin;
1125 p->fTruthMin = fTruthMin;
1126 p->fVerbose = fVerbose;
1127 p->pGia = pGia;
1128 p->vRefs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
1129 p->vCuts = Vec_WecStart( Gia_ManObjNum(pGia) );
1130 p->vTtMem = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
1131 return p;
1132}
1133void Sdb_StoFree( Sdb_Sto_t * p )
1134{
1135 Vec_IntFree( p->vRefs );
1136 Vec_WecFree( p->vCuts );
1137 if ( p->fCutMin )
1138 Vec_MemHashFree( p->vTtMem );
1139 if ( p->fCutMin )
1140 Vec_MemFree( p->vTtMem );
1141 ABC_FREE( p );
1142}
1143void Sdb_StoComputeCutsConst0( Sdb_Sto_t * p, int iObj )
1144{
1145 Sdb_CutAddZero( p, iObj );
1146}
1147void Sdb_StoComputeCutsCi( Sdb_Sto_t * p, int iObj )
1148{
1149 Sdb_CutAddUnit( p, iObj );
1150}
1151void Sdb_StoComputeCutsNode( Sdb_Sto_t * p, int iObj )
1152{
1153 Sdb_StoMergeCuts( p, iObj );
1154}
1155void Sdb_StoRefObj( Sdb_Sto_t * p, int iObj )
1156{
1157 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
1158 assert( iObj == Vec_IntSize(p->vRefs) );
1159 Vec_IntPush( p->vRefs, 0 );
1160 if ( Gia_ObjIsAnd(pObj) )
1161 {
1162 Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
1163 Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId1(pObj, iObj), 1 );
1164 }
1165 else if ( Gia_ObjIsCo(pObj) )
1166 Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
1167}
1168Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia )
1169{
1170 Vec_Int_t * vRes = NULL;
1171 Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 5, 20, 1, 0, 1 );
1172 Gia_Obj_t * pObj;
1173 int i, iObj;
1174 // prepare references
1175 Gia_ManForEachObj( p->pGia, pObj, iObj )
1176 Sdb_StoRefObj( p, iObj );
1177 // compute cuts
1178 Sdb_StoComputeCutsConst0( p, 0 );
1179 Gia_ManForEachCiId( p->pGia, iObj, i )
1180 Sdb_StoComputeCutsCi( p, iObj );
1181 Gia_ManForEachAnd( p->pGia, pObj, iObj )
1182 Sdb_StoComputeCutsNode( p, iObj );
1183 if ( p->fVerbose )
1184 {
1185 printf( "Running cut computation with CutSize = %d CutNum = %d:\n", p->nCutSize, p->nCutNum );
1186 printf( "CutPair = %.0f ", p->CutCount[0] );
1187 printf( "Merge = %.0f (%.2f %%) ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
1188 printf( "Eval = %.0f (%.2f %%) ", p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
1189 printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
1190 printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
1191 printf( "\n" );
1192 printf( "Over = %4d ", p->nCutsOver );
1193 Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
1194 }
1195 vRes = Sdb_StoIterCuts( p );
1196 Sdb_StoFree( p );
1197 return vRes;
1198}
1199void Sdb_StoComputeCutsTest( Gia_Man_t * pGia )
1200{
1201 Vec_Int_t * vRes = Sdb_StoComputeCutsDetect( pGia );
1202 Vec_IntFree( vRes );
1203}
1204
1208
1209
1210ABC_NAMESPACE_IMPL_END
1211
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Sdb_StoComputeCutsDetect
Vec_Int_t * Sdb_StoComputeCutsDetect(Gia_Man_t *pGia)
Definition acec2Mult.c:1168
SDB_CUT_NO_LEAF
#define SDB_CUT_NO_LEAF
Definition acec2Mult.c:279
Sdb_ForEachCut
#define Sdb_ForEachCut(pList, pCut, i)
Definition acec2Mult.c:317
SDB_MAX_TT_WORDS
#define SDB_MAX_TT_WORDS
Definition acec2Mult.c:277
Sdb_StoRefObj
void Sdb_StoRefObj(Sdb_Sto_t *p, int iObj)
Definition acec2Mult.c:1155
Sdb_StoIterCutsOne
int Sdb_StoIterCutsOne(Sdb_Sto_t *p, int iObj, int CutSize, int **ppCut)
Definition acec2Mult.c:955
Sdb_Cut_t
struct Sdb_Cut_t_ Sdb_Cut_t
Definition acec2Mult.c:281
Sdb_StoFindAll
Vec_Int_t * Sdb_StoFindAll(Vec_Wec_t *vCuts)
Definition acec2Mult.c:856
SDB_MAX_CUTSIZE
#define SDB_MAX_CUTSIZE
DECLARATIONS ///.
Definition acec2Mult.c:275
Sdb_StoAlloc
Sdb_Sto_t * Sdb_StoAlloc(Gia_Man_t *pGia, int nCutSize, int nCutNum, int fCutMin, int fTruthMin, int fVerbose)
Definition acec2Mult.c:1114
Sdb_StoComputeCutsCi
void Sdb_StoComputeCutsCi(Sdb_Sto_t *p, int iObj)
Definition acec2Mult.c:1147
Sdb_StoFindInputs
Vec_Int_t * Sdb_StoFindInputs(Vec_Wec_t *vCuts, int Front)
Definition acec2Mult.c:881
SDB_MAX_CUTNUM
#define SDB_MAX_CUTNUM
Definition acec2Mult.c:276
Sdb_StoDiffExactlyOne2
int Sdb_StoDiffExactlyOne2(Vec_Int_t *vAll, int *pCut)
Definition acec2Mult.c:865
Sdb_StoDiffExactlyOne3
int Sdb_StoDiffExactlyOne3(Vec_Wec_t *vCuts, int Limit, int *pCut, int *pCount)
Definition acec2Mult.c:827
Sdb_StoIterCuts
Vec_Int_t * Sdb_StoIterCuts(Sdb_Sto_t *p)
Definition acec2Mult.c:1044
Sdb_StoMergeCuts
void Sdb_StoMergeCuts(Sdb_Sto_t *p, int iObj)
Definition acec2Mult.c:726
Sdb_StoFree
void Sdb_StoFree(Sdb_Sto_t *p)
Definition acec2Mult.c:1133
Sdb_StoComputeCutsTest
void Sdb_StoComputeCutsTest(Gia_Man_t *pGia)
Definition acec2Mult.c:1199
Sdb_StoDiffExactlyOne
int Sdb_StoDiffExactlyOne(Vec_Wec_t *vCuts, int Limit, int *pCut)
Definition acec2Mult.c:795
Sdb_Sto_t
struct Sdb_Sto_t_ Sdb_Sto_t
Definition acec2Mult.c:293
Sdb_StoComputeCutsConst0
void Sdb_StoComputeCutsConst0(Sdb_Sto_t *p, int iObj)
Definition acec2Mult.c:1143
Sdb_StoComputeCutsNode
void Sdb_StoComputeCutsNode(Sdb_Sto_t *p, int iObj)
Definition acec2Mult.c:1151
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Sdb_Cut_t_
Definition acec2Mult.c:283
Sdb_Cut_t_::Sign
word Sign
Definition acec2Mult.c:284
Sdb_Cut_t_::pLeaves
int pLeaves[SDB_MAX_CUTSIZE]
Definition acec2Mult.c:290
Sdb_Cut_t_::nLeaves
unsigned nLeaves
Definition acec2Mult.c:289
Sdb_Cut_t_::Cost
int Cost
Definition acec2Mult.c:286
Sdb_Cut_t_::nTreeLeaves
unsigned nTreeLeaves
Definition acec2Mult.c:288
Sdb_Cut_t_::iFunc
int iFunc
Definition acec2Mult.c:285
Sdb_Cut_t_::CostLev
int CostLev
Definition acec2Mult.c:287
Sdb_Sto_t_
Definition acec2Mult.c:295
Sdb_Sto_t_::iCutBest
int iCutBest
Definition acec2Mult.c:309
Sdb_Sto_t_::nCutsR
int nCutsR
Definition acec2Mult.c:307
Sdb_Sto_t_::nCutsOver
int nCutsOver
Definition acec2Mult.c:310
Sdb_Sto_t_::fTruthMin
int fTruthMin
Definition acec2Mult.c:299
Sdb_Sto_t_::clkStart
abctime clkStart
Definition acec2Mult.c:312
Sdb_Sto_t_::vTtMem
Vec_Mem_t * vTtMem
Definition acec2Mult.c:304
Sdb_Sto_t_::vCuts
Vec_Wec_t * vCuts
Definition acec2Mult.c:303
Sdb_Sto_t_::CutCount
double CutCount[4]
Definition acec2Mult.c:311
Sdb_Sto_t_::fVerbose
int fVerbose
Definition acec2Mult.c:300
Sdb_Sto_t_::fCutMin
int fCutMin
Definition acec2Mult.c:298
Sdb_Sto_t_::pCuts
Sdb_Cut_t pCuts[3][SDB_MAX_CUTNUM]
Definition acec2Mult.c:305
Sdb_Sto_t_::vRefs
Vec_Int_t * vRefs
Definition acec2Mult.c:302
Sdb_Sto_t_::nCutNum
int nCutNum
Definition acec2Mult.c:297
Sdb_Sto_t_::ppCuts
Sdb_Cut_t * ppCuts[SDB_MAX_CUTNUM]
Definition acec2Mult.c:306
Sdb_Sto_t_::nCutSize
int nCutSize
Definition acec2Mult.c:296
Sdb_Sto_t_::pGia
Gia_Man_t * pGia
Definition acec2Mult.c:301
Sdb_Sto_t_::Pivot
int Pivot
Definition acec2Mult.c:308
Vec_Mem_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42