From 8eef7f8326e715ea4e9e84f46487cf4657601c25 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 20 Feb 2006 08:01:00 -0800 Subject: Version abc60220 --- src/sat/asat/asatmem.c | 527 +++++++++++++++++++++++++++++++++++++++++++++++ src/sat/asat/asatmem.h | 76 +++++++ src/sat/asat/module.make | 1 + src/sat/asat/solver.c | 65 +++++- src/sat/asat/solver.h | 9 +- 5 files changed, 669 insertions(+), 9 deletions(-) create mode 100644 src/sat/asat/asatmem.c create mode 100644 src/sat/asat/asatmem.h (limited to 'src/sat/asat') 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 ] + + 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<nMapSize = (4<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<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 ] + + 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 +#include + +//////////////////////////////////////////////////////////////////////// +/// 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; }; -- cgit v1.2.3