ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fxuSingle.c File Reference
#include "fxuInt.h"
#include "misc/vec/vec.h"
Include dependency graph for fxuSingle.c:

Go to the source code of this file.

Functions

void Fxu_MatrixComputeSingles (Fxu_Matrix *p, int fUse0, int nSingleMax)
 FUNCTION DEFINITIONS ///.
 
void Fxu_MatrixComputeSinglesOne (Fxu_Matrix *p, Fxu_Var *pVar)
 
int Fxu_SingleCountCoincidence (Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2)
 

Function Documentation

◆ Fxu_MatrixComputeSingles()

void Fxu_MatrixComputeSingles ( Fxu_Matrix * p,
int fUse0,
int nSingleMax )

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes and adds all single-cube divisors to storage.]

Description [This procedure should be called once when the matrix is already contructed before the process of logic extraction begins..]

SideEffects []

SeeAlso []

Definition at line 47 of file fxuSingle.c.

48{
49 Fxu_Var * pVar;
50 Vec_Ptr_t * vSingles;
51 int i, k;
52 // set the weight limit
53 p->nWeightLimit = 1 - fUse0;
54 // iterate through columns in the matrix and collect single-cube divisors
55 vSingles = Vec_PtrAlloc( 10000 );
57 Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
58 p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
59 // check if divisors should be filtered
60 if ( Vec_PtrSize(vSingles) > nSingleMax )
61 {
62 int * pWeigtCounts, nDivCount, Weight, i, c;;
63 assert( Vec_PtrSize(vSingles) % 3 == 0 );
64 // count how many divisors have the given weight
65 pWeigtCounts = ABC_ALLOC( int, 1000 );
66 memset( pWeigtCounts, 0, sizeof(int) * 1000 );
67 for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
68 {
69 Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
70 if ( Weight >= 999 )
71 pWeigtCounts[999]++;
72 else
73 pWeigtCounts[Weight]++;
74 }
75 // select the bound on the weight (above this bound, singles will be included)
76 nDivCount = 0;
77 for ( c = 999; c >= 0; c-- )
78 {
79 nDivCount += pWeigtCounts[c];
80 if ( nDivCount >= nSingleMax )
81 break;
82 }
83 ABC_FREE( pWeigtCounts );
84 // collect singles with the given costs
85 k = 0;
86 for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
87 {
88 Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
89 if ( Weight < c )
90 continue;
91 Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
92 Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
93 Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
94 if ( k/3 == nSingleMax )
95 break;
96 }
97 Vec_PtrShrink( vSingles, k );
98 // adjust the weight limit
99 p->nWeightLimit = c;
100 }
101 // collect the selected divisors
102 assert( Vec_PtrSize(vSingles) % 3 == 0 );
103 for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
104 {
106 (Fxu_Var *)Vec_PtrEntry(vSingles,i),
107 (Fxu_Var *)Vec_PtrEntry(vSingles,i+1),
108 (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles,i+2) );
109 }
110 Vec_PtrFree( vSingles );
111}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
Cube * p
Definition exorList.c:222
struct FxuVar Fxu_Var
Definition fxuInt.h:67
#define Fxu_MatrixForEachVariable(Matrix, Var)
Definition fxuInt.h:303
void Fxu_MatrixAddSingle(Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2, int Weight)
Definition fxuMatrix.c:274
#define assert(ex)
Definition util_old.h:213
char * memset()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixComputeSinglesOne()

void Fxu_MatrixComputeSinglesOne ( Fxu_Matrix * p,
Fxu_Var * pVar )

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

Synopsis [Adds the single-cube divisors associated with a new column.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file fxuSingle.c.

185{
186 Fxu_Lit * pLitV, * pLitH;
187 Fxu_Var * pVar2;
188 int Coin;
189 int WeightCur;
190
191 // start collecting the affected vars
193 // go through all the literals of this variable
194 for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
195 // for this literal, go through all the horizontal literals
196 for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
197 {
198 // get another variable
199 pVar2 = pLitH->pVar;
200 // skip the var if it is already used
201 if ( pVar2->pOrder )
202 continue;
203 // skip the var if it belongs to the same node
204// if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
205// continue;
206 // collect the var
207 Fxu_MatrixRingVarsAdd( p, pVar2 );
208 }
209 // stop collecting the selected vars
211
212 // iterate through the selected vars
214 {
215 // count the coincidence
216 Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
217 assert( Coin > 0 );
218 // get the new weight
219 WeightCur = Coin - 2;
220 // peformance fix (August 24, 2007)
221// if ( WeightCur >= 0 )
222// Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
223 if ( WeightCur >= p->nWeightLimit )
224 Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
225 }
226 // unmark the vars
228}
#define Fxu_MatrixForEachVarInRing(Matrix, Var)
Definition fxuInt.h:407
#define Fxu_MatrixRingVarsStart( Matrix)
Definition fxuInt.h:386
#define Fxu_MatrixRingVarsAdd( Matrix, Var)
Definition fxuInt.h:395
#define Fxu_MatrixRingVarsStop( Matrix)
Definition fxuInt.h:389
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
int Fxu_SingleCountCoincidence(Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2)
Definition fxuSingle.c:241
void Fxu_MatrixRingVarsUnmark(Fxu_Matrix *p)
Definition fxu.c:206
Fxu_Lit * pHead
Definition fxuInt.h:109
Fxu_Lit * pVNext
Definition fxuInt.h:235
Fxu_Lit * pHPrev
Definition fxuInt.h:232
Fxu_Var * pVar
Definition fxuInt.h:231
Fxu_Var * pOrder
Definition fxuInt.h:222
Fxu_ListLit lLits
Definition fxuInt.h:219
Here is the call graph for this function:

◆ Fxu_SingleCountCoincidence()

int Fxu_SingleCountCoincidence ( Fxu_Matrix * p,
Fxu_Var * pVar1,
Fxu_Var * pVar2 )

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

Synopsis [Computes the coincidence count of two columns.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file fxuSingle.c.

242{
243 Fxu_Lit * pLit1, * pLit2;
244 int Result;
245
246 // compute the coincidence count
247 Result = 0;
248 pLit1 = pVar1->lLits.pHead;
249 pLit2 = pVar2->lLits.pHead;
250 while ( 1 )
251 {
252 if ( pLit1 && pLit2 )
253 {
254 if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
255 { // the variables are the same
256 if ( pLit1->iCube == pLit2->iCube )
257 { // the literals are the same
258 pLit1 = pLit1->pVNext;
259 pLit2 = pLit2->pVNext;
260 // add this literal to the coincidence
261 Result++;
262 }
263 else if ( pLit1->iCube < pLit2->iCube )
264 pLit1 = pLit1->pVNext;
265 else
266 pLit2 = pLit2->pVNext;
267 }
268 else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
269 pLit1 = pLit1->pVNext;
270 else
271 pLit2 = pLit2->pVNext;
272 }
273 else if ( pLit1 && !pLit2 )
274 pLit1 = pLit1->pVNext;
275 else if ( !pLit1 && pLit2 )
276 pLit2 = pLit2->pVNext;
277 else
278 break;
279 }
280 return Result;
281}
Fxu_Var * pVar
Definition fxuInt.h:205
Fxu_Cube * pCube
Definition fxuInt.h:230
int iCube
Definition fxuInt.h:229
int iVar
Definition fxuInt.h:215
Here is the caller graph for this function: