| /**CFile**************************************************************** |
| |
| FileName [xsatMemory.h] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [xSAT - A SAT solver written in C. |
| Read the license file for more info.] |
| |
| Synopsis [Memory management implementation.] |
| |
| Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] |
| |
| Affiliation [UC Berkeley / UFRGS] |
| |
| Date [Ver. 1.0. Started - November 10, 2016.] |
| |
| Revision [] |
| |
| ***********************************************************************/ |
| #ifndef ABC__sat__xSAT__xsatMemory_h |
| #define ABC__sat__xSAT__xsatMemory_h |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// INCLUDES /// |
| //////////////////////////////////////////////////////////////////////// |
| #include "misc/util/abc_global.h" |
| |
| #include "xsatClause.h" |
| |
| ABC_NAMESPACE_HEADER_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// STRUCTURE DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| typedef struct xSAT_Mem_t_ xSAT_Mem_t; |
| struct xSAT_Mem_t_ |
| { |
| unsigned nSize; |
| unsigned nCap; |
| unsigned nWasted; |
| unsigned * pData; |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h ) |
| { |
| return h != 0xFFFFFFFF ? ( xSAT_Clause_t * )( p->pData + h ) : NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap ) |
| { |
| unsigned nPrevCap = p->nCap; |
| if ( p->nCap >= nCap ) |
| return; |
| while (p->nCap < nCap) |
| { |
| unsigned delta = ( ( p->nCap >> 1 ) + ( p->nCap >> 3 ) + 2 ) & ~1; |
| p->nCap += delta; |
| assert(p->nCap >= nPrevCap); |
| } |
| assert(p->nCap > 0); |
| p->pData = ABC_REALLOC( unsigned, p->pData, p->nCap ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Allocating vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline xSAT_Mem_t * xSAT_MemAlloc( int nCap ) |
| { |
| xSAT_Mem_t * p; |
| p = ABC_CALLOC( xSAT_Mem_t, 1 ); |
| if (nCap <= 0) |
| nCap = 1024*1024; |
| |
| xSAT_MemGrow(p, nCap); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resetting vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void xSAT_MemRestart( xSAT_Mem_t * p ) |
| { |
| p->nSize = 0; |
| p->nWasted = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Freeing vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void xSAT_MemFree( xSAT_Mem_t * p ) |
| { |
| ABC_FREE( p->pData ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates new clause.] |
| |
| Description [The resulting clause is fully initialized.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) |
| { |
| unsigned nPrevSize; |
| assert(nSize > 0); |
| xSAT_MemGrow( p, p->nSize + nSize ); |
| nPrevSize = p->nSize; |
| p->nSize += nSize; |
| assert(p->nSize > nPrevSize); |
| return nPrevSize; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned xSAT_MemCRef( xSAT_Mem_t * p, unsigned * pC ) |
| { |
| return ( unsigned )( pC - &(p->pData[0]) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned xSAT_MemCap( xSAT_Mem_t * p ) |
| { |
| return p->nCap; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned xSAT_MemWastedCap( xSAT_Mem_t * p ) |
| { |
| return p->nWasted; |
| } |
| |
| ABC_NAMESPACE_HEADER_END |
| |
| #endif |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
