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

Go to the source code of this file.

Functions

int Fxch_DivCreate (Fxch_Man_t *pFxchMan, Fxch_SubCube_t *pSubCube0, Fxch_SubCube_t *pSubCube1)
 
int Fxch_DivAdd (Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
 
int Fxch_DivRemove (Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
 
void Fxch_DivSepareteCubes (Vec_Int_t *vDiv, Vec_Int_t *vCube0, Vec_Int_t *vCube1)
 
int Fxch_DivRemoveLits (Vec_Int_t *vCube0, Vec_Int_t *vCube1, Vec_Int_t *vDiv, int *fCompl)
 
void Fxch_DivPrint (Fxch_Man_t *pFxchMan, int iDiv)
 
int Fxch_DivIsNotConstant1 (Vec_Int_t *vDiv)
 

Function Documentation

◆ Fxch_DivAdd()

int Fxch_DivAdd ( Fxch_Man_t * pFxchMan,
int fUpdate,
int fSingleCube,
int fBase )

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

Synopsis [ Add a divisor to the divisors hash table. ]

Description [ This functions will try to add the divisor store in vCubeFree to the divisor hash table. If the divisor is already present in the hash table it will just increment its weight, otherwise it will add the divisor and asign an initial weight. ]

SideEffects [ If the fUpdate option is set, the function will also update the divisor priority queue. ]

SeeAlso []

Definition at line 228 of file FxchDiv.c.

232{
233 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
234
235 /* Verify if the divisor already exist */
236 if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
237 {
238 Vec_WecPushLevel( pFxchMan->vDivCubePairs );
239
240 /* Assign initial weight */
241 if ( fSingleCube )
242 {
243 Vec_FltPush( pFxchMan->vDivWeights,
244 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
245 -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
246 }
247 else
248 {
249 Vec_FltPush( pFxchMan->vDivWeights,
250 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
251 -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
252 }
253
254 }
255
256 /* Increment weight */
257 if ( fSingleCube )
258 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
259 else
260 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
261
262 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
263
264 if ( fUpdate )
265 if ( pFxchMan->vDivPrio )
266 {
267 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
268 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
269 else
270 Vec_QuePush( pFxchMan->vDivPrio, iDiv );
271 }
272
273 return iDiv;
274}
Fxch_ManComputeLevelDiv
int Fxch_ManComputeLevelDiv(Fxch_Man_t *pFxchMan, Vec_Int_t *vCubeFree)
Definition FxchMan.c:312
Fxch_Man_t_::vDivWeights
Vec_Flt_t * vDivWeights
Definition Fxch.h:104
Fxch_Man_t_::pDivHash
Hsh_VecMan_t * pDivHash
Definition Fxch.h:103
Fxch_Man_t_::vCubeFree
Vec_Int_t * vCubeFree
Definition Fxch.h:119
Fxch_Man_t_::vDivPrio
Vec_Que_t * vDivPrio
Definition Fxch.h:105
Fxch_Man_t_::vDivCubePairs
Vec_Wec_t * vDivCubePairs
Definition Fxch.h:106
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxch_DivCreate()

int Fxch_DivCreate ( Fxch_Man_t * pFxchMan,
Fxch_SubCube_t * pSubCube0,
Fxch_SubCube_t * pSubCube1 )

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

Synopsis [ Creates a Divisor. ]

Description [ This functions receive as input two sub-cubes and creates a divisor using their information. The divisor is stored in vCubeFree vector of the pFxchMan structure.

It returns the base value, which is the number of elements that the cubes pair used to generate the devisor have in common. ]

SideEffects []

SeeAlso []

Definition at line 112 of file FxchDiv.c.

115{
116 int Base = 0;
117
118 int SC0_Lit0,
119 SC0_Lit1,
120 SC1_Lit0,
121 SC1_Lit1;
122
123 int Cube0Size,
124 Cube1Size;
125
126 Vec_IntClear( pFxchMan->vCubeFree );
127
128 SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
129 SC0_Lit1 = 0;
130 SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
131 SC1_Lit1 = 0;
132
133 if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
134 {
135 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
136 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
137 }
138 else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
139 {
140 int RetValue;
141
142 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
143 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
144
145 if ( SC0_Lit0 < SC1_Lit0 )
146 {
147 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
148 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
149 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
150 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
151 }
152 else
153 {
154 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
155 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
156 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
157 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
158 }
159
160 RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
161 if ( RetValue == -1 )
162 return -1;
163 }
164 else
165 {
166 if ( pSubCube0->iLit1 > 0 )
167 {
168 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
169
170 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
171 if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
172 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
173 else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
174 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
175 }
176 else
177 {
178 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
179
180 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
181 if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
182 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
183 else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
184 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
185 }
186 }
187
188 if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
189 return -1;
190
191 if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
192 {
193 Vec_IntSort( pFxchMan->vCubeFree, 0 );
194
195 Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
196 Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
197 }
198
199 Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
200 Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
201 if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
202 {
203 Base = Abc_MinInt( Cube0Size, Cube1Size )
204 -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */
205 }
206 else
207 return -1;
208
209 return Base;
210}
Fxch_SubCube_t_::iLit1
uint32_t iLit1
Definition Fxch.h:64
Fxch_SubCube_t_::iLit0
uint32_t iLit0
Definition Fxch.h:63
Fxch_SubCube_t_::iCube
uint32_t iCube
Definition Fxch.h:62
Here is the caller graph for this function:

◆ Fxch_DivIsNotConstant1()

int Fxch_DivIsNotConstant1 ( Vec_Int_t * vDiv)

Definition at line 470 of file FxchDiv.c.

471{
472 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
473 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) );
474
475 if ( ( Vec_IntSize( vDiv ) == 2 ) && ( Lit0 == Abc_LitNot( Lit1 ) ) )
476 return 0;
477
478 return 1;
479}
Here is the caller graph for this function:

◆ Fxch_DivPrint()

void Fxch_DivPrint ( Fxch_Man_t * pFxchMan,
int iDiv )

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

Synopsis [ Print the divisor identified by iDiv. ]

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file FxchDiv.c.

448{
449 Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
450 int i,
451 Lit;
452
453 printf( "Div %7d : ", iDiv );
454 printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
455
456 Vec_IntForEachEntry( vDiv, Lit, i )
457 if ( !Abc_LitIsCompl( Lit ) )
458 printf( "%d(1)", Abc_Lit2Var( Lit ) );
459
460 printf( " + " );
461
462 Vec_IntForEachEntry( vDiv, Lit, i )
463 if ( Abc_LitIsCompl( Lit ) )
464 printf( "%d(2)", Abc_Lit2Var( Lit ) );
465
466 printf( " Lits =%7d ", pFxchMan->nLits );
467 printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) );
468}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Fxch_Man_t_::nLits
int nLits
Definition plaFxch.c:66
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Fxch_DivRemove()

int Fxch_DivRemove ( Fxch_Man_t * pFxchMan,
int fUpdate,
int fSingleCube,
int fBase )

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

Synopsis [ Removes a divisor to the divisors hash table. ]

Description [ This function don't effectively removes a divisor from the hash table (the hash table implementation don't support such operation). It only assures its existence and decrement its weight. ]

SideEffects [ If the fUpdate option is set, the function will also update the divisor priority queue. ]

SeeAlso []

Definition at line 291 of file FxchDiv.c.

295{
296 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
297
298 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
299
300 /* Decrement weight */
301 if ( fSingleCube )
302 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
303 else
304 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
305
306 if ( fUpdate )
307 if ( pFxchMan->vDivPrio )
308 {
309 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
310 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
311 }
312
313 return iDiv;
314}
Here is the caller graph for this function:

◆ Fxch_DivRemoveLits()

int Fxch_DivRemoveLits ( Vec_Int_t * vCube0,
Vec_Int_t * vCube1,
Vec_Int_t * vDiv,
int * fCompl )

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

Synopsis [ Removes the literals present in the divisor from their original cubes. ]

Description [ This function returns the numeber of removed literals which should be equal to the size of the divisor. ]

SideEffects []

SeeAlso []

Definition at line 380 of file FxchDiv.c.

384{
385 int i,
386 Lit,
387 CountP = 0,
388 CountN = 0,
389 Count = 0,
390 ret = 0;
391
392 Vec_IntForEachEntry( vDiv, Lit, i )
393 if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
394 CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
395 else
396 CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
397
398 Vec_IntForEachEntry( vDiv, Lit, i )
399 Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
400
401 if ( Vec_IntSize( vDiv ) == 2 )
402 Vec_IntForEachEntry( vDiv, Lit, i )
403 {
404 Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
405 Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
406 }
407
408 ret = Count + CountP + CountN;
409
410 if ( Vec_IntSize( vDiv ) == 4 )
411 {
412 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
413 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
414 Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
415 Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
416
417 if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
418 *fCompl = 1;
419
420 if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
421 {
422 *fCompl = 1;
423
424 Vec_IntForEachEntry( vDiv, Lit, i )
425 ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
426
427 Vec_IntForEachEntry( vDiv, Lit, i )
428 ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
429 }
430 }
431
432 return ret;
433}

◆ Fxch_DivSepareteCubes()

void Fxch_DivSepareteCubes ( Vec_Int_t * vDiv,
Vec_Int_t * vCube0,
Vec_Int_t * vCube1 )

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

Synopsis [ Separete the cubes in present in a divisor ]

Description [ In this implementation all stored divsors are composed of two cubes.

In order to save space and to be able to use the Vec_Int_t hash table both cubes are stored in the same vector - using a little hack to differentiate which literal belongs to each cube.

This function separetes the two cubes in their own vectors so that they can be added to the cover.

Note* that this also applies to single cube divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]

SideEffects []

SeeAlso []

Definition at line 339 of file FxchDiv.c.

342{
343 int* pArray;
344 int i,
345 Lit;
346
347 Vec_IntForEachEntry( vDiv, Lit, i )
348 if ( Abc_LitIsCompl(Lit) )
349 Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
350 else
351 Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
352
353 if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
354 {
355 assert( Vec_IntSize( vCube1 ) == 3 );
356
357 pArray = Vec_IntArray( vCube0 );
358 if ( pArray[1] > pArray[2] )
359 ABC_SWAP( int, pArray[1], pArray[2] );
360
361 pArray = Vec_IntArray( vCube1 );
362 if ( pArray[1] > pArray[2] )
363 ABC_SWAP( int, pArray[1], pArray[2] );
364 }
365}
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253