ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
mioSop.c File Reference
#include "mioInt.h"
#include "exp.h"
Include dependency graph for mioSop.c:

Go to the source code of this file.

Functions

void Mio_SopPushSCC (Vec_Int_t *p, unsigned c)
 FUNCTION DEFINITIONS ///.
 
Vec_Int_t * Mio_SopCoverOr (Vec_Int_t *p, Vec_Int_t *q)
 
Vec_Int_t * Mio_SopCoverAnd (Vec_Int_t *p, Vec_Int_t *q)
 
Vec_Int_t * Mio_SopVar0 (int i)
 
Vec_Int_t * Mio_SopVar1 (int i)
 
Vec_Int_t * Mio_SopConst0 ()
 
Vec_Int_t * Mio_SopConst1 ()
 
char * Mio_SopDeriveFromArray (Vec_Int_t *vSop, int nVars, Vec_Str_t *vStr, int fPolarity)
 
char * Mio_LibDeriveSop (int nVars, Vec_Int_t *vExpr, Vec_Str_t *vStr)
 

Function Documentation

◆ Mio_LibDeriveSop()

char * Mio_LibDeriveSop ( int nVars,
Vec_Int_t * vExpr,
Vec_Str_t * vStr )

Function*************************************************************

Synopsis [Derives SOP representation.]

Description [The SOP is guaranteed to be SCC-free but not minimal.]

SideEffects []

SeeAlso []

Definition at line 257 of file mioSop.c.

258{
259 Vec_Int_t * vSop;
260 Vec_Ptr_t * vSops0, * vSops1, * vTemp;
261 int i, Index0, Index1, fCompl0, fCompl1;
262 Vec_StrClear( vStr );
263 if ( Exp_IsConst0(vExpr) )
264 {
265 Vec_StrPrintStr( vStr, " 0\n" );
266 Vec_StrPush( vStr, '\0' );
267 return Vec_StrArray( vStr );
268 }
269 if ( Exp_IsConst1(vExpr) )
270 {
271 Vec_StrPrintStr( vStr, " 1\n" );
272 Vec_StrPush( vStr, '\0' );
273 return Vec_StrArray( vStr );
274 }
275 if ( Exp_IsLit(vExpr) )
276 {
277 for ( i = 0; i < nVars; i++ )
278 Vec_StrPush( vStr, '-' );
279 Vec_StrPrintStr( vStr, " 1\n" );
280 Vec_StrPush( vStr, '\0' );
281 assert( (Vec_IntEntry(vExpr,0) >> 1) < nVars );
282 Vec_StrWriteEntry( vStr, Vec_IntEntry(vExpr,0) >> 1, (char)('1' - (Vec_IntEntry(vExpr,0) & 1)) );
283 return Vec_StrArray( vStr );
284 }
285 vSops0 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
286 vSops1 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
287 for ( i = 0; i < nVars; i++ )
288 {
289 Vec_PtrPush( vSops0, Mio_SopVar0(i) );
290 Vec_PtrPush( vSops1, Mio_SopVar1(i) );
291 }
292 for ( i = 0; i < Exp_NodeNum(vExpr); i++ )
293 {
294 Index0 = Vec_IntEntry( vExpr, 2*i+0 ) >> 1;
295 Index1 = Vec_IntEntry( vExpr, 2*i+1 ) >> 1;
296 fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1;
297 fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1;
298 // positive polarity
299 vSop = Mio_SopCoverAnd( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0),
300 fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) );
301 Vec_PtrPush( vSops1, vSop );
302 // negative polarity
303 vSop = Mio_SopCoverOr( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0),
304 fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) );
305 Vec_PtrPush( vSops0, vSop );
306 }
307 // complement
308 if ( Vec_IntEntryLast(vExpr) & 1 )
309 {
310 vTemp = vSops0;
311 vSops0 = vSops1;
312 vSops1 = vTemp;
313 }
314 // select the best polarity
315 if ( Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops0) ) < Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops1) ) )
316 vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops0);
317 else
318 vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops1);
319 // convert positive polarity into SOP
320 Mio_SopDeriveFromArray( vSop, nVars, vStr, (vSop == Vec_PtrEntryLast(vSops1)) );
321 Vec_VecFree( (Vec_Vec_t *)vSops0 );
322 Vec_VecFree( (Vec_Vec_t *)vSops1 );
323 return Vec_StrArray( vStr );
324}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Mio_SopVar0
Vec_Int_t * Mio_SopVar0(int i)
Definition mioSop.c:130
Mio_SopVar1
Vec_Int_t * Mio_SopVar1(int i)
Definition mioSop.c:149
Mio_SopDeriveFromArray
char * Mio_SopDeriveFromArray(Vec_Int_t *vSop, int nVars, Vec_Str_t *vStr, int fPolarity)
Definition mioSop.c:205
Mio_SopCoverOr
Vec_Int_t * Mio_SopCoverOr(Vec_Int_t *p, Vec_Int_t *q)
Definition mioSop.c:82
Mio_SopCoverAnd
Vec_Int_t * Mio_SopCoverAnd(Vec_Int_t *p, Vec_Int_t *q)
Definition mioSop.c:106
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mio_SopConst0()

Vec_Int_t * Mio_SopConst0 ( )

Function*************************************************************

Synopsis [Create constant 0 literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file mioSop.c.

169{
170 Vec_Int_t * vSop;
171 vSop = Vec_IntAlloc( 1 );
172 return vSop;
173}

◆ Mio_SopConst1()

Vec_Int_t * Mio_SopConst1 ( )

Function*************************************************************

Synopsis [Create constant 1 literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file mioSop.c.

187{
188 Vec_Int_t * vSop;
189 vSop = Vec_IntAlloc( 1 );
190 Vec_IntPush( vSop, 0 );
191 return vSop;
192}

◆ Mio_SopCoverAnd()

Vec_Int_t * Mio_SopCoverAnd ( Vec_Int_t * p,
Vec_Int_t * q )

Function*************************************************************

Synopsis [Make the AND of two covers.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file mioSop.c.

107{
108 Vec_Int_t * r;
109 unsigned EntryP, EntryQ;
110 int i, k;
111 r = Vec_IntAlloc( Vec_IntSize(p) * Vec_IntSize(q) );
112 Vec_IntForEachEntry( p, EntryP, i )
113 Vec_IntForEachEntry( q, EntryQ, k )
114 if ( !Mio_CubeEmpty( Mio_CubeAnd(EntryP, EntryQ) ) )
115 Mio_SopPushSCC( r, Mio_CubeAnd(EntryP, EntryQ) );
116 return r;
117}
p
Cube * p
Definition exorList.c:222
Mio_SopPushSCC
void Mio_SopPushSCC(Vec_Int_t *p, unsigned c)
FUNCTION DEFINITIONS ///.
Definition mioSop.c:52
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mio_SopCoverOr()

Vec_Int_t * Mio_SopCoverOr ( Vec_Int_t * p,
Vec_Int_t * q )

Function*************************************************************

Synopsis [Make the OR of two covers.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file mioSop.c.

83{
84 Vec_Int_t * r;
85 unsigned Entry;
86 int i;
87 r = Vec_IntAlloc( Vec_IntSize(p) + Vec_IntSize(q) );
88 Vec_IntForEachEntry( p, Entry, i )
89 Vec_IntPush( r, Entry );
90 Vec_IntForEachEntry( q, Entry, i )
91 Mio_SopPushSCC( r, Entry );
92 return r;
93}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mio_SopDeriveFromArray()

char * Mio_SopDeriveFromArray ( Vec_Int_t * vSop,
int nVars,
Vec_Str_t * vStr,
int fPolarity )

Function*************************************************************

Synopsis [Derives SOP representation as the char string.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file mioSop.c.

206{
207 unsigned Entry;
208 int i, k;
209 Vec_StrClear( vStr );
210 if ( Vec_IntSize(vSop) == 0 )
211 {
212 Vec_StrPush( vStr, ' ' );
213 Vec_StrPush( vStr, (char)('1'-fPolarity) );
214 Vec_StrPush( vStr, '\n' );
215 Vec_StrPush( vStr, '\0' );
216 return Vec_StrArray( vStr );
217 }
218 if ( Vec_IntSize(vSop) == 1 && Vec_IntEntry(vSop, 0) == 0 )
219 {
220 Vec_StrPush( vStr, ' ' );
221 Vec_StrPush( vStr, (char)('0'+fPolarity) );
222 Vec_StrPush( vStr, '\n' );
223 Vec_StrPush( vStr, '\0' );
224 return Vec_StrArray( vStr );
225 }
226 // create cubes
227 Vec_IntForEachEntry( vSop, Entry, i )
228 {
229 for ( k = 0; k < nVars; k++ )
230 {
231 if ( Mio_CubeHasVar0( Entry, k ) )
232 Vec_StrPush( vStr, '0' );
233 else if ( Mio_CubeHasVar1( Entry, k ) )
234 Vec_StrPush( vStr, '1' );
235 else
236 Vec_StrPush( vStr, '-' );
237 }
238 Vec_StrPush( vStr, ' ' );
239 Vec_StrPush( vStr, (char)('0'+fPolarity) );
240 Vec_StrPush( vStr, '\n' );
241 }
242 Vec_StrPush( vStr, '\0' );
243 return Vec_StrArray( vStr );
244}
Here is the caller graph for this function:

◆ Mio_SopPushSCC()

void Mio_SopPushSCC ( Vec_Int_t * p,
unsigned c )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Push while performing SCC.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file mioSop.c.

53{
54 unsigned Entry;
55 int i, k = 0;
56 Vec_IntForEachEntry( p, Entry, i )
57 {
58 if ( Mio_CubeContains( Entry, c ) ) // Entry contains c
59 {
60 assert( i == k );
61 return;
62 }
63 if ( Mio_CubeContains( c, Entry ) ) // c contains Entry
64 continue;
65 Vec_IntWriteEntry( p, k++, Entry );
66 }
67 Vec_IntShrink( p, k );
68 Vec_IntPush( p, c );
69}
Here is the caller graph for this function:

◆ Mio_SopVar0()

Vec_Int_t * Mio_SopVar0 ( int i)

Function*************************************************************

Synopsis [Create negative literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file mioSop.c.

131{
132 Vec_Int_t * vSop;
133 vSop = Vec_IntAlloc( 1 );
134 Vec_IntPush( vSop, Mio_CubeVar0(i) );
135 return vSop;
136}
Here is the caller graph for this function:

◆ Mio_SopVar1()

Vec_Int_t * Mio_SopVar1 ( int i)

Function*************************************************************

Synopsis [Create positive literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file mioSop.c.

150{
151 Vec_Int_t * vSop;
152 vSop = Vec_IntAlloc( 1 );
153 Vec_IntPush( vSop, Mio_CubeVar1(i) );
154 return vSop;
155}
Here is the caller graph for this function: