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

Go to the source code of this file.

Macros

#define MAX_SIZE_LOOKAHEAD   20
 DECLARATIONS ///.
 

Functions

Fxu_Double * Fxu_MatrixFindDouble (Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
 
void Fxu_MatrixGetDoubleVars (Fxu_Matrix *p, Fxu_Double *pDouble, int piVarsC1[], int piVarsC2[], int *pnVarsC1, int *pnVarsC2)
 
int Fxu_Select (Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
 FUNCTION DEFINITIONS ///.
 
int Fxu_SelectSCD (Fxu_Matrix *p, int WeightLimit, Fxu_Var **ppVar1, Fxu_Var **ppVar2)
 

Macro Definition Documentation

◆ MAX_SIZE_LOOKAHEAD

#define MAX_SIZE_LOOKAHEAD   20

DECLARATIONS ///.

CFile****************************************************************

FileName [fxuSelect.c]

PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

Synopsis [Procedures to select the best divisor/complement pair.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id
fxuSelect.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

]

Definition at line 28 of file fxuSelect.c.

Function Documentation

◆ Fxu_MatrixFindDouble()

Fxu_Double * Fxu_MatrixFindDouble ( Fxu_Matrix * p,
int piVarsC1[],
int piVarsC2[],
int nVarsC1,
int nVarsC2 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 466 of file fxuSelect.c.

468{
469 int piVarsC1_[100], piVarsC2_[100];
470 int nVarsC1_, nVarsC2_, i;
471 Fxu_Double * pDouble;
472 Fxu_Pair * pPair;
473 unsigned Key;
474
475 assert( nVarsC1 > 0 );
476 assert( nVarsC2 > 0 );
477 assert( piVarsC1[0] < piVarsC2[0] );
478
479 // get the hash key
480 Key = Fxu_PairHashKeyArray( p, piVarsC1, piVarsC2, nVarsC1, nVarsC2 );
481
482 // check if the divisor for this pair already exists
483 Key %= p->nTableSize;
484 Fxu_TableForEachDouble( p, Key, pDouble )
485 {
486 pPair = pDouble->lPairs.pHead;
487 if ( pPair->nLits1 != nVarsC1 )
488 continue;
489 if ( pPair->nLits2 != nVarsC2 )
490 continue;
491 // get the cubes of this divisor
492 Fxu_MatrixGetDoubleVars( p, pDouble, piVarsC1_, piVarsC2_, &nVarsC1_, &nVarsC2_ );
493 // compare lits of the first cube
494 for ( i = 0; i < nVarsC1; i++ )
495 if ( piVarsC1[i] != piVarsC1_[i] )
496 break;
497 if ( i != nVarsC1 )
498 continue;
499 // compare lits of the second cube
500 for ( i = 0; i < nVarsC2; i++ )
501 if ( piVarsC2[i] != piVarsC2_[i] )
502 break;
503 if ( i != nVarsC2 )
504 continue;
505 return pDouble;
506 }
507 return NULL;
508}
p
Cube * p
Definition exorList.c:222
Fxu_PairHashKeyArray
unsigned Fxu_PairHashKeyArray(Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
Definition fxuPair.c:137
Fxu_Pair
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
Fxu_TableForEachDouble
#define Fxu_TableForEachDouble(Matrix, Key, Div)
Definition fxuInt.h:321
Fxu_Double
struct FxuDouble Fxu_Double
Definition fxuInt.h:72
Fxu_MatrixGetDoubleVars
void Fxu_MatrixGetDoubleVars(Fxu_Matrix *p, Fxu_Double *pDouble, int piVarsC1[], int piVarsC2[], int *pnVarsC1, int *pnVarsC2)
Definition fxuSelect.c:403
FxuDouble::lPairs
Fxu_ListPair lPairs
Definition fxuInt.h:260
FxuListPair::pHead
Fxu_Pair * pHead
Definition fxuInt.h:117
FxuPair::nLits2
int nLits2
Definition fxuInt.h:242
FxuPair::nLits1
int nLits1
Definition fxuInt.h:241
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Fxu_MatrixGetDoubleVars()

void Fxu_MatrixGetDoubleVars ( Fxu_Matrix * p,
Fxu_Double * pDouble,
int piVarsC1[],
int piVarsC2[],
int * pnVarsC1,
int * pnVarsC2 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 403 of file fxuSelect.c.

405{
406 Fxu_Pair * pPair;
407 Fxu_Lit * pLit1, * pLit2;
408 int nLits1, nLits2;
409
410 // get the first pair
411 pPair = pDouble->lPairs.pHead;
412 // init the parameters
413 nLits1 = 0;
414 nLits2 = 0;
415 pLit1 = pPair->pCube1->lLits.pHead;
416 pLit2 = pPair->pCube2->lLits.pHead;
417 while ( 1 )
418 {
419 if ( pLit1 && pLit2 )
420 {
421 if ( pLit1->iVar == pLit2->iVar )
422 { // ensure cube-free
423 pLit1 = pLit1->pHNext;
424 pLit2 = pLit2->pHNext;
425 }
426 else if ( pLit1->iVar < pLit2->iVar )
427 {
428 piVarsC1[nLits1++] = pLit1->iVar;
429 pLit1 = pLit1->pHNext;
430 }
431 else
432 {
433 piVarsC2[nLits2++] = pLit2->iVar;
434 pLit2 = pLit2->pHNext;
435 }
436 }
437 else if ( pLit1 && !pLit2 )
438 {
439 piVarsC1[nLits1++] = pLit1->iVar;
440 pLit1 = pLit1->pHNext;
441 }
442 else if ( !pLit1 && pLit2 )
443 {
444 piVarsC2[nLits2++] = pLit2->iVar;
445 pLit2 = pLit2->pHNext;
446 }
447 else
448 break;
449 }
450 *pnVarsC1 = nLits1;
451 *pnVarsC2 = nLits2;
452}
Fxu_Lit
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
FxuCube::lLits
Fxu_ListLit lLits
Definition fxuInt.h:206
FxuListLit::pHead
Fxu_Lit * pHead
Definition fxuInt.h:109
FxuLit::pHNext
Fxu_Lit * pHNext
Definition fxuInt.h:233
FxuLit::iVar
int iVar
Definition fxuInt.h:228
FxuPair::pCube1
Fxu_Cube * pCube1
Definition fxuInt.h:245
FxuPair::pCube2
Fxu_Cube * pCube2
Definition fxuInt.h:246
Here is the caller graph for this function:

◆ Fxu_Select()

int Fxu_Select ( Fxu_Matrix * p,
Fxu_Single ** ppSingle,
Fxu_Double ** ppDouble )

FUNCTION DEFINITIONS ///.

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

Synopsis [Selects the best pair (Single,Double) and returns their weight.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file fxuSelect.c.

58{
59 // the top entries
60 Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD] = {0};
61 Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD] = {0};
62 // the complements
63 Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD] = {0};
64 Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD] = {0};
65 Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD] = {0};
66 Fxu_Pair * pPair;
67 int nSingles;
68 int nDoubles;
69 int i;
70 int WeightBest;
71 int WeightCur;
72 int iNum, fBestS;
73
74 // collect the top entries from the queues
75 for ( nSingles = 0; nSingles < MAX_SIZE_LOOKAHEAD; nSingles++ )
76 {
77 pSingles[nSingles] = Fxu_HeapSingleGetMax( p->pHeapSingle );
78 if ( pSingles[nSingles] == NULL )
79 break;
80 }
81 // put them back into the queue
82 for ( i = 0; i < nSingles; i++ )
83 if ( pSingles[i] )
84 Fxu_HeapSingleInsert( p->pHeapSingle, pSingles[i] );
85
86 // the same for doubles
87 // collect the top entries from the queues
88 for ( nDoubles = 0; nDoubles < MAX_SIZE_LOOKAHEAD; nDoubles++ )
89 {
90 pDoubles[nDoubles] = Fxu_HeapDoubleGetMax( p->pHeapDouble );
91 if ( pDoubles[nDoubles] == NULL )
92 break;
93 }
94 // put them back into the queue
95 for ( i = 0; i < nDoubles; i++ )
96 if ( pDoubles[i] )
97 Fxu_HeapDoubleInsert( p->pHeapDouble, pDoubles[i] );
98
99 // for each single, find the complement double (if any)
100 for ( i = 0; i < nSingles; i++ )
101 if ( pSingles[i] )
102 pSCompl[i] = Fxu_MatrixFindComplementSingle( p, pSingles[i] );
103
104 // for each double, find the complement single or double (if any)
105 for ( i = 0; i < nDoubles; i++ )
106 if ( pDoubles[i] )
107 {
108 pPair = pDoubles[i]->lPairs.pHead;
109 if ( pPair->nLits1 == 1 && pPair->nLits2 == 1 )
110 {
111 pDComplS[i] = Fxu_MatrixFindComplementDouble2( p, pDoubles[i] );
112 pDComplD[i] = NULL;
113 }
114// else if ( pPair->nLits1 == 2 && pPair->nLits2 == 2 )
115// {
116// pDComplS[i] = NULL;
117// pDComplD[i] = Fxu_MatrixFindComplementDouble4( p, pDoubles[i] );
118// }
119 else
120 {
121 pDComplS[i] = NULL;
122 pDComplD[i] = NULL;
123 }
124 }
125
126 // select the best pair
127 WeightBest = -1;
128 for ( i = 0; i < nSingles; i++ )
129 {
130 WeightCur = pSingles[i]->Weight;
131 if ( pSCompl[i] )
132 {
133 // add the weight of the double
134 WeightCur += pSCompl[i]->Weight;
135 // there is no need to implement this double, so...
136 pPair = pSCompl[i]->lPairs.pHead;
137 WeightCur += pPair->nLits1 + pPair->nLits2;
138 }
139 if ( WeightBest < WeightCur )
140 {
141 WeightBest = WeightCur;
142 *ppSingle = pSingles[i];
143 *ppDouble = pSCompl[i];
144 fBestS = 1;
145 iNum = i;
146 }
147 }
148 for ( i = 0; i < nDoubles; i++ )
149 {
150 WeightCur = pDoubles[i]->Weight;
151 if ( pDComplS[i] )
152 {
153 // add the weight of the single
154 WeightCur += pDComplS[i]->Weight;
155 // there is no need to implement this double, so...
156 pPair = pDoubles[i]->lPairs.pHead;
157 WeightCur += pPair->nLits1 + pPair->nLits2;
158 }
159 if ( WeightBest < WeightCur )
160 {
161 WeightBest = WeightCur;
162 *ppSingle = pDComplS[i];
163 *ppDouble = pDoubles[i];
164 fBestS = 0;
165 iNum = i;
166 }
167 }
168/*
169 // print the statistics
170 printf( "\n" );
171 for ( i = 0; i < nSingles; i++ )
172 {
173 printf( "Single #%d: Weight = %3d. ", i, pSingles[i]->Weight );
174 printf( "Compl: " );
175 if ( pSCompl[i] == NULL )
176 printf( "None." );
177 else
178 printf( "D Weight = %3d Sum = %3d",
179 pSCompl[i]->Weight, pSCompl[i]->Weight + pSingles[i]->Weight );
180 printf( "\n" );
181 }
182 printf( "\n" );
183 for ( i = 0; i < nDoubles; i++ )
184 {
185 printf( "Double #%d: Weight = %3d. ", i, pDoubles[i]->Weight );
186 printf( "Compl: " );
187 if ( pDComplS[i] == NULL && pDComplD[i] == NULL )
188 printf( "None." );
189 else if ( pDComplS[i] )
190 printf( "S Weight = %3d Sum = %3d",
191 pDComplS[i]->Weight, pDComplS[i]->Weight + pDoubles[i]->Weight );
192 else if ( pDComplD[i] )
193 printf( "D Weight = %3d Sum = %3d",
194 pDComplD[i]->Weight, pDComplD[i]->Weight + pDoubles[i]->Weight );
195 printf( "\n" );
196 }
197 if ( WeightBest == -1 )
198 printf( "Selected NONE\n" );
199 else
200 {
201 printf( "Selected = %s. ", fBestS? "S": "D" );
202 printf( "Number = %d. ", iNum );
203 printf( "Weight = %d.\n", WeightBest );
204 }
205 printf( "\n" );
206*/
207 return WeightBest;
208}
Fxu_HeapDoubleInsert
void Fxu_HeapDoubleInsert(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:201
Fxu_HeapDoubleGetMax
Fxu_Double * Fxu_HeapDoubleGetMax(Fxu_HeapDouble *p)
Definition fxuHeapD.c:291
Fxu_HeapSingleGetMax
Fxu_Single * Fxu_HeapSingleGetMax(Fxu_HeapSingle *p)
Definition fxuHeapS.c:293
Fxu_HeapSingleInsert
void Fxu_HeapSingleInsert(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:204
Fxu_Single
struct FxuSingle Fxu_Single
Definition fxuInt.h:73
MAX_SIZE_LOOKAHEAD
#define MAX_SIZE_LOOKAHEAD
DECLARATIONS ///.
Definition fxuSelect.c:28
FxuDouble::Weight
int Weight
Definition fxuInt.h:258
FxuSingle::Weight
int Weight
Definition fxuInt.h:271
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_SelectSCD()

int Fxu_SelectSCD ( Fxu_Matrix * p,
int WeightLimit,
Fxu_Var ** ppVar1,
Fxu_Var ** ppVar2 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 525 of file fxuSelect.c.

526{
527// int * pValue2Node = p->pValue2Node;
528 Fxu_Var * pVar1;
529 Fxu_Var * pVar2, * pVarTemp;
530 Fxu_Lit * pLitV, * pLitH;
531 int Coin;
532 int CounterAll;
533 int CounterTest;
534 int WeightCur;
535 int WeightBest;
536
537 CounterAll = 0;
538 CounterTest = 0;
539
540 WeightBest = -10;
541
542 // iterate through the columns in the matrix
543 Fxu_MatrixForEachVariable( p, pVar1 )
544 {
545 // start collecting the affected vars
546 Fxu_MatrixRingVarsStart( p );
547
548 // go through all the literals of this variable
549 for ( pLitV = pVar1->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
550 {
551 // for this literal, go through all the horizontal literals
552 for ( pLitH = pLitV->pHNext; pLitH; pLitH = pLitH->pHNext )
553 {
554 // get another variable
555 pVar2 = pLitH->pVar;
556 CounterAll++;
557 // skip the var if it is already used
558 if ( pVar2->pOrder )
559 continue;
560 // skip the var if it belongs to the same node
561// if ( pValue2Node[pVar1->iVar] == pValue2Node[pVar2->iVar] )
562// continue;
563 // collect the var
564 Fxu_MatrixRingVarsAdd( p, pVar2 );
565 }
566 }
567 // stop collecting the selected vars
568 Fxu_MatrixRingVarsStop( p );
569
570 // iterate through the selected vars
571 Fxu_MatrixForEachVarInRing( p, pVar2 )
572 {
573 CounterTest++;
574
575 // count the coincidence
576 Coin = Fxu_SingleCountCoincidence( p, pVar1, pVar2 );
577 assert( Coin > 0 );
578
579 // get the new weight
580 WeightCur = Coin - 2;
581
582 // compare the weights
583 if ( WeightBest < WeightCur )
584 {
585 WeightBest = WeightCur;
586 *ppVar1 = pVar1;
587 *ppVar2 = pVar2;
588 }
589 }
590 // unmark the vars
591 Fxu_MatrixForEachVarInRingSafe( p, pVar2, pVarTemp )
592 pVar2->pOrder = NULL;
593 Fxu_MatrixRingVarsReset( p );
594 }
595
596// if ( WeightBest == WeightLimit )
597// return -1;
598 return WeightBest;
599}
Fxu_MatrixForEachVarInRing
#define Fxu_MatrixForEachVarInRing(Matrix, Var)
Definition fxuInt.h:407
Fxu_SingleCountCoincidence
int Fxu_SingleCountCoincidence(Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2)
Definition fxuSingle.c:241
Fxu_Var
struct FxuVar Fxu_Var
Definition fxuInt.h:67
Fxu_MatrixRingVarsStart
#define Fxu_MatrixRingVarsStart( Matrix)
Definition fxuInt.h:386
Fxu_MatrixRingVarsAdd
#define Fxu_MatrixRingVarsAdd( Matrix, Var)
Definition fxuInt.h:395
Fxu_MatrixForEachVarInRingSafe
#define Fxu_MatrixForEachVarInRingSafe(Matrix, Var, Var2)
Definition fxuInt.h:412
Fxu_MatrixRingVarsReset
#define Fxu_MatrixRingVarsReset( Matrix)
Definition fxuInt.h:392
Fxu_MatrixRingVarsStop
#define Fxu_MatrixRingVarsStop( Matrix)
Definition fxuInt.h:389
Fxu_MatrixForEachVariable
#define Fxu_MatrixForEachVariable(Matrix, Var)
Definition fxuInt.h:303
FxuLit::pVNext
Fxu_Lit * pVNext
Definition fxuInt.h:235
FxuLit::pVar
Fxu_Var * pVar
Definition fxuInt.h:231
FxuVar::pOrder
Fxu_Var * pOrder
Definition fxuInt.h:222
FxuVar::lLits
Fxu_ListLit lLits
Definition fxuInt.h:219
Here is the call graph for this function: