ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mvcContain.c
Go to the documentation of this file.
1
18
19#include "mvc.h"
20
22
23
27
28static void Mvc_CoverRemoveDuplicates( Mvc_Cover_t * pCover );
29static void Mvc_CoverRemoveContained( Mvc_Cover_t * pCover );
30
34
35
48{
49 int nCubes;
50 nCubes = Mvc_CoverReadCubeNum( pCover );
51 if ( nCubes < 2 )
52 return 0;
55 Mvc_CoverRemoveDuplicates( pCover );
56 if ( nCubes > 1 )
57 Mvc_CoverRemoveContained( pCover );
58 return (nCubes != Mvc_CoverReadCubeNum(pCover));
59}
60
72void Mvc_CoverRemoveDuplicates( Mvc_Cover_t * pCover )
73{
74 Mvc_Cube_t * pPrev, * pCube, * pCube2;
75 int fEqual;
76
77 // set the first cube of the cover
78 pPrev = Mvc_CoverReadCubeHead(pCover);
79 // go through all the cubes after this one
80 Mvc_CoverForEachCubeStartSafe( Mvc_CubeReadNext(pPrev), pCube, pCube2 )
81 {
82 // compare the current cube with the prev cube
83 Mvc_CubeBitEqual( fEqual, pPrev, pCube );
84 if ( fEqual )
85 { // they are equal - remove the current cube
86 Mvc_CoverDeleteCube( pCover, pPrev, pCube );
87 Mvc_CubeFree( pCover, pCube );
88 // don't change the previous cube cube
89 }
90 else
91 { // they are not equal - update the previous cube
92 pPrev = pCube;
93 }
94 }
95}
96
108void Mvc_CoverRemoveContained( Mvc_Cover_t * pCover )
109{
110 Mvc_Cube_t * pCubeBeg, * pCubeEnd, * pCubeLarge;
111 Mvc_Cube_t * pCube, * pCube2, * pPrev;
112 unsigned sizeCur;
113 int Result;
114
115 // since the cubes are sorted by size, it is sufficient
116 // to compare each cube with other cubes that have larger sizes
117 // if the given cube implies a larger cube, the larger cube is removed
118 pCubeBeg = Mvc_CoverReadCubeHead(pCover);
119 do
120 {
121 // get the current cube size
122 sizeCur = Mvc_CubeReadSize(pCubeBeg);
123
124 // initialize the end of the given size group
125 pCubeEnd = pCubeBeg;
126 // find the beginning of the next size group
128 {
129 if ( sizeCur == Mvc_CubeReadSize(pCube) )
130 pCubeEnd = pCube;
131 else // pCube is the first cube in the new size group
132 break;
133 }
134 // if we could not find the next size group
135 // the containment check is finished
136 if ( pCube == NULL )
137 break;
138 // otherwise, pCubeBeg/pCubeEnd are the first/last cubes of the group
139
140 // go through all the cubes between pCubeBeg and pCubeEnd, inclusive,
141 // and for each of them, try removing cubes after pCubeEnd
142 Mvc_CoverForEachCubeStart( pCubeBeg, pCubeLarge )
143 {
144 pPrev = pCubeEnd;
145 Mvc_CoverForEachCubeStartSafe( Mvc_CubeReadNext(pCubeEnd), pCube, pCube2 )
146 {
147 // check containment
148 Mvc_CubeBitNotImpl( Result, pCube, pCubeLarge );
149 if ( !Result )
150 { // pCubeLarge implies pCube - remove pCube
151 Mvc_CoverDeleteCube( pCover, pPrev, pCube );
152 Mvc_CubeFree( pCover, pCube );
153 // don't update the previous cube
154 }
155 else
156 { // update the previous cube
157 pPrev = pCube;
158 }
159 }
160 // quit, if the main cube was the last one of this size
161 if ( pCubeLarge == pCubeEnd )
162 break;
163 }
164
165 // set the beginning of the next group
166 pCubeBeg = Mvc_CubeReadNext(pCubeEnd);
167 }
168 while ( pCubeBeg );
169}
170
171
175
176
178
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
int Mvc_CoverContain(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition mvcContain.c:47
#define Mvc_CubeBitNotImpl(Res, Cube1, Cube2)
Definition mvc.h:429
struct MvcCubeStruct Mvc_Cube_t
Definition mvc.h:56
#define Mvc_CoverForEachCubeStartSafe(Start, Cube, Cube2)
Definition mvc.h:546
#define Mvc_CubeReadNext(Cube)
MACRO DEFINITIONS ///.
Definition mvc.h:121
#define Mvc_CubeReadSize(Cube)
Definition mvc.h:124
struct MvcCoverStruct Mvc_Cover_t
Definition mvc.h:58
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
int Mvc_CubeCompareSizeAndInt(Mvc_Cube_t *pC1, Mvc_Cube_t *pC2, Mvc_Cube_t *pMask)
Definition mvcCompare.c:91
Mvc_Cube_t * Mvc_CoverReadCubeHead(Mvc_Cover_t *pCover)
Definition mvcApi.c:46
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition mvcApi.c:45
void Mvc_CubeFree(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcCube.c:114
#define Mvc_CubeBitEqual(Res, Cube1, Cube2)
Definition mvc.h:417
int Mvc_CoverSetCubeSizes(Mvc_Cover_t *pCover)
Definition mvcUtils.c:272
#define Mvc_CoverDeleteCube(pCover, pPrev, pCube)
Definition mvc.h:506
#define Mvc_CoverForEachCubeStart(Start, Cube)
Definition mvc.h:542