abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
mvc.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [mvc.h]
4 
5  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
6 
7  Synopsis [Data structure for MV cube/cover manipulation.]
8 
9  Author [MVSIS Group]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 1.0. Started - February 1, 2003.]
14 
15  Revision [$Id: mvc.h,v 1.10 2003/05/02 23:23:59 wjiang Exp $]
16 
17 ***********************************************************************/
18 
19 #ifndef ABC__misc__mvc__mvc_h
20 #define ABC__misc__mvc__mvc_h
21 
22 
23 ////////////////////////////////////////////////////////////////////////
24 /// INCLUDES ///
25 ////////////////////////////////////////////////////////////////////////
26 
27 #include <stdio.h>
28 #include "misc/extra/extra.h"
29 
31 
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// PARAMETERS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 // this is the only part of Mvc package, which should be modified
38 // when compiling the package for other platforms
39 
40 // these parameters can be computed but setting them manually makes it faster
41 #define BITS_PER_WORD 32 // sizeof(Mvc_CubeWord_t) * 8
42 #define BITS_PER_WORD_MINUS 31 // the same minus 1
43 #define BITS_PER_WORD_LOG 5 // log2(sizeof(Mvc_CubeWord_t) * 8)
44 #define BITS_DISJOINT ((Mvc_CubeWord_t)0x55555555) // the mask of the type "01010101"
45 #define BITS_FULL ((Mvc_CubeWord_t)0xffffffff) // the mask of the type "11111111"
46 
47 // uncomment this macro to switch to standard memory management
48 //#define USE_SYSTEM_MEMORY_MANAGEMENT
49 
50 ////////////////////////////////////////////////////////////////////////
51 /// STRUCTURE DEFINITIONS ///
52 ////////////////////////////////////////////////////////////////////////
53 
54 // cube/list/cover/data
55 typedef unsigned int Mvc_CubeWord_t;
56 typedef struct MvcCubeStruct Mvc_Cube_t;
57 typedef struct MvcListStruct Mvc_List_t;
58 typedef struct MvcCoverStruct Mvc_Cover_t;
59 typedef struct MvcDataStruct Mvc_Data_t;
61 
62 // the cube data structure
64 {
65  Mvc_Cube_t * pNext; // the next cube in the linked list
66  unsigned iLast : 24; // the index of the last word
67  unsigned nUnused : 6; // the number of unused bits in the last word
68  unsigned fPrime : 1; // marks the prime cube
69  unsigned fEssen : 1; // marks the essential cube
70  unsigned nOnes; // the number of 1's in the bit data
71  Mvc_CubeWord_t pData[1]; // the first Mvc_CubeWord_t filled with bit data
72 };
73 
74 // the single-linked list of cubes in the cover
76 {
77  Mvc_Cube_t * pHead; // the first cube in the list
78  Mvc_Cube_t * pTail; // the last cube in the list
79  int nItems; // the number of cubes in the list
80 };
81 
82 // the cover data structure
84 {
85  int nWords; // the number of machine words
86  int nUnused; // the number of unused bits in the last word
87  int nBits; // the number of used data bits in the cube
88  Mvc_List_t lCubes; // the single-linked list of cubes
89  Mvc_Cube_t ** pCubes; // the array of cubes (for sorting)
90  int nCubesAlloc; // the size of allocated storage
91  int * pLits; // the counter of lit occurrances in cubes
92  Mvc_Cube_t * pMask; // the multipurpose mask
93  Mvc_Manager_t * pMem; // the memory manager
94 };
95 
96 // data structure to store information about MV variables
98 {
99  Mvc_Manager_t * pMan; // the memory manager
100 // Vm_VarMap_t * pVm; // the MV variable data
101  int nBinVars; // the number of binary variables
102  Mvc_Cube_t * pMaskBin; // the mask to select the binary bits only
103  Mvc_Cube_t ** ppMasks; // the mask to select each MV variable
104  Mvc_Cube_t * ppTemp[3]; // the temporary cubes
105 };
106 
107 // the manager of covers and cubes (as of today, only managing memory)
109 {
110  Extra_MmFixed_t * pManC; // the manager for covers
111  Extra_MmFixed_t * pMan1; // the manager for 1-word cubes
112  Extra_MmFixed_t * pMan2; // the manager for 2-word cubes
113  Extra_MmFixed_t * pMan4; // the manager for 3-word cubes
114 };
115 
116 ////////////////////////////////////////////////////////////////////////
117 /// MACRO DEFINITIONS ///
118 ////////////////////////////////////////////////////////////////////////
119 
120 // reading data from the header of the cube
121 #define Mvc_CubeReadNext(Cube) ((Cube)->pNext)
122 #define Mvc_CubeReadNextP(Cube) (&(Cube)->pNext)
123 #define Mvc_CubeReadLast(Cube) ((Cube)->iLast)
124 #define Mvc_CubeReadSize(Cube) ((Cube)->nOnes)
125 // setting data to the header of the cube
126 #define Mvc_CubeSetNext(Cube,Next) ((Cube)->pNext = (Next))
127 #define Mvc_CubeSetLast(Cube,Last) ((Cube)->iLast = (Last))
128 #define Mvc_CubeSetSize(Cube,Size) ((Cube)->nOnes = (Size))
129 // checking the number of words
130 
131 #define Mvc_Cube1Words(Cube) ((Cube)->iLast == 0)
132 #define Mvc_Cube2Words(Cube) ((Cube)->iLast == 1)
133 #define Mvc_CubeNWords(Cube) ((Cube)->iLast > 1)
134 // getting one data bit
135 #define Mvc_CubeWhichWord(Bit) ((Bit) >> BITS_PER_WORD_LOG)
136 #define Mvc_CubeWhichBit(Bit) ((Bit) & BITS_PER_WORD_MINUS)
137 // accessing individual bits
138 #define Mvc_CubeBitValue(Cube, Bit) (((Cube)->pData[Mvc_CubeWhichWord(Bit)] & (((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit)))) > 0)
139 #define Mvc_CubeBitInsert(Cube, Bit) ((Cube)->pData[Mvc_CubeWhichWord(Bit)] |= (((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit))))
140 #define Mvc_CubeBitRemove(Cube, Bit) ((Cube)->pData[Mvc_CubeWhichWord(Bit)] &= ~(((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit))))
141 // accessing values of the binary variables
142 #define Mvc_CubeVarValue(Cube, Var) (((Cube)->pData[Mvc_CubeWhichWord(2*(Var))] >> (Mvc_CubeWhichBit(2*(Var)))) & ((Mvc_CubeWord_t)3))
143 
144 // various macros
145 
146 // cleaning the data bits of the cube
147 #define Mvc_Cube1BitClean( Cube )\
148  ((Cube)->pData[0] = 0)
149 #define Mvc_Cube2BitClean( Cube )\
150  (((Cube)->pData[0] = 0),\
151  ((Cube)->pData[1] = 0))
152 #define Mvc_CubeNBitClean( Cube )\
153 {\
154  int _i_;\
155  for( _i_ = (Cube)->iLast; _i_ >= 0; _i_--)\
156  (Cube)->pData[_i_] = 0;\
157 }
158 
159 // cleaning the unused part of the lat word
160 #define Mvc_CubeBitCleanUnused( Cube )\
161  ((Cube)->pData[(Cube)->iLast] &= (BITS_FULL >> (Cube)->nUnused))
162 
163 // filling the used data bits with 1's
164 #define Mvc_Cube1BitFill( Cube )\
165  (Cube)->pData[0] = (BITS_FULL >> (Cube)->nUnused);
166 #define Mvc_Cube2BitFill( Cube )\
167  (((Cube)->pData[0] = BITS_FULL),\
168  ((Cube)->pData[1] = (BITS_FULL >> (Cube)->nUnused)))
169 #define Mvc_CubeNBitFill( Cube )\
170 {\
171  int _i_;\
172  (Cube)->pData[(Cube)->iLast] = (BITS_FULL >> (Cube)->nUnused);\
173  for( _i_ = (Cube)->iLast - 1; _i_ >= 0; _i_-- )\
174  (Cube)->pData[_i_] = BITS_FULL;\
175 }
176 
177 // complementing the data bits
178 #define Mvc_Cube1BitNot( Cube )\
179  ((Cube)->pData[0] ^= (BITS_FULL >> (Cube)->nUnused))
180 #define Mvc_Cube2BitNot( Cube )\
181  (((Cube)->pData[0] ^= BITS_FULL),\
182  ((Cube)->pData[1] ^= (BITS_FULL >> (Cube)->nUnused)))
183 #define Mvc_CubeNBitNot( Cube )\
184 {\
185  int _i_;\
186  (Cube)->pData[(Cube)->iLast] ^= (BITS_FULL >> (Cube)->nUnused);\
187  for( _i_ = (Cube)->iLast - 1; _i_ >= 0; _i_-- )\
188  (Cube)->pData[_i_] ^= BITS_FULL;\
189 }
190 
191 #define Mvc_Cube1BitCopy( Cube1, Cube2 )\
192  (((Cube1)->pData[0]) = ((Cube2)->pData[0]))
193 #define Mvc_Cube2BitCopy( Cube1, Cube2 )\
194  ((((Cube1)->pData[0]) = ((Cube2)->pData[0])),\
195  (((Cube1)->pData[1])= ((Cube2)->pData[1])))
196 #define Mvc_CubeNBitCopy( Cube1, Cube2 )\
197 {\
198  int _i_;\
199  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
200  ((Cube1)->pData[_i_]) = ((Cube2)->pData[_i_]);\
201 }
202 
203 #define Mvc_Cube1BitOr( CubeR, Cube1, Cube2 )\
204  (((CubeR)->pData[0]) = ((Cube1)->pData[0] | (Cube2)->pData[0]))
205 #define Mvc_Cube2BitOr( CubeR, Cube1, Cube2 )\
206  ((((CubeR)->pData[0]) = ((Cube1)->pData[0] | (Cube2)->pData[0])),\
207  (((CubeR)->pData[1]) = ((Cube1)->pData[1] | (Cube2)->pData[1])))
208 #define Mvc_CubeNBitOr( CubeR, Cube1, Cube2 )\
209 {\
210  int _i_;\
211  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
212  (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] | (Cube2)->pData[_i_]));\
213 }
214 
215 #define Mvc_Cube1BitExor( CubeR, Cube1, Cube2 )\
216  (((CubeR)->pData[0]) = ((Cube1)->pData[0] ^ (Cube2)->pData[0]))
217 #define Mvc_Cube2BitExor( CubeR, Cube1, Cube2 )\
218  ((((CubeR)->pData[0]) = ((Cube1)->pData[0] ^ (Cube2)->pData[0])),\
219  (((CubeR)->pData[1]) = ((Cube1)->pData[1] ^ (Cube2)->pData[1])))
220 #define Mvc_CubeNBitExor( CubeR, Cube1, Cube2 )\
221 {\
222  int _i_;\
223  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
224  (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] ^ (Cube2)->pData[_i_]));\
225 }
226 
227 #define Mvc_Cube1BitAnd( CubeR, Cube1, Cube2 )\
228  (((CubeR)->pData[0]) = ((Cube1)->pData[0] & (Cube2)->pData[0]))
229 #define Mvc_Cube2BitAnd( CubeR, Cube1, Cube2 )\
230  ((((CubeR)->pData[0]) = ((Cube1)->pData[0] & (Cube2)->pData[0])),\
231  (((CubeR)->pData[1]) = ((Cube1)->pData[1] & (Cube2)->pData[1])))
232 #define Mvc_CubeNBitAnd( CubeR, Cube1, Cube2 )\
233 {\
234  int _i_;\
235  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
236  (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] & (Cube2)->pData[_i_]));\
237 }
238 
239 #define Mvc_Cube1BitSharp( CubeR, Cube1, Cube2 )\
240  (((CubeR)->pData[0]) = ((Cube1)->pData[0] & ~((Cube2)->pData[0])))
241 #define Mvc_Cube2BitSharp( CubeR, Cube1, Cube2 )\
242  ((((CubeR)->pData[0]) = ((Cube1)->pData[0] & ~((Cube2)->pData[0]))),\
243  (((CubeR)->pData[1]) = ((Cube1)->pData[1] & ~((Cube2)->pData[1]))))
244 #define Mvc_CubeNBitSharp( CubeR, Cube1, Cube2 )\
245 {\
246  int _i_;\
247  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
248  (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] & ~(Cube2)->pData[_i_]));\
249 }
250 
251 #define Mvc_Cube1BitEmpty( Res, Cube )\
252  (Res = ((Cube)->pData[0] == 0))
253 #define Mvc_Cube2BitEmpty( Res, Cube )\
254  (Res = ((Cube)->pData[0] == 0 && (Cube)->pData[1] == 0))
255 #define Mvc_CubeNBitEmpty( Res, Cube )\
256 {\
257  int _i_; Res = 1;\
258  for (_i_ = (Cube)->iLast; _i_ >= 0; _i_--)\
259  if ( (Cube)->pData[_i_] )\
260  { Res = 0; break; }\
261 }
262 
263 #define Mvc_Cube1BitEqual( Res, Cube1, Cube2 )\
264  (Res = (((Cube1)->pData[0]) == ((Cube2)->pData[0])))
265 #define Mvc_Cube2BitEqual( Res, Cube1, Cube2 )\
266  (Res = ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) &&\
267  (((Cube1)->pData[1]) == ((Cube2)->pData[1]))))
268 #define Mvc_CubeNBitEqual( Res, Cube1, Cube2 )\
269 {\
270  int _i_; Res = 1;\
271  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
272  if (((Cube1)->pData[_i_]) != ((Cube2)->pData[_i_]))\
273  { Res = 0; break; }\
274 }
275 
276 #define Mvc_Cube1BitLess( Res, Cube1, Cube2 )\
277  (Res = (((Cube1)->pData[0]) < ((Cube2)->pData[0])))
278 #define Mvc_Cube2BitLess( Res, Cube1, Cube2 )\
279  (Res = ((((Cube1)->pData[0]) < ((Cube2)->pData[0])) ||\
280  ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) && (((Cube1)->pData[1]) < ((Cube2)->pData[1])))))
281 #define Mvc_CubeNBitLess( Res, Cube1, Cube2 )\
282 {\
283  int _i_; Res = 1;\
284  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
285  if (((Cube1)->pData[_i_]) >= ((Cube2)->pData[_i_]))\
286  { Res = 0; break; }\
287 }
288 
289 #define Mvc_Cube1BitMore( Res, Cube1, Cube2 )\
290  (Res = (((Cube1)->pData[0]) > ((Cube2)->pData[0])))
291 #define Mvc_Cube2BitMore( Res, Cube1, Cube2 )\
292  (Res = ((((Cube1)->pData[0]) > ((Cube2)->pData[0])) ||\
293  ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) && (((Cube1)->pData[1]) > ((Cube2)->pData[1])))))
294 #define Mvc_CubeNBitMore( Res, Cube1, Cube2 )\
295 {\
296  int _i_; Res = 1;\
297  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
298  if (((Cube1)->pData[_i_]) <= ((Cube2)->pData[_i_]))\
299  { Res = 0; break; }\
300 }
301 
302 #define Mvc_Cube1BitNotImpl( Res, Cube1, Cube2 )\
303  (Res = (((Cube1)->pData[0]) & ~((Cube2)->pData[0])))
304 #define Mvc_Cube2BitNotImpl( Res, Cube1, Cube2 )\
305  (Res = ((((Cube1)->pData[0]) & ~((Cube2)->pData[0])) ||\
306  (((Cube1)->pData[1]) & ~((Cube2)->pData[1]))))
307 #define Mvc_CubeNBitNotImpl( Res, Cube1, Cube2 )\
308 {\
309  int _i_; Res = 0;\
310  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
311  if (((Cube1)->pData[_i_]) & ~((Cube2)->pData[_i_]))\
312  { Res = 1; break; }\
313 }
314 
315 #define Mvc_Cube1BitDisjoint( Res, Cube1, Cube2 )\
316  (Res = ((((Cube1)->pData[0]) & ((Cube2)->pData[0])) == 0 ))
317 #define Mvc_Cube2BitDisjoint( Res, Cube1, Cube2 )\
318  (Res = (((((Cube1)->pData[0]) & ((Cube2)->pData[0])) == 0 ) &&\
319  ((((Cube1)->pData[1]) & ((Cube2)->pData[1])) == 0 )))
320 #define Mvc_CubeNBitDisjoint( Res, Cube1, Cube2 )\
321 {\
322  int _i_; Res = 1;\
323  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
324  if (((Cube1)->pData[_i_]) & ((Cube2)->pData[_i_]))\
325  { Res = 0; break; }\
326 }
327 
328 #define Mvc_Cube1BitEqualUnderMask( Res, Cube1, Cube2, Mask )\
329  (Res = ((((Cube1)->pData[0]) & ((Mask)->pData[0])) == (((Cube2)->pData[0]) & ((Mask)->pData[0]))))
330 #define Mvc_Cube2BitEqualUnderMask( Res, Cube1, Cube2, Mask )\
331  (Res = (((((Cube1)->pData[0]) & ((Mask)->pData[0])) == (((Cube2)->pData[0]) & ((Mask)->pData[0]))) &&\
332  ((((Cube1)->pData[1]) & ((Mask)->pData[1])) == (((Cube2)->pData[1]) & ((Mask)->pData[1])))))
333 #define Mvc_CubeNBitEqualUnderMask( Res, Cube1, Cube2, Mask )\
334 {\
335  int _i_; Res = 1;\
336  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
337  if ((((Cube1)->pData[_i_]) & ((Mask)->pData[_i_])) != (((Cube2)->pData[_i_]) & ((Mask)->pData[_i_])))\
338  { Res = 0; break; }\
339 }
340 
341 #define Mvc_Cube1BitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
342  (Res = ((((Cube1)->pData[0]) | ((Mask)->pData[0])) == (((Cube2)->pData[0]) | ((Mask)->pData[0]))))
343 #define Mvc_Cube2BitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
344  (Res = (((((Cube1)->pData[0]) | ((Mask)->pData[0])) == (((Cube2)->pData[0]) | ((Mask)->pData[0]))) &&\
345  ((((Cube1)->pData[1]) | ((Mask)->pData[1])) == (((Cube2)->pData[1]) | ((Mask)->pData[1])))))
346 #define Mvc_CubeNBitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
347 {\
348  int _i_; Res = 1;\
349  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
350  if ((((Cube1)->pData[_i_]) | ((Mask)->pData[_i_])) != (((Cube2)->pData[_i_]) | ((Mask)->pData[_i_])))\
351  { Res = 0; break; }\
352 }
353 
354 #define Mvc_Cube1BitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
355  (Res = ((((Cube1)->pData[0]) & ((Cube2)->pData[0]) & ((Mask)->pData[0])) > 0))
356 #define Mvc_Cube2BitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
357  (Res = (((((Cube1)->pData[0]) & ((Cube2)->pData[0]) & ((Mask)->pData[0])) > 0) ||\
358  ((((Cube1)->pData[1]) & ((Cube2)->pData[1]) & ((Mask)->pData[1])) > 0)))
359 #define Mvc_CubeNBitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
360 {\
361  int _i_; Res = 0;\
362  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
363  if (((Cube1)->pData[_i_]) & ((Cube2)->pData[_i_]) & ((Mask)->pData[_i_]))\
364  { Res = 1; break; }\
365 }
366 
367 #define Mvc_Cube1BitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
368  (Res = (((Mask)->pData[0]) & ((Cube1)->pData[0]) & ~((Cube2)->pData[0])))
369 #define Mvc_Cube2BitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
370  (Res = ((((Mask)->pData[0]) & ((Cube1)->pData[0]) & ~((Cube2)->pData[0])) ||\
371  (((Mask)->pData[1]) & ((Cube1)->pData[1]) & ~((Cube2)->pData[1]))))
372 #define Mvc_CubeNBitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
373 {\
374  int _i_; Res = 0;\
375  for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
376  if (((Mask)->pData[_i_]) & ((Cube1)->pData[_i_]) & ~((Cube2)->pData[_i_]))\
377  { Res = 1; break; }\
378 }
379 
380 // the following macros make no assumption about the cube's bitset size
381 #define Mvc_CubeBitClean( Cube )\
382  if ( Mvc_Cube1Words(Cube) ) { Mvc_Cube1BitClean( Cube ); }\
383  else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitClean( Cube ); }\
384  else { Mvc_CubeNBitClean( Cube ); }
385 #define Mvc_CubeBitFill( Cube )\
386  if ( Mvc_Cube1Words(Cube) ) { Mvc_Cube1BitFill( Cube ); }\
387  else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitFill( Cube ); }\
388  else { Mvc_CubeNBitFill( Cube ); }
389 #define Mvc_CubeBitNot( Cube )\
390  if ( Mvc_Cube1Words(Cube) ) { Mvc_Cube1BitNot( Cube ); }\
391  else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitNot( Cube ); }\
392  else { Mvc_CubeNBitNot( Cube ); }
393 #define Mvc_CubeBitCopy( Cube1, Cube2 )\
394  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitCopy( Cube1, Cube2 ); }\
395  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitCopy( Cube1, Cube2 ); }\
396  else { Mvc_CubeNBitCopy( Cube1, Cube2 ); }
397 #define Mvc_CubeBitOr( CubeR, Cube1, Cube2 )\
398  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitOr( CubeR, Cube1, Cube2 ); }\
399  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitOr( CubeR, Cube1, Cube2 ); }\
400  else { Mvc_CubeNBitOr( CubeR, Cube1, Cube2 ); }
401 #define Mvc_CubeBitExor( CubeR, Cube1, Cube2 )\
402  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitExor( CubeR, Cube1, Cube2 ); }\
403  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitExor( CubeR, Cube1, Cube2 ); }\
404  else { Mvc_CubeNBitExor( CubeR, Cube1, Cube2 ); }
405 #define Mvc_CubeBitAnd( CubeR, Cube1, Cube2 )\
406  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitAnd( CubeR, Cube1, Cube2 ); }\
407  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitAnd( CubeR, Cube1, Cube2 ); }\
408  else { Mvc_CubeNBitAnd( CubeR, Cube1, Cube2 ); }
409 #define Mvc_CubeBitSharp( CubeR, Cube1, Cube2 )\
410  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitSharp( CubeR, Cube1, Cube2 ); }\
411  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitSharp( CubeR, Cube1, Cube2 ); }\
412  else { Mvc_CubeNBitSharp( CubeR, Cube1, Cube2 ); }
413 #define Mvc_CubeBitEmpty( Res, Cube )\
414  if ( Mvc_Cube1Words(Cube) ) { Mvc_Cube1BitEmpty( Res, Cube ); }\
415  else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitEmpty( Res, Cube ); }\
416  else { Mvc_CubeNBitEmpty( Res, Cube ); }
417 #define Mvc_CubeBitEqual( Res, Cube1, Cube2 )\
418  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitEqual( Res, Cube1, Cube2 ); }\
419  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqual( Res, Cube1, Cube2 ); }\
420  else { Mvc_CubeNBitEqual( Res, Cube1, Cube2 ); }
421 #define Mvc_CubeBitLess( Res, Cube1, Cube2 )\
422  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitLess( Res, Cube1, Cube2 ); }\
423  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitLess( Res, Cube1, Cube2 ); }\
424  else { Mvc_CubeNBitLess( Res, Cube1, Cube2 ); }
425 #define Mvc_CubeBitMore( Res, Cube1, Cube2 )\
426  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitMore( Res, Cube1, Cube2 ); }\
427  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitMore( Res, Cube1, Cube2 ); }\
428  else { Mvc_CubeNBitMore( Res, Cube1, Cube2 ); }
429 #define Mvc_CubeBitNotImpl( Res, Cube1, Cube2 )\
430  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitNotImpl( Res, Cube1, Cube2 ); }\
431  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitNotImpl( Res, Cube1, Cube2 ); }\
432  else { Mvc_CubeNBitNotImpl( Res, Cube1, Cube2 ); }
433 #define Mvc_CubeBitDisjoint( Res, Cube1, Cube2 )\
434  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitDisjoint( Res, Cube1, Cube2 ); }\
435  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitDisjoint( Res, Cube1, Cube2 ); }\
436  else { Mvc_CubeNBitDisjoint( Res, Cube1, Cube2 ); }
437 #define Mvc_CubeBitEqualUnderMask( Res, Cube1, Cube2, Mask )\
438  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitEqualUnderMask( Res, Cube1, Cube2, Mask ); }\
439  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqualUnderMask( Res, Cube1, Cube2, Mask ); }\
440  else { Mvc_CubeNBitEqualUnderMask( Res, Cube1, Cube2, Mask ); }
441 #define Mvc_CubeBitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
442  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }\
443  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }\
444  else { Mvc_CubeNBitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }
445 #define Mvc_CubeBitIntersectUnderMask( Res, Cube1, Cube2, Mask )\
446  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }\
447  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }\
448  else { Mvc_CubeNBitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }
449 #define Mvc_CubeBitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
450  if ( Mvc_Cube1Words(Cube1) ) { Mvc_Cube1BitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }\
451  else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }\
452  else { Mvc_CubeNBitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }
453 
454 
455 // managing linked lists
456 #define Mvc_ListAddCubeHead( pList, pCube )\
457  {\
458  if ( pList->pHead == NULL )\
459  {\
460  Mvc_CubeSetNext( pCube, NULL );\
461  pList->pHead = pCube;\
462  pList->pTail = pCube;\
463  }\
464  else\
465  {\
466  Mvc_CubeSetNext( pCube, pList->pHead );\
467  pList->pHead = pCube;\
468  }\
469  pList->nItems++;\
470  }
471 #define Mvc_ListAddCubeTail( pList, pCube )\
472  {\
473  if ( pList->pHead == NULL )\
474  pList->pHead = pCube;\
475  else\
476  Mvc_CubeSetNext( pList->pTail, pCube );\
477  pList->pTail = pCube;\
478  Mvc_CubeSetNext( pCube, NULL );\
479  pList->nItems++;\
480  }
481 #define Mvc_ListDeleteCube( pList, pPrev, pCube )\
482 {\
483  if ( pPrev == NULL )\
484  pList->pHead = pCube->pNext;\
485  else\
486  pPrev->pNext = pCube->pNext;\
487  if ( pList->pTail == pCube )\
488  {\
489  assert( pCube->pNext == NULL );\
490  pList->pTail = pPrev;\
491  }\
492  pList->nItems--;\
493 }
494 
495 // managing linked lists inside the cover
496 #define Mvc_CoverAddCubeHead( pCover, pCube )\
497 {\
498  Mvc_List_t * pList = &pCover->lCubes;\
499  Mvc_ListAddCubeHead( pList, pCube );\
500 }
501 #define Mvc_CoverAddCubeTail( pCover, pCube )\
502 {\
503  Mvc_List_t * pList = &pCover->lCubes;\
504  Mvc_ListAddCubeTail( pList, pCube );\
505 }
506 #define Mvc_CoverDeleteCube( pCover, pPrev, pCube )\
507 {\
508  Mvc_List_t * pList = &pCover->lCubes;\
509  Mvc_ListDeleteCube( pList, pPrev, pCube );\
510 }
511 
512 
513 
514 
515 
516 
517 // iterator through the cubes in the cube list
518 #define Mvc_ListForEachCube( List, Cube )\
519  for ( Cube = List->pHead;\
520  Cube;\
521  Cube = Cube->pNext )
522 #define Mvc_ListForEachCubeSafe( List, Cube, Cube2 )\
523  for ( Cube = List->pHead, Cube2 = (Cube? Cube->pNext: NULL);\
524  Cube;\
525  Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
526 
527 // iterator through cubes in the cover
528 #define Mvc_CoverForEachCube( Cover, Cube )\
529  for ( Cube = (Cover)->lCubes.pHead;\
530  Cube;\
531  Cube = Cube->pNext )
532 #define Mvc_CoverForEachCubeWithIndex( Cover, Cube, Index )\
533  for ( Index = 0, Cube = (Cover)->lCubes.pHead;\
534  Cube;\
535  Index++, Cube = Cube->pNext )
536 #define Mvc_CoverForEachCubeSafe( Cover, Cube, Cube2 )\
537  for ( Cube = (Cover)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
538  Cube;\
539  Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
540 
541 // iterator which starts from the given cube
542 #define Mvc_CoverForEachCubeStart( Start, Cube )\
543  for ( Cube = Start;\
544  Cube;\
545  Cube = Cube->pNext )
546 #define Mvc_CoverForEachCubeStartSafe( Start, Cube, Cube2 )\
547  for ( Cube = Start, Cube2 = (Cube? Cube->pNext: NULL);\
548  Cube;\
549  Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
550 
551 
552 // iterator through literals of the cube
553 #define Mvc_CubeForEachBit( Cover, Cube, iBit, Value )\
554  for ( iBit = 0;\
555  iBit < Cover->nBits && ((Value = Mvc_CubeBitValue(Cube,iBit))>=0);\
556  iBit++ )
557 // iterator through values of binary variables
558 #define Mvc_CubeForEachVarValue( Cover, Cube, iVar, Value )\
559  for ( iVar = 0;\
560  iVar < Cover->nBits/2 && (Value = Mvc_CubeVarValue(Cube,iVar));\
561  iVar++ )
562 
563 
564 // macros which work with memory
565 // MEM_ALLOC: allocate the given number (Size) of items of type (Type)
566 // MEM_FREE: deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
567 #define MEM_ALLOC( Manager, Type, Size ) ((Type *)ABC_ALLOC( char, (Size) * sizeof(Type) ))
568 #define MEM_FREE( Manager, Type, Size, Pointer ) if ( Pointer ) { ABC_FREE(Pointer); Pointer = NULL; }
569 
570 ////////////////////////////////////////////////////////////////////////
571 /// FUNCTION DEFINITIONS ///
572 ////////////////////////////////////////////////////////////////////////
573 
574 /*=== mvcApi.c ====================================================*/
575 extern int Mvc_CoverReadWordNum( Mvc_Cover_t * pCover );
576 extern int Mvc_CoverReadBitNum( Mvc_Cover_t * pCover );
577 extern int Mvc_CoverReadCubeNum( Mvc_Cover_t * pCover );
578 extern Mvc_Cube_t * Mvc_CoverReadCubeHead( Mvc_Cover_t * pCover );
579 extern Mvc_Cube_t * Mvc_CoverReadCubeTail( Mvc_Cover_t * pCover );
580 extern Mvc_List_t * Mvc_CoverReadCubeList( Mvc_Cover_t * pCover );
581 extern int Mvc_ListReadCubeNum( Mvc_List_t * pList );
582 extern Mvc_Cube_t * Mvc_ListReadCubeHead( Mvc_List_t * pList );
583 extern Mvc_Cube_t * Mvc_ListReadCubeTail( Mvc_List_t * pList );
584 extern void Mvc_CoverSetCubeNum( Mvc_Cover_t * pCover,int nItems );
585 extern void Mvc_CoverSetCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
586 extern void Mvc_CoverSetCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
587 extern void Mvc_CoverSetCubeList( Mvc_Cover_t * pCover, Mvc_List_t * pList );
588 extern int Mvc_CoverIsEmpty( Mvc_Cover_t * pCover );
589 extern int Mvc_CoverIsTautology( Mvc_Cover_t * pCover );
590 extern int Mvc_CoverIsBinaryBuffer( Mvc_Cover_t * pCover );
591 extern void Mvc_CoverMakeEmpty( Mvc_Cover_t * pCover );
592 extern void Mvc_CoverMakeTautology( Mvc_Cover_t * pCover );
593 extern Mvc_Cover_t * Mvc_CoverCreateEmpty( Mvc_Cover_t * pCover );
595 /*=== mvcCover.c ====================================================*/
596 extern Mvc_Cover_t * Mvc_CoverAlloc( Mvc_Manager_t * pMem, int nBits );
597 extern Mvc_Cover_t * Mvc_CoverCreateConst( Mvc_Manager_t * pMem, int nBits, int Phase );
598 extern Mvc_Cover_t * Mvc_CoverClone( Mvc_Cover_t * pCover );
599 extern Mvc_Cover_t * Mvc_CoverDup( Mvc_Cover_t * pCover );
600 extern void Mvc_CoverFree( Mvc_Cover_t * pCover );
601 extern void Mvc_CoverAllocateMask( Mvc_Cover_t * pCover );
602 extern void Mvc_CoverAllocateArrayLits( Mvc_Cover_t * pCover );
603 extern void Mvc_CoverAllocateArrayCubes( Mvc_Cover_t * pCover );
604 extern void Mvc_CoverDeallocateMask( Mvc_Cover_t * pCover );
605 extern void Mvc_CoverDeallocateArrayLits( Mvc_Cover_t * pCover );
606 /*=== mvcCube.c ====================================================*/
607 extern Mvc_Cube_t * Mvc_CubeAlloc( Mvc_Cover_t * pCover );
608 extern Mvc_Cube_t * Mvc_CubeDup( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
609 extern void Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
610 extern void Mvc_CubeBitRemoveDcs( Mvc_Cube_t * pCube );
611 /*=== mvcCompare.c ====================================================*/
612 extern int Mvc_CubeCompareInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
613 extern int Mvc_CubeCompareSizeAndInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
614 extern int Mvc_CubeCompareIntUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
615 extern int Mvc_CubeCompareIntOutsideMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
616 extern int Mvc_CubeCompareIntOutsideAndUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
617 /*=== mvcDd.c ====================================================*/
618 /*
619 extern DdNode * Mvc_CoverConvertToBdd( DdManager * dd, Mvc_Cover_t * pCover );
620 extern DdNode * Mvc_CoverConvertToZdd( DdManager * dd, Mvc_Cover_t * pCover );
621 extern DdNode * Mvc_CoverConvertToZdd2( DdManager * dd, Mvc_Cover_t * pCover );
622 extern DdNode * Mvc_CubeConvertToBdd( DdManager * dd, Mvc_Cube_t * pCube );
623 extern DdNode * Mvc_CubeConvertToZdd( DdManager * dd, Mvc_Cube_t * pCube );
624 extern DdNode * Mvc_CubeConvertToZdd2( DdManager * dd, Mvc_Cube_t * pCube );
625 */
626 /*=== mvcDivisor.c ====================================================*/
627 extern Mvc_Cover_t * Mvc_CoverDivisor( Mvc_Cover_t * pCover );
628 /*=== mvcDivide.c ====================================================*/
629 extern void Mvc_CoverDivide( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
630 extern void Mvc_CoverDivideInternal( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
631 extern void Mvc_CoverDivideByLiteral( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
632 extern void Mvc_CoverDivideByCube( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
633 extern void Mvc_CoverDivideByLiteralQuo( Mvc_Cover_t * pCover, int iLit );
634 /*=== mvcList.c ====================================================*/
635 // these functions are available as macros
636 extern void Mvc_ListAddCubeHead_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
637 extern void Mvc_ListAddCubeTail_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
638 extern void Mvc_ListDeleteCube_( Mvc_List_t * pList, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
639 extern void Mvc_CoverAddCubeHead_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
640 extern void Mvc_CoverAddCubeTail_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
641 extern void Mvc_CoverDeleteCube_( Mvc_Cover_t * pCover, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
642 extern void Mvc_CoverAddDupCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
643 extern void Mvc_CoverAddDupCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
644 // other functions
645 extern void Mvc_CoverAddLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
646 extern void Mvc_CoverDeleteLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
647 extern void Mvc_CoverList2Array( Mvc_Cover_t * pCover );
648 extern void Mvc_CoverArray2List( Mvc_Cover_t * pCover );
649 extern Mvc_Cube_t * Mvc_ListGetTailFromHead( Mvc_Cube_t * pHead );
650 /*=== mvcPrint.c ====================================================*/
651 extern void Mvc_CoverPrint( Mvc_Cover_t * pCover );
652 extern void Mvc_CubePrint( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
653 extern void Mvc_CoverPrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover );
654 extern void Mvc_CubePrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
655 /*=== mvcSort.c ====================================================*/
656 extern void Mvc_CoverSort( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) );
657 /*=== mvcUtils.c ====================================================*/
658 extern void Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp );
659 extern int Mvc_CoverSupportSizeBinary( Mvc_Cover_t * pCover );
660 extern int Mvc_CoverSupportVarBelongs( Mvc_Cover_t * pCover, int iVar );
661 extern void Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube );
662 extern int Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover );
663 extern void Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover );
665 extern int Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
666 extern int Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover );
667 extern int Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube );
668 extern int Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] );
669 extern Mvc_Cover_t * Mvc_CoverRemap( Mvc_Cover_t * pCover, int * pVarsRem, int nVarsRem );
670 extern void Mvc_CoverInverse( Mvc_Cover_t * pCover );
672 extern Mvc_Cover_t * Mvc_CoverCofactor( Mvc_Cover_t * pCover, int iValue, int iValueOther );
673 extern Mvc_Cover_t * Mvc_CoverFlipVar( Mvc_Cover_t * pCover, int iValue0, int iValue1 );
674 extern Mvc_Cover_t * Mvc_CoverUnivQuantify( Mvc_Cover_t * p, int iValueA0, int iValueA1, int iValueB0, int iValueB1 );
675 extern Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar );
676 extern int Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue );
677 //extern Mvc_Cover_t * Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew );
678 extern Mvc_Cover_t * Mvc_CoverTranspose( Mvc_Cover_t * pCover );
679 extern int Mvc_UtilsCheckUnusedZeros( Mvc_Cover_t * pCover );
680 /*=== mvcLits.c ====================================================*/
681 extern int Mvc_CoverAnyLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
682 extern int Mvc_CoverBestLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
683 extern int Mvc_CoverWorstLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
684 extern Mvc_Cover_t * Mvc_CoverBestLiteralCover( Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
685 extern int Mvc_CoverFirstCubeFirstLit( Mvc_Cover_t * pCover );
686 extern int Mvc_CoverCountLiterals( Mvc_Cover_t * pCover );
687 extern int Mvc_CoverIsOneLiteral( Mvc_Cover_t * pCover );
688 /*=== mvcOpAlg.c ====================================================*/
689 extern Mvc_Cover_t * Mvc_CoverAlgebraicMultiply( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
690 extern Mvc_Cover_t * Mvc_CoverAlgebraicSubtract( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
691 extern int Mvc_CoverAlgebraicEqual( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
692 /*=== mvcOpBool.c ====================================================*/
693 extern Mvc_Cover_t * Mvc_CoverBooleanOr( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
694 extern Mvc_Cover_t * Mvc_CoverBooleanAnd( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
695 extern int Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
696 
697 /*=== mvcContain.c ====================================================*/
698 extern int Mvc_CoverContain( Mvc_Cover_t * pCover );
699 /*=== mvcTau.c ====================================================*/
700 extern int Mvc_CoverTautology( Mvc_Data_t * p, Mvc_Cover_t * pCover );
701 /*=== mvcCompl.c ====================================================*/
702 extern Mvc_Cover_t * Mvc_CoverComplement( Mvc_Data_t * p, Mvc_Cover_t * pCover );
703 /*=== mvcSharp.c ====================================================*/
705 extern int Mvc_CoverDist0Cubes( Mvc_Data_t * pData, Mvc_Cube_t * pA, Mvc_Cube_t * pB );
706 extern void Mvc_CoverIntersectCubes( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
707 extern int Mvc_CoverIsIntersecting( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
708 extern void Mvc_CoverAppendCubes( Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
709 extern void Mvc_CoverCopyAndAppendCubes( Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
710 extern void Mvc_CoverRemoveCubes( Mvc_Cover_t * pC );
711 
712 /*=== mvcReshape.c ====================================================*/
713 extern void Mvc_CoverMinimizeByReshape( Mvc_Data_t * pData, Mvc_Cover_t * pCover );
714 
715 /*=== mvcMerge.c ====================================================*/
716 extern void Mvc_CoverDist1Merge( Mvc_Data_t * p, Mvc_Cover_t * pCover );
717 
718 /*=== mvcData.c ====================================================*/
719 //extern Mvc_Data_t * Mvc_CoverDataAlloc( Vm_VarMap_t * pVm, Mvc_Cover_t * pCover );
720 //extern void Mvc_CoverDataFree( Mvc_Data_t * p, Mvc_Cover_t * pCover );
721 
722 /*=== mvcMan.c ====================================================*/
723 extern void Mvc_ManagerFree( Mvc_Manager_t * p );
727 extern Mvc_Manager_t * Mvc_ManagerFreeCover( Mvc_Cover_t * pCover );
728 extern Mvc_Manager_t * Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords );
729 
730 
731 
733 
734 #endif
735 
736 ////////////////////////////////////////////////////////////////////////
737 /// END OF FILE ///
738 ////////////////////////////////////////////////////////////////////////
739 
Mvc_Cube_t ** pCubes
Definition: mvc.h:89
int Mvc_CoverContain(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcContain.c:47
void Mvc_CoverFree(Mvc_Cover_t *pCover)
Definition: mvcCover.c:138
int Mvc_CoverIsIntersecting(Mvc_Data_t *pData, Mvc_Cover_t *pC1, Mvc_Cover_t *pC2)
Mvc_Cube_t * Mvc_CubeDup(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcCube.c:94
Mvc_Manager_t * Mvc_ManagerFreeCube(Mvc_Cover_t *pCube, int nWords)
void Mvc_CoverDeleteLiteralsOfCube(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:265
Mvc_Cover_t * Mvc_CoverBooleanAnd(Mvc_Data_t *p, Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
void Mvc_CoverAllocateArrayLits(Mvc_Cover_t *pCover)
Definition: mvcCover.c:185
int Mvc_CoverSupportVarBelongs(Mvc_Cover_t *pCover, int iVar)
Definition: mvcUtils.c:130
int Mvc_CoverReadWordNum(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcApi.c:43
int Mvc_CoverDist0Cubes(Mvc_Data_t *pData, Mvc_Cube_t *pA, Mvc_Cube_t *pB)
Mvc_Cover_t * Mvc_CoverCommonCubeCover(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:220
void Mvc_CoverDivideInternal(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
Definition: mvcDivide.c:81
int nWords
Definition: mvc.h:85
int Mvc_CoverReadBitNum(Mvc_Cover_t *pCover)
Definition: mvcApi.c:44
unsigned int Mvc_CubeWord_t
STRUCTURE DEFINITIONS ///.
Definition: mvc.h:55
void Mvc_CoverRemoveCubes(Mvc_Cover_t *pC)
void Mvc_CoverPrint(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcPrint.c:47
Mvc_Cover_t * Mvc_CoverAlgebraicMultiply(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
DECLARATIONS ///.
Definition: mvcOpAlg.c:43
unsigned fEssen
Definition: mvc.h:69
Mvc_Cover_t * Mvc_CoverCreateConst(Mvc_Manager_t *pMem, int nBits, int Phase)
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Mvc_CoverDeallocateMask(Mvc_Cover_t *pCover)
Definition: mvcCover.c:224
void Mvc_CoverDist1Merge(Mvc_Data_t *p, Mvc_Cover_t *pCover)
void Mvc_CoverAddCubeTail_(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:149
int Mvc_CoverIsOneLiteral(Mvc_Cover_t *pCover)
Definition: mvcLits.c:324
int Mvc_CoverIsBinaryBuffer(Mvc_Cover_t *pCover)
Definition: mvcApi.c:135
Mvc_Manager_t * Mvc_ManagerAllocCube(int nWords)
Mvc_Cube_t * Mvc_CoverReadCubeTail(Mvc_Cover_t *pCover)
Definition: mvcApi.c:47
Mvc_Cover_t * Mvc_CoverCofactor(Mvc_Cover_t *pCover, int iValue, int iValueOther)
Definition: mvcUtils.c:518
void Mvc_CoverDivideByCube(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
Definition: mvcDivide.c:269
Mvc_Cover_t ** Mvc_CoverCofactors(Mvc_Data_t *pData, Mvc_Cover_t *pCover, int iVar)
Extra_MmFixed_t * pMan1
Definition: mvc.h:111
Extra_MmFixed_t * pMan4
Definition: mvc.h:113
int Mvc_CoverFirstCubeFirstLit(Mvc_Cover_t *pCover)
Definition: mvcLits.c:261
void Mvc_CoverMinimizeByReshape(Mvc_Data_t *pData, Mvc_Cover_t *pCover)
Mvc_Cube_t * ppTemp[3]
Definition: mvc.h:104
void Mvc_CoverSupport(Mvc_Cover_t *pCover, Mvc_Cube_t *pSupp)
FUNCTION DEFINITIONS ///.
Definition: mvcUtils.c:58
int nItems
Definition: mvc.h:79
Mvc_Cover_t * Mvc_CoverFlipVar(Mvc_Cover_t *pCover, int iValue0, int iValue1)
Definition: mvcUtils.c:546
Mvc_List_t * Mvc_CoverReadCubeList(Mvc_Cover_t *pCover)
Definition: mvcApi.c:48
int Mvc_ListReadCubeNum(Mvc_List_t *pList)
Definition: mvcApi.c:62
int Mvc_CubeCompareIntOutsideMask(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
Definition: mvcCompare.c:205
int Mvc_CoverWorstLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
Definition: mvcLits.c:162
int Mvc_CubeCompareSizeAndInt(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
Definition: mvcCompare.c:91
void Mvc_CoverSetCubeTail(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcApi.c:79
void Mvc_ListAddCubeTail_(Mvc_List_t *pList, Mvc_Cube_t *pCube)
Definition: mvcList.c:71
int Mvc_CoverAlgebraicEqual(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
Definition: mvcOpAlg.c:134
Mvc_Cover_t * Mvc_CoverRemap(Mvc_Cover_t *pCover, int *pVarsRem, int nVarsRem)
Definition: mvcUtils.c:400
void Mvc_CoverDeallocateArrayLits(Mvc_Cover_t *pCover)
Definition: mvcCover.c:241
void Mvc_CoverArray2List(Mvc_Cover_t *pCover)
Definition: mvcList.c:310
int nWords
Definition: abcNpn.c:127
void Mvc_CoverMakeCubeFree(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:198
Mvc_Cover_t * Mvc_CoverTranspose(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:804
int * pLits
Definition: mvc.h:91
void Mvc_CoverMakeEmpty(Mvc_Cover_t *pCover)
Definition: mvcApi.c:160
int Mvc_CoverBestLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
Definition: mvcLits.c:104
Mvc_Cover_t * Mvc_CoverUnivQuantify(Mvc_Cover_t *p, int iValueA0, int iValueA1, int iValueB0, int iValueB1)
Definition: mvcUtils.c:606
Mvc_CubeWord_t pData[1]
Definition: mvc.h:71
Mvc_Cover_t * Mvc_CoverRemoveDontCareLits(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:496
void Mvc_CoverDivide(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
FUNCTION DEFINITIONS ///.
Definition: mvcDivide.c:47
Mvc_Cube_t * Mvc_CubeAlloc(Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition: mvcCube.c:43
int Mvr_CoverCountLitsWithValue(Mvc_Data_t *pData, Mvc_Cover_t *pCover, int iVar, int iValue)
int nBinVars
Definition: mvc.h:101
int nUnused
Definition: mvc.h:86
void Mvc_CoverInverse(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:477
void Mvc_ManagerFree(Mvc_Manager_t *p)
Definition: mvcMan.c:67
Mvc_Manager_t * pMan
Definition: mvc.h:99
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition: mvcApi.c:45
void Mvc_CoverList2Array(Mvc_Cover_t *pCover)
Definition: mvcList.c:286
Mvc_Cube_t * pMask
Definition: mvc.h:92
Mvc_List_t lCubes
Definition: mvc.h:88
Mvc_Cube_t * pNext
Definition: mvc.h:65
int Mvc_UtilsCheckUnusedZeros(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:842
Mvc_Manager_t * Mvc_ManagerStart()
DECLARATIONS ///.
Definition: mvcMan.c:44
unsigned iLast
Definition: mvc.h:66
void Mvc_CoverIntersectCubes(Mvc_Data_t *pData, Mvc_Cover_t *pC1, Mvc_Cover_t *pC2)
int Mvc_CoverGetCubeSize(Mvc_Cube_t *pCube)
Definition: mvcUtils.c:308
int Mvc_CoverIsTautology(Mvc_Cover_t *pCover)
Definition: mvcApi.c:109
Mvc_Cube_t ** ppMasks
Definition: mvc.h:103
void Mvc_CoverMakeTautology(Mvc_Cover_t *pCover)
Definition: mvcApi.c:181
Mvc_Cover_t * Mvc_CoverClone(Mvc_Cover_t *pCover)
Definition: mvcCover.c:79
Mvc_Cover_t * Mvc_CoverSharp(Mvc_Data_t *p, Mvc_Cover_t *pA, Mvc_Cover_t *pB)
unsigned nUnused
Definition: mvc.h:67
Mvc_Manager_t * Mvc_ManagerAllocCover()
Mvc_Cube_t * pMaskBin
Definition: mvc.h:102
int Mvc_CubeCompareInt(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
DECLARATIONS ///.
Definition: mvcCompare.c:43
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
void Mvc_ListAddCubeHead_(Mvc_List_t *pList, Mvc_Cube_t *pCube)
DECLARATIONS ///.
Definition: mvcList.c:43
void Mvc_CoverPrintMv(Mvc_Data_t *pData, Mvc_Cover_t *pCover)
int Mvc_CubeCompareIntOutsideAndUnderMask(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
Definition: mvcCompare.c:265
void Mvc_CoverSetCubeHead(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcApi.c:78
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Mvc_Cube_t * pTail
Definition: mvc.h:78
void Mvc_CoverSetCubeList(Mvc_Cover_t *pCover, Mvc_List_t *pList)
Definition: mvcApi.c:80
Mvc_Cover_t * Mvc_CoverComplement(Mvc_Data_t *p, Mvc_Cover_t *pCover)
int Mvc_CubeCompareIntUnderMask(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
Definition: mvcCompare.c:146
Mvc_Cube_t * Mvc_ListGetTailFromHead(Mvc_Cube_t *pHead)
Definition: mvcList.c:351
void Mvc_CoverCopyAndAppendCubes(Mvc_Cover_t *pC1, Mvc_Cover_t *pC2)
unsigned fPrime
Definition: mvc.h:68
Mvc_Cube_t * pHead
Definition: mvc.h:77
void Mvc_CoverDivideByLiteralQuo(Mvc_Cover_t *pCover, int iLit)
Definition: mvcDivide.c:374
Mvc_Cover_t * Mvc_CoverBooleanOr(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
DECLARATIONS ///.
Definition: mvcOpBool.c:43
void Mvc_CoverAppendCubes(Mvc_Cover_t *pC1, Mvc_Cover_t *pC2)
void Mvc_CoverSetCubeNum(Mvc_Cover_t *pCover, int nItems)
Definition: mvcApi.c:77
int Mvc_CoverCheckSuppContainment(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
Definition: mvcUtils.c:247
Mvc_Cover_t * Mvc_CoverBestLiteralCover(Mvc_Cover_t *pCover, Mvc_Cover_t *pSimple)
Definition: mvcLits.c:223
int Mvc_CoverCountCubePairDiffs(Mvc_Cover_t *pCover, unsigned char pDiffs[])
Definition: mvcUtils.c:342
Extra_MmFixed_t * pMan2
Definition: mvc.h:112
void Mvc_CoverDivideByLiteral(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
Definition: mvcDivide.c:323
void Mvc_CoverCommonCube(Mvc_Cover_t *pCover, Mvc_Cube_t *pComCube)
Definition: mvcUtils.c:155
int Mvc_CoverIsCubeFree(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:176
Mvc_Cube_t * Mvc_ListReadCubeHead(Mvc_List_t *pList)
Definition: mvcApi.c:63
int Mvc_CoverSetCubeSizes(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:272
void Mvc_CoverAllocateArrayCubes(Mvc_Cover_t *pCover)
Definition: mvcCover.c:202
int nCubesAlloc
Definition: mvc.h:90
void Mvc_CoverAddDupCubeTail(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:221
Mvc_Cover_t * Mvc_CoverCreateEmpty(Mvc_Cover_t *pCover)
Definition: mvcApi.c:202
int nBits
Definition: mvc.h:87
int Mvc_CoverBooleanEqual(Mvc_Data_t *p, Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
void Mvc_CoverDeleteCube_(Mvc_Cover_t *pCover, Mvc_Cube_t *pPrev, Mvc_Cube_t *pCube)
Definition: mvcList.c:173
void Mvc_ListDeleteCube_(Mvc_List_t *pList, Mvc_Cube_t *pPrev, Mvc_Cube_t *pCube)
Definition: mvcList.c:94
Mvc_Cover_t * Mvc_CoverCreateTautology(Mvc_Cover_t *pCover)
Definition: mvcApi.c:220
void Mvc_CoverAddLiteralsOfCube(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:245
Extra_MmFixed_t * pManC
Definition: mvc.h:110
int Mvc_CoverCountLiterals(Mvc_Cover_t *pCover)
Definition: mvcLits.c:287
void Mvc_CubeBitRemoveDcs(Mvc_Cube_t *pCube)
Definition: mvcCube.c:159
Mvc_Cube_t * Mvc_ListReadCubeTail(Mvc_List_t *pList)
Definition: mvcApi.c:64
Mvc_Manager_t * Mvc_ManagerFreeCover(Mvc_Cover_t *pCover)
void Mvc_CubeFree(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcCube.c:114
void Mvc_CoverSort(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask, int(*pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *))
FuNCTION DEFINITIONS ///.
Definition: mvcSort.c:47
Mvc_Cover_t * Mvc_CoverAlgebraicSubtract(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
Definition: mvcOpAlg.c:88
Mvc_Cover_t * Mvc_CoverAlloc(Mvc_Manager_t *pMem, int nBits)
DECLARATIONS ///.
Definition: mvcCover.c:43
unsigned nOnes
Definition: mvc.h:70
void Mvc_CubePrint(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcPrint.c:79
int Mvc_CoverAnyLiteral(Mvc_Cover_t *pCover, Mvc_Cube_t *pMask)
DECLARATIONS ///.
Definition: mvcLits.c:43
Mvc_Cover_t * Mvc_CoverDup(Mvc_Cover_t *pCover)
Definition: mvcCover.c:112
Mvc_Cube_t * Mvc_CoverReadCubeHead(Mvc_Cover_t *pCover)
Definition: mvcApi.c:46
int Mvc_CoverTautology(Mvc_Data_t *p, Mvc_Cover_t *pCover)
void Mvc_CoverAllocateMask(Mvc_Cover_t *pCover)
Definition: mvcCover.c:168
void Mvc_CoverAddDupCubeHead(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:202
int Mvc_CoverSupportSizeBinary(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:100
void Mvc_CoverAddCubeHead_(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition: mvcList.c:121
int Mvc_CoverIsEmpty(Mvc_Cover_t *pCover)
Definition: mvcApi.c:93
Mvc_Cover_t * Mvc_CoverDivisor(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcDivisor.c:46
Mvc_Manager_t * pMem
Definition: mvc.h:93
void Mvc_CubePrintMv(Mvc_Data_t *pData, Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)