1 /**CFile****************************************************************
2
3 FileName [aigIso.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [AIG package.]
8
9 Synopsis [Graph isomorphism package.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - April 28, 2007.]
16
17 Revision [$Id: aigIso.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "saig.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25 /*
26 #define ISO_MASK 0x3FF
27 static int s_1kPrimes[ISO_MASK+1] =
28 {
29 901403,984877,908741,966307,924437,965639,918787,931067,982621,917669,981473,936407,990487,926077,922897,970861,
30 942317,961747,979717,978947,940157,987821,981221,917713,983083,992231,928253,961187,991817,927643,923129,934291,
31 998071,967567,961087,988661,910031,930481,904489,974167,941351,959911,963811,921463,900161,934489,905629,930653,
32 901819,909457,939871,924083,915113,937969,928457,946291,973787,912869,994093,959279,905803,995219,949903,911011,
33 986707,995053,930583,955511,928307,930889,968729,911507,949043,939359,961679,918041,937681,909091,963913,923539,
34 929587,953347,917573,913037,995387,976483,986239,946949,922489,917887,957553,931529,929813,949567,941683,905161,
35 928819,932417,900089,935903,926587,914467,967361,944833,945881,941741,915949,903407,904157,971863,993893,963607,
36 918943,912463,980957,962963,968089,904513,963763,907363,904097,904093,991343,918347,986983,986659,935819,903569,
37 929171,913933,999749,923123,961531,935861,915053,994853,943511,969923,927191,968333,949391,950959,968311,991409,
38 911681,987101,904027,975259,907399,946223,907259,900409,957221,901063,974657,912337,979001,970147,982301,968213,
39 923959,964219,935443,950161,989251,936127,985679,958159,930077,971899,944857,956083,914293,941981,909481,909047,
40 960527,958183,970687,914827,949051,928159,933551,964423,914041,915869,929953,901367,914219,975551,912391,917809,
41 991499,904781,949153,959887,961957,970943,947741,941263,984541,951437,984301,947423,905761,964913,971357,927709,
42 916441,941933,956993,988243,921197,905453,922081,950813,946331,998561,929023,937421,956231,907651,977897,905491,
43 960173,931837,955217,911951,990643,971021,949439,988453,996781,951497,906011,944309,911293,917123,983803,928097,
44 977747,928703,949957,919189,925513,923953,904997,986351,930689,902009,912007,906757,955793,926803,906809,962743,
45 911917,909329,949021,974651,959083,945367,905137,948377,931757,945409,920279,915007,960121,920609,946163,946391,
46 928903,932951,944329,901529,959809,918469,978643,911159,982573,965411,962233,911269,953273,974437,907589,992269,
47 929399,980431,905693,968267,970481,911089,950557,913799,920407,974489,909863,918529,975277,929323,971549,969181,
48 972787,964267,939971,943763,940483,971501,921637,945341,955211,920701,978349,969041,929861,904103,908539,995369,
49 995567,917471,908879,993821,947783,954599,978463,914519,942869,947263,988343,914657,956987,903641,943343,991063,
50 985403,926327,982829,958439,942017,960353,944987,934793,948971,999331,990767,915199,912211,946459,997019,965059,
51 924907,983233,943273,945359,919613,933883,928927,942763,994087,996211,918971,924871,938491,957139,918839,914629,
52 974329,900577,952823,941641,900461,946997,983123,935149,923693,908419,995651,912871,987067,920201,913921,929209,
53 962509,974599,972001,920273,922099,951781,958549,909971,975133,937207,929941,961397,980677,923579,980081,942199,
54 940319,942979,912349,942691,986989,947711,972343,932663,937877,940369,919571,927187,981439,932353,952313,915947,
55 915851,974041,989381,921029,997013,999199,914801,918751,997327,992843,982133,932051,964861,903979,937463,916781,
56 944389,986719,958369,961451,917767,954367,949853,934939,958807,975797,949699,957097,980773,969989,934907,909281,
57 904679,909833,991741,946769,908381,932447,957889,981697,905701,919033,999023,993541,912953,911719,934603,925019,
58 989341,912269,917789,981049,959149,989909,960521,952183,922627,936253,910957,972047,945037,940399,928313,928471,
59 962459,959947,927541,917333,926899,911837,985631,955127,922729,911171,900511,926251,918209,943477,955277,959773,
60 971039,917353,955313,930301,990799,957731,917519,938507,988111,911657,999721,968917,934537,903073,921703,966227,
61 904661,998213,954307,931309,909331,933643,910099,958627,914533,902903,950149,972721,915157,969037,988219,944137,
62 976411,952873,964787,970927,968963,920741,975187,966817,982909,975281,931907,959267,980711,924617,975691,962309,
63 976307,932209,989921,907969,947927,932207,945397,948929,904903,938563,961691,977671,963173,927149,951061,966547,
64 937661,983597,948139,948041,982759,941093,993703,910097,902347,990307,978217,996763,904919,924641,902299,929549,
65 977323,975071,932917,996293,925579,925843,915487,917443,999541,943043,919109,959879,912173,986339,939193,939599,
66 927077,977183,966521,959471,991943,985951,942187,932557,904297,972337,931751,964097,942341,966221,929113,960131,
67 906427,970133,996511,925637,971651,983443,981703,933613,939749,929029,958043,961511,957241,901079,950479,975493,
68 985799,909401,945601,911077,978359,948151,950333,968879,978727,961151,957823,950393,960293,915683,971513,915659,
69 943841,902477,916837,911161,958487,963691,949607,935707,987607,901613,972557,938947,931949,919021,982217,914737,
70 913753,971279,981683,915631,907807,970421,983173,916099,984587,912049,981391,947747,966233,932101,991733,969757,
71 904283,996601,979807,974419,964693,931537,917251,967961,910093,989321,988129,997307,963427,999221,962447,991171,
72 993137,914339,964973,908617,968567,920497,980719,949649,912239,907367,995623,906779,914327,918131,983113,962993,
73 977849,914941,932681,905713,932579,923977,965507,916469,984119,931981,998423,984407,993841,901273,910799,939847,
74 997153,971429,994927,912631,931657,968377,927833,920149,978041,947449,993233,927743,939737,975017,961861,984539,
75 938857,977437,950921,963659,923917,932983,922331,982393,983579,935537,914357,973051,904531,962077,990281,989231,
76 910643,948281,961141,911839,947413,923653,982801,903883,931943,930617,928679,962119,969977,926921,999773,954181,
77 963019,973411,918139,959719,918823,941471,931883,925273,918173,949453,946993,945457,959561,968857,935603,978283,
78 978269,947389,931267,902599,961189,947621,920039,964049,947603,913259,997811,943843,978277,972119,929431,918257,
79 991663,954043,910883,948797,929197,985057,990023,960961,967139,923227,923371,963499,961601,971591,976501,989959,
80 908731,951331,989887,925307,909299,949159,913447,969797,959449,976957,906617,901213,922667,953731,960199,960049,
81 985447,942061,955613,965443,947417,988271,945887,976369,919823,971353,962537,929963,920473,974177,903649,955777,
82 963877,973537,929627,994013,940801,985709,995341,936319,904681,945817,996617,953191,952859,934889,949513,965407,
83 988357,946801,970391,953521,905413,976187,968419,940669,908591,976439,915731,945473,948517,939181,935183,978067,
84 907663,967511,968111,981599,913907,933761,994933,980557,952073,906557,935621,914351,967903,949129,957917,971821,
85 925937,926179,955729,966871,960737,968521,949997,956999,961273,962683,990377,908851,932231,929749,932149,966971,
86 922079,978149,938453,958313,995381,906259,969503,922321,918947,972443,916411,935021,944429,928643,952199,918157,
87 917783,998497,944777,917771,936731,999953,975157,908471,989557,914189,933787,933157,938953,922931,986569,964363,
88 906473,963419,941467,946079,973561,957431,952429,965267,978473,924109,979529,991901,988583,918259,961991,978037,
89 938033,949967,986071,986333,974143,986131,963163,940553,950933,936587,923407,950357,926741,959099,914891,976231,
90 949387,949441,943213,915353,983153,975739,934243,969359,926557,969863,961097,934463,957547,916501,904901,928231,
91 903673,974359,932219,916933,996019,934399,955813,938089,907693,918223,969421,940903,940703,913027,959323,940993,
92 937823,906691,930841,923701,933259,911959,915601,960251,985399,914359,930827,950251,975379,903037,905783,971237
93 };
94 */
95
96 /*
97 #define ISO_MASK 0x7F
98 static int s_1kPrimes[ISO_MASK+1] = {
99 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
100 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
101 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
102 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
103 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
104 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
105 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
106 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
107 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
108 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
109 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
110 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
111 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
112 };
113 */
114
115 /*
116 #define ISO_MASK 0x7
117 static int s_1kPrimes[ISO_MASK+1] = {
118 12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741
119 };
120 */
121
122 #define ISO_MASK 0x3FF
123 static unsigned int s_1kPrimes[ISO_MASK+1] =
124 //#define ISO_MASK 0xFF
125 //static int s_1kPrimes[0x3FF+1] =
126 {
127 0x38c19891,0xde37b0ed,0xdebcd025,0xe19b7bbe,0x7e7ebd0e,0xaeed03a1,0x811230dc,0x10bfece0,
128 0xb3b23fb1,0x74176098,0xc34ec7c5,0x6bef8939,0xc40be5e3,0x2ab51a09,0xafc17cea,0x0dccc7a2,
129 0xdf7db34d,0x1009c96f,0x93fd7494,0x54385b33,0x6f36eed8,0xa1953f82,0xfbd1144a,0xde533a46,
130 0x23aa1cad,0x9a18943c,0xb65000d8,0x867e9974,0xe7880035,0xf9931ad4,0xcfca1e45,0x6b5aec96,
131 0xe9c1a119,0xfa4968c5,0x94cf93da,0xe8c9eac4,0x95884242,0x1bba52c7,0x9232c321,0x9cec8658,
132 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
133 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
134 0x50d66b74,0x2f01ae9e,0xa1a80123,0x3e1ce2dc,0xebedbc57,0x4e68bc34,0x855ee0cf,0x17275120,
135 0x2ae7f2df,0xf71039eb,0x7c283eec,0x70cd1137,0x7cf651f3,0xa87bfa7a,0x14d87f02,0xe82e197d,
136 0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
137 0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10,
138 0x8fa783f7,0x252062ce,0x3dc46b4b,0xf70f6432,0x3f378276,0x44b137a1,0x2bf74b77,0x04892ed6,
139 0xfd318de1,0xd58c235e,0x94c6d25b,0x7aa5f218,0x35c9e921,0x5732fbbb,0x06026481,0xf584a44f,
140 0x946e1b5f,0x8463d5b2,0x4ebca7b2,0x54887b15,0x08d1e804,0x5b22067d,0x794580f6,0xb351ea43,
141 0xbce555b9,0x19ae2194,0xd32f1396,0x6fc1a7f1,0x1fd8a867,0x3a89fdb0,0xea49c61c,0x25f8a879,
142 0xde1e6437,0x7c74afca,0x8ba63e50,0xb1572074,0xe4655092,0xdb6f8b1c,0xc2955f3c,0x327f85ba,
143 0x60a17021,0x95bd261d,0xdea94f28,0x04528b65,0xbe0109cc,0x26dd5688,0x6ab2729d,0xc4f029ce,
144 0xacf7a0be,0x4c912f55,0x34c06e65,0x4fbb938e,0x1533fb5f,0x03da06bd,0x48262889,0xc2523d7d,
145 0x28a71d57,0x89f9713a,0xf574c551,0x7a99deb5,0x52834d91,0x5a6f4484,0xc67ba946,0x13ae698f,
146 0x3e390f34,0x34fc9593,0x894c7932,0x6cf414a3,0xdb7928ab,0x13a3b8a3,0x4b381c1d,0xa10b54cb,
147 0x55359d9d,0x35a3422a,0x58d1b551,0x0fd4de20,0x199eb3f4,0x167e09e2,0x3ee6a956,0x5371a7fa,
148 0xd424efda,0x74f521c5,0xcb899ff6,0x4a42e4f4,0x747917b6,0x4b08df0b,0x090c7a39,0x11e909e4,
149 0x258e2e32,0xd9fad92d,0x48fe5f69,0x0545cde6,0x55937b37,0x9b4ae4e4,0x1332b40e,0xc3792351,
150 0xaff982ef,0x4dba132a,0x38b81ef1,0x28e641bf,0x227208c1,0xec4bbe37,0xc4e1821c,0x512c9d09,
151 0xdaef1257,0xb63e7784,0x043e04d7,0x9c2cea47,0x45a0e59a,0x281315ca,0x849f0aac,0xa4071ed3,
152 0x0ef707b3,0xfe8dac02,0x12173864,0x471f6d46,0x24a53c0a,0x35ab9265,0xbbf77406,0xa2144e79,
153 0xb39a884a,0x0baf5b6d,0xcccee3dd,0x12c77584,0x2907325b,0xfd1adcd2,0xd16ee972,0x345ad6c1,
154 0x315ebe66,0xc7ad2b8d,0x99e82c8d,0xe52da8c8,0xba50f1d3,0x66689cd8,0x2e8e9138,0x43e15e74,
155 0xf1ced14d,0x188ec52a,0xe0ef3cbb,0xa958aedc,0x4107a1bc,0x5a9e7a3e,0x3bde939f,0xb5b28d5a,
156 0x596fe848,0xe85ad00c,0x0b6b3aae,0x44503086,0x25b5695c,0xc0c31dcd,0x5ee617f0,0x74d40c3a,
157 0xd2cb2b9f,0x1e19f5fa,0x81e24faf,0xa01ed68f,0xcee172fc,0x7fdf2e4d,0x002f4774,0x664f82dd,
158 0xc569c39a,0xa2d4dcbe,0xaadea306,0xa4c947bf,0xa413e4e3,0x81fb5486,0x8a404970,0x752c980c,
159 0x98d1d881,0x5c932c1e,0xeee65dfb,0x37592cdd,0x0fd4e65b,0xad1d383f,0x62a1452f,0x8872f68d,
160 0xb58c919b,0x345c8ee3,0xb583a6d6,0x43d72cb3,0x77aaa0aa,0xeb508242,0xf2db64f8,0x86294328,
161 0x82211731,0x1239a9d5,0x673ba5de,0xaf4af007,0x44203b19,0x2399d955,0xa175cd12,0x595928a7,
162 0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0,
163 0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d,
164 0x214d04ab,0xe093e487,0x10607ada,0x42b261cc,0x1a85e0f6,0xb851bfc3,0x77d5591c,0xda13f344,
165 0xc39c4c00,0xe60d75fc,0x7edae36a,0x3e4ac3ec,0x8bc38db4,0xe848dce9,0xb2407d4d,0x0d79c61e,
166 0x1e6c293a,0x7bc30986,0xdf18cb8f,0x23003172,0x6948e3fa,0x9b7e4f09,0x14b3b339,0x9c8078c2,
167 0x9a47c29f,0x85bb45ec,0x9ca35a93,0xd7db5227,0x1d9b0a10,0xb7fbbfe9,0x05b72426,0x6f30b2fa,
168 0x9fb44078,0xedffd3f8,0x1b02b7bc,0x43e3cfd3,0x0d44293e,0x25c8d552,0xedd3f85d,0x6f921c8c,
169 0x953cca0c,0x9c975b70,0xc6bd0b53,0x4f204f3e,0xa3cc69cc,0xceec390b,0x34905626,0x82ad5d41,
170 0xe46589a5,0x7989841d,0x045d7d9f,0xe49b7b2f,0x46baf101,0x996f92de,0x427566c8,0x918a1ee1,
171 0xf4baa589,0x6bdff7c7,0x3c6936ea,0xe85bfb70,0x5d96ea26,0x6d5a8991,0x7f0a528d,0x852f0634,
172 0x2ec04501,0x5ca15c35,0xd8695e7a,0x456876c7,0x52e97b83,0x34b4c5ed,0x54d73fbb,0x44a6be01,
173 0xf8019155,0x33d55a31,0x3fe51c99,0xe1cb94fd,0x8c39cd60,0xd585efba,0x2765579b,0xb8f7ed12,
174 0xbb04b2cd,0xd8859981,0xd966988d,0xa68bfeda,0x73110705,0x38d6aec0,0x613bc275,0xc7283c2d,
175 0xe051d0b1,0x32b8c2ee,0x0e73fb9e,0x7ab05c25,0x6ff652b9,0x45aeabc6,0x6be1a891,0x5b43531b,
176 0xcd711248,0x2b777d40,0x46956d16,0x474355a8,0xe872d6c6,0xe4158d96,0xabe03036,0x5b4fd9a4,
177 0xeceba1db,0xaac9713f,0xe953153b,0xf44a9229,0x460cba72,0xfd13fdf6,0x8bbf82ae,0xaf55778f,
178 0xa447a5b2,0x98b647b3,0x5f351c57,0x69d0bb71,0xf14d2706,0x78b1a3af,0x7206c73f,0x3f5cd4a6,
179 0x5c0e4515,0xdb46a663,0x10c3a9b0,0x8eda7748,0x52bb44c9,0x3df62689,0xc83e2732,0xf36c99af,
180 0x7ec7a94c,0x5c823718,0x6586e58e,0x4b726e75,0xcfe03a05,0x34eb2f4b,0xf4eec9cf,0xb38d6d73,
181 0x71fafa9e,0x0371a29a,0xc405f83b,0x889f49c2,0xd1443000,0x469665bf,0x609ed65d,0x67c8f9ba,
182 0x9d2f6055,0xb91b8eb1,0x96c809fe,0x2d6ab0f5,0xc16d4f04,0x590171ab,0x73d67526,0xf724e44c,
183 0x6aef02b7,0x6489a325,0x4458401e,0x22d94ad7,0x05e5be57,0x5634fad8,0x951fcf70,0x4baad7f0,
184 0x40c1090d,0xedc28abd,0x343cc6e4,0x4ff7c030,0x0734a641,0x2635a90e,0x2e000c84,0x4b617a70,
185 0x872e9c9e,0x3dceeb42,0xd0fcc398,0x9cc9b9c8,0x2de02f0c,0xaf0e2614,0xa60253aa,0xe0517492,
186 0xa7bde4b4,0x3bb66d7d,0x7f215e82,0xf259de66,0xe17380fe,0xdbc718b4,0x66abcc29,0xf0826e1f,
187 0x08f60995,0xce81b933,0xa832c0e9,0x37aed7d4,0x8a75c261,0x916627b4,0xd486a04b,0x64fd0fde,
188 0x1261328a,0xe037772f,0xb5b71117,0x55d04bd8,0x8f6c1c7b,0xb9f5fcdd,0x5918f756,0x25c90099,
189 0x2e8787db,0x58e14e38,0x0d397852,0x32c8e33b,0x5ae2b795,0x3a7b3ff7,0x5eebf893,0x1aeee816,
190 0xc2ef31d0,0x1d86e615,0x183f1de3,0xb89d46c4,0x525ebbf6,0xfe0198ca,0x4986cc4a,0x2a75701e,
191 0x382158b1,0x192ee88f,0x3e512912,0xcd571c3d,0xdf694fe8,0xec8ead1d,0x83719ac3,0x3f654079,
192 0xf6a623c5,0x33e1fc6e,0xe7f7c426,0x5bff0f6c,0x698a9bb1,0xec2a29ba,0x75358b45,0x40c6ffef,
193 0x6605bb55,0x53a8c97a,0x7bba1569,0x499bc51b,0x5849c89a,0xe6ddb267,0x8659c719,0x14a05548,
194 0xeec648a9,0x618af87a,0x62214521,0x7f36e610,0x152efeeb,0xc2b0f0ed,0x1d657588,0xa5fcec4b,
195 0xf872f109,0x46903038,0x04b57b97,0xe5d51b14,0x06c264ec,0x68aa8d14,0xa4e1bed8,0xdae169c2,
196 0xeb90debd,0xe8c11a7a,0xcafce013,0x63820cee,0x948c23e5,0xc1d42ea3,0x8256c951,0x9b587773,
197 0x2fa8380c,0x30255e09,0x1a809cdc,0xe1446068,0x2714621d,0xb3347d64,0x1f4cbf3d,0xd068bc26,
198 0x2c422740,0x06c4a3ad,0x5dc9d63c,0x4724bf48,0x28e34add,0x27d5221d,0xe349c7e2,0x6119e0a5,
199 0x4ae7d29f,0x53a7912d,0xfc5db779,0x7d28d357,0xfd80036d,0x06bcc597,0x36d70a8a,0x37738cb7,
200 0xf11e6272,0xfdd5d153,0x5dc666dc,0x6b5a415d,0x1073b415,0x36f30d9a,0x807daf7b,0x387f6823,
201 0x8970fe00,0xee560be5,0xea8c0bad,0xfac2b422,0xc845861d,0xa181a2ee,0x29c4dffd,0x4d441bb2,
202 0x7a64cf93,0x0c33e6ac,0x0a35d034,0x1067d26d,0x8c7da0cc,0x2d6e2d5a,0x9932c25a,0x5fca4e2c,
203 0x2c82fd71,0x41730b70,0x244bdbb9,0x96514307,0xc6a32a6b,0xc4c256a7,0x38517fd8,0x541aa859,
204 0x0752afe3,0x741e22f9,0xa2565483,0x7588b0b9,0xdd404e42,0x4d86c49d,0x6fa93fc1,0x163bd200,
205 0x745d0d31,0x8d3dd20e,0xebdc64db,0x9315c149,0x39db3299,0xb0c22004,0xa4c0295b,0x8b3573eb,
206 0xd92a40a3,0x73d6c379,0x67673309,0xdaff1d7f,0x42fcfeb8,0xd57c11a4,0x402066ef,0x9d1134e0,
207 0x9f417081,0x10f49e00,0x7e7ee855,0x314e6d25,0x602bdbe6,0xa4be4045,0xac511dc4,0x33d6bda8,
208 0x2f2bc412,0x4b9c0b6c,0x98aaab06,0x7f0a5801,0xfbf1f16d,0x058f54ae,0x4fd97724,0x348cb50b,
209 0xef6f659f,0x0cd8b184,0x1d71a666,0xae3c87dd,0x7bd56793,0xe0f8f6a8,0x90429c55,0x8a3cc4d0,
210 0x49957b70,0x3baf3912,0x755efebb,0xa5eca17f,0x486065a1,0x1dffcefb,0xd914b3a0,0x1ced93c1,
211 0xa4262dcd,0xc12a4adc,0x08f6de4e,0x4c204faf,0xca1815de,0xa4af836f,0x91d5e44d,0xd2a7caa4,
212 0x68a9a3fe,0x844f8dac,0x3fc36c67,0x8be23937,0x69879d94,0x5d0dbecb,0x1f0f59a4,0x94721142,
213 0xfca6064a,0x6d28aa48,0x804cd04e,0x4a3906de,0x8e352509,0x302326d9,0xed4937ed,0x4a570e63,
214 0xcaa57efb,0x64bd4878,0x3419334a,0x712e5f6b,0x9fa9d687,0x06f8645f,0x620ca96f,0xdc5d6cce,
215 0x392f3257,0x52140f06,0xc4b3bda4,0xe8c7eba7,0x066bd754,0xc5941f26,0xe6dfd573,0x328dd14d,
216 0xb1cb4ba7,0x1d37a9b8,0x96a195a5,0x970e535a,0x290351b8,0x570000f6,0xe14ae341,0x35ede6a6,
217 0x9a02f032,0xaf2ebb58,0x146be492,0x670b3e4b,0x72fa6cfd,0xa243af97,0xbbd5fc21,0xcb8852a2,
218 0x5d5b4a42,0xeefff0ac,0xa59ad1b6,0x3ec55544,0x48d64f69,0x9065d3d0,0xdd09485b,0xdd63bd09,
219 0x605e811d,0xc4b4ed7d,0xb0b58558,0x0644400b,0x12222346,0x086f146a,0xad6dee36,0x5488d1a3,
220 0x0c93bc0c,0x18555d92,0x9f4427bf,0xa590a66a,0x3a630fda,0xf1681c2e,0x948a16fb,0x16fe3338,
221 0xc9832357,0xd1e8e6b5,0xd9cfe034,0x05b22f26,0x27233c6e,0x355890e1,0xfbe6eaf3,0x0dcd8e8f,
222 0x00b5df46,0xd97730ac,0xc6dfd8ff,0x0cb1840a,0x41e9d249,0xbb471b4e,0x480b8f63,0x1ffe8871,
223 0x17b11821,0x1709e440,0xcefb3668,0xa4954ddd,0xf03ef8b5,0x6b3e633c,0xe5813096,0x3697c9a6,
224 0x7800f52f,0x73a7aa39,0x59ac23b7,0xb4663166,0x9ca9d6f8,0x2d441072,0x38cef3d3,0x39a3faf6,
225 0x89299fb9,0xd558295f,0xcf79c633,0x232dd96e,0xadb2955b,0xe962cbb9,0xab7c0061,0x1027c329,
226 0xb4b43e07,0x25240a7a,0x98ea4825,0xdbf2edbd,0x8be15d26,0x879f3cd9,0xa4138089,0xa32dcb06,
227 0x602af961,0x4b13f451,0x1c87d0d5,0xc3bb141b,0x9ebf55a1,0xef030a9a,0x8d199b93,0xdabcbb56,
228 0xf412f80f,0x302e90ad,0xc4d9878b,0xc392f650,0x4fd3a614,0x0a96ddc4,0xcd1878c7,0x9ddd3ae1,
229 0xdaf46458,0xba7c8656,0xf667948f,0xc37e3c23,0x04a577c6,0xbe615f1e,0xcc97406c,0xd497f16f,
230 0x79586586,0xd2057d14,0x1bb92028,0xab888e5e,0x26bef100,0xf46b3671,0xf21f1acc,0x67f288c8,
231 0x39c722df,0x61d21eaf,0x9c5853a0,0x63b693c7,0x1ea53c0a,0x95bc0a85,0xa7372f2d,0x3ef6a6b3,
232 0x82c9c4ac,0x4dea10ee,0xdfcb543d,0xd412f427,0x53e27f2c,0x875d8422,0x5367a7d8,0x41acf3fa,
233 0xbce47234,0x8056fb9a,0x4e9a4c48,0xe4a45945,0x2cfee3ae,0xb4554b10,0x5e37a915,0x591b1963,
234 0x4fa255c1,0xe01c897b,0x504e6208,0x7c7368eb,0x13808fd7,0x02ac0816,0x30305d2c,0x6c4bbdb7,
235 0xa48a9599,0x57466059,0x4c6ebfc7,0x8587ccdf,0x6ff0abf0,0x5b6b63fe,0x31d9ec64,0x63458abd,
236 0x21245905,0xccdb28fc,0xac828acb,0xe5e82bea,0xa7d76141,0xa699038e,0xcaba7e06,0x2710253f,
237 0x2ff9c94d,0x26e48a2c,0xd713ec5e,0x869f2ed4,0x25bcd712,0xcb3e918f,0x615c3a5a,0x9fb43903,
238 0x37900eb9,0x4f682db0,0x35a80dc6,0x4eb27c65,0x502735ab,0xb163b4c8,0x604649a8,0xb23a6cd3,
239 0x9f715091,0x2e6fbb51,0x2ec9144b,0x272cbe65,0x90a0a453,0x420e1503,0x2d00d338,0x4aa96675,
240 0xd025b61c,0xab02d9d7,0x2afe2a37,0xf8129b9b,0x4db04c54,0x654a5c06,0x3213ff51,0x4e09d0b1,
241 0x333369a3,0xae27310a,0x91d076d0,0xa96ebcd0,0xefde54f4,0x021c309a,0xd506f53d,0xa5635251,
242 0x2f23916e,0x1fe86bb1,0xcbc62160,0x2147c8cc,0xdeb3e47c,0x028e3987,0x8061de42,0x39be931b,
243 0x2b7e54c5,0xe64d2f96,0x4069522d,0x4aa66857,0x83b62634,0x4ba72095,0x9aade2a9,0xf1223cd9,
244 0x91cbddf0,0xec5d237f,0x593f3280,0x0b924439,0x446f4063,0xc66f8d8c,0x8b7128ba,0xb597f451,
245 0xc8925236,0x1720f235,0x7cd2e9a0,0x4c130339,0x8a665a52,0x5bef2733,0xba35d9bc,0x6d26644c,
246 0x385cdce1,0x509e4280,0x12aa9ed7,0xf5314d21,0xbe249d4a,0xf32e9753,0x91821cf9,0x01d63491,
247 0x49afa237,0x80e0bc27,0x844d796b,0xeff5ccb7,0x46303091,0x743484b4,0x77de1ab7,0x5ab00bea,
248 0x6316cd81,0x8ded07f4,0x3845a3a5,0x206625c4,0x8c123c6f,0xc80a971e,0xd4d4fa3f,0x5eba911d,
249 0xee168406,0x61cdcbad,0x981a44cd,0x718d030f,0xf653e92e,0xd5b77859,0x11e9e5d9,0xf6fe6ff3,
250 0x5239f010,0xe289b21b,0x0b52832b,0xca700c62,0xee7a5e15,0x8543ce2c,0x94a703cc,0x0b844d34,
251 0xf70638e5,0xfa286206,0xf8778906,0x1419e883,0xdb0fc46b,0xbeb74261,0xc6957b62,0x8352d2a8,
252 0x460586ce,0x90b28336,0xc9107ea8,0x3590403b,0x259a4279,0x6a1a7bbe,0x0f3b76e1,0x4872a716,
253 0xa5bfff13,0x8b30be72,0xe5a68957,0x17dbbc52,0x33a40187,0x7074220c,0xd8221b92,0x40ec7448,
254 0x7dbbcdfc,0xd5a9bb83,0xb4c0d25c,0xa0040390,0x6fb429dc,0xb8cede12,0x87d193bd,0x55c6e004
255 };
256
257 ////////////////////////////////////////////////////////////////////////
258 /// DECLARATIONS ///
259 ////////////////////////////////////////////////////////////////////////
260
261 #define ISO_NUM_INTS 3
262
263 typedef struct Iso_Obj_t_ Iso_Obj_t;
264 struct Iso_Obj_t_
265 {
266 // hashing entries (related to the parameter ISO_NUM_INTS!)
267 unsigned Level : 30;
268 unsigned nFinNeg : 2;
269 unsigned FaninSig;
270 unsigned FanoutSig;
271 // other data
272 int iNext; // hash table entry
273 int iClass; // next one in class
274 int Id; // unique ID
275 };
276
277 typedef struct Iso_Man_t_ Iso_Man_t;
278 struct Iso_Man_t_
279 {
280 Aig_Man_t * pAig; // user's AIG manager
281 Iso_Obj_t * pObjs; // isomorphism objects
282 int nObjIds; // counter of object IDs
283 int nClasses; // total number of classes
284 int nEntries; // total number of entries
285 int nSingles; // total number of singletons
286 int nObjs; // total objects
287 int nBins; // hash table size
288 int * pBins; // hash table
289 Vec_Ptr_t * vSingles; // singletons
290 Vec_Ptr_t * vClasses; // other classes
291 Vec_Ptr_t * vTemp1; // other classes
292 Vec_Ptr_t * vTemp2; // other classes
293 abctime timeHash;
294 abctime timeFout;
295 abctime timeSort;
296 abctime timeOther;
297 abctime timeTotal;
298 };
299
Iso_ManObj(Iso_Man_t * p,int i)300 static inline Iso_Obj_t * Iso_ManObj( Iso_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
Iso_ObjId(Iso_Man_t * p,Iso_Obj_t * pObj)301 static inline int Iso_ObjId( Iso_Man_t * p, Iso_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
Iso_AigObj(Iso_Man_t * p,Iso_Obj_t * q)302 static inline Aig_Obj_t * Iso_AigObj( Iso_Man_t * p, Iso_Obj_t * q ) { return Aig_ManObj( p->pAig, Iso_ObjId(p, q) ); }
303
304 #define Iso_ManForEachObj( p, pObj, i ) \
305 for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else
306
307 ////////////////////////////////////////////////////////////////////////
308 /// FUNCTION DEFINITIONS ///
309 ////////////////////////////////////////////////////////////////////////
310
311 //extern void Iso_ReadPrimes( char * pFileName );
312 //Iso_ReadPrimes( "primes.txt" );
313
314 /**Function*************************************************************
315
316 Synopsis [Read primes from file.]
317
318 Description []
319
320 SideEffects []
321
322 SeeAlso []
323
324 ***********************************************************************/
Iso_ReadPrimes(char * pFileName)325 void Iso_ReadPrimes( char * pFileName )
326 {
327 FILE * pFile;
328 int Nums[10000];
329 int i, j, Temp, nSize = 0;
330 // read the numbers
331 pFile = fopen( pFileName, "rb" );
332 while ( fscanf( pFile, "%d", Nums + nSize++ ) == 1 );
333 fclose( pFile );
334 assert( nSize >= (1<<10) );
335 // randomly permute
336 srand( 111 );
337 for ( i = 0; i < nSize; i++ )
338 {
339 j = rand() % nSize;
340 Temp = Nums[i];
341 Nums[i] = Nums[j];
342 Nums[j] = Temp;
343 }
344 // write out
345 for ( i = 0; i < 64; i++ )
346 {
347 printf( " " );
348 for ( j = 0; j < 16; j++ )
349 printf( "%d,", Nums[i*16+j] );
350 printf( "\n" );
351 }
352 }
353
354 /**Function*************************************************************
355
356 Synopsis [Read primes from file.]
357
358 Description []
359
360 SideEffects []
361
362 SeeAlso []
363
364 ***********************************************************************/
Iso_FindNumbers()365 void Iso_FindNumbers()
366 {
367 unsigned Nums[1024];
368 unsigned char * pNums = (unsigned char *)Nums;
369 int i, j;
370 srand( 111 );
371 for ( i = 0; i < 1024 * 4; i++ )
372 pNums[i] = (unsigned char)rand();
373 // write out
374 for ( i = 0; i < 128; i++ )
375 {
376 printf( " " );
377 for ( j = 0; j < 8; j++ )
378 printf( "0x%08x,", Nums[i*8+j] );
379 printf( "\n" );
380 }
381 }
382
383 /**Function*************************************************************
384
385 Synopsis []
386
387 Description []
388
389 SideEffects []
390
391 SeeAlso []
392
393 ***********************************************************************/
Iso_ManObjCount_rec(Aig_Man_t * p,Aig_Obj_t * pObj,int * pnNodes,int * pnEdges)394 void Iso_ManObjCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
395 {
396 if ( Aig_ObjIsCi(pObj) )
397 return;
398 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
399 return;
400 Aig_ObjSetTravIdCurrent(p, pObj);
401 Iso_ManObjCount_rec( p, Aig_ObjFanin0(pObj), pnNodes, pnEdges );
402 Iso_ManObjCount_rec( p, Aig_ObjFanin1(pObj), pnNodes, pnEdges );
403 (*pnEdges) += Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
404 (*pnNodes)++;
405 }
Iso_ManObjCount(Aig_Man_t * p,Aig_Obj_t * pObj,int * pnNodes,int * pnEdges)406 void Iso_ManObjCount( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
407 {
408 assert( Aig_ObjIsNode(pObj) );
409 *pnNodes = *pnEdges = 0;
410 Aig_ManIncrementTravId( p );
411 Iso_ManObjCount_rec( p, pObj, pnNodes, pnEdges );
412 }
413
414 /**Function*************************************************************
415
416 Synopsis []
417
418 Description []
419
420 SideEffects []
421
422 SeeAlso []
423
424 ***********************************************************************/
Iso_ManStart(Aig_Man_t * pAig)425 Iso_Man_t * Iso_ManStart( Aig_Man_t * pAig )
426 {
427 Iso_Man_t * p;
428 p = ABC_CALLOC( Iso_Man_t, 1 );
429 p->pAig = pAig;
430 p->nObjs = Aig_ManObjNumMax( pAig );
431 p->pObjs = ABC_CALLOC( Iso_Obj_t, p->nObjs );
432 p->nBins = Abc_PrimeCudd( p->nObjs );
433 p->pBins = ABC_CALLOC( int, p->nBins );
434 p->vSingles = Vec_PtrAlloc( 1000 );
435 p->vClasses = Vec_PtrAlloc( 1000 );
436 p->vTemp1 = Vec_PtrAlloc( 1000 );
437 p->vTemp2 = Vec_PtrAlloc( 1000 );
438 p->nObjIds = 1;
439 return p;
440 }
Iso_ManStop(Iso_Man_t * p,int fVerbose)441 void Iso_ManStop( Iso_Man_t * p, int fVerbose )
442 {
443 if ( fVerbose )
444 {
445 p->timeOther = p->timeTotal - p->timeHash - p->timeFout;
446 ABC_PRTP( "Building ", p->timeFout, p->timeTotal );
447 ABC_PRTP( "Hashing ", p->timeHash-p->timeSort, p->timeTotal );
448 ABC_PRTP( "Sorting ", p->timeSort, p->timeTotal );
449 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
450 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
451 }
452 Vec_PtrFree( p->vTemp1 );
453 Vec_PtrFree( p->vTemp2 );
454 Vec_PtrFree( p->vClasses );
455 Vec_PtrFree( p->vSingles );
456 ABC_FREE( p->pBins );
457 ABC_FREE( p->pObjs );
458 ABC_FREE( p );
459 }
460
461
462 /**Function*************************************************************
463
464 Synopsis [Compares two objects by their signature.]
465
466 Description []
467
468 SideEffects []
469
470 SeeAlso []
471
472 ***********************************************************************/
Iso_ObjCompare(Iso_Obj_t ** pp1,Iso_Obj_t ** pp2)473 int Iso_ObjCompare( Iso_Obj_t ** pp1, Iso_Obj_t ** pp2 )
474 {
475 return -memcmp( *pp1, *pp2, sizeof(int) * ISO_NUM_INTS );
476 }
477
478 /**Function*************************************************************
479
480 Synopsis [Compares two objects by their ID.]
481
482 Description []
483
484 SideEffects []
485
486 SeeAlso []
487
488 ***********************************************************************/
Iso_ObjCompareByData(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)489 int Iso_ObjCompareByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
490 {
491 Aig_Obj_t * pIso1 = *pp1;
492 Aig_Obj_t * pIso2 = *pp2;
493 assert( Aig_ObjIsCi(pIso1) || Aig_ObjIsCo(pIso1) );
494 assert( Aig_ObjIsCi(pIso2) || Aig_ObjIsCo(pIso2) );
495 return pIso1->iData - pIso2->iData;
496 }
497
498 /**Function*************************************************************
499
500 Synopsis []
501
502 Description []
503
504 SideEffects []
505
506 SeeAlso []
507
508 ***********************************************************************/
Iso_ObjHash(Iso_Obj_t * pIso,int nBins)509 static inline int Iso_ObjHash( Iso_Obj_t * pIso, int nBins )
510 {
511 static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
512 unsigned * pArray = (unsigned *)pIso;
513 unsigned i, Value = 0;
514 assert( ISO_NUM_INTS < 8 );
515 for ( i = 0; i < ISO_NUM_INTS; i++ )
516 Value ^= BigPrimes[i] * pArray[i];
517 return Value % nBins;
518 }
Iso_ObjHashAdd(Iso_Man_t * p,Iso_Obj_t * pIso)519 static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso )
520 {
521 Iso_Obj_t * pThis;
522 int * pPlace = p->pBins + Iso_ObjHash( pIso, p->nBins );
523 p->nEntries++;
524 for ( pThis = Iso_ManObj(p, *pPlace);
525 pThis; pPlace = &pThis->iNext,
526 pThis = Iso_ManObj(p, *pPlace) )
527 if ( Iso_ObjCompare( &pThis, &pIso ) == 0 ) // equal signatures
528 {
529 if ( pThis->iClass == 0 )
530 {
531 p->nClasses++;
532 p->nSingles--;
533 }
534 // add to the list
535 pIso->iClass = pThis->iClass;
536 pThis->iClass = Iso_ObjId( p, pIso );
537 return 1;
538 }
539 // create new list
540 *pPlace = Iso_ObjId( p, pIso );
541 p->nSingles++;
542 return 0;
543 }
544
545 /**Function*************************************************************
546
547 Synopsis []
548
549 Description []
550
551 SideEffects []
552
553 SeeAlso []
554
555 ***********************************************************************/
Iso_ManCollectClasses(Iso_Man_t * p)556 void Iso_ManCollectClasses( Iso_Man_t * p )
557 {
558 Iso_Obj_t * pIso;
559 int i;
560 abctime clk = Abc_Clock();
561 Vec_PtrClear( p->vSingles );
562 Vec_PtrClear( p->vClasses );
563 for ( i = 0; i < p->nBins; i++ )
564 {
565 for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
566 {
567 assert( pIso->Id == 0 );
568 if ( pIso->iClass )
569 Vec_PtrPush( p->vClasses, pIso );
570 else
571 Vec_PtrPush( p->vSingles, pIso );
572 }
573 }
574 clk = Abc_Clock();
575 Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
576 Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
577 p->timeSort += Abc_Clock() - clk;
578 assert( Vec_PtrSize(p->vSingles) == p->nSingles );
579 assert( Vec_PtrSize(p->vClasses) == p->nClasses );
580 // assign IDs to singletons
581 Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
582 if ( pIso->Id == 0 )
583 pIso->Id = p->nObjIds++;
584 }
585
586 /**Function*************************************************************
587
588 Synopsis []
589
590 Description []
591
592 SideEffects []
593
594 SeeAlso []
595
596 ***********************************************************************/
Iso_ManCreate(Aig_Man_t * pAig)597 Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
598 {
599 int fUseXor = 0;
600 Iso_Man_t * p;
601 Iso_Obj_t * pIso, * pIsoF;
602 Aig_Obj_t * pObj, * pObjLi;
603 int i;
604 p = Iso_ManStart( pAig );
605
606 // create TFI signatures
607 Aig_ManForEachObj( pAig, pObj, i )
608 {
609 if ( Aig_ObjIsCo(pObj) )
610 continue;
611 pIso = p->pObjs + i;
612 pIso->Level = pObj->Level;
613 // pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
614
615 assert( pIso->FaninSig == 0 );
616 assert( pIso->FanoutSig == 0 );
617 if ( fUseXor )
618 {
619 if ( Aig_ObjIsNode(pObj) )
620 {
621 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
622 pIso->FaninSig ^= pIsoF->FaninSig;
623 pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
624
625 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
626 pIso->FaninSig ^= pIsoF->FaninSig;
627 pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
628 }
629 }
630 else
631 {
632 if ( Aig_ObjIsNode(pObj) )
633 {
634 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
635 pIso->FaninSig += pIsoF->FaninSig;
636 pIso->FaninSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
637
638 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
639 pIso->FaninSig += pIsoF->FaninSig;
640 pIso->FaninSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
641 }
642 }
643 }
644
645 // create TFO signatures
646 Aig_ManForEachObjReverse( pAig, pObj, i )
647 {
648 if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
649 continue;
650 pIso = p->pObjs + i;
651 if ( fUseXor )
652 {
653 if ( Aig_ObjIsNode(pObj) )
654 {
655 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
656 pIsoF->FanoutSig ^= pIso->FanoutSig;
657 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
658
659 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
660 pIsoF->FanoutSig ^= pIso->FanoutSig;
661 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
662 }
663 else if ( Aig_ObjIsCo(pObj) )
664 {
665 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
666 pIsoF->FanoutSig ^= pIso->FanoutSig;
667 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
668 }
669 }
670 else
671 {
672 if ( Aig_ObjIsNode(pObj) )
673 {
674 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
675 pIsoF->FanoutSig += pIso->FanoutSig;
676 pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
677
678 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
679 pIsoF->FanoutSig += pIso->FanoutSig;
680 pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
681 }
682 else if ( Aig_ObjIsCo(pObj) )
683 {
684 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
685 pIsoF->FanoutSig += pIso->FanoutSig;
686 pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
687 }
688 }
689 }
690
691 // consider flops
692 Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
693 {
694 if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
695 continue;
696 pIso = Iso_ManObj( p, Aig_ObjId(pObj) );
697 pIsoF = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );
698
699 assert( pIso->FaninSig == 0 );
700 pIso->FaninSig = pIsoF->FaninSig;
701
702 // assert( pIsoF->FanoutSig == 0 );
703 pIsoF->FanoutSig += pIso->FanoutSig;
704 }
705 /*
706 Aig_ManForEachObj( pAig, pObj, i )
707 {
708 pIso = p->pObjs + i;
709 Aig_ObjPrint( pAig, pObj );
710 printf( "Lev = %4d. Pos = %4d. FaninSig = %10d. FanoutSig = %10d.\n",
711 pIso->Level, pIso->nFinNeg, pIso->FaninSig, pIso->FanoutSig );
712 }
713 */
714 // add to the hash table
715 Aig_ManForEachObj( pAig, pObj, i )
716 {
717 if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
718 continue;
719 pIso = p->pObjs + i;
720 Iso_ObjHashAdd( p, pIso );
721 }
722 // derive classes for the first time
723 Iso_ManCollectClasses( p );
724 return p;
725 }
726
727 /**Function*************************************************************
728
729 Synopsis [Creates adjacency lists.]
730
731 Description []
732
733 SideEffects []
734
735 SeeAlso []
736
737 ***********************************************************************/
Iso_ManAssignAdjacency(Iso_Man_t * p)738 void Iso_ManAssignAdjacency( Iso_Man_t * p )
739 {
740 int fUseXor = 0;
741 Iso_Obj_t * pIso, * pIsoF;
742 Aig_Obj_t * pObj, * pObjLi;
743 int i;
744
745 // create TFI signatures
746 Aig_ManForEachObj( p->pAig, pObj, i )
747 {
748 pIso = p->pObjs + i;
749 pIso->FaninSig = 0;
750 pIso->FanoutSig = 0;
751
752 if ( Aig_ObjIsCo(pObj) )
753 continue;
754 if ( fUseXor )
755 {
756 if ( Aig_ObjIsNode(pObj) )
757 {
758 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
759 pIso->FaninSig ^= pIsoF->FaninSig;
760 if ( pIsoF->Id )
761 pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
762
763 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
764 pIso->FaninSig ^= pIsoF->FaninSig;
765 if ( pIsoF->Id )
766 pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
767 }
768 }
769 else
770 {
771 if ( Aig_ObjIsNode(pObj) )
772 {
773 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
774 pIso->FaninSig += pIsoF->FaninSig;
775 if ( pIsoF->Id )
776 pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
777
778 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
779 pIso->FaninSig += pIsoF->FaninSig;
780 if ( pIsoF->Id )
781 pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
782 }
783 }
784 }
785 // create TFO signatures
786 Aig_ManForEachObjReverse( p->pAig, pObj, i )
787 {
788 if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
789 continue;
790 pIso = p->pObjs + i;
791 assert( !Aig_ObjIsCo(pObj) || pIso->Id == 0 );
792 if ( fUseXor )
793 {
794 if ( Aig_ObjIsNode(pObj) )
795 {
796 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
797 pIsoF->FanoutSig ^= pIso->FanoutSig;
798 if ( pIso->Id )
799 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
800
801 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
802 pIsoF->FanoutSig ^= pIso->FanoutSig;
803 if ( pIso->Id )
804 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
805 }
806 else if ( Aig_ObjIsCo(pObj) )
807 {
808 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
809 pIsoF->FanoutSig ^= pIso->FanoutSig;
810 if ( pIso->Id )
811 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
812 }
813 }
814 else
815 {
816 if ( Aig_ObjIsNode(pObj) )
817 {
818 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
819 pIsoF->FanoutSig += pIso->FanoutSig;
820 if ( pIso->Id )
821 pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
822
823 pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
824 pIsoF->FanoutSig += pIso->FanoutSig;
825 if ( pIso->Id )
826 pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
827 }
828 else if ( Aig_ObjIsCo(pObj) )
829 {
830 pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
831 pIsoF->FanoutSig += pIso->FanoutSig;
832 if ( pIso->Id )
833 pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
834 }
835 }
836 }
837
838 // consider flops
839 Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
840 {
841 if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
842 continue;
843 pIso = Iso_ManObj( p, Aig_ObjId(pObj) );
844 pIsoF = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );
845 assert( pIso->FaninSig == 0 );
846 // assert( pIsoF->FanoutSig == 0 );
847
848 if ( fUseXor )
849 {
850 pIso->FaninSig = pIsoF->FaninSig;
851 if ( pIsoF->Id )
852 pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
853
854 pIsoF->FanoutSig += pIso->FanoutSig;
855 if ( pIso->Id )
856 pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
857 }
858 else
859 {
860 pIso->FaninSig = pIsoF->FaninSig;
861 if ( pIsoF->Id )
862 pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
863
864 pIsoF->FanoutSig += pIso->FanoutSig;
865 if ( pIso->Id )
866 pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
867 }
868 }
869 }
870
871
872
873 /**Function*************************************************************
874
875 Synopsis []
876
877 Description []
878
879 SideEffects []
880
881 SeeAlso []
882
883 ***********************************************************************/
Iso_ManPrintClasseSizes(Iso_Man_t * p)884 void Iso_ManPrintClasseSizes( Iso_Man_t * p )
885 {
886 Iso_Obj_t * pIso, * pTemp;
887 int i, Counter;
888 Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
889 {
890 Counter = 0;
891 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
892 Counter++;
893 printf( "%d ", Counter );
894 }
895 printf( "\n" );
896 }
897
898 /**Function*************************************************************
899
900 Synopsis []
901
902 Description []
903
904 SideEffects []
905
906 SeeAlso []
907
908 ***********************************************************************/
Iso_ManPrintClasses(Iso_Man_t * p,int fVerbose,int fVeryVerbose)909 void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
910 {
911 int fOnlyCis = 0;
912 Iso_Obj_t * pIso, * pTemp;
913 int i;
914
915 // count unique objects
916 if ( fVerbose )
917 printf( "Total objects =%7d. Entries =%7d. Classes =%7d. Singles =%7d.\n",
918 p->nObjs, p->nEntries, p->nClasses, p->nSingles );
919
920 if ( !fVeryVerbose )
921 return;
922
923 printf( "Non-trivial classes:\n" );
924 Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
925 {
926 if ( fOnlyCis && pIso->Level > 0 )
927 continue;
928
929 printf( "%5d : {", i );
930 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
931 {
932 if ( fOnlyCis )
933 printf( " %d", Aig_ObjCioId( Iso_AigObj(p, pTemp) ) );
934 else
935 {
936 Aig_Obj_t * pObj = Iso_AigObj(p, pTemp);
937 if ( Aig_ObjIsNode(pObj) )
938 printf( " %d{%s%d(%d),%s%d(%d)}", Iso_ObjId(p, pTemp),
939 Aig_ObjFaninC0(pObj)? "-": "+", Aig_ObjFaninId0(pObj), Aig_ObjLevel(Aig_ObjFanin0(pObj)),
940 Aig_ObjFaninC1(pObj)? "-": "+", Aig_ObjFaninId1(pObj), Aig_ObjLevel(Aig_ObjFanin1(pObj)) );
941 else
942 printf( " %d", Iso_ObjId(p, pTemp) );
943 }
944 printf( "(%d)", pTemp->Level );
945 }
946 printf( " }\n" );
947 }
948 }
949
950
951 /**Function*************************************************************
952
953 Synopsis []
954
955 Description []
956
957 SideEffects []
958
959 SeeAlso []
960
961 ***********************************************************************/
Iso_ManRehashClassNodes(Iso_Man_t * p)962 void Iso_ManRehashClassNodes( Iso_Man_t * p )
963 {
964 Iso_Obj_t * pIso, * pTemp;
965 int i;
966 // collect nodes
967 Vec_PtrClear( p->vTemp1 );
968 Vec_PtrClear( p->vTemp2 );
969 Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
970 {
971 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
972 if ( pTemp->Id == 0 )
973 Vec_PtrPush( p->vTemp1, pTemp );
974 else
975 Vec_PtrPush( p->vTemp2, pTemp );
976 }
977 // clean and add nodes
978 p->nClasses = 0; // total number of classes
979 p->nEntries = 0; // total number of entries
980 p->nSingles = 0; // total number of singletons
981 memset( p->pBins, 0, sizeof(int) * p->nBins );
982 Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp1, pTemp, i )
983 {
984 assert( pTemp->Id == 0 );
985 pTemp->iClass = pTemp->iNext = 0;
986 Iso_ObjHashAdd( p, pTemp );
987 }
988 Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp2, pTemp, i )
989 {
990 assert( pTemp->Id != 0 );
991 pTemp->iClass = pTemp->iNext = 0;
992 }
993 // collect new classes
994 Iso_ManCollectClasses( p );
995 }
996
997 /**Function*************************************************************
998
999 Synopsis [Find nodes with the min number of edges.]
1000
1001 Description []
1002
1003 SideEffects []
1004
1005 SeeAlso []
1006
1007 ***********************************************************************/
Iso_ManFindBestObj(Iso_Man_t * p,Iso_Obj_t * pIso)1008 Iso_Obj_t * Iso_ManFindBestObj( Iso_Man_t * p, Iso_Obj_t * pIso )
1009 {
1010 Iso_Obj_t * pTemp, * pBest = NULL;
1011 int nNodesBest = -1, nNodes;
1012 int nEdgesBest = -1, nEdges;
1013 assert( pIso->Id == 0 );
1014 if ( pIso->Level == 0 )
1015 return pIso;
1016 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
1017 {
1018 assert( pTemp->Id == 0 );
1019 Iso_ManObjCount( p->pAig, Iso_AigObj(p, pTemp), &nNodes, &nEdges );
1020 // printf( "%d,%d ", nNodes, nEdges );
1021 if ( nNodesBest < nNodes || (nNodesBest == nNodes && nEdgesBest < nEdges) )
1022 {
1023 nNodesBest = nNodes;
1024 nEdgesBest = nEdges;
1025 pBest = pTemp;
1026 }
1027 }
1028 // printf( "\n" );
1029 return pBest;
1030 }
1031
1032 /**Function*************************************************************
1033
1034 Synopsis [Find nodes with the min number of edges.]
1035
1036 Description []
1037
1038 SideEffects []
1039
1040 SeeAlso []
1041
1042 ***********************************************************************/
Iso_ManBreakTies(Iso_Man_t * p,int fVerbose)1043 void Iso_ManBreakTies( Iso_Man_t * p, int fVerbose )
1044 {
1045 int fUseOneBest = 0;
1046 Iso_Obj_t * pIso, * pTemp;
1047 int i, LevelStart = 0;
1048 pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
1049 LevelStart = pIso->Level;
1050 if ( fVerbose )
1051 printf( "Best level %d\n", LevelStart );
1052 Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
1053 {
1054 if ( (int)pIso->Level < LevelStart )
1055 break;
1056 if ( !fUseOneBest )
1057 {
1058 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
1059 {
1060 assert( pTemp->Id == 0 );
1061 pTemp->Id = p->nObjIds++;
1062 }
1063 continue;
1064 }
1065 if ( pIso->Level == 0 )//&& pIso->nFoutPos + pIso->nFoutNeg == 0 )
1066 {
1067 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
1068 pTemp->Id = p->nObjIds++;
1069 continue;
1070 }
1071 pIso = Iso_ManFindBestObj( p, pIso );
1072 pIso->Id = p->nObjIds++;
1073 }
1074 }
1075
1076 /**Function*************************************************************
1077
1078 Synopsis [Finalizes unification of combinational outputs.]
1079
1080 Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]
1081
1082 SideEffects []
1083
1084 SeeAlso []
1085
1086 ***********************************************************************/
Iso_ManFinalize(Iso_Man_t * p)1087 Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
1088 {
1089 Vec_Int_t * vRes;
1090 Aig_Obj_t * pObj;
1091 int i;
1092 assert( p->nClasses == 0 );
1093 assert( Vec_PtrSize(p->vClasses) == 0 );
1094 // set canonical numbers
1095 Aig_ManForEachObj( p->pAig, pObj, i )
1096 {
1097 if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
1098 {
1099 pObj->iData = -1;
1100 continue;
1101 }
1102 pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
1103 assert( pObj->iData > 0 );
1104 }
1105 Aig_ManConst1(p->pAig)->iData = 0;
1106 // assign unique IDs to the CIs
1107 Vec_PtrClear( p->vTemp1 );
1108 Vec_PtrClear( p->vTemp2 );
1109 Aig_ManForEachCi( p->pAig, pObj, i )
1110 {
1111 assert( pObj->iData > 0 );
1112 if ( Aig_ObjCioId(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop
1113 Vec_PtrPush( p->vTemp2, pObj );
1114 else // PI
1115 Vec_PtrPush( p->vTemp1, pObj );
1116 }
1117 // sort CIs by their IDs
1118 Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareByData );
1119 Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareByData );
1120 // create the result
1121 vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) );
1122 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i )
1123 Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
1124 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i )
1125 Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
1126 return vRes;
1127 }
1128
1129 /**Function*************************************************************
1130
1131 Synopsis [Find nodes with the min number of edges.]
1132
1133 Description []
1134
1135 SideEffects []
1136
1137 SeeAlso []
1138
1139 ***********************************************************************/
Iso_ManDumpOneClass(Iso_Man_t * p)1140 void Iso_ManDumpOneClass( Iso_Man_t * p )
1141 {
1142 Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
1143 Iso_Obj_t * pIso, * pTemp;
1144 Aig_Man_t * pNew = NULL;
1145 assert( p->nClasses > 0 );
1146 pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
1147 assert( pIso->Id == 0 );
1148 for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
1149 {
1150 assert( pTemp->Id == 0 );
1151 Vec_PtrPush( vNodes, Iso_AigObj(p, pTemp) );
1152 }
1153 pNew = Aig_ManDupNodes( p->pAig, vNodes );
1154 Vec_PtrFree( vNodes );
1155 Aig_ManShow( pNew, 0, NULL );
1156 Aig_ManStopP( &pNew );
1157 }
1158
1159 /**Function*************************************************************
1160
1161 Synopsis [Finds canonical permutation of CIs and assigns unique IDs.]
1162
1163 Description []
1164
1165 SideEffects []
1166
1167 SeeAlso []
1168
1169 ***********************************************************************/
Saig_ManFindIsoPerm(Aig_Man_t * pAig,int fVerbose)1170 Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
1171 {
1172 int fVeryVerbose = 0;
1173 Vec_Int_t * vRes;
1174 Iso_Man_t * p;
1175 abctime clk = Abc_Clock(), clk2 = Abc_Clock();
1176 p = Iso_ManCreate( pAig );
1177 p->timeFout += Abc_Clock() - clk;
1178 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1179 while ( p->nClasses )
1180 {
1181 // assign adjacency to classes
1182 clk = Abc_Clock();
1183 Iso_ManAssignAdjacency( p );
1184 p->timeFout += Abc_Clock() - clk;
1185 // rehash the class nodes
1186 clk = Abc_Clock();
1187 Iso_ManRehashClassNodes( p );
1188 p->timeHash += Abc_Clock() - clk;
1189 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1190 // force refinement
1191 while ( p->nSingles == 0 && p->nClasses )
1192 {
1193 // Iso_ManPrintClasseSizes( p );
1194 // assign IDs to the topmost level of classes
1195 Iso_ManBreakTies( p, fVerbose );
1196 // assign adjacency to classes
1197 clk = Abc_Clock();
1198 Iso_ManAssignAdjacency( p );
1199 p->timeFout += Abc_Clock() - clk;
1200 // rehash the class nodes
1201 clk = Abc_Clock();
1202 Iso_ManRehashClassNodes( p );
1203 p->timeHash += Abc_Clock() - clk;
1204 Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
1205 }
1206 }
1207 p->timeTotal = Abc_Clock() - clk2;
1208 // printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
1209 assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
1210 // if ( p->nClasses )
1211 // Iso_ManDumpOneClass( p );
1212 vRes = Iso_ManFinalize( p );
1213 Iso_ManStop( p, fVerbose );
1214 return vRes;
1215 }
1216
1217
1218 ////////////////////////////////////////////////////////////////////////
1219 /// END OF FILE ///
1220 ////////////////////////////////////////////////////////////////////////
1221
1222
1223 ABC_NAMESPACE_IMPL_END
1224
1225