ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
mapperCanon.c File Reference
#include "mapperInt.h"
Include dependency graph for mapperCanon.c:

Go to the source code of this file.

Functions

int Map_CanonComputeSlow (unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
 FUNCTION DEFINITIONS ///.
 
int Map_CanonComputeFast (Map_Man_t *p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
 

Function Documentation

◆ Map_CanonComputeFast()

int Map_CanonComputeFast ( Map_Man_t * p,
int nVarsMax,
int nVarsReal,
unsigned uTruth[],
unsigned char * puPhases,
unsigned uTruthRes[] )

Function*************************************************************

Synopsis [Computes the N-canonical form of the Boolean function.]

Description [The N-canonical form is defined as the truth table with the minimum integer value. This function exhaustively enumerates through the complete set of 2^N phase assignments.]

SideEffects []

SeeAlso []

Definition at line 173 of file mapperCanon.c.

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}
p
Cube * p
Definition exorList.c:222
Extra_TruthPolarize
unsigned Extra_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
Definition extraUtilMisc.c:401
Map_CanonComputeSlow
int Map_CanonComputeSlow(unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
FUNCTION DEFINITIONS ///.
Definition mapperCanon.c:48
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Map_CanonComputeSlow()

int Map_CanonComputeSlow ( unsigned uTruths[][2],
int nVarsMax,
int nVarsReal,
unsigned uTruth[],
unsigned char * puPhases,
unsigned uTruthRes[] )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Computes the N-canonical form of the Boolean function.]

Description [The N-canonical form is defined as the truth table with the minimum integer value. This function exhaustively enumerates through the complete set of 2^N phase assignments.]

SideEffects []

SeeAlso []

Definition at line 48 of file mapperCanon.c.

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}
MAP_MASK
#define MAP_MASK(n)
INCLUDES ///.
Definition mapperInt.h:52
Here is the caller graph for this function: