/**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