ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mvcList.c
Go to the documentation of this file.
1
18
19#include "mvc.h"
20
22
23
27
31
44{
45 if ( pList->pHead == NULL )
46 {
47 Mvc_CubeSetNext( pCube, NULL );
48 pList->pHead = pCube;
49 pList->pTail = pCube;
50 }
51 else
52 {
53 Mvc_CubeSetNext( pCube, pList->pHead );
54 pList->pHead = pCube;
55 }
56 pList->nItems++;
57}
58
59
72{
73 if ( pList->pHead == NULL )
74 pList->pHead = pCube;
75 else
76 Mvc_CubeSetNext( pList->pTail, pCube );
77 pList->pTail = pCube;
78 Mvc_CubeSetNext( pCube, NULL );
79 pList->nItems++;
80}
81
82
94void Mvc_ListDeleteCube_( Mvc_List_t * pList, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube )
95{
96 if ( pPrev == NULL ) // deleting the head cube
97 pList->pHead = Mvc_CubeReadNext(pCube);
98 else
99 pPrev->pNext = pCube->pNext;
100 if ( pList->pTail == pCube ) // deleting the tail cube
101 {
102 assert( Mvc_CubeReadNext(pCube) == NULL );
103 pList->pTail = pPrev;
104 }
105 pList->nItems--;
106}
107
108
109
122{
123 Mvc_List_t * pList = &pCover->lCubes;
124 if ( pList->pHead == NULL )
125 {
126 Mvc_CubeSetNext( pCube, NULL );
127 pList->pHead = pCube;
128 pList->pTail = pCube;
129 }
130 else
131 {
132 Mvc_CubeSetNext( pCube, pList->pHead );
133 pList->pHead = pCube;
134 }
135 pList->nItems++;
136}
137
150{
151 Mvc_List_t * pList = &pCover->lCubes;
152
153 if ( pList->pHead == NULL )
154 pList->pHead = pCube;
155 else
156 Mvc_CubeSetNext( pList->pTail, pCube );
157 pList->pTail = pCube;
158 Mvc_CubeSetNext( pCube, NULL );
159 pList->nItems++;
160}
161
173void Mvc_CoverDeleteCube_( Mvc_Cover_t * pCover, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube )
174{
175 Mvc_List_t * pList = &pCover->lCubes;
176
177 if ( pPrev == NULL ) // deleting the head cube
178 pList->pHead = Mvc_CubeReadNext(pCube);
179 else
180 pPrev->pNext = pCube->pNext;
181 if ( pList->pTail == pCube ) // deleting the tail cube
182 {
183 assert( Mvc_CubeReadNext(pCube) == NULL );
184 pList->pTail = pPrev;
185 }
186 pList->nItems--;
187}
188
189
190
203{
204 Mvc_Cube_t * pCubeNew;
205 pCubeNew = Mvc_CubeAlloc( pCover );
206 Mvc_CubeBitCopy( pCubeNew, pCube );
207 Mvc_CoverAddCubeHead( pCover, pCubeNew );
208}
209
222{
223 Mvc_Cube_t * pCubeNew;
224 // copy the cube as part of this cover
225 pCubeNew = Mvc_CubeAlloc( pCover );
226 Mvc_CubeBitCopy( pCubeNew, pCube );
227 // clean the last bits of the new cube
228// pCubeNew->pData[pCubeNew->iLast] &= (BITS_FULL >> pCubeNew->nUnused);
229 // add the cube at the end
230 Mvc_CoverAddCubeTail( pCover, pCubeNew );
231}
232
233
246{
247// int iBit, Value;
248// assert( pCover->pLits );
249// Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
250// if ( Value )
251// pCover->pLits[iBit] += Value;
252}
253
266{
267// int iBit, Value;
268// assert( pCover->pLits );
269// Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
270// if ( Value )
271// pCover->pLits[iBit] -= Value;
272}
273
274
287{
288 Mvc_Cube_t * pCube;
289 int Counter;
290 // resize storage if necessary
292 // iterate through the cubes
293 Counter = 0;
294 Mvc_CoverForEachCube( pCover, pCube )
295 pCover->pCubes[ Counter++ ] = pCube;
296 assert( Counter == Mvc_CoverReadCubeNum(pCover) );
297}
298
311{
312 Mvc_Cube_t * pCube;
313 int nCubes, i;
314
315 assert( pCover->pCubes );
316
317 nCubes = Mvc_CoverReadCubeNum(pCover);
318 if ( nCubes == 0 )
319 return;
320 if ( nCubes == 1 )
321 {
322 pCube = pCover->pCubes[0];
323 pCube->pNext = NULL;
324 pCover->lCubes.pHead = pCover->lCubes.pTail = pCube;
325 return;
326 }
327 // set up the first cube
328 pCube = pCover->pCubes[0];
329 pCover->lCubes.pHead = pCube;
330 // set up the last cube
331 pCube = pCover->pCubes[nCubes-1];
332 pCube->pNext = NULL;
333 pCover->lCubes.pTail = pCube;
334
335 // link all cubes starting from the first one
336 for ( i = 0; i < nCubes - 1; i++ )
337 pCover->pCubes[i]->pNext = pCover->pCubes[i+1];
338}
339
352{
353 Mvc_Cube_t * pCube, * pTail;
354 for ( pTail = pCube = pHead;
355 pCube;
356 pTail = pCube, pCube = Mvc_CubeReadNext(pCube) );
357 return pTail;
358}
359
360
364
365
367
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void Mvc_CoverAddDupCubeTail(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:221
void Mvc_ListAddCubeTail_(Mvc_List_t *pList, Mvc_Cube_t *pCube)
Definition mvcList.c:71
void Mvc_CoverAddCubeTail_(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:149
ABC_NAMESPACE_IMPL_START void Mvc_ListAddCubeHead_(Mvc_List_t *pList, Mvc_Cube_t *pCube)
DECLARATIONS ///.
Definition mvcList.c:43
void Mvc_CoverDeleteLiteralsOfCube(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:265
void Mvc_CoverList2Array(Mvc_Cover_t *pCover)
Definition mvcList.c:286
void Mvc_CoverAddLiteralsOfCube(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:245
void Mvc_CoverAddDupCubeHead(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:202
void Mvc_ListDeleteCube_(Mvc_List_t *pList, Mvc_Cube_t *pPrev, Mvc_Cube_t *pCube)
Definition mvcList.c:94
Mvc_Cube_t * Mvc_ListGetTailFromHead(Mvc_Cube_t *pHead)
Definition mvcList.c:351
void Mvc_CoverAddCubeHead_(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcList.c:121
void Mvc_CoverDeleteCube_(Mvc_Cover_t *pCover, Mvc_Cube_t *pPrev, Mvc_Cube_t *pCube)
Definition mvcList.c:173
void Mvc_CoverArray2List(Mvc_Cover_t *pCover)
Definition mvcList.c:310
#define Mvc_CoverAddCubeTail(pCover, pCube)
Definition mvc.h:501
struct MvcCubeStruct Mvc_Cube_t
Definition mvc.h:56
void Mvc_CoverAllocateArrayCubes(Mvc_Cover_t *pCover)
Definition mvcCover.c:202
#define Mvc_CubeReadNext(Cube)
MACRO DEFINITIONS ///.
Definition mvc.h:121
#define Mvc_CubeSetNext(Cube, Next)
Definition mvc.h:126
#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
struct MvcListStruct Mvc_List_t
Definition mvc.h:57
#define Mvc_CoverAddCubeHead(pCover, pCube)
Definition mvc.h:496
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition mvcApi.c:45
#define Mvc_CubeBitCopy(Cube1, Cube2)
Definition mvc.h:393
Mvc_Cube_t ** pCubes
Definition mvc.h:89
Mvc_List_t lCubes
Definition mvc.h:88
Mvc_Cube_t * pNext
Definition mvc.h:65
Mvc_Cube_t * pHead
Definition mvc.h:77
Mvc_Cube_t * pTail
Definition mvc.h:78
int nItems
Definition mvc.h:79
#define assert(ex)
Definition util_old.h:213