From 5351ab4b13aa46db5710ca3ffe659e8e691ba126 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Mon, 12 Dec 2016 16:20:38 -0200 Subject: =?UTF-8?q?xSAT=20is=20an=20experimental=20SAT=20Solver=20based=20?= =?UTF-8?q?on=20Glucose=20v3(see=20Glucose=20copyrights=20below)=20and=20A?= =?UTF-8?q?BC=20C=20version=20of=20MiniSat=20(bsat)=20developed=20by=20Nik?= =?UTF-8?q?las=20Sorensson=20and=20modified=20by=20Alan=20Mishchenko.=20It?= =?UTF-8?q?=E2=80=99s=20development=20has=20reached=20sufficient=20maturit?= =?UTF-8?q?y=20to=20be=20committed=20in=20ABC,=20but=20still=20in=20a=20be?= =?UTF-8?q?ta=20state.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TODO: * Read compressed CNF files. * Study the use of floating point for variables and clauses activity. * Better documentation. * Improve verbose messages. * Expose parameters for tuning. --- src/sat/xsat/xsatMemory.h | 225 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 225 insertions(+) create mode 100644 src/sat/xsat/xsatMemory.h (limited to 'src/sat/xsat/xsatMemory.h') diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h new file mode 100644 index 00000000..3a961b97 --- /dev/null +++ b/src/sat/xsat/xsatMemory.h @@ -0,0 +1,225 @@ +/**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 ] + + 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_ +{ + uint32_t nSize; + uint32_t nCap; + uint32_t nWasted; + uint32_t * pData; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h ) +{ + return h != UINT32_MAX ? ( xSAT_Clause_t * )( p->pData + h ) : NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_MemGrow( xSAT_Mem_t * p, uint32_t nCap ) +{ + if ( p->nCap >= nCap ) + return; + + uint32_t nPrevCap = p->nCap; + while (p->nCap < nCap) + { + uint32_t delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1; + p->nCap += delta; + assert(p->nCap >= nPrevCap); + } + + assert(p->nCap > 0); + p->pData = ABC_REALLOC(uint32_t, 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 uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) +{ + assert(nSize > 0); + xSAT_MemGrow(p, p->nSize + nSize); + + uint32_t nPrevSize = p->nSize; + p->nSize += nSize; + assert(p->nSize > nPrevSize); + + return nPrevSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC ) +{ + return ( uint32_t )( pC - &(p->pData[0]) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p ) +{ + return p->nCap; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemWastedCap( xSAT_Mem_t * p ) +{ + return p->nWasted; +} + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// -- cgit v1.2.3