| /**CFile**************************************************************** |
| |
| FileName [msatVec.c] |
| |
| PackageName [A C version of SAT solver MINISAT, originally developed |
| in C++ by Niklas Een and Niklas Sorensson, Chalmers University of |
| Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] |
| |
| Synopsis [Integer vector borrowed from Extra.] |
| |
| Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - January 1, 2004.] |
| |
| Revision [$Id: msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "msatInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static int Msat_IntVecSortCompare1( int * pp1, int * pp2 ); |
| static int Msat_IntVecSortCompare2( int * pp1, int * pp2 ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Allocates a vector with the given capacity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) |
| { |
| Msat_IntVec_t * p; |
| p = ABC_ALLOC( Msat_IntVec_t, 1 ); |
| if ( nCap > 0 && nCap < 16 ) |
| nCap = 16; |
| p->nSize = 0; |
| p->nCap = nCap; |
| p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates the vector from an integer array of the given size.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) |
| { |
| Msat_IntVec_t * p; |
| p = ABC_ALLOC( Msat_IntVec_t, 1 ); |
| p->nSize = nSize; |
| p->nCap = nSize; |
| p->pArray = pArray; |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates the vector from an integer array of the given size.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) |
| { |
| Msat_IntVec_t * p; |
| p = ABC_ALLOC( Msat_IntVec_t, 1 ); |
| p->nSize = nSize; |
| p->nCap = nSize; |
| p->pArray = ABC_ALLOC( int, nSize ); |
| memcpy( p->pArray, pArray, sizeof(int) * nSize ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the integer array.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) |
| { |
| Msat_IntVec_t * p; |
| p = ABC_ALLOC( Msat_IntVec_t, 1 ); |
| p->nSize = pVec->nSize; |
| p->nCap = pVec->nCap; |
| p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; |
| memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transfers the array into another vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) |
| { |
| Msat_IntVec_t * p; |
| p = ABC_ALLOC( Msat_IntVec_t, 1 ); |
| p->nSize = pVec->nSize; |
| p->nCap = pVec->nCap; |
| p->pArray = pVec->pArray; |
| pVec->nSize = 0; |
| pVec->nCap = 0; |
| pVec->pArray = NULL; |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecFree( Msat_IntVec_t * p ) |
| { |
| ABC_FREE( p->pArray ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Fills the vector with given number of entries.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry ) |
| { |
| int i; |
| Msat_IntVecGrow( p, nSize ); |
| p->nSize = nSize; |
| for ( i = 0; i < p->nSize; i++ ) |
| p->pArray[i] = Entry; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Msat_IntVecReleaseArray( Msat_IntVec_t * p ) |
| { |
| int * pArray = p->pArray; |
| p->nCap = 0; |
| p->nSize = 0; |
| p->pArray = NULL; |
| return pArray; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Msat_IntVecReadArray( Msat_IntVec_t * p ) |
| { |
| return p->pArray; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecReadSize( Msat_IntVec_t * p ) |
| { |
| return p->nSize; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i ) |
| { |
| assert( i >= 0 && i < p->nSize ); |
| return p->pArray[i]; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry ) |
| { |
| assert( i >= 0 && i < p->nSize ); |
| p->pArray[i] = Entry; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecReadEntryLast( Msat_IntVec_t * p ) |
| { |
| return p->pArray[p->nSize-1]; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resizes the vector to the given capacity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ) |
| { |
| if ( p->nCap >= nCapMin ) |
| return; |
| p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); |
| p->nCap = nCapMin; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew ) |
| { |
| assert( p->nSize >= nSizeNew ); |
| p->nSize = nSizeNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecClear( Msat_IntVec_t * p ) |
| { |
| p->nSize = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecPush( Msat_IntVec_t * p, int Entry ) |
| { |
| if ( p->nSize == p->nCap ) |
| { |
| if ( p->nCap < 16 ) |
| Msat_IntVecGrow( p, 16 ); |
| else |
| Msat_IntVecGrow( p, 2 * p->nCap ); |
| } |
| p->pArray[p->nSize++] = 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 [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry ) |
| { |
| int i; |
| for ( i = 0; i < p->nSize; i++ ) |
| if ( p->pArray[i] == Entry ) |
| return 1; |
| Msat_IntVecPush( p, Entry ); |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts the element while sorting in the increasing order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease ) |
| { |
| int Entry1, Entry2; |
| int i; |
| Msat_IntVecPushUnique( p, Entry ); |
| // find the p of the node |
| for ( i = p->nSize-1; i > 0; i-- ) |
| { |
| Entry1 = p->pArray[i ]; |
| Entry2 = p->pArray[i-1]; |
| if (( fIncrease && Entry1 >= Entry2) || |
| (!fIncrease && Entry1 <= Entry2) ) |
| break; |
| p->pArray[i ] = Entry2; |
| p->pArray[i-1] = Entry1; |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the last entry and removes it from the list.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecPop( Msat_IntVec_t * p ) |
| { |
| assert( p->nSize > 0 ); |
| return p->pArray[--p->nSize]; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sorting the entries by their integer value.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse ) |
| { |
| if ( fReverse ) |
| qsort( (void *)p->pArray, p->nSize, sizeof(int), |
| (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 ); |
| else |
| qsort( (void *)p->pArray, p->nSize, sizeof(int), |
| (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Comparison procedure for two clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecSortCompare1( int * pp1, int * pp2 ) |
| { |
| // for some reason commenting out lines (as shown) led to crashing of the release version |
| if ( *pp1 < *pp2 ) |
| return -1; |
| if ( *pp1 > *pp2 ) // |
| return 1; |
| return 0; // |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Comparison procedure for two clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_IntVecSortCompare2( int * pp1, int * pp2 ) |
| { |
| // for some reason commenting out lines (as shown) led to crashing of the release version |
| if ( *pp1 > *pp2 ) |
| return -1; |
| if ( *pp1 < *pp2 ) // |
| return 1; |
| return 0; // |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
