src/sat/fraig/fraigVec.c File Reference

#include "fraigInt.h"
Include dependency graph for fraigVec.c:

Go to the source code of this file.

Functions

Fraig_NodeVec_t * Fraig_NodeVecAlloc (int nCap)
void Fraig_NodeVecFree (Fraig_NodeVec_t *p)
Fraig_NodeVec_t * Fraig_NodeVecDup (Fraig_NodeVec_t *pVec)
Fraig_Node_t ** Fraig_NodeVecReadArray (Fraig_NodeVec_t *p)
int Fraig_NodeVecReadSize (Fraig_NodeVec_t *p)
void Fraig_NodeVecGrow (Fraig_NodeVec_t *p, int nCapMin)
void Fraig_NodeVecShrink (Fraig_NodeVec_t *p, int nSizeNew)
void Fraig_NodeVecClear (Fraig_NodeVec_t *p)
void Fraig_NodeVecPush (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
int Fraig_NodeVecPushUnique (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
void Fraig_NodeVecPushOrder (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
int Fraig_NodeVecPushUniqueOrder (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
void Fraig_NodeVecPushOrderByLevel (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
int Fraig_NodeVecPushUniqueOrderByLevel (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
Fraig_Node_t * Fraig_NodeVecPop (Fraig_NodeVec_t *p)
void Fraig_NodeVecRemove (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
void Fraig_NodeVecWriteEntry (Fraig_NodeVec_t *p, int i, Fraig_Node_t *Entry)
Fraig_Node_t * Fraig_NodeVecReadEntry (Fraig_NodeVec_t *p, int i)
int Fraig_NodeVecCompareLevelsIncreasing (Fraig_Node_t **pp1, Fraig_Node_t **pp2)
int Fraig_NodeVecCompareLevelsDecreasing (Fraig_Node_t **pp1, Fraig_Node_t **pp2)
int Fraig_NodeVecCompareNumbers (Fraig_Node_t **pp1, Fraig_Node_t **pp2)
int Fraig_NodeVecCompareRefCounts (Fraig_Node_t **pp1, Fraig_Node_t **pp2)
void Fraig_NodeVecSortByLevel (Fraig_NodeVec_t *p, int fIncreasing)
void Fraig_NodeVecSortByNumber (Fraig_NodeVec_t *p)
void Fraig_NodeVecSortByRefCount (Fraig_NodeVec_t *p)

Function Documentation

Fraig_NodeVec_t* Fraig_NodeVecAlloc ( int  nCap  ) 

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

FileName [fraigVec.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Vector of FRAIG nodes.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id
fraigVec.c,v 1.7 2005/07/08 01:01:34 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 40 of file fraigVec.c.

00041 {
00042     Fraig_NodeVec_t * p;
00043     p = ALLOC( Fraig_NodeVec_t, 1 );
00044     if ( nCap > 0 && nCap < 8 )
00045         nCap = 8;
00046     p->nSize  = 0;
00047     p->nCap   = nCap;
00048     p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
00049     return p;
00050 }

void Fraig_NodeVecClear ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file fraigVec.c.

00171 {
00172     p->nSize = 0;
00173 }

int Fraig_NodeVecCompareLevelsDecreasing ( Fraig_Node_t **  pp1,
Fraig_Node_t **  pp2 
)

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 423 of file fraigVec.c.

00424 {
00425     int Level1 = Fraig_Regular(*pp1)->Level;
00426     int Level2 = Fraig_Regular(*pp2)->Level;
00427     if ( Level1 > Level2 )
00428         return -1;
00429     if ( Level1 < Level2 )
00430         return 1;
00431     return 0; 
00432 }

int Fraig_NodeVecCompareLevelsIncreasing ( Fraig_Node_t **  pp1,
Fraig_Node_t **  pp2 
)

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file fraigVec.c.

00402 {
00403     int Level1 = Fraig_Regular(*pp1)->Level;
00404     int Level2 = Fraig_Regular(*pp2)->Level;
00405     if ( Level1 < Level2 )
00406         return -1;
00407     if ( Level1 > Level2 )
00408         return 1;
00409     return 0; 
00410 }

int Fraig_NodeVecCompareNumbers ( Fraig_Node_t **  pp1,
Fraig_Node_t **  pp2 
)

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 445 of file fraigVec.c.

00446 {
00447     int Num1 = Fraig_Regular(*pp1)->Num;
00448     int Num2 = Fraig_Regular(*pp2)->Num;
00449     if ( Num1 < Num2 )
00450         return -1;
00451     if ( Num1 > Num2 )
00452         return 1;
00453     return 0; 
00454 }

int Fraig_NodeVecCompareRefCounts ( Fraig_Node_t **  pp1,
Fraig_Node_t **  pp2 
)

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 467 of file fraigVec.c.

00468 {
00469     int nRefs1 = Fraig_Regular(*pp1)->nRefs;
00470     int nRefs2 = Fraig_Regular(*pp2)->nRefs;
00471 
00472     if ( nRefs1 < nRefs2 )
00473         return -1;
00474     if ( nRefs1 > nRefs2 )
00475         return 1;
00476 
00477     nRefs1 = Fraig_Regular(*pp1)->Level;
00478     nRefs2 = Fraig_Regular(*pp2)->Level;
00479 
00480     if ( nRefs1 < nRefs2 )
00481         return -1;
00482     if ( nRefs1 > nRefs2 )
00483         return 1;
00484     return 0; 
00485 }

Fraig_NodeVec_t* Fraig_NodeVecDup ( Fraig_NodeVec_t *  pVec  ) 

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

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file fraigVec.c.

00081 {
00082     Fraig_NodeVec_t * p;
00083     p = ALLOC( Fraig_NodeVec_t, 1 );
00084     p->nSize  = pVec->nSize;
00085     p->nCap   = pVec->nCap;
00086     p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
00087     memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize );
00088     return p;
00089 }

void Fraig_NodeVecFree ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file fraigVec.c.

00064 {
00065     FREE( p->pArray );
00066     FREE( p );
00067 }

void Fraig_NodeVecGrow ( Fraig_NodeVec_t *  p,
int  nCapMin 
)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fraigVec.c.

00135 {
00136     if ( p->nCap >= nCapMin )
00137         return;
00138     p->pArray = REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); 
00139     p->nCap   = nCapMin;
00140 }

Fraig_Node_t* Fraig_NodeVecPop ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file fraigVec.c.

00329 {
00330     return p->pArray[--p->nSize];
00331 }

void Fraig_NodeVecPush ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file fraigVec.c.

00187 {
00188     if ( p->nSize == p->nCap )
00189     {
00190         if ( p->nCap < 16 )
00191             Fraig_NodeVecGrow( p, 16 );
00192         else
00193             Fraig_NodeVecGrow( p, 2 * p->nCap );
00194     }
00195     p->pArray[p->nSize++] = Entry;
00196 }

void Fraig_NodeVecPushOrder ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Inserts a new node in the order by arrival times.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file fraigVec.c.

00231 {
00232     Fraig_Node_t * pNode1, * pNode2;
00233     int i;
00234     Fraig_NodeVecPush( p, pNode );
00235     // find the p of the node
00236     for ( i = p->nSize-1; i > 0; i-- )
00237     {
00238         pNode1 = p->pArray[i  ];
00239         pNode2 = p->pArray[i-1];
00240         if ( pNode1 >= pNode2 )
00241             break;
00242         p->pArray[i  ] = pNode2;
00243         p->pArray[i-1] = pNode1;
00244     }
00245 }

void Fraig_NodeVecPushOrderByLevel ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Inserts a new node in the order by arrival times.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file fraigVec.c.

00280 {
00281     Fraig_Node_t * pNode1, * pNode2;
00282     int i;
00283     Fraig_NodeVecPush( p, pNode );
00284     // find the p of the node
00285     for ( i = p->nSize-1; i > 0; i-- )
00286     {
00287         pNode1 = p->pArray[i  ];
00288         pNode2 = p->pArray[i-1];
00289         if ( Fraig_Regular(pNode1)->Level <= Fraig_Regular(pNode2)->Level )
00290             break;
00291         p->pArray[i  ] = pNode2;
00292         p->pArray[i-1] = pNode1;
00293     }
00294 }

int Fraig_NodeVecPushUnique ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis [Add the element while ensuring uniqueness.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 209 of file fraigVec.c.

00210 {
00211     int i;
00212     for ( i = 0; i < p->nSize; i++ )
00213         if ( p->pArray[i] == Entry )
00214             return 1;
00215     Fraig_NodeVecPush( p, Entry );
00216     return 0;
00217 }

int Fraig_NodeVecPushUniqueOrder ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Add the element while ensuring uniqueness in the order.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 258 of file fraigVec.c.

00259 {
00260     int i;
00261     for ( i = 0; i < p->nSize; i++ )
00262         if ( p->pArray[i] == pNode )
00263             return 1;
00264     Fraig_NodeVecPushOrder( p, pNode );
00265     return 0;
00266 }

int Fraig_NodeVecPushUniqueOrderByLevel ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Add the element while ensuring uniqueness in the order.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 307 of file fraigVec.c.

00308 {
00309     int i;
00310     for ( i = 0; i < p->nSize; i++ )
00311         if ( p->pArray[i] == pNode )
00312             return 1;
00313     Fraig_NodeVecPushOrderByLevel( p, pNode );
00314     return 0;
00315 }

Fraig_Node_t** Fraig_NodeVecReadArray ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file fraigVec.c.

00103 {
00104     return p->pArray;
00105 }

Fraig_Node_t* Fraig_NodeVecReadEntry ( Fraig_NodeVec_t *  p,
int  i 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file fraigVec.c.

00385 {
00386     assert( i >= 0 && i < p->nSize );
00387     return p->pArray[i];
00388 }

int Fraig_NodeVecReadSize ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file fraigVec.c.

00119 {
00120     return p->nSize;
00121 }

void Fraig_NodeVecRemove ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file fraigVec.c.

00345 {
00346     int i;
00347     for ( i = 0; i < p->nSize; i++ )
00348         if ( p->pArray[i] == Entry )
00349             break;
00350     assert( i < p->nSize );
00351     for ( i++; i < p->nSize; i++ )
00352         p->pArray[i-1] = p->pArray[i];
00353     p->nSize--;
00354 }

void Fraig_NodeVecShrink ( Fraig_NodeVec_t *  p,
int  nSizeNew 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file fraigVec.c.

00154 {
00155     assert( p->nSize >= nSizeNew );
00156     p->nSize = nSizeNew;
00157 }

void Fraig_NodeVecSortByLevel ( Fraig_NodeVec_t *  p,
int  fIncreasing 
)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file fraigVec.c.

00499 {
00500     if ( fIncreasing )
00501         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00502                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsIncreasing );
00503     else 
00504         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00505                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsDecreasing );
00506 }

void Fraig_NodeVecSortByNumber ( Fraig_NodeVec_t *  p  ) 

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 519 of file fraigVec.c.

00520 {
00521     qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00522             (int (*)(const void *, const void *)) Fraig_NodeVecCompareNumbers );
00523 }

void Fraig_NodeVecSortByRefCount ( Fraig_NodeVec_t *  p  ) 

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 536 of file fraigVec.c.

00537 {
00538     qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00539             (int (*)(const void *, const void *)) Fraig_NodeVecCompareRefCounts );
00540 }

void Fraig_NodeVecWriteEntry ( Fraig_NodeVec_t *  p,
int  i,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file fraigVec.c.

00368 {
00369     assert( i >= 0 && i < p->nSize );
00370     p->pArray[i] = Entry;
00371 }

Generated on Tue Jan 5 12:19:39 2010 for abc70930 by  doxygen 1.6.1