summaryrefslogtreecommitdiffstats
path: root/src/sat/asat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/asat')
-rw-r--r--src/sat/asat/asatmem.c527
-rw-r--r--src/sat/asat/asatmem.h76
-rw-r--r--src/sat/asat/module.make1
-rw-r--r--src/sat/asat/solver.c65
-rw-r--r--src/sat/asat/solver.h9
5 files changed, 669 insertions, 9 deletions
diff --git a/src/sat/asat/asatmem.c b/src/sat/asat/asatmem.c
new file mode 100644
index 00000000..24c1b1a8
--- /dev/null
+++ b/src/sat/asat/asatmem.c
@@ -0,0 +1,527 @@
+/**CFile****************************************************************
+
+ FileName [asatmem.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: asatmem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "asatmem.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct Asat_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 Asat_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 Asat_MmStep_t_
+{
+ int nMems; // the number of fixed memory managers employed
+ Asat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
+ int nMapSize; // the size of the memory array
+ Asat_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 []
+
+***********************************************************************/
+Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize )
+{
+ Asat_MmFixed_t * p;
+
+ p = ALLOC( Asat_MmFixed_t, 1 );
+ memset( p, 0, sizeof(Asat_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 Asat_MmFixedStop( Asat_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 * Asat_MmFixedEntryFetch( Asat_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 Asat_MmFixedEntryRecycle( Asat_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 Asat_MmFixedRestart( Asat_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 Asat_MmFixedReadMemUsage( Asat_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 []
+
+***********************************************************************/
+Asat_MmFlex_t * Asat_MmFlexStart()
+{
+ Asat_MmFlex_t * p;
+
+ p = ALLOC( Asat_MmFlex_t, 1 );
+ memset( p, 0, sizeof(Asat_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 Asat_MmFlexStop( Asat_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 * Asat_MmFlexEntryFetch( Asat_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 Asat_MmFlexReadMemUsage( Asat_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 []
+
+***********************************************************************/
+Asat_MmStep_t * Asat_MmStepStart( int nSteps )
+{
+ Asat_MmStep_t * p;
+ int i, k;
+ p = ALLOC( Asat_MmStep_t, 1 );
+ p->nMems = nSteps;
+ // start the fixed memory managers
+ p->pMems = ALLOC( Asat_MmFixed_t *, p->nMems );
+ for ( i = 0; i < p->nMems; i++ )
+ p->pMems[i] = Asat_MmFixedStart( (8<<i) );
+ // set up the mapping of the required memory size into the corresponding manager
+ p->nMapSize = (4<<p->nMems);
+ p->pMap = ALLOC( Asat_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 Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose )
+{
+ int i;
+ for ( i = 0; i < p->nMems; i++ )
+ Asat_MmFixedStop( p->pMems[i], fVerbose );
+ free( p->pMems );
+ free( p->pMap );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Asat_MmStepEntryFetch( Asat_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 Asat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes )
+{
+ if ( nBytes == 0 )
+ return;
+ if ( nBytes > p->nMapSize )
+ {
+ free( pEntry );
+ return;
+ }
+ Asat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Asat_MmStepReadMemUsage( Asat_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/asat/asatmem.h b/src/sat/asat/asatmem.h
new file mode 100644
index 00000000..56115e7d
--- /dev/null
+++ b/src/sat/asat/asatmem.h
@@ -0,0 +1,76 @@
+/**CFile****************************************************************
+
+ FileName [asatmem.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: asatmem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __ASAT_MEM_H__
+#define __ASAT_MEM_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"
+#include <stdio.h>
+#include <stdlib.h>
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Asat_MmFixed_t_ Asat_MmFixed_t;
+typedef struct Asat_MmFlex_t_ Asat_MmFlex_t;
+typedef struct Asat_MmStep_t_ Asat_MmStep_t;
+
+////////////////////////////////////////////////////////////////////////
+/// GLOBAL VARIABLES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// fixed-size-block memory manager
+extern Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize );
+extern void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose );
+extern char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p );
+extern void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry );
+extern void Asat_MmFixedRestart( Asat_MmFixed_t * p );
+extern int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Asat_MmFlex_t * Asat_MmFlexStart();
+extern void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose );
+extern char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes );
+extern int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p );
+// hierarchical memory manager
+extern Asat_MmStep_t * Asat_MmStepStart( int nSteps );
+extern void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose );
+extern char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes );
+extern void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes );
+extern int Asat_MmStepReadMemUsage( Asat_MmStep_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make
index 882176fa..d5cf69bf 100644
--- a/src/sat/asat/module.make
+++ b/src/sat/asat/module.make
@@ -1,2 +1,3 @@
SRC += src/sat/asat/added.c \
+ src/sat/asat/asatmem.c \
src/sat/asat/solver.c
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 3927fac3..1130d437 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "solver.h"
+//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+
//=================================================================================================
// Simple (var/literal) helpers:
@@ -275,7 +277,14 @@ 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 ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+ c = (clause*)Asat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
c->size_learnt = (size << 1) | learnt;
assert(((unsigned int)c & 1) == 0);
@@ -324,7 +333,12 @@ static void clause_remove(solver* s, clause* c)
s->solver_stats.clauses_literals -= clause_size(c);
}
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
free(c);
+#else
+ Asat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+
}
@@ -829,12 +843,24 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
// NO CONFLICT
int next;
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+ 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);
vec_delete(&learnt_clause);
- return l_Undef; }
+ return l_Undef;
+ }
+
+ if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit ||
+ s->nImpLimit && s->solver_stats.propagations > s->nImpLimit )
+ {
+ // Reached bound on number of conflicts:
+ s->progress_estimate = solver_progress(s);
+ solver_canceluntil(s,s->root_level);
+ vec_delete(&learnt_clause);
+ return l_Undef;
+ }
if (solver_dlevel(s) == 0)
// Simplify the set of problem clauses:
@@ -922,18 +948,28 @@ solver* solver_new(void)
s->solver_stats.max_literals = 0;
s->solver_stats.tot_literals = 0;
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ s->pMem = NULL;
+#else
+ s->pMem = Asat_MmStepStart( 10 );
+#endif
+
return s;
}
void solver_delete(solver* s)
{
+
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
int i;
for (i = 0; i < vec_size(&s->clauses); i++)
free(vec_begin(&s->clauses)[i]);
-
for (i = 0; i < vec_size(&s->learnts); i++)
free(vec_begin(&s->learnts)[i]);
+#else
+ Asat_MmStepStop( s->pMem, 0 );
+#endif
// delete vectors
vec_delete(&s->clauses);
@@ -1056,14 +1092,18 @@ bool solver_simplify(solver* s)
}
-bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
+bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit )
{
double nof_conflicts = 100;
double nof_learnts = solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
- int timeStart = clock();
+
+ // set the external limits
+ s->nConfLimit = nConfLimit; // external limit on the number of conflicts
+ s->nImpLimit = nImpLimit; // external limit on the number of implications
+
for (i = begin; i < end; i++)
if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
@@ -1098,9 +1138,18 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
- // if the runtime limit is exceeded, quit the restart loop
- if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) )
+
+ // quit the loop if reached an external limit
+ if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit )
+ {
+// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
break;
+ }
+ if ( s->nImpLimit && s->solver_stats.propagations > s->nImpLimit )
+ {
+// printf( "Reached the limit on the number of implications (%d).\n", s->nImpLimit );
+ break;
+ }
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 9618603c..d798a7a9 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#endif
#include "solver_vec.h"
+#include "asatmem.h"
//=================================================================================================
// Simple types:
@@ -67,7 +68,7 @@ extern void solver_delete(solver* s);
extern bool solver_addclause(solver* s, lit* begin, lit* end);
extern bool solver_simplify(solver* s);
-extern int solver_solve(solver* s, lit* begin, lit* end, int nSeconds);
+extern int solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit );
extern int * solver_get_model( solver * p, int * pVars, int nVars );
extern int solver_nvars(solver* s);
@@ -132,6 +133,12 @@ struct solver_t
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
+ int nConfLimit; // external limit on the number of conflicts
+ int nImpLimit; // external limit on the number of implications
+
+ // the memory manager
+ Asat_MmStep_t * pMem;
+
stats solver_stats;
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:20:11 +0000