summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/asat/asat60525.zipbin25597 -> 0 bytes
-rw-r--r--src/sat/bsat/module.make3
-rw-r--r--src/sat/bsat/satMem.c527
-rw-r--r--src/sat/bsat/satMem.h78
-rw-r--r--src/sat/bsat/satSolver.c (renamed from src/sat/asat_fixed/satSolver.c)267
-rw-r--r--src/sat/bsat/satSolver.h (renamed from src/sat/asat_fixed/satSolver.h)60
-rw-r--r--src/sat/bsat/satUtil.c161
-rw-r--r--src/sat/bsat/satVec.h83
-rw-r--r--src/sat/csat/csat_apis.c7
-rw-r--r--src/sat/fraig/fraigMan.c4
10 files changed, 1068 insertions, 122 deletions
diff --git a/src/sat/asat/asat60525.zip b/src/sat/asat/asat60525.zip
deleted file mode 100644
index b8361af1..00000000
--- a/src/sat/asat/asat60525.zip
+++ /dev/null
Binary files differ
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
new file mode 100644
index 00000000..c8ec65dd
--- /dev/null
+++ b/src/sat/bsat/module.make
@@ -0,0 +1,3 @@
+SRC += src/sat/bsat/satMem.c \
+ src/sat/bsat/satSolver.c \
+ src/sat/bsat/satUtil.c
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
new file mode 100644
index 00000000..bb234f66
--- /dev/null
+++ b/src/sat/bsat/satMem.c
@@ -0,0 +1,527 @@
+/**CFile****************************************************************
+
+ FileName [satMem.c]
+
+ PackageName [SAT solver.]
+
+ Synopsis [Memory management.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: satMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "satMem.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct Sat_MmFixed_t_
+{
+ // information about individual entries
+ int nEntrySize; // the size of one entry
+ int nEntriesAlloc; // the total number of entries allocated
+ int nEntriesUsed; // the number of entries in use
+ int nEntriesMax; // the max number of entries in use
+ char * pEntriesFree; // the linked list of free entries
+
+ // this is where the memory is stored
+ int nChunkSize; // the size of one chunk
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
+
+ // statistics
+ int nMemoryUsed; // memory used in the allocated entries
+ int nMemoryAlloc; // memory allocated
+};
+
+struct Sat_MmFlex_t_
+{
+ // information about individual entries
+ int nEntriesUsed; // the number of entries allocated
+ char * pCurrent; // the current pointer to free memory
+ char * pEnd; // the first entry outside the free memory
+
+ // this is where the memory is stored
+ int nChunkSize; // the size of one chunk
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
+
+ // statistics
+ int nMemoryUsed; // memory used in the allocated entries
+ int nMemoryAlloc; // memory allocated
+};
+
+struct Sat_MmStep_t_
+{
+ int nMems; // the number of fixed memory managers employed
+ Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
+ int nMapSize; // the size of the memory array
+ Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates memory pieces of fixed size.]
+
+ Description [The size of the chunk is computed as the minimum of
+ 1024 entries and 64K. Can only work with entry size at least 4 byte long.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
+{
+ Sat_MmFixed_t * p;
+
+ p = ALLOC( Sat_MmFixed_t, 1 );
+ memset( p, 0, sizeof(Sat_MmFixed_t) );
+
+ p->nEntrySize = nEntrySize;
+ p->nEntriesAlloc = 0;
+ p->nEntriesUsed = 0;
+ p->pEntriesFree = NULL;
+
+ if ( nEntrySize * (1 << 10) < (1<<16) )
+ p->nChunkSize = (1 << 10);
+ else
+ p->nChunkSize = (1<<16) / nEntrySize;
+ if ( p->nChunkSize < 8 )
+ p->nChunkSize = 8;
+
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
+
+ p->nMemoryUsed = 0;
+ p->nMemoryAlloc = 0;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
+{
+ int i;
+ if ( p == NULL )
+ return;
+ if ( fVerbose )
+ {
+ printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+ p->nEntrySize, p->nChunkSize, p->nChunks );
+ printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+ p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+ }
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
+{
+ char * pTemp;
+ int i;
+
+ // check if there are still free entries
+ if ( p->nEntriesUsed == p->nEntriesAlloc )
+ { // need to allocate more entries
+ assert( p->pEntriesFree == NULL );
+ if ( p->nChunks == p->nChunksAlloc )
+ {
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
+ }
+ p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+ p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+ // transform these entries into a linked list
+ pTemp = p->pEntriesFree;
+ for ( i = 1; i < p->nChunkSize; i++ )
+ {
+ *((char **)pTemp) = pTemp + p->nEntrySize;
+ pTemp += p->nEntrySize;
+ }
+ // set the last link
+ *((char **)pTemp) = NULL;
+ // add the chunk to the chunk storage
+ p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+ // add to the number of entries allocated
+ p->nEntriesAlloc += p->nChunkSize;
+ }
+ // incrememt the counter of used entries
+ p->nEntriesUsed++;
+ if ( p->nEntriesMax < p->nEntriesUsed )
+ p->nEntriesMax = p->nEntriesUsed;
+ // return the first entry in the free entry list
+ pTemp = p->pEntriesFree;
+ p->pEntriesFree = *((char **)pTemp);
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
+{
+ // decrement the counter of used entries
+ p->nEntriesUsed--;
+ // add the entry to the linked list of free entries
+ *((char **)pEntry) = p->pEntriesFree;
+ p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description [Relocates all the memory except the first chunk.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedRestart( Sat_MmFixed_t * p )
+{
+ int i;
+ char * pTemp;
+
+ // deallocate all chunks except the first one
+ for ( i = 1; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ p->nChunks = 1;
+ // transform these entries into a linked list
+ pTemp = p->pChunks[0];
+ for ( i = 1; i < p->nChunkSize; i++ )
+ {
+ *((char **)pTemp) = pTemp + p->nEntrySize;
+ pTemp += p->nEntrySize;
+ }
+ // set the last link
+ *((char **)pTemp) = NULL;
+ // set the free entry list
+ p->pEntriesFree = p->pChunks[0];
+ // set the correct statistics
+ p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
+ p->nMemoryUsed = 0;
+ p->nEntriesAlloc = p->nChunkSize;
+ p->nEntriesUsed = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p )
+{
+ return p->nMemoryAlloc;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocates entries of flexible size.]
+
+ Description [Can only work with entry size at least 4 byte long.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmFlex_t * Sat_MmFlexStart()
+{
+ Sat_MmFlex_t * p;
+
+ p = ALLOC( Sat_MmFlex_t, 1 );
+ memset( p, 0, sizeof(Sat_MmFlex_t) );
+
+ p->nEntriesUsed = 0;
+ p->pCurrent = NULL;
+ p->pEnd = NULL;
+
+ p->nChunkSize = (1 << 12);
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
+
+ p->nMemoryUsed = 0;
+ p->nMemoryAlloc = 0;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
+{
+ int i;
+ if ( p == NULL )
+ return;
+ if ( fVerbose )
+ {
+ printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
+ p->nChunkSize, p->nChunks );
+ printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
+ p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
+ }
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
+{
+ char * pTemp;
+ // check if there are still free entries
+ if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
+ { // need to allocate more entries
+ if ( p->nChunks == p->nChunksAlloc )
+ {
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
+ }
+ if ( nBytes > p->nChunkSize )
+ {
+ // resize the chunk size if more memory is requested than it can give
+ // (ideally, this should never happen)
+ p->nChunkSize = 2 * nBytes;
+ }
+ p->pCurrent = ALLOC( char, p->nChunkSize );
+ p->pEnd = p->pCurrent + p->nChunkSize;
+ p->nMemoryAlloc += p->nChunkSize;
+ // add the chunk to the chunk storage
+ p->pChunks[ p->nChunks++ ] = p->pCurrent;
+ }
+ assert( p->pCurrent + nBytes <= p->pEnd );
+ // increment the counter of used entries
+ p->nEntriesUsed++;
+ // keep track of the memory used
+ p->nMemoryUsed += nBytes;
+ // return the next entry
+ pTemp = p->pCurrent;
+ p->pCurrent += nBytes;
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p )
+{
+ return p->nMemoryAlloc;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Starts the hierarchical memory manager.]
+
+ Description [This manager can allocate entries of any size.
+ Iternally they are mapped into the entries with the number of bytes
+ equal to the power of 2. The smallest entry size is 8 bytes. The
+ next one is 16 bytes etc. So, if the user requests 6 bytes, he gets
+ 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
+ The input parameters "nSteps" says how many fixed memory managers
+ are employed internally. Calling this procedure with nSteps equal
+ to 10 results in 10 hierarchically arranged internal memory managers,
+ which can allocate up to 4096 (1Kb) entries. Requests for larger
+ entries are handed over to malloc() and then free()ed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmStep_t * Sat_MmStepStart( int nSteps )
+{
+ Sat_MmStep_t * p;
+ int i, k;
+ p = ALLOC( Sat_MmStep_t, 1 );
+ p->nMems = nSteps;
+ // start the fixed memory managers
+ p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
+ for ( i = 0; i < p->nMems; i++ )
+ p->pMems[i] = Sat_MmFixedStart( (8<<i) );
+ // set up the mapping of the required memory size into the corresponding manager
+ p->nMapSize = (4<<p->nMems);
+ p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
+ p->pMap[0] = NULL;
+ for ( k = 1; k <= 4; k++ )
+ p->pMap[k] = p->pMems[0];
+ for ( i = 0; i < p->nMems; i++ )
+ for ( k = (4<<i)+1; k <= (8<<i); k++ )
+ p->pMap[k] = p->pMems[i];
+//for ( i = 1; i < 100; i ++ )
+//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the memory manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
+{
+ int i;
+ for ( i = 0; i < p->nMems; i++ )
+ Sat_MmFixedStop( p->pMems[i], fVerbose );
+ free( p->pMems );
+ free( p->pMap );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
+{
+ if ( nBytes == 0 )
+ return NULL;
+ if ( nBytes > p->nMapSize )
+ {
+// printf( "Allocating %d bytes.\n", nBytes );
+ return ALLOC( char, nBytes );
+ }
+ return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
+{
+ if ( nBytes == 0 )
+ return;
+ if ( nBytes > p->nMapSize )
+ {
+ free( pEntry );
+ return;
+ }
+ Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmStepReadMemUsage( Sat_MmStep_t * p )
+{
+ int i, nMemTotal = 0;
+ for ( i = 0; i < p->nMems; i++ )
+ nMemTotal += p->pMems[i]->nMemoryAlloc;
+ return nMemTotal;
+}
diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h
new file mode 100644
index 00000000..5c5ddd9c
--- /dev/null
+++ b/src/sat/bsat/satMem.h
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+ FileName [satMem.h]
+
+ PackageName [SAT solver.]
+
+ Synopsis [Memory management.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SAT_MEM_H__
+#define __SAT_MEM_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"
+#include <stdio.h>
+#include <stdlib.h>
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sat_MmFixed_t_ Sat_MmFixed_t;
+typedef struct Sat_MmFlex_t_ Sat_MmFlex_t;
+typedef struct Sat_MmStep_t_ Sat_MmStep_t;
+
+////////////////////////////////////////////////////////////////////////
+/// GLOBAL VARIABLES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// fixed-size-block memory manager
+extern Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize );
+extern void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose );
+extern char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p );
+extern void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry );
+extern void Sat_MmFixedRestart( Sat_MmFixed_t * p );
+extern int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Sat_MmFlex_t * Sat_MmFlexStart();
+extern void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose );
+extern char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes );
+extern int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
+// hierarchical memory manager
+extern Sat_MmStep_t * Sat_MmStepStart( int nSteps );
+extern void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
+extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
+extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
+extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/asat_fixed/satSolver.c b/src/sat/bsat/satSolver.c
index d3b99c9d..a84c82ef 100644
--- a/src/sat/asat_fixed/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -21,9 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <stdio.h>
#include <assert.h>
+#include <string.h>
#include <math.h>
-#include "solver.h"
+#include "satSolver.h"
+
+//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
//=================================================================================================
// Debug:
@@ -32,7 +35,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
// For derivation output (verbosity level 2)
#define L_IND "%-*d"
-#define L_ind solver_dlevel(s)*3+3,solver_dlevel(s)
+#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
#define L_LIT "%sx%d"
#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
@@ -67,7 +70,7 @@ static inline int irand(double* seed, int size) {
//=================================================================================================
// Predeclarations:
-void sort(void** array, int size, int(*comp)(const void *, const void *));
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
//=================================================================================================
// Clause datatype + minor functions:
@@ -87,20 +90,19 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
-clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
-bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
-lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
+static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
+static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
+static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
//=================================================================================================
// Simple helpers:
-static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); }
-static inline vecp* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; }
+static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); }
+static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
static inline void vecp_remove(vecp* v, void* e)
{
void** ws = vecp_begin(v);
int j = 0;
-
for (; ws[j] != e ; j++);
assert(j < vecp_size(v));
for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
@@ -110,7 +112,7 @@ static inline void vecp_remove(vecp* v, void* e)
//=================================================================================================
// Variable order functions:
-static inline void order_update(solver* s, int v) // updateorder
+static inline void order_update(sat_solver* s, int v) // updateorder
{
int* orderpos = s->orderpos;
double* activity = s->activity;
@@ -131,21 +133,22 @@ static inline void order_update(solver* s, int v) // updateorder
orderpos[x] = i;
}
-static inline void order_assigned(solver* s, int v)
+static inline void order_assigned(sat_solver* s, int v)
{
}
-static inline void order_unassigned(solver* s, int v) // undoorder
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
{
int* orderpos = s->orderpos;
if (orderpos[v] == -1){
orderpos[v] = veci_size(&s->order);
veci_push(&s->order,v);
order_update(s,v);
+//printf( "+%d ", v );
}
}
-static int order_select(solver* s, float random_var_freq) // selectvar
+static int order_select(sat_solver* s, float random_var_freq) // selectvar
{
int* heap;
double* activity;
@@ -202,6 +205,7 @@ static int order_select(solver* s, float random_var_freq) // selectvar
orderpos[heap[i]] = i;
}
+//printf( "-%d ", next );
if (values[next] == l_Undef)
return next;
}
@@ -212,7 +216,7 @@ static int order_select(solver* s, float random_var_freq) // selectvar
//=================================================================================================
// Activity functions:
-static inline void act_var_rescale(solver* s) {
+static inline void act_var_rescale(sat_solver* s) {
double* activity = s->activity;
int i;
for (i = 0; i < s->size; i++)
@@ -220,21 +224,27 @@ static inline void act_var_rescale(solver* s) {
s->var_inc *= 1e-100;
}
-static inline void act_var_bump(solver* s, int v) {
- double* activity = s->activity;
- if ((activity[v] += s->var_inc) > 1e100)
+static inline void act_var_bump(sat_solver* s, int v) {
+ s->activity[v] += s->var_inc;
+ if (s->activity[v] > 1e100)
act_var_rescale(s);
-
//printf("bump %d %f\n", v-1, activity[v]);
-
if (s->orderpos[v] != -1)
order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+ s->activity[v] += (s->var_inc * s->factors[v]);
+ if (s->activity[v] > 1e100)
+ act_var_rescale(s);
+ //printf("bump %d %f\n", v-1, activity[v]);
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
}
-static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; }
+static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
-static inline void act_clause_rescale(solver* s) {
+static inline void act_clause_rescale(sat_solver* s) {
clause** cs = (clause**)vecp_begin(&s->learnts);
int i;
for (i = 0; i < vecp_size(&s->learnts); i++){
@@ -245,21 +255,20 @@ static inline void act_clause_rescale(solver* s) {
}
-static inline void act_clause_bump(solver* s, clause *c) {
+static inline void act_clause_bump(sat_solver* s, clause *c) {
float a = clause_activity(c) + s->cla_inc;
clause_setactivity(c,a);
if (a > 1e20) act_clause_rescale(s);
}
-static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; }
-
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
//=================================================================================================
// Clause functions:
/* pre: size > 1 && no variable occurs twice
*/
-static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
+static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int size;
clause* c;
@@ -268,7 +277,13 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
size = end - begin;
- c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+ c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
c->size_learnt = (size << 1) | learnt;
assert(((unsigned int)c & 1) == 0);
@@ -286,28 +301,28 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
assert(lit_neg(begin[0]) < s->size*2);
assert(lit_neg(begin[1]) < s->size*2);
- //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
- //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
- vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
- vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+ vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+ vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
return c;
}
-static void clause_remove(solver* s, clause* c)
+static void clause_remove(sat_solver* s, clause* c)
{
lit* lits = clause_begin(c);
assert(lit_neg(lits[0]) < s->size*2);
assert(lit_neg(lits[1]) < s->size*2);
- //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
assert(lits[0] < s->size*2);
- vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->stats.learnts--;
@@ -317,17 +332,21 @@ static void clause_remove(solver* s, clause* c)
s->stats.clauses_literals -= clause_size(c);
}
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
free(c);
+#else
+ Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
}
-static lbool clause_simplify(solver* s, clause* c)
+static lbool clause_simplify(sat_solver* s, clause* c)
{
lit* lits = clause_begin(c);
lbool* values = s->assigns;
int i;
- assert(solver_dlevel(s) == 0);
+ assert(sat_solver_dlevel(s) == 0);
for (i = 0; i < clause_size(c); i++){
lbool sig = !lit_sign(lits[i]); sig += sig - 1;
@@ -340,7 +359,7 @@ static lbool clause_simplify(solver* s, clause* c)
//=================================================================================================
// Minor (solver) functions:
-void solver_setnvars(solver* s,int n)
+void sat_solver_setnvars(sat_solver* s,int n)
{
int var;
@@ -350,6 +369,7 @@ void solver_setnvars(solver* s,int n)
s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2);
s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap);
+ s->factors = (double*) realloc(s->factors, sizeof(double)*s->cap);
s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap);
s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap);
s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap);
@@ -362,6 +382,7 @@ void solver_setnvars(solver* s,int n)
vecp_new(&s->wlists[2*var]);
vecp_new(&s->wlists[2*var+1]);
s->activity [var] = 0;
+ s->factors [var] = 0;
s->assigns [var] = l_Undef;
s->orderpos [var] = veci_size(&s->order);
s->reasons [var] = (clause*)0;
@@ -379,7 +400,7 @@ void solver_setnvars(solver* s,int n)
}
-static inline bool enqueue(solver* s, lit l, clause* from)
+static inline bool enqueue(sat_solver* s, lit l, clause* from)
{
lbool* values = s->assigns;
int v = lit_var(l);
@@ -400,7 +421,7 @@ static inline bool enqueue(solver* s, lit l, clause* from)
clause** reasons = s->reasons;
values [v] = sig;
- levels [v] = solver_dlevel(s);
+ levels [v] = sat_solver_dlevel(s);
reasons[v] = from;
s->trail[s->qtail++] = l;
@@ -410,7 +431,7 @@ static inline bool enqueue(solver* s, lit l, clause* from)
}
-static inline void assume(solver* s, lit l){
+static inline void assume(sat_solver* s, lit l){
assert(s->qtail == s->qhead);
assert(s->assigns[lit_var(l)] == l_Undef);
#ifdef VERBOSEDEBUG
@@ -421,14 +442,14 @@ static inline void assume(solver* s, lit l){
}
-static inline void solver_canceluntil(solver* s, int level) {
+static inline void sat_solver_canceluntil(sat_solver* s, int level) {
lit* trail;
lbool* values;
clause** reasons;
int bound;
int c;
- if (solver_dlevel(s) <= level)
+ if (sat_solver_dlevel(s) <= level)
return;
trail = s->trail;
@@ -449,7 +470,7 @@ static inline void solver_canceluntil(solver* s, int level) {
veci_resize(&s->trail_lim,level);
}
-static void solver_record(solver* s, veci* cls)
+static void sat_solver_record(sat_solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
@@ -467,7 +488,7 @@ static void solver_record(solver* s, veci* cls)
}
-static double solver_progress(solver* s)
+static double sat_solver_progress(sat_solver* s)
{
lbool* values = s->assigns;
int* levels = s->levels;
@@ -484,7 +505,7 @@ static double solver_progress(solver* s)
//=================================================================================================
// Major methods:
-static bool solver_lit_removable(solver* s, lit l, int minl)
+static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
{
lbool* tags = s->tags;
clause** reasons = s->reasons;
@@ -547,7 +568,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
return true;
}
-static void solver_analyze(solver* s, clause* c, veci* learnt)
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
{
lit* trail = s->trail;
lbool* tags = s->tags;
@@ -572,7 +593,7 @@ static void solver_analyze(solver* s, clause* c, veci* learnt)
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == solver_dlevel(s))
+ if (levels[lit_var(q)] == sat_solver_dlevel(s))
cnt++;
else
veci_push(learnt,q);
@@ -591,7 +612,7 @@ static void solver_analyze(solver* s, clause* c, veci* learnt)
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == solver_dlevel(s))
+ if (levels[lit_var(q)] == sat_solver_dlevel(s))
cnt++;
else
veci_push(learnt,q);
@@ -618,7 +639,7 @@ static void solver_analyze(solver* s, clause* c, veci* learnt)
// simplify (full)
for (i = j = 1; i < veci_size(learnt); i++){
- if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl))
+ if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
lits[j++] = lits[i];
}
@@ -666,16 +687,16 @@ static void solver_analyze(solver* s, clause* c, veci* learnt)
}
-clause* solver_propagate(solver* s)
+clause* sat_solver_propagate(sat_solver* s)
{
lbool* values = s->assigns;
clause* confl = (clause*)0;
lit* lits;
- //printf("solver_propagate\n");
+ //printf("sat_solver_propagate\n");
while (confl == 0 && s->qtail - s->qhead > 0){
lit p = s->trail[s->qhead++];
- vecp* ws = solver_read_wlist(s,p);
+ vecp* ws = sat_solver_read_wlist(s,p);
clause **begin = (clause**)vecp_begin(ws);
clause **end = begin + vecp_size(ws);
clause **i, **j;
@@ -724,7 +745,7 @@ clause* solver_propagate(solver* s)
if (values[lit_var(*k)] != sig){
lits[1] = *k;
*k = false_lit;
- vecp_push(solver_read_wlist(s,lit_neg(lits[1])),*i);
+ vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
goto next; }
}
@@ -752,14 +773,14 @@ clause* solver_propagate(solver* s)
static inline int clause_cmp (const void* x, const void* y) {
return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-void solver_reducedb(solver* s)
+void sat_solver_reducedb(sat_solver* s)
{
int i, j;
double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)vecp_begin(&s->learnts);
clause** reasons = s->reasons;
- sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+ sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
@@ -780,7 +801,7 @@ void solver_reducedb(solver* s)
vecp_resize(&s->learnts,j);
}
-static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
+static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts)
{
int* levels = s->levels;
double var_decay = 0.95;
@@ -789,17 +810,24 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
int conflictC = 0;
veci learnt_clause;
+ int i;
- assert(s->root_level == solver_dlevel(s));
+ assert(s->root_level == sat_solver_dlevel(s));
+ s->nRestarts++;
s->stats.starts++;
s->var_decay = (float)(1 / var_decay );
s->cla_decay = (float)(1 / clause_decay);
veci_resize(&s->model,0);
veci_new(&learnt_clause);
+ // use activity factors in every even restart
+ if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
+ for ( i = 0; i < s->act_vars.size; i++ )
+ act_var_bump_factor(s, s->act_vars.ptr[i]);
+
for (;;){
- clause* confl = solver_propagate(s);
+ clause* confl = sat_solver_propagate(s);
if (confl != 0){
// CONFLICT
int blevel;
@@ -808,17 +836,17 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
printf(L_IND"**CONFLICT**\n", L_ind);
#endif
s->stats.conflicts++; conflictC++;
- if (solver_dlevel(s) == s->root_level){
+ if (sat_solver_dlevel(s) == s->root_level){
veci_delete(&learnt_clause);
return l_False;
}
veci_resize(&learnt_clause,0);
- solver_analyze(s, confl, &learnt_clause);
+ sat_solver_analyze(s, confl, &learnt_clause);
blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
blevel = s->root_level > blevel ? s->root_level : blevel;
- solver_canceluntil(s,blevel);
- solver_record(s,&learnt_clause);
+ sat_solver_canceluntil(s,blevel);
+ sat_solver_record(s,&learnt_clause);
act_var_decay(s);
act_clause_decay(s);
@@ -828,18 +856,28 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
// Reached bound on number of conflicts:
- s->progress_estimate = solver_progress(s);
- solver_canceluntil(s,s->root_level);
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_Undef; }
- if (solver_dlevel(s) == 0)
+ if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ||
+ s->nInsLimit && s->stats.inspects > s->nInsLimit )
+ {
+ // Reached bound on number of conflicts:
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef;
+ }
+
+ if (sat_solver_dlevel(s) == 0)
// Simplify the set of problem clauses:
- solver_simplify(s);
+ sat_solver_simplify(s);
if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
- solver_reducedb(s);
+ sat_solver_reducedb(s);
// New variable decision:
s->stats.decisions++;
@@ -849,8 +887,10 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
// Model found:
lbool* values = s->assigns;
int i;
- for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
- solver_canceluntil(s,s->root_level);
+ veci_resize(&s->model, 0);
+ for (i = 0; i < s->size; i++)
+ veci_push(&s->model,(int)values[i]);
+ sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
/*
@@ -874,9 +914,10 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
//=================================================================================================
// External solver functions:
-solver* solver_new(void)
+sat_solver* sat_solver_new(void)
{
- solver* s = (solver*)malloc(sizeof(solver));
+ sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
+ memset( s, 0, sizeof(sat_solver) );
// initialize vectors
vecp_new(&s->clauses);
@@ -886,10 +927,12 @@ solver* solver_new(void)
veci_new(&s->tagged);
veci_new(&s->stack);
veci_new(&s->model);
+ veci_new(&s->act_vars);
// initialize arrays
s->wlists = 0;
s->activity = 0;
+ s->factors = 0;
s->assigns = 0;
s->orderpos = 0;
s->reasons = 0;
@@ -928,18 +971,27 @@ solver* solver_new(void)
s->stats.max_literals = 0;
s->stats.tot_literals = 0;
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ s->pMem = NULL;
+#else
+ s->pMem = Sat_MmStepStart( 10 );
+#endif
return s;
}
-void solver_delete(solver* s)
+void sat_solver_delete(sat_solver* s)
{
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
int i;
for (i = 0; i < vecp_size(&s->clauses); i++)
free(vecp_begin(&s->clauses)[i]);
-
for (i = 0; i < vecp_size(&s->learnts); i++)
free(vecp_begin(&s->learnts)[i]);
+#else
+ Sat_MmStepStop( s->pMem, 0 );
+#endif
// delete vectors
vecp_delete(&s->clauses);
@@ -949,6 +1001,7 @@ void solver_delete(solver* s)
veci_delete(&s->tagged);
veci_delete(&s->stack);
veci_delete(&s->model);
+ veci_delete(&s->act_vars);
free(s->binary);
// delete arrays
@@ -958,8 +1011,9 @@ void solver_delete(solver* s)
vecp_delete(&s->wlists[i]);
// if one is different from null, all are
- free(s->wlists);
+ free(s->wlists );
free(s->activity );
+ free(s->factors );
free(s->assigns );
free(s->orderpos );
free(s->reasons );
@@ -972,7 +1026,7 @@ void solver_delete(solver* s)
}
-bool solver_addclause(solver* s, lit* begin, lit* end)
+bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
lit *i,*j;
int maxvar;
@@ -991,7 +1045,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
*j = *(j-1);
*j = l;
}
- solver_setnvars(s,maxvar+1);
+ sat_solver_setnvars(s,maxvar+1);
//printlits(begin,end); printf("\n");
values = s->assigns;
@@ -1025,14 +1079,14 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
}
-bool solver_simplify(solver* s)
+bool sat_solver_simplify(sat_solver* s)
{
clause** reasons;
int type;
- assert(solver_dlevel(s) == 0);
+ assert(sat_solver_dlevel(s) == 0);
- if (solver_propagate(s) != 0)
+ if (sat_solver_propagate(s) != 0)
return false;
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
@@ -1062,14 +1116,27 @@ bool solver_simplify(solver* s)
}
-bool solver_solve(solver* s, lit* begin, lit* end)
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
{
double nof_conflicts = 100;
- double nof_learnts = solver_nclauses(s) / 3;
+ double nof_learnts = sat_solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
-
+
+ // set the external limits
+ s->nRestarts = 0;
+ s->nConfLimit = 0;
+ s->nInsLimit = 0;
+ if ( nConfLimit )
+ s->nConfLimit = s->stats.conflicts + nConfLimit;
+ if ( nInsLimit )
+ s->nInsLimit = s->stats.inspects + nInsLimit;
+ if ( nConfLimitGlobal && s->nConfLimit > nConfLimitGlobal )
+ s->nConfLimit = nConfLimitGlobal;
+ if ( nInsLimitGlobal && s->nInsLimit > nInsLimitGlobal )
+ s->nInsLimit = nInsLimitGlobal;
+
//printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){
switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
@@ -1077,16 +1144,16 @@ bool solver_solve(solver* s, lit* begin, lit* end)
break;
case 0: /* l_Undef */
assume(s, *i);
- if (solver_propagate(s) == NULL)
+ if (sat_solver_propagate(s) == NULL)
break;
// falltrough
case -1: /* l_False */
- solver_canceluntil(s, 0);
- return false;
+ sat_solver_canceluntil(s, 0);
+ return l_False;
}
}
- s->root_level = solver_dlevel(s);
+ s->root_level = sat_solver_dlevel(s);
if (s->verbosity >= 1){
printf("==================================[MINISAT]===================================\n");
@@ -1111,31 +1178,43 @@ bool solver_solve(solver* s, lit* begin, lit* end)
s->progress_estimate*100);
fflush(stdout);
}
- status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
+ status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
+
+ // quit the loop if reached an external limit
+ if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+ {
+// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+ break;
+ }
+ if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
+ {
+// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+ break;
+ }
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
- solver_canceluntil(s,0);
- return status != l_False;
+ sat_solver_canceluntil(s,0);
+ return status;
}
-int solver_nvars(solver* s)
+int sat_solver_nvars(sat_solver* s)
{
return s->size;
}
-int solver_nclauses(solver* s)
+int sat_solver_nclauses(sat_solver* s)
{
return vecp_size(&s->clauses);
}
-int solver_nconflicts(solver* s)
+int sat_solver_nconflicts(sat_solver* s)
{
return (int)s->stats.conflicts;
}
@@ -1184,7 +1263,7 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
}
}
-void sort(void** array, int size, int(*comp)(const void *, const void *))
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
{
double seed = 91648253;
sortrnd(array,size,comp,&seed);
diff --git a/src/sat/asat_fixed/satSolver.h b/src/sat/bsat/satSolver.h
index c9ce0219..6c05a14a 100644
--- a/src/sat/asat_fixed/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -19,14 +19,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
**************************************************************************************************/
// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-#ifndef solver_h
-#define solver_h
+#ifndef satSolver_h
+#define satSolver_h
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
-#include "vec.h"
+#include "satVec.h"
+#include "satMem.h"
//=================================================================================================
// Simple types:
@@ -40,9 +41,9 @@ typedef int lit;
typedef char lbool;
#ifdef _WIN32
-typedef signed __int64 uint64; // compatible with MS VS 6.0
+typedef signed __int64 sint64; // compatible with MS VS 6.0
#else
-typedef unsigned long long uint64;
+typedef long long sint64;
#endif
static const int var_Undef = -1;
@@ -52,45 +53,49 @@ static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
-static inline lit toLit (int v) { return v + v; }
-static inline lit lit_neg (lit l) { return l ^ 1; }
-static inline int lit_var (lit l) { return l >> 1; }
-static inline int lit_sign(lit l) { return (l & 1); }
+static inline lit toLit (int v) { return v + v; }
+static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit lit_neg (lit l) { return l ^ 1; }
+static inline int lit_var (lit l) { return l >> 1; }
+static inline int lit_sign (lit l) { return l & 1; }
//=================================================================================================
// Public interface:
-struct solver_t;
-typedef struct solver_t solver;
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
-extern solver* solver_new(void);
-extern void solver_delete(solver* s);
+extern sat_solver* sat_solver_new(void);
+extern void sat_solver_delete(sat_solver* s);
-extern bool solver_addclause(solver* s, lit* begin, lit* end);
-extern bool solver_simplify(solver* s);
-extern bool solver_solve(solver* s, lit* begin, lit* end);
+extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern bool sat_solver_simplify(sat_solver* s);
+extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
-extern int solver_nvars(solver* s);
-extern int solver_nclauses(solver* s);
-extern int solver_nconflicts(solver* s);
+extern int sat_solver_nvars(sat_solver* s);
+extern int sat_solver_nclauses(sat_solver* s);
+extern int sat_solver_nconflicts(sat_solver* s);
-extern void solver_setnvars(solver* s,int n);
+extern void sat_solver_setnvars(sat_solver* s,int n);
struct stats_t
{
- uint64 starts, decisions, propagations, inspects, conflicts;
- uint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+ sint64 starts, decisions, propagations, inspects, conflicts;
+ sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
};
typedef struct stats_t stats;
+extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+
//=================================================================================================
// Solver representation:
struct clause_t;
typedef struct clause_t clause;
-struct solver_t
+struct sat_solver_t
{
int size; // nof variables
int cap; // size of varmaps
@@ -132,6 +137,15 @@ struct solver_t
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
stats stats;
+
+ sint64 nConfLimit; // external limit on the number of conflicts
+ sint64 nInsLimit; // external limit on the number of implications
+
+ veci act_vars; // variables whose activity has changed
+ double* factors; // the activity factors
+ int nRestarts; // the number of local restarts
+
+ Sat_MmStep_t * pMem;
};
#endif
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
new file mode 100644
index 00000000..f2b78fe6
--- /dev/null
+++ b/src/sat/bsat/satUtil.c
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+ FileName [satUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [C-language MiniSat solver.]
+
+ Synopsis [Additional SAT solver procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "satSolver.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct clause_t
+{
+ int size_learnt;
+ lit lits[0];
+};
+
+static inline int clause_size( clause* c ) { return c->size_learnt >> 1; }
+static inline lit* clause_begin( clause* c ) { return c->lits; }
+
+static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Write the clauses in the solver into a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+{
+ FILE * pFile;
+ void ** pClauses;
+ int nClauses, i;
+
+ // count the number of clauses
+ nClauses = p->clauses.size + p->learnts.size;
+ for ( i = 0; i < p->size; i++ )
+ if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+ nClauses++;
+
+ // start the file
+ pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ {
+ printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+ return;
+ }
+ fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+ fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
+
+ // write the original clauses
+ nClauses = p->clauses.size;
+ pClauses = p->clauses.ptr;
+ for ( i = 0; i < nClauses; i++ )
+ Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+ // write the learned clauses
+ nClauses = p->learnts.size;
+ pClauses = p->learnts.ptr;
+ for ( i = 0; i < nClauses; i++ )
+ Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+ // write zero-level assertions
+ for ( i = 0; i < p->size; i++ )
+ if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+ fprintf( pFile, "%s%d%s\n",
+ (p->assigns[i] == l_False)? "-": "",
+ i + (int)(incrementVars>0),
+ (incrementVars) ? " 0" : "");
+
+ // write the assumptions
+ if (assumptionsBegin) {
+ for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+ fprintf( pFile, "%s%d%s\n",
+ lit_sign(*assumptionsBegin)? "-": "",
+ lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+ (incrementVars) ? " 0" : "");
+ }
+ }
+
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the given clause in a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
+{
+ lit * pLits = clause_begin(pC);
+ int nLits = clause_size(pC);
+ int i;
+
+ for ( i = 0; i < nLits; i++ )
+ fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) );
+ if ( fIncrement )
+ fprintf( pFile, "0" );
+ fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the given clause in a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
+{
+ printf( "starts : %d\n", (int)p->stats.starts );
+ printf( "conflicts : %d\n", (int)p->stats.conflicts );
+ printf( "decisions : %d\n", (int)p->stats.decisions );
+ printf( "propagations : %d\n", (int)p->stats.propagations );
+ printf( "inspects : %d\n", (int)p->stats.inspects );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
new file mode 100644
index 00000000..d7fce5c0
--- /dev/null
+++ b/src/sat/bsat/satVec.h
@@ -0,0 +1,83 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satVec_h
+#define satVec_h
+
+#include <stdlib.h>
+
+// vector of 32-bit intergers (added for 64-bit portability)
+struct veci_t {
+ int size;
+ int cap;
+ int* ptr;
+};
+typedef struct veci_t veci;
+
+static inline void veci_new (veci* v) {
+ v->size = 0;
+ v->cap = 4;
+ v->ptr = (int*)malloc(sizeof(int)*v->cap);
+}
+
+static inline void veci_delete (veci* v) { free(v->ptr); }
+static inline int* veci_begin (veci* v) { return v->ptr; }
+static inline int veci_size (veci* v) { return v->size; }
+static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !!
+static inline void veci_push (veci* v, int e)
+{
+ if (v->size == v->cap) {
+ int newsize = v->cap * 2;//+1;
+ v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+ v->cap = newsize; }
+ v->ptr[v->size++] = e;
+}
+
+
+// vector of 32- or 64-bit pointers
+struct vecp_t {
+ int size;
+ int cap;
+ void** ptr;
+};
+typedef struct vecp_t vecp;
+
+static inline void vecp_new (vecp* v) {
+ v->size = 0;
+ v->cap = 4;
+ v->ptr = (void**)malloc(sizeof(void*)*v->cap);
+}
+
+static inline void vecp_delete (vecp* v) { free(v->ptr); }
+static inline void** vecp_begin (vecp* v) { return v->ptr; }
+static inline int vecp_size (vecp* v) { return v->size; }
+static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !!
+static inline void vecp_push (vecp* v, void* e)
+{
+ if (v->size == v->cap) {
+ int newsize = v->cap * 2;//+1;
+ v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
+ v->cap = newsize; }
+ v->ptr[v->size++] = e;
+}
+
+
+#endif
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 76543e37..5bf0158c 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -571,8 +571,8 @@ void ABC_SolveInit( ABC_Manager mng )
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
// set the new target network
- mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
-
+// mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
+ mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1 );
}
/**Function*************************************************************
@@ -614,7 +614,8 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
if ( mng->mode )
RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
else
- RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams );
+// RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
+ RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
// analyze the result
mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index ffb51a07..b43f1093 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -52,9 +52,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
// iterations
pParams->nItersMax = 6; // the number of iterations
// mitering
- pParams->nMiteringLimitStart = 1000; // starting mitering limit
+ pParams->nMiteringLimitStart = 300; // starting mitering limit
pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration
- // rewriting
+ // rewriting (currently not used)
pParams->nRewritingLimitStart = 3; // the number of rewriting iterations
pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration
// fraiging
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 04:17:31 +0000