ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mvcOpBool.c
Go to the documentation of this file.
1
18
19#include "mvc.h"
20
22
23
27
31
44{
45 Mvc_Cover_t * pCover;
46 Mvc_Cube_t * pCube, * pCubeCopy;
47 // make sure the covers are compatible
48 assert( pCover1->nBits == pCover2->nBits );
49 // clone the cover
50 pCover = Mvc_CoverClone( pCover1 );
51 // create the cubes by making pair-wise products
52 // of cubes in pCover1 and pCover2
53 Mvc_CoverForEachCube( pCover1, pCube )
54 {
55 pCubeCopy = Mvc_CubeDup( pCover, pCube );
56 Mvc_CoverAddCubeTail( pCover, pCubeCopy );
57 }
58 Mvc_CoverForEachCube( pCover2, pCube )
59 {
60 pCubeCopy = Mvc_CubeDup( pCover, pCube );
61 Mvc_CoverAddCubeTail( pCover, pCubeCopy );
62 }
63 return pCover;
64}
65
66#if 0
67
80{
81 Mvc_Cover_t * pCover;
82 Mvc_Cube_t * pCube1, * pCube2, * pCubeCopy;
83 // make sure the covers are compatible
84 assert( pCover1->nBits == pCover2->nBits );
85 // clone the cover
86 pCover = Mvc_CoverClone( pCover1 );
87 // create the cubes by making pair-wise products
88 // of cubes in pCover1 and pCover2
89 Mvc_CoverForEachCube( pCover1, pCube1 )
90 {
91 Mvc_CoverForEachCube( pCover2, pCube2 )
92 {
93 if ( Mvc_CoverDist0Cubes( p, pCube1, pCube2 ) )
94 {
95 pCubeCopy = Mvc_CubeAlloc( pCover );
96 Mvc_CubeBitAnd( pCubeCopy, pCube1, pCube2 );
97 Mvc_CoverAddCubeTail( pCover, pCubeCopy );
98 }
99 }
100 // if the number of cubes in the new cover is too large
101 // try compressing them
102 if ( Mvc_CoverReadCubeNum( pCover ) > 500 )
103 Mvc_CoverContain( pCover );
104 }
105 return pCover;
106}
107
119int Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
120{
121 Mvc_Cover_t * pSharp;
122
123 pSharp = Mvc_CoverSharp( p, pCover1, pCover2 );
124 if ( Mvc_CoverReadCubeNum( pSharp ) )
125 {
126Mvc_CoverContain( pSharp );
127printf( "Sharp \n" );
128Mvc_CoverPrint( pSharp );
129 Mvc_CoverFree( pSharp );
130 return 0;
131 }
132 Mvc_CoverFree( pSharp );
133
134 pSharp = Mvc_CoverSharp( p, pCover2, pCover1 );
135 if ( Mvc_CoverReadCubeNum( pSharp ) )
136 {
137Mvc_CoverContain( pSharp );
138printf( "Sharp \n" );
139Mvc_CoverPrint( pSharp );
140 Mvc_CoverFree( pSharp );
141 return 0;
142 }
143 Mvc_CoverFree( pSharp );
144
145 return 1;
146}
147
148#endif
149
153
154
156
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
ABC_NAMESPACE_IMPL_START Mvc_Cover_t * Mvc_CoverBooleanOr(Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
DECLARATIONS ///.
Definition mvcOpBool.c:43
#define Mvc_CoverAddCubeTail(pCover, pCube)
Definition mvc.h:501
Mvc_Cover_t * Mvc_CoverSharp(Mvc_Data_t *p, Mvc_Cover_t *pA, Mvc_Cover_t *pB)
Mvc_Cover_t * Mvc_CoverClone(Mvc_Cover_t *pCover)
Definition mvcCover.c:79
Mvc_Cover_t * Mvc_CoverBooleanAnd(Mvc_Data_t *p, Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
struct MvcCubeStruct Mvc_Cube_t
Definition mvc.h:56
void Mvc_CoverFree(Mvc_Cover_t *pCover)
Definition mvcCover.c:138
#define Mvc_CubeBitAnd(CubeR, Cube1, Cube2)
Definition mvc.h:405
struct MvcDataStruct Mvc_Data_t
Definition mvc.h:59
int Mvc_CoverContain(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition mvcContain.c:47
int Mvc_CoverBooleanEqual(Mvc_Data_t *p, Mvc_Cover_t *pCover1, Mvc_Cover_t *pCover2)
#define Mvc_CoverForEachCube(Cover, Cube)
Definition mvc.h:528
Mvc_Cube_t * Mvc_CubeAlloc(Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition mvcCube.c:43
void Mvc_CoverPrint(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition mvcPrint.c:47
struct MvcCoverStruct Mvc_Cover_t
Definition mvc.h:58
int Mvc_CoverDist0Cubes(Mvc_Data_t *pData, Mvc_Cube_t *pA, Mvc_Cube_t *pB)
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition mvcApi.c:45
Mvc_Cube_t * Mvc_CubeDup(Mvc_Cover_t *pCover, Mvc_Cube_t *pCube)
Definition mvcCube.c:94
int nBits
Definition mvc.h:87
#define assert(ex)
Definition util_old.h:213