1 /**CFile****************************************************************
2
3 FileName [mvcDivide.c]
4
5 PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
6
7 Synopsis [Procedures for algebraic division.]
8
9 Author [MVSIS Group]
10
11 Affiliation [UC Berkeley]
12
13 Date [Ver. 1.0. Started - February 1, 2003.]
14
15 Revision [$Id: mvcDivide.c,v 1.5 2003/04/26 20:41:36 alanmi Exp $]
16
17 ***********************************************************************/
18
19 #include "mvc.h"
20
21 ABC_NAMESPACE_IMPL_START
22
23
24 ////////////////////////////////////////////////////////////////////////
25 /// DECLARATIONS ///
26 ////////////////////////////////////////////////////////////////////////
27
28 static void Mvc_CoverVerifyDivision( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t * pQuo, Mvc_Cover_t * pRem );
29
30 int s_fVerbose = 0;
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis []
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Mvc_CoverDivide(Mvc_Cover_t * pCover,Mvc_Cover_t * pDiv,Mvc_Cover_t ** ppQuo,Mvc_Cover_t ** ppRem)47 void Mvc_CoverDivide( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
48 {
49 // check the number of cubes
50 if ( Mvc_CoverReadCubeNum( pCover ) < Mvc_CoverReadCubeNum( pDiv ) )
51 {
52 *ppQuo = NULL;
53 *ppRem = NULL;
54 return;
55 }
56
57 // make sure that support of pCover contains that of pDiv
58 if ( !Mvc_CoverCheckSuppContainment( pCover, pDiv ) )
59 {
60 *ppQuo = NULL;
61 *ppRem = NULL;
62 return;
63 }
64
65 // perform the general division
66 Mvc_CoverDivideInternal( pCover, pDiv, ppQuo, ppRem );
67 }
68
69
70 /**Function*************************************************************
71
72 Synopsis [Merge the cubes inside the groups.]
73
74 Description []
75
76 SideEffects []
77
78 SeeAlso []
79
80 ***********************************************************************/
Mvc_CoverDivideInternal(Mvc_Cover_t * pCover,Mvc_Cover_t * pDiv,Mvc_Cover_t ** ppQuo,Mvc_Cover_t ** ppRem)81 void Mvc_CoverDivideInternal( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
82 {
83 Mvc_Cover_t * pQuo, * pRem;
84 Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
85 Mvc_Cube_t * pCube1, * pCube2;
86 int * pGroups, nGroups; // the cube groups
87 int nCubesC, nCubesD, nMerges, iCubeC, iCubeD;
88 int iMerge = -1; // Suppress "might be used uninitialized"
89 int fSkipG, GroupSize, g, c, RetValue;
90 int nCubes;
91
92 // get cover sizes
93 nCubesD = Mvc_CoverReadCubeNum( pDiv );
94 nCubesC = Mvc_CoverReadCubeNum( pCover );
95
96 // check trivial cases
97 if ( nCubesD == 1 )
98 {
99 if ( Mvc_CoverIsOneLiteral( pDiv ) )
100 Mvc_CoverDivideByLiteral( pCover, pDiv, ppQuo, ppRem );
101 else
102 Mvc_CoverDivideByCube( pCover, pDiv, ppQuo, ppRem );
103 return;
104 }
105
106 // create the divisor and the remainder
107 pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
108 pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
109
110 // get the support of the divisor
111 Mvc_CoverAllocateMask( pDiv );
112 Mvc_CoverSupport( pDiv, pDiv->pMask );
113
114 // sort the cubes of the divisor
115 Mvc_CoverSort( pDiv, NULL, Mvc_CubeCompareInt );
116 // sort the cubes of the cover
117 Mvc_CoverSort( pCover, pDiv->pMask, Mvc_CubeCompareIntOutsideAndUnderMask );
118
119 // allocate storage for cube groups
120 pGroups = MEM_ALLOC( pCover->pMem, int, nCubesC + 1 );
121
122 // mask contains variables in the support of Div
123 // split the cubes into groups using the mask
124 Mvc_CoverList2Array( pCover );
125 Mvc_CoverList2Array( pDiv );
126 pGroups[0] = 0;
127 nGroups = 1;
128 for ( c = 1; c < nCubesC; c++ )
129 {
130 // get the cubes
131 pCube1 = pCover->pCubes[c-1];
132 pCube2 = pCover->pCubes[c ];
133 // compare the cubes
134 Mvc_CubeBitEqualOutsideMask( RetValue, pCube1, pCube2, pDiv->pMask );
135 if ( !RetValue )
136 pGroups[nGroups++] = c;
137 }
138 // finish off the last group
139 pGroups[nGroups] = nCubesC;
140
141 // consider each group separately and decide
142 // whether it can produce a quotient cube
143 nCubes = 0;
144 for ( g = 0; g < nGroups; g++ )
145 {
146 // if the group has less than nCubesD cubes,
147 // there is no way it can produce the quotient cube
148 // copy the cubes to the remainder
149 GroupSize = pGroups[g+1] - pGroups[g];
150 if ( GroupSize < nCubesD )
151 {
152 for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
153 {
154 pCubeCopy = Mvc_CubeDup( pRem, pCover->pCubes[c] );
155 Mvc_CoverAddCubeTail( pRem, pCubeCopy );
156 nCubes++;
157 }
158 continue;
159 }
160
161 // mark the cubes as those that should be added to the remainder
162 for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
163 Mvc_CubeSetSize( pCover->pCubes[c], 1 );
164
165 // go through the cubes in the group and at the same time
166 // go through the cubes in the divisor
167 iCubeD = 0;
168 iCubeC = 0;
169 pCubeD = pDiv->pCubes[iCubeD++];
170 pCubeC = pCover->pCubes[pGroups[g]+iCubeC++];
171 fSkipG = 0;
172 nMerges = 0;
173
174 while ( 1 )
175 {
176 // compare the topmost cubes in F and in D
177 RetValue = Mvc_CubeCompareIntUnderMask( pCubeC, pCubeD, pDiv->pMask );
178 // cube are ordered in increasing order of their int value
179 if ( RetValue == -1 ) // pCubeC is above pCubeD
180 { // cube in C should be added to the remainder
181 // check that there is enough cubes in the group
182 if ( GroupSize - iCubeC < nCubesD - nMerges )
183 {
184 fSkipG = 1;
185 break;
186 }
187 // get the next cube in the cover
188 pCubeC = pCover->pCubes[pGroups[g]+iCubeC++];
189 continue;
190 }
191 if ( RetValue == 1 ) // pCubeD is above pCubeC
192 { // given cube in D does not have a corresponding cube in the cover
193 fSkipG = 1;
194 break;
195 }
196 // mark the cube as the one that should NOT be added to the remainder
197 Mvc_CubeSetSize( pCubeC, 0 );
198 // remember this merged cube
199 iMerge = iCubeC-1;
200 nMerges++;
201
202 // stop if we considered the last cube of the group
203 if ( iCubeD == nCubesD )
204 break;
205
206 // advance the cube of the divisor
207 assert( iCubeD < nCubesD );
208 pCubeD = pDiv->pCubes[iCubeD++];
209
210 // advance the cube of the group
211 assert( pGroups[g]+iCubeC < nCubesC );
212 pCubeC = pCover->pCubes[pGroups[g]+iCubeC++];
213 }
214
215 if ( fSkipG )
216 {
217 // the group has failed, add all the cubes to the remainder
218 for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
219 {
220 pCubeCopy = Mvc_CubeDup( pRem, pCover->pCubes[c] );
221 Mvc_CoverAddCubeTail( pRem, pCubeCopy );
222 nCubes++;
223 }
224 continue;
225 }
226
227 // the group has worked, add left-over cubes to the remainder
228 for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
229 {
230 pCubeC = pCover->pCubes[c];
231 if ( Mvc_CubeReadSize(pCubeC) )
232 {
233 pCubeCopy = Mvc_CubeDup( pRem, pCubeC );
234 Mvc_CoverAddCubeTail( pRem, pCubeCopy );
235 nCubes++;
236 }
237 }
238
239 // create the quotient cube
240 pCube1 = Mvc_CubeAlloc( pQuo );
241 Mvc_CubeBitSharp( pCube1, pCover->pCubes[pGroups[g]+iMerge], pDiv->pMask );
242 // add the cube to the quotient
243 Mvc_CoverAddCubeTail( pQuo, pCube1 );
244 nCubes += nCubesD;
245 }
246 assert( nCubes == nCubesC );
247
248 // deallocate the memory
249 MEM_FREE( pCover->pMem, int, nCubesC + 1, pGroups );
250
251 // return the results
252 *ppRem = pRem;
253 *ppQuo = pQuo;
254 // Mvc_CoverVerifyDivision( pCover, pDiv, pQuo, pRem );
255 }
256
257
258 /**Function*************************************************************
259
260 Synopsis [Divides the cover by a cube.]
261
262 Description []
263
264 SideEffects []
265
266 SeeAlso []
267
268 ***********************************************************************/
Mvc_CoverDivideByCube(Mvc_Cover_t * pCover,Mvc_Cover_t * pDiv,Mvc_Cover_t ** ppQuo,Mvc_Cover_t ** ppRem)269 void Mvc_CoverDivideByCube( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
270 {
271 Mvc_Cover_t * pQuo, * pRem;
272 Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
273 int CompResult;
274
275 // get the only cube of D
276 assert( Mvc_CoverReadCubeNum(pDiv) == 1 );
277
278 // start the quotient and the remainder
279 pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
280 pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
281
282 // get the first and only cube of the divisor
283 pCubeD = Mvc_CoverReadCubeHead( pDiv );
284
285 // iterate through the cubes in the cover
286 Mvc_CoverForEachCube( pCover, pCubeC )
287 {
288 // check the containment of literals from pCubeD in pCube
289 Mvc_Cube2BitNotImpl( CompResult, pCubeD, pCubeC );
290 if ( !CompResult )
291 { // this cube belongs to the quotient
292 // alloc the cube
293 pCubeCopy = Mvc_CubeAlloc( pQuo );
294 // clean the support of D
295 Mvc_CubeBitSharp( pCubeCopy, pCubeC, pCubeD );
296 // add the cube to the quotient
297 Mvc_CoverAddCubeTail( pQuo, pCubeCopy );
298 }
299 else
300 {
301 // copy the cube
302 pCubeCopy = Mvc_CubeDup( pRem, pCubeC );
303 // add the cube to the remainder
304 Mvc_CoverAddCubeTail( pRem, pCubeCopy );
305 }
306 }
307 // return the results
308 *ppRem = pRem;
309 *ppQuo = pQuo;
310 }
311
312 /**Function*************************************************************
313
314 Synopsis [Divides the cover by a literal.]
315
316 Description []
317
318 SideEffects []
319
320 SeeAlso []
321
322 ***********************************************************************/
Mvc_CoverDivideByLiteral(Mvc_Cover_t * pCover,Mvc_Cover_t * pDiv,Mvc_Cover_t ** ppQuo,Mvc_Cover_t ** ppRem)323 void Mvc_CoverDivideByLiteral( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
324 {
325 Mvc_Cover_t * pQuo, * pRem;
326 Mvc_Cube_t * pCubeC, * pCubeCopy;
327 int iLit;
328
329 // get the only cube of D
330 assert( Mvc_CoverReadCubeNum(pDiv) == 1 );
331
332 // start the quotient and the remainder
333 pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
334 pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
335
336 // get the first and only literal in the divisor cube
337 iLit = Mvc_CoverFirstCubeFirstLit( pDiv );
338
339 // iterate through the cubes in the cover
340 Mvc_CoverForEachCube( pCover, pCubeC )
341 {
342 // copy the cube
343 pCubeCopy = Mvc_CubeDup( pCover, pCubeC );
344 // add the cube to the quotient or to the remainder depending on the literal
345 if ( Mvc_CubeBitValue( pCubeCopy, iLit ) )
346 { // remove the literal
347 Mvc_CubeBitRemove( pCubeCopy, iLit );
348 // add the cube ot the quotient
349 Mvc_CoverAddCubeTail( pQuo, pCubeCopy );
350 }
351 else
352 { // add the cube ot the remainder
353 Mvc_CoverAddCubeTail( pRem, pCubeCopy );
354 }
355 }
356 // return the results
357 *ppRem = pRem;
358 *ppQuo = pQuo;
359 }
360
361
362 /**Function*************************************************************
363
364 Synopsis [Derives the quotient of division by literal.]
365
366 Description [Reduces the cover to be the equal to the result of
367 division of the given cover by the literal.]
368
369 SideEffects []
370
371 SeeAlso []
372
373 ***********************************************************************/
Mvc_CoverDivideByLiteralQuo(Mvc_Cover_t * pCover,int iLit)374 void Mvc_CoverDivideByLiteralQuo( Mvc_Cover_t * pCover, int iLit )
375 {
376 Mvc_Cube_t * pCube, * pCube2, * pPrev;
377 // delete those cubes that do not have this literal
378 // remove this literal from other cubes
379 pPrev = NULL;
380 Mvc_CoverForEachCubeSafe( pCover, pCube, pCube2 )
381 {
382 if ( Mvc_CubeBitValue( pCube, iLit ) == 0 )
383 { // delete the cube from the cover
384 Mvc_CoverDeleteCube( pCover, pPrev, pCube );
385 Mvc_CubeFree( pCover, pCube );
386 // don't update the previous cube
387 }
388 else
389 { // delete this literal from the cube
390 Mvc_CubeBitRemove( pCube, iLit );
391 // update the previous cube
392 pPrev = pCube;
393 }
394 }
395 }
396
397
398 /**Function*************************************************************
399
400 Synopsis [Verifies that the result of algebraic division is correct.]
401
402 Description []
403
404 SideEffects []
405
406 SeeAlso []
407
408 ***********************************************************************/
Mvc_CoverVerifyDivision(Mvc_Cover_t * pCover,Mvc_Cover_t * pDiv,Mvc_Cover_t * pQuo,Mvc_Cover_t * pRem)409 void Mvc_CoverVerifyDivision( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t * pQuo, Mvc_Cover_t * pRem )
410 {
411 Mvc_Cover_t * pProd;
412 Mvc_Cover_t * pDiff;
413
414 pProd = Mvc_CoverAlgebraicMultiply( pDiv, pQuo );
415 pDiff = Mvc_CoverAlgebraicSubtract( pCover, pProd );
416
417 if ( Mvc_CoverAlgebraicEqual( pDiff, pRem ) )
418 printf( "Verification OKAY!\n" );
419 else
420 {
421 printf( "Verification FAILED!\n" );
422 printf( "pCover:\n" );
423 Mvc_CoverPrint( pCover );
424 printf( "pDiv:\n" );
425 Mvc_CoverPrint( pDiv );
426 printf( "pRem:\n" );
427 Mvc_CoverPrint( pRem );
428 printf( "pQuo:\n" );
429 Mvc_CoverPrint( pQuo );
430 }
431
432 Mvc_CoverFree( pProd );
433 Mvc_CoverFree( pDiff );
434 }
435
436 ////////////////////////////////////////////////////////////////////////
437 /// END OF FILE ///
438 ////////////////////////////////////////////////////////////////////////
439
440
441 ABC_NAMESPACE_IMPL_END
442
443