ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mvcLits.c
Go to the documentation of this file.
1
18
19#include "mvc.h"
20
22
23
27
31
44{
45 Mvc_Cube_t * pCube;
46 int nWord, nBit, i;
47 int nLitsCur;
48 int fUseFirst = 0;
49
50 // go through each literal
51 if ( fUseFirst )
52 {
53 for ( i = 0; i < pCover->nBits; i++ )
54 if ( !pMask || Mvc_CubeBitValue(pMask,i) )
55 {
56 // get the word and bit of this literal
57 nWord = Mvc_CubeWhichWord(i);
58 nBit = Mvc_CubeWhichBit(i);
59 // go through all the cubes
60 nLitsCur = 0;
61 Mvc_CoverForEachCube( pCover, pCube )
62 if ( pCube->pData[nWord] & (1<<nBit) )
63 {
64 nLitsCur++;
65 if ( nLitsCur > 1 )
66 return i;
67 }
68 }
69 }
70 else
71 {
72 for ( i = pCover->nBits - 1; i >=0; i-- )
73 if ( !pMask || Mvc_CubeBitValue(pMask,i) )
74 {
75 // get the word and bit of this literal
76 nWord = Mvc_CubeWhichWord(i);
77 nBit = Mvc_CubeWhichBit(i);
78 // go through all the cubes
79 nLitsCur = 0;
80 Mvc_CoverForEachCube( pCover, pCube )
81 if ( pCube->pData[nWord] & (1<<nBit) )
82 {
83 nLitsCur++;
84 if ( nLitsCur > 1 )
85 return i;
86 }
87 }
88 }
89 return -1;
90}
91
105{
106 Mvc_Cube_t * pCube;
107 int nWord, nBit;
108 int i, iMax, nLitsMax, nLitsCur;
109 int fUseFirst = 1;
110
111 // go through each literal
112 iMax = -1;
113 nLitsMax = -1;
114 for ( i = 0; i < pCover->nBits; i++ )
115 if ( !pMask || Mvc_CubeBitValue(pMask,i) )
116 {
117 // get the word and bit of this literal
118 nWord = Mvc_CubeWhichWord(i);
119 nBit = Mvc_CubeWhichBit(i);
120 // go through all the cubes
121 nLitsCur = 0;
122 Mvc_CoverForEachCube( pCover, pCube )
123 if ( pCube->pData[nWord] & (1<<nBit) )
124 nLitsCur++;
125
126 // check if this is the best literal
127 if ( fUseFirst )
128 {
129 if ( nLitsMax < nLitsCur )
130 {
131 nLitsMax = nLitsCur;
132 iMax = i;
133 }
134 }
135 else
136 {
137 if ( nLitsMax <= nLitsCur )
138 {
139 nLitsMax = nLitsCur;
140 iMax = i;
141 }
142 }
143 }
144
145 if ( nLitsMax > 1 )
146 return iMax;
147 return -1;
148}
149
163{
164 Mvc_Cube_t * pCube;
165 int nWord, nBit;
166 int i, iMin, nLitsMin, nLitsCur;
167 int fUseFirst = 1;
168
169 // go through each literal
170 iMin = -1;
171 nLitsMin = 1000000;
172 for ( i = 0; i < pCover->nBits; i++ )
173 if ( !pMask || Mvc_CubeBitValue(pMask,i) )
174 {
175 // get the word and bit of this literal
176 nWord = Mvc_CubeWhichWord(i);
177 nBit = Mvc_CubeWhichBit(i);
178 // go through all the cubes
179 nLitsCur = 0;
180 Mvc_CoverForEachCube( pCover, pCube )
181 if ( pCube->pData[nWord] & (1<<nBit) )
182 nLitsCur++;
183
184 // skip the literal that does not occur or occurs once
185 if ( nLitsCur < 2 )
186 continue;
187
188 // check if this is the best literal
189 if ( fUseFirst )
190 {
191 if ( nLitsMin > nLitsCur )
192 {
193 nLitsMin = nLitsCur;
194 iMin = i;
195 }
196 }
197 else
198 {
199 if ( nLitsMin >= nLitsCur )
200 {
201 nLitsMin = nLitsCur;
202 iMin = i;
203 }
204 }
205 }
206
207 if ( nLitsMin < 1000000 )
208 return iMin;
209 return -1;
210}
211
224{
225 Mvc_Cover_t * pCoverNew;
226 Mvc_Cube_t * pCubeNew;
227 Mvc_Cube_t * pCubeS;
228 int iLitBest;
229
230 // create the new cover
231 pCoverNew = Mvc_CoverClone( pCover );
232 // get the new cube
233 pCubeNew = Mvc_CubeAlloc( pCoverNew );
234 // clean the cube
235 Mvc_CubeBitClean( pCubeNew );
236
237 // get the first cube of pSimple
238 assert( Mvc_CoverReadCubeNum(pSimple) == 1 );
239 pCubeS = Mvc_CoverReadCubeHead( pSimple );
240 // find the best literal among those of pCubeS
241 iLitBest = Mvc_CoverBestLiteral( pCover, pCubeS );
242
243 // insert this literal into the cube
244 Mvc_CubeBitInsert( pCubeNew, iLitBest );
245 // add the cube to the cover
246 Mvc_CoverAddCubeTail( pCoverNew, pCubeNew );
247 return pCoverNew;
248}
249
262{
263 Mvc_Cube_t * pCube;
264 int iBit, Value;
265
266 // get the first cube
267 pCube = Mvc_CoverReadCubeHead( pCover );
268 // get the first literal
269 Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
270 if ( Value )
271 return iBit;
272 return -1;
273}
274
288{
289 Mvc_Cube_t * pCube;
290 int nWord, nBit;
291 int i, CounterTot, CounterCur;
292
293 // allocate/clean the storage for literals
294// Mvc_CoverAllocateArrayLits( pCover );
295// memset( pCover->pLits, 0, pCover->nBits * sizeof(int) );
296 // go through each literal
297 CounterTot = 0;
298 for ( i = 0; i < pCover->nBits; i++ )
299 {
300 // get the word and bit of this literal
301 nWord = Mvc_CubeWhichWord(i);
302 nBit = Mvc_CubeWhichBit(i);
303 // go through all the cubes
304 CounterCur = 0;
305 Mvc_CoverForEachCube( pCover, pCube )
306 if ( pCube->pData[nWord] & (1<<nBit) )
307 CounterCur++;
308 CounterTot += CounterCur;
309 }
310 return CounterTot;
311}
312
325{
326 Mvc_Cube_t * pCube;
327 int iBit, Counter, Value;
328 if ( Mvc_CoverReadCubeNum(pCover) != 1 )
329 return 0;
330 pCube = Mvc_CoverReadCubeHead(pCover);
331 // count literals
332 Counter = 0;
333 Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
334 {
335 if ( Value )
336 {
337 if ( Counter++ )
338 return 0;
339 }
340 }
341 return 1;
342}
343
347
348
350
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START int Mvc_CoverAnyLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
DECLARATIONS ///.
Definition mvcLits.c:43
int Mvc_CoverWorstLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
Definition mvcLits.c:162
int Mvc_CoverBestLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
Definition mvcLits.c:104
int Mvc_CoverCountLiterals(Mvc_Cover_t *pCover)
Definition mvcLits.c:287
Mvc_Cover_t * Mvc_CoverBestLiteralCover(Mvc_Cover_t *pCover, Mvc_Cover_t *pSimple)
Definition mvcLits.c:223
int Mvc_CoverFirstCubeFirstLit(Mvc_Cover_t *pCover)
Definition mvcLits.c:261
int Mvc_CoverIsOneLiteral(Mvc_Cover_t *pCover)
Definition mvcLits.c:324
#define Mvc_CoverAddCubeTail(pCover, pCube)
Definition mvc.h:501
#define Mvc_CubeWhichWord(Bit)
Definition mvc.h:135
Mvc_Cover_t * Mvc_CoverClone(Mvc_Cover_t *pCover)
Definition mvcCover.c:79
struct MvcCubeStruct Mvc_Cube_t
Definition mvc.h:56
#define Mvc_CubeBitClean(Cube)
Definition mvc.h:381
#define Mvc_CubeBitValue(Cube, Bit)
Definition mvc.h:138
#define Mvc_CoverForEachCube(Cover, Cube)
Definition mvc.h:528
Mvc_Cube_t * Mvc_CubeAlloc(Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition mvcCube.c:43
struct MvcCoverStruct Mvc_Cover_t
Definition mvc.h:58
#define Mvc_CubeForEachBit(Cover, Cube, iBit, Value)
Definition mvc.h:553
Mvc_Cube_t * Mvc_CoverReadCubeHead(Mvc_Cover_t *pCover)
Definition mvcApi.c:46
#define Mvc_CubeWhichBit(Bit)
Definition mvc.h:136
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition mvcApi.c:45
#define Mvc_CubeBitInsert(Cube, Bit)
Definition mvc.h:139
int nBits
Definition mvc.h:87
Mvc_CubeWord_t pData[1]
Definition mvc.h:71
#define assert(ex)
Definition util_old.h:213