1 files changed, 222 insertions, 0 deletions
diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h
new file mode 100644
index 00000000..129c2f50
--- /dev/null
+++ b/src/sat/xsat/xsatMemory.h
@@ -0,0 +1,222 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////