ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mapperCanon.c
Go to the documentation of this file.
1
18
19#include "mapperInt.h"
20
22
23
27
28static unsigned Map_CanonComputePhase( unsigned uTruths[][2], int nVars, unsigned uTruth, unsigned uPhase );
29static void Map_CanonComputePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[], unsigned uPhase, unsigned uTruthRes[] );
30
34
48int Map_CanonComputeSlow( unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] )
49{
50 unsigned uTruthPerm[2];
51 int nMints, nPhases, m;
52
53 nPhases = 0;
54 nMints = (1 << nVarsReal);
55 if ( nVarsMax < 6 )
56 {
57 uTruthRes[0] = MAP_MASK(32);
58 for ( m = 0; m < nMints; m++ )
59 {
60 uTruthPerm[0] = Map_CanonComputePhase( uTruths, nVarsMax, uTruth[0], m );
61 if ( uTruthRes[0] > uTruthPerm[0] )
62 {
63 uTruthRes[0] = uTruthPerm[0];
64 nPhases = 0;
65 puPhases[nPhases++] = (unsigned char)m;
66 }
67 else if ( uTruthRes[0] == uTruthPerm[0] )
68 {
69 if ( nPhases < 4 ) // the max number of phases in Map_Super_t
70 puPhases[nPhases++] = (unsigned char)m;
71 }
72 }
73 uTruthRes[1] = uTruthRes[0];
74 }
75 else
76 {
77 uTruthRes[0] = MAP_MASK(32);
78 uTruthRes[1] = MAP_MASK(32);
79 for ( m = 0; m < nMints; m++ )
80 {
81 Map_CanonComputePhase6( uTruths, nVarsMax, uTruth, m, uTruthPerm );
82 if ( uTruthRes[1] > uTruthPerm[1] || (uTruthRes[1] == uTruthPerm[1] && uTruthRes[0] > uTruthPerm[0]) )
83 {
84 uTruthRes[0] = uTruthPerm[0];
85 uTruthRes[1] = uTruthPerm[1];
86 nPhases = 0;
87 puPhases[nPhases++] = (unsigned char)m;
88 }
89 else if ( uTruthRes[1] == uTruthPerm[1] && uTruthRes[0] == uTruthPerm[0] )
90 {
91 if ( nPhases < 4 ) // the max number of phases in Map_Super_t
92 puPhases[nPhases++] = (unsigned char)m;
93 }
94 }
95 }
96 assert( nPhases > 0 );
97// printf( "%d ", nPhases );
98 return nPhases;
99}
100
112unsigned Map_CanonComputePhase( unsigned uTruths[][2], int nVars, unsigned uTruth, unsigned uPhase )
113{
114 int v, Shift;
115 for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
116 if ( uPhase & Shift )
117 uTruth = (((uTruth & ~uTruths[v][0]) << Shift) | ((uTruth & uTruths[v][0]) >> Shift));
118 return uTruth;
119}
120
132void Map_CanonComputePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[], unsigned uPhase, unsigned uTruthRes[] )
133{
134 unsigned uTemp;
135 int v, Shift;
136
137 // initialize the result
138 uTruthRes[0] = uTruth[0];
139 uTruthRes[1] = uTruth[1];
140 if ( uPhase == 0 )
141 return;
142 // compute the phase
143 for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
144 if ( uPhase & Shift )
145 {
146 if ( Shift < 32 )
147 {
148 uTruthRes[0] = (((uTruthRes[0] & ~uTruths[v][0]) << Shift) | ((uTruthRes[0] & uTruths[v][0]) >> Shift));
149 uTruthRes[1] = (((uTruthRes[1] & ~uTruths[v][1]) << Shift) | ((uTruthRes[1] & uTruths[v][1]) >> Shift));
150 }
151 else
152 {
153 uTemp = uTruthRes[0];
154 uTruthRes[0] = uTruthRes[1];
155 uTruthRes[1] = uTemp;
156 }
157 }
158}
159
173int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] )
174{
175 unsigned uTruth0, uTruth1;
176 unsigned uCanon0, uCanon1, uCanonBest;
177 unsigned uPhaseBest = 16; // Suppress "might be used uninitialized" (asserts require < 16)
178 int i, Limit;
179
180 if ( nVarsMax == 6 )
181 return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
182
183 if ( nVarsReal < 5 )
184 {
185// return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
186
187 uTruth0 = uTruth[0] & 0xFFFF;
188 assert( p->pCounters[uTruth0] > 0 );
189 uTruthRes[0] = (p->uCanons[uTruth0] << 16) | p->uCanons[uTruth0];
190 uTruthRes[1] = uTruthRes[0];
191 puPhases[0] = p->uPhases[uTruth0][0];
192 return 1;
193 }
194
195 assert( nVarsMax == 5 );
196 assert( nVarsReal == 5 );
197 uTruth0 = uTruth[0] & 0xFFFF;
198 uTruth1 = (uTruth[0] >> 16);
199 if ( uTruth1 == 0 )
200 {
201 uTruthRes[0] = p->uCanons[uTruth0];
202 uTruthRes[1] = uTruthRes[0];
203 Limit = (p->pCounters[uTruth0] > 4)? 4 : p->pCounters[uTruth0];
204 for ( i = 0; i < Limit; i++ )
205 puPhases[i] = p->uPhases[uTruth0][i];
206 return Limit;
207 }
208 else if ( uTruth0 == 0 )
209 {
210 uTruthRes[0] = p->uCanons[uTruth1];
211 uTruthRes[1] = uTruthRes[0];
212 Limit = (p->pCounters[uTruth1] > 4)? 4 : p->pCounters[uTruth1];
213 for ( i = 0; i < Limit; i++ )
214 {
215 puPhases[i] = p->uPhases[uTruth1][i];
216 puPhases[i] |= (1 << 4);
217 }
218 return Limit;
219 }
220 uCanon0 = p->uCanons[uTruth0];
221 uCanon1 = p->uCanons[uTruth1];
222 if ( uCanon0 >= uCanon1 ) // using nCanon1 as the main one
223 {
224 assert( p->pCounters[uTruth1] > 0 );
225 uCanonBest = 0xFFFFFFFF;
226 for ( i = 0; i < p->pCounters[uTruth1]; i++ )
227 {
228 uCanon0 = Extra_TruthPolarize( uTruth0, p->uPhases[uTruth1][i], 4 );
229 if ( uCanonBest > uCanon0 )
230 {
231 uCanonBest = uCanon0;
232 uPhaseBest = p->uPhases[uTruth1][i];
233 assert( uPhaseBest < 16 );
234 }
235 }
236 uTruthRes[0] = (uCanon1 << 16) | uCanonBest;
237 uTruthRes[1] = uTruthRes[0];
238 puPhases[0] = uPhaseBest;
239 return 1;
240 }
241 else if ( uCanon0 < uCanon1 )
242 {
243 assert( p->pCounters[uTruth0] > 0 );
244 uCanonBest = 0xFFFFFFFF;
245 for ( i = 0; i < p->pCounters[uTruth0]; i++ )
246 {
247 uCanon1 = Extra_TruthPolarize( uTruth1, p->uPhases[uTruth0][i], 4 );
248 if ( uCanonBest > uCanon1 )
249 {
250 uCanonBest = uCanon1;
251 uPhaseBest = p->uPhases[uTruth0][i];
252 assert( uPhaseBest < 16 );
253 }
254 }
255 uTruthRes[0] = (uCanon0 << 16) | uCanonBest;
256 uTruthRes[1] = uTruthRes[0];
257 puPhases[0] = uPhaseBest | (1 << 4);
258 return 1;
259 }
260 else
261 {
262 assert( 0 );
263 return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
264 }
265}
266
267
268
269
270
274
275
277
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
unsigned Extra_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
int Map_CanonComputeSlow(unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
FUNCTION DEFINITIONS ///.
Definition mapperCanon.c:48
int Map_CanonComputeFast(Map_Man_t *p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
#define MAP_MASK(n)
INCLUDES ///.
Definition mapperInt.h:52
typedefABC_NAMESPACE_HEADER_START struct Map_ManStruct_t_ Map_Man_t
INCLUDES ///.
Definition mapper.h:40
#define assert(ex)
Definition util_old.h:213