xSAT is an experimental SAT Solver based on Glucose v3(see Glucose copyrights below) and ABC C version of

MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. It’s development has reached
sufficient maturity to be committed in ABC, but still in a beta state.

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.

1 files changed, 225 insertions, 0 deletions

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 <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_
+{
+    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                                ///
+////////////////////////////////////////////////////////////////////////