diff options
Diffstat (limited to 'src/sat/asat')
| -rw-r--r-- | src/sat/asat/added.c | 234 | ||||
| -rw-r--r-- | src/sat/asat/asatmem.c | 527 | ||||
| -rw-r--r-- | src/sat/asat/asatmem.h | 78 | ||||
| -rw-r--r-- | src/sat/asat/jfront.c | 514 | ||||
| -rw-r--r-- | src/sat/asat/main.c | 195 | ||||
| -rw-r--r-- | src/sat/asat/module.make | 4 | ||||
| -rw-r--r-- | src/sat/asat/satTrace.c | 112 | ||||
| -rw-r--r-- | src/sat/asat/solver.c | 1290 | ||||
| -rw-r--r-- | src/sat/asat/solver.h | 189 | ||||
| -rw-r--r-- | src/sat/asat/solver_vec.h | 83 |
10 files changed, 0 insertions, 3226 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c deleted file mode 100644 index 222693ad..00000000 --- a/src/sat/asat/added.c +++ /dev/null @@ -1,234 +0,0 @@ -/**CFile**************************************************************** - - FileName [added.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: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.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 inline int lit_var(lit l) { return l >> 1; } -static inline int lit_sign(lit l) { return (l & 1); } - -static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); - -extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Write the clauses in the solver into a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverWriteDimacs( 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( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); - return; - } - fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); -// Io_WriteCnfOutputPiMapping( pFile, incrementVars ); - 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++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); - - // write the learned clauses - nClauses = p->learnts.size; - pClauses = p->learnts.ptr; - for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( 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 Asat_ClauseWriteDimacs( 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 [Returns a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * solver_get_model( solver * p, int * pVars, int nVars ) -{ - int * pModel; - int i; - pModel = ALLOC( int, nVars ); - for ( i = 0; i < nVars; i++ ) - { - assert( pVars[i] >= 0 && pVars[i] < p->size ); - pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True); - } - return pModel; -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SatPrintStats( FILE * pFile, solver * p ) -{ - printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n", - (int)p->solver_stats.starts, - (int)p->solver_stats.conflicts, - (int)p->solver_stats.decisions, - (int)p->solver_stats.propagations, - (int)p->solver_stats.inspects ); - printf( "Total runtime = %7.2f sec. Var select = %7.2f sec. Var update = %7.2f sec.\n", - (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC), - (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC), - (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) ); -} - -/**Function************************************************************* - - Synopsis [Sets the preferred variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) -{ - int i; - assert( s->pPrefVars == NULL ); - for ( i = 0; i < nPrefVars; i++ ) - assert( pPrefVars[i] < s->size ); - s->pPrefVars = pPrefVars; - s->nPrefVars = nPrefVars; -} - -/**Function************************************************************* - - Synopsis [Sets the preferred variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverSetFactors(solver * s, float * pFactors) -{ - assert( s->factors == NULL ); - s->factors = pFactors; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/asat/asatmem.c b/src/sat/asat/asatmem.c deleted file mode 100644 index 24c1b1a8..00000000 --- a/src/sat/asat/asatmem.c +++ /dev/null @@ -1,527 +0,0 @@ -/**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 deleted file mode 100644 index 7351d77b..00000000 --- a/src/sat/asat/asatmem.h +++ /dev/null @@ -1,78 +0,0 @@ -/**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 ); - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c deleted file mode 100644 index efbe7883..00000000 --- a/src/sat/asat/jfront.c +++ /dev/null @@ -1,514 +0,0 @@ -/**CFile**************************************************************** - - FileName [jfront.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [C-language MiniSat solver.] - - Synopsis [Implementation of J-frontier.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: jfront.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.h" -#include "extra.h" -#include "vec.h" - -/* - At any time during the solving process, the J-frontier is the set of currently - unassigned variables, each of which has at least one fanin/fanout variable that - is currently assigned. In the context of a CNF-based solver, default decisions - based on variable activity are modified to choose the most active variable among - those currently on the J-frontier. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// variable on the J-frontier -typedef struct Asat_JVar_t_ Asat_JVar_t; -struct Asat_JVar_t_ -{ - unsigned int Num; // variable number - unsigned int nRefs; // the number of adjacent assigned vars - unsigned int Prev; // the previous variable - unsigned int Next; // the next variable - unsigned int nFans; // the number of fanins/fanouts - unsigned int Fans[0]; // the fanin/fanout variables -}; - -// the J-frontier as a ring of variables -// (ring is used instead of list because it allows to control the insertion point) -typedef struct Asat_JRing_t_ Asat_JRing_t; -struct Asat_JRing_t_ -{ - Asat_JVar_t * pRoot; // the pointer to the root - int nItems; // the number of variables in the ring -}; - -// the J-frontier manager -struct Asat_JMan_t_ -{ - solver * pSat; // the SAT solver - Asat_JRing_t rVars; // the ring of variables - Vec_Ptr_t * vVars; // the pointers to variables - Extra_MmFlex_t * pMem; // the memory manager for variables -}; - -// getting hold of the given variable -static inline Asat_JVar_t * Asat_JManVar( Asat_JMan_t * p, int Num ) { return !Num? NULL : Vec_PtrEntry(p->vVars, Num); } -static inline Asat_JVar_t * Asat_JVarPrev( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Prev); } -static inline Asat_JVar_t * Asat_JVarNext( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Next); } - -//The solver can communicate to the variable order the following parts: -//- the array of current assignments (pSat->pAssigns) -//- the array of variable activities (pSat->pdActivity) -//- the array of variables currently in the cone -//- the array of arrays of variables adjacent to each other - -static inline int Asat_JVarIsInBoundary( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return pVar->Next > 0; } -static inline int Asat_JVarIsAssigned( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return p->pSat->assigns[pVar->Num] != l_Undef; } -//static inline int Asat_JVarIsUsedInCone( Asat_JMan_t * p, int Var ) { return p->pSat->vVarsUsed->pArray[i]; } - -// manipulating the ring of variables -static void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ); -static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ); - -// iterator through the entries in J-boundary -#define Asat_JRingForEachEntry( p, pVar, pNext ) \ - for ( pVar = p->rVars.pRoot, \ - pNext = pVar? Asat_JVarNext(p, pVar) : NULL; \ - pVar; \ - pVar = (pNext != p->rVars.pRoot)? pNext : NULL, \ - pNext = pVar? Asat_JVarNext(p, pVar) : NULL ) - -// iterator through the adjacent variables -#define Asat_JVarForEachFanio( p, pVar, pFan, i ) \ - for ( i = 0; (i < (int)pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ ) - -extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Start the J-frontier.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Asat_JMan_t * Asat_JManStart( solver * pSat, void * pCircuit ) -{ - Vec_Vec_t * vCircuit = pCircuit; - Asat_JMan_t * p; - Asat_JVar_t * pVar; - Vec_Int_t * vConnect; - int i, nBytes, Entry, k; - // make sure the number of variables is less than sizeof(unsigned int) - assert( Vec_VecSize(vCircuit) < (1 << 16) ); - assert( Vec_VecSize(vCircuit) == pSat->size ); - // allocate the manager - p = ALLOC( Asat_JMan_t, 1 ); - memset( p, 0, sizeof(Asat_JMan_t) ); - p->pSat = pSat; - p->pMem = Extra_MmFlexStart(); - // fill in the variables - p->vVars = Vec_PtrAlloc( Vec_VecSize(vCircuit) ); - for ( i = 0; i < Vec_VecSize(vCircuit); i++ ) - { - vConnect = Vec_VecEntry( vCircuit, i ); - nBytes = sizeof(Asat_JVar_t) + sizeof(int) * Vec_IntSize(vConnect); - nBytes = sizeof(void *) * (nBytes / sizeof(void *) + ((nBytes % sizeof(void *)) != 0)); - pVar = (Asat_JVar_t *)Extra_MmFlexEntryFetch( p->pMem, nBytes ); - memset( pVar, 0, nBytes ); - pVar->Num = i; - // add fanins/fanouts - pVar->nFans = Vec_IntSize( vConnect ); - Vec_IntForEachEntry( vConnect, Entry, k ) - pVar->Fans[k] = Entry; - // add the variable - Vec_PtrPush( p->vVars, pVar ); - } - // set the current assignments - Vec_PtrForEachEntryStart( p->vVars, pVar, i, 1 ) - { -// if ( !Asat_JVarIsUsedInCone(p, pVar) ) -// continue; - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Asat_JVarIsAssigned(p, pVar) ) - Asat_JManAssign( p, pVar->Num ); - } - - pSat->pJMan = p; - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the J-frontier.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManStop( solver * pSat ) -{ - Asat_JMan_t * p = pSat->pJMan; - if ( p == NULL ) - return; - pSat->pJMan = NULL; - Extra_MmFlexStop( p->pMem ); - Vec_PtrFree( p->vVars ); - free( p ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_JManCheck( Asat_JMan_t * p ) -{ - Asat_JVar_t * pVar, * pNext, * pFan; -// Msat_IntVec_t * vRound; -// int * pRound, nRound; -// int * pVars, nVars, i, k; - int i, k; - int Counter = 0; - - // go through all the variables in the boundary - Asat_JRingForEachEntry( p, pVar, pNext ) - { - assert( !Asat_JVarIsAssigned(p, pVar) ); - // go though all the variables in the neighborhood - // and check that it is true that there is least one assigned -// vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num ); -// nRound = Msat_IntVecReadSize( vRound ); -// pRound = Msat_IntVecReadArray( vRound ); -// for ( i = 0; i < nRound; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - if ( Asat_JVarIsAssigned(p, pFan) ) - break; - } -// assert( i != pVar->nFans ); -// if ( i == pVar->nFans ) -// return 0; - if ( i == (int)pVar->nFans ) - Counter++; - } - if ( Counter > 0 ) - printf( "%d(%d) ", Counter, p->rVars.nItems ); - - // we may also check other unassigned variables in the cone - // to make sure that if they are not in J-boundary, - // then they do not have an assigned neighbor -// nVars = Msat_IntVecReadSize( p->pSat->vConeVars ); -// pVars = Msat_IntVecReadArray( p->pSat->vConeVars ); -// for ( i = 0; i < nVars; i++ ) - Vec_PtrForEachEntry( p->vVars, pVar, i ) - { -// assert( Asat_JVarIsUsedInCone(p, pVar) ); - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Asat_JVarIsAssigned(p, pVar) || Asat_JVarIsInBoundary(p, pVar) ) - continue; - // make sure, it does not have assigned neighbors -// vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] ); -// nRound = Msat_IntVecReadSize( vRound ); -// pRound = Msat_IntVecReadArray( vRound ); -// for ( i = 0; i < nRound; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, k ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - if ( Asat_JVarIsAssigned(p, pFan) ) - break; - } -// assert( k == pVar->nFans ); -// if ( k != pVar->nFans ) -// return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManAssign( Asat_JMan_t * p, int Var ) -{ -// Msat_IntVec_t * vRound; - Asat_JVar_t * pVar, * pFan; - int i, clk = clock(); - - // make sure the variable is in the boundary - assert( Var < Vec_PtrSize(p->vVars) ); - // if it is not in the boundary (initial decision, random decision), do not remove - pVar = Asat_JManVar( p, Var ); - if ( Asat_JVarIsInBoundary( p, pVar ) ) - Asat_JRingRemove( p, pVar ); - // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary - // because for them we know that there is a variable (Var) which is assigned -// vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; -// for ( i = 0; i < vRound->nSize; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - pFan->nRefs++; - if ( Asat_JVarIsAssigned(p, pFan) || Asat_JVarIsInBoundary(p, pFan) ) - continue; - Asat_JRingAddLast( p, pFan ); - } -//timeSelect += clock() - clk; -// Asat_JManCheck( p ); - p->pSat->timeUpdate += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManUnassign( Asat_JMan_t * p, int Var ) -{ -// Msat_IntVec_t * vRound, * vRound2; - Asat_JVar_t * pVar, * pFan; - int i, clk = clock();//, k - - // make sure the variable is not in the boundary - assert( Var < Vec_PtrSize(p->vVars) ); - pVar = Asat_JManVar( p, Var ); - assert( !Asat_JVarIsInBoundary( p, pVar ) ); - // go through its neigbors - if one of them is assigned add this var - // add to the boundary those neighbors that are not there already - // this will also get rid of variable outside of the current cone - // because they are unassigned in Msat_SolverPrepare() -// vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; -// for ( i = 0; i < vRound->nSize; i++ ) -// if ( Asat_JVarIsAssigned(p, vRound->pArray[i]) ) -// break; -// if ( i != vRound->nSize ) -// Asat_JRingAddLast( &p->rVars, &p->pVars[Var] ); - if ( pVar->nRefs != 0 ) - Asat_JRingAddLast( p, pVar ); - -/* - // unassigning a variable may lead to its adjacents dropping from the boundary - for ( i = 0; i < vRound->nSize; i++ ) - if ( Asat_JVarIsInBoundary(p, vRound->pArray[i]) ) - { // the neighbor is in the J-boundary (and unassigned) - assert( !Asat_JVarIsAssigned(p, vRound->pArray[i]) ); - vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]]; - // go through its neighbors and determine if there is at least one assigned - for ( k = 0; k < vRound2->nSize; k++ ) - if ( Asat_JVarIsAssigned(p, vRound2->pArray[k]) ) - break; - if ( k == vRound2->nSize ) // there is no assigned vars, delete this one - Asat_JRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -*/ - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - assert( pFan->nRefs > 0 ); - pFan->nRefs--; - if ( !Asat_JVarIsInBoundary(p, pFan) ) - continue; - // the neighbor is in the J-boundary (and unassigned) - assert( !Asat_JVarIsAssigned(p, pFan) ); - // if there is no assigned vars, delete this one - if ( pFan->nRefs == 0 ) - Asat_JRingRemove( p, pFan ); - } - -//timeSelect += clock() - clk; -// Asat_JManCheck( p ); - p->pSat->timeUpdate += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_JManSelect( Asat_JMan_t * p ) -{ - Asat_JVar_t * pVar, * pNext, * pVarBest; - double * pdActs = p->pSat->activity; - double dfActBest; - int clk = clock(); - - pVarBest = NULL; - dfActBest = -1.0; - Asat_JRingForEachEntry( p, pVar, pNext ) - { - if ( dfActBest <= pdActs[pVar->Num] )//+ 0.00001 ) - { - dfActBest = pdActs[pVar->Num]; - pVarBest = pVar; - } - } -//timeSelect += clock() - clk; -//timeAssign += clock() - clk; -//if ( pVarBest && pVarBest->Num % 1000 == 0 ) -//printf( "%d ", p->rVars.nItems ); - -// Asat_JManCheck( p ); - p->pSat->timeSelect += clock() - clk; - if ( pVarBest ) - { -// assert( Asat_JVarIsUsedInCone(p, pVarBest) ); - return pVarBest->Num; - } - return var_Undef; -} - - - -/**Function************************************************************* - - Synopsis [Adds node to the end of the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ) -{ - Asat_JRing_t * pRing = &p->rVars; -//printf( "adding %d\n", pVar->Num ); - // check that the node is not in a ring - assert( pVar->Prev == 0 ); - assert( pVar->Next == 0 ); - // if the ring is empty, make the node point to itself - pRing->nItems++; - if ( pRing->pRoot == NULL ) - { - pRing->pRoot = pVar; -// pVar->pPrev = pVar; - pVar->Prev = pVar->Num; -// pVar->pNext = pVar; - pVar->Next = pVar->Num; - return; - } - // if the ring is not empty, add it as the last entry -// pVar->pPrev = pRing->pRoot->pPrev; - pVar->Prev = pRing->pRoot->Prev; -// pVar->pNext = pRing->pRoot; - pVar->Next = pRing->pRoot->Num; -// pVar->pPrev->pNext = pVar; - Asat_JVarPrev(p, pVar)->Next = pVar->Num; -// pVar->pNext->pPrev = pVar; - Asat_JVarNext(p, pVar)->Prev = pVar->Num; - - // move the root so that it points to the new entry -// pRing->pRoot = pRing->pRoot->pPrev; - pRing->pRoot = Asat_JVarPrev(p, pRing->pRoot); -} - -/**Function************************************************************* - - Synopsis [Removes the node from the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ) -{ - Asat_JRing_t * pRing = &p->rVars; -//printf( "removing %d\n", pVar->Num ); - // check that the var is in a ring - assert( pVar->Prev ); - assert( pVar->Next ); - pRing->nItems--; - if ( pRing->nItems == 0 ) - { - assert( pRing->pRoot == pVar ); -// pVar->pPrev = NULL; - pVar->Prev = 0; -// pVar->pNext = NULL; - pVar->Next = 0; - pRing->pRoot = NULL; - return; - } - // move the root if needed - if ( pRing->pRoot == pVar ) -// pRing->pRoot = pVar->pNext; - pRing->pRoot = Asat_JVarNext(p, pVar); - // move the root to the next entry after pVar - // this way all the additions to the list will be traversed first -// pRing->pRoot = pVar->pNext; - pRing->pRoot = Asat_JVarPrev(p, pVar); - // delete the node -// pVar->pPrev->pNext = pVar->pNext; - Asat_JVarPrev(p, pVar)->Next = Asat_JVarNext(p, pVar)->Num; -// pVar->pNext->pPrev = pVar->pPrev; - Asat_JVarNext(p, pVar)->Prev = Asat_JVarPrev(p, pVar)->Num; -// pVar->pPrev = NULL; - pVar->Prev = 0; -// pVar->pNext = NULL; - pVar->Next = 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/asat/main.c b/src/sat/asat/main.c deleted file mode 100644 index cbad5ba1..00000000 --- a/src/sat/asat/main.c +++ /dev/null @@ -1,195 +0,0 @@ -/************************************************************************************************** -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 - -#include "solver.h" - -#include <stdio.h> -#include <stdlib.h> -#include <time.h> -//#include <unistd.h> -//#include <signal.h> -//#include <zlib.h> -//#include <sys/time.h> -//#include <sys/resource.h> - -//================================================================================================= -// Helpers: - - -// Reads an input stream to end-of-file and returns the result as a 'char*' terminated by '\0' -// (dynamic allocation in case 'in' is standard input). -// -char* readFile(FILE * in) -{ - char* data = malloc(65536); - int cap = 65536; - int size = 0; - - while (!feof(in)){ - if (size == cap){ - cap *= 2; - data = realloc(data, cap); } - size += fread(&data[size], 1, 65536, in); - } - data = realloc(data, size+1); - data[size] = '\0'; - - return data; -} - -//static inline double cpuTime(void) { -// struct rusage ru; -// getrusage(RUSAGE_SELF, &ru); -// return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } - - -//================================================================================================= -// DIMACS Parser: - - -static inline void skipWhitespace(char** in) { - while ((**in >= 9 && **in <= 13) || **in == 32) - (*in)++; } - -static inline void skipLine(char** in) { - for (;;){ - if (**in == 0) return; - if (**in == '\n') { (*in)++; return; } - (*in)++; } } - -static inline int parseInt(char** in) { - int val = 0; - int _neg = 0; - skipWhitespace(in); - if (**in == '-') _neg = 1, (*in)++; - else if (**in == '+') (*in)++; - if (**in < '0' || **in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **in), exit(1); - while (**in >= '0' && **in <= '9') - val = val*10 + (**in - '0'), - (*in)++; - return _neg ? -val : val; } - -static void readClause(char** in, solver* s, vec* lits) { - int parsed_lit, var; - vec_resize(lits,0); - for (;;){ - parsed_lit = parseInt(in); - if (parsed_lit == 0) break; - var = abs(parsed_lit)-1; - vec_push(lits, (void*)(parsed_lit > 0 ? toLit(var) : neg(toLit(var)))); - } -} - -static lbool parse_DIMACS_main(char* in, solver* s) { - vec lits; - vec_new(&lits); - - for (;;){ - skipWhitespace(&in); - if (*in == 0) - break; - else if (*in == 'c' || *in == 'p') - skipLine(&in); - else{ - lit* begin; - readClause(&in, s, &lits); - begin = (lit*)vec_begin(&lits); - if (solver_addclause(s, begin, begin+vec_size(&lits)) == l_False){ - vec_delete(&lits); - return l_False; - } - } - } - vec_delete(&lits); - return solver_simplify(s); -} - - -// Inserts problem into solver. Returns FALSE upon immediate conflict. -// -static lbool parse_DIMACS(FILE * in, solver* s) { - char* text = readFile(in); - lbool ret = parse_DIMACS_main(text, s); - free(text); - return ret; } - - -//================================================================================================= - - -void printStats(stats* stats, int cpu_time) -{ - double Time = (float)(cpu_time)/(float)(CLOCKS_PER_SEC); - printf("restarts : %12d\n", stats->starts); - printf("conflicts : %12.0f (%9.0f / sec )\n", (double)stats->conflicts , (double)stats->conflicts /Time); - printf("decisions : %12.0f (%9.0f / sec )\n", (double)stats->decisions , (double)stats->decisions /Time); - printf("propagations : %12.0f (%9.0f / sec )\n", (double)stats->propagations, (double)stats->propagations/Time); - printf("inspects : %12.0f (%9.0f / sec )\n", (double)stats->inspects , (double)stats->inspects /Time); - printf("conflict literals : %12.0f (%9.2f %% deleted )\n", (double)stats->tot_literals, (double)(stats->max_literals - stats->tot_literals) * 100.0 / (double)stats->max_literals); - printf("CPU time : %12.2f sec\n", Time); -} - -//solver* slv; -//static void SIGINT_handler(int signum) { -// printf("\n"); printf("*** INTERRUPTED ***\n"); -// printStats(&slv->stats, cpuTime()); -// printf("\n"); printf("*** INTERRUPTED ***\n"); -// exit(0); } - - -//================================================================================================= - - -int main(int argc, char** argv) -{ - solver* s = solver_new(); - lbool st; - FILE * in; - int clk = clock(); - - if (argc != 2) - fprintf(stderr, "ERROR! Not enough command line arguments.\n"), - exit(1); - - in = fopen(argv[1], "rb"); - if (in == NULL) - fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), - exit(1); - st = parse_DIMACS(in, s); - fclose(in); - - if (st == l_False){ - solver_delete(s); - printf("Trivial problem\nUNSATISFIABLE\n"); - exit(20); - } - - s->verbosity = 1; -// slv = s; -// signal(SIGINT,SIGINT_handler); - st = solver_solve(s,0,0); - printStats(&s->stats, clock() - clk); - printf("\n"); - printf(st == l_True ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); - - solver_delete(s); - return 0; -} diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make deleted file mode 100644 index 26489191..00000000 --- a/src/sat/asat/module.make +++ /dev/null @@ -1,4 +0,0 @@ -SRC += src/sat/asat/added.c \ - src/sat/asat/asatmem.c \ - src/sat/asat/jfront.c \ - src/sat/asat/solver.c diff --git a/src/sat/asat/satTrace.c b/src/sat/asat/satTrace.c deleted file mode 100644 index 3318933a..00000000 --- a/src/sat/asat/satTrace.c +++ /dev/null @@ -1,112 +0,0 @@ -/**CFile**************************************************************** - - FileName [satTrace.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [C-language MiniSat solver.] - - Synopsis [Records the trace of SAT solving in the CNF form.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.h" - -/* - The trace of SAT solving contains the original clause of the problem - along with the learned clauses derived during SAT solving. - The first line of the resulting file contains 3 numbers instead of 2: - c <num_vars> <num_all_clauses> <num_root_clauses> -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Start the trace recording.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceStart( solver * pSat, char * pName ) -{ - assert( pSat->pFile == NULL ); - pSat->pFile = fopen( pName, "w" ); - fprintf( pSat->pFile, " \n" ); - pSat->nClauses = 0; - pSat->nRoots = 0; -} - -/**Function************************************************************* - - Synopsis [Stops the trace recording.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceStop( solver * pSat ) -{ - if ( pSat->pFile == NULL ) - return; - rewind( pSat->pFile ); - fprintf( pSat->pFile, "p %d %d %d", solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); - fclose( pSat->pFile ); - pSat->pFile = NULL; -} - - -/**Function************************************************************* - - Synopsis [Writes one clause into the trace file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ) -{ - if ( pSat->pFile == NULL ) - return; - pSat->nClauses++; - pSat->nRoots += fRoot; - for ( ; pBeg < pEnd ; pBeg++ ) - fprintf( pSat->pFile, " %d", lit_print(*pBeg) ); - fprintf( pSat->pFile, " 0\n" ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c deleted file mode 100644 index b9851a54..00000000 --- a/src/sat/asat/solver.c +++ /dev/null @@ -1,1290 +0,0 @@ -/************************************************************************************************** -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 - -#include <stdio.h> -#include <string.h> -#include <assert.h> -#include <math.h> -#include <time.h> - -#include "solver.h" - -#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - -//================================================================================================= -// Simple (var/literal) helpers: - -static inline int lit_var(lit l) { return l >> 1; } -static inline int lit_sign(lit l) { return (l & 1); } - -//================================================================================================= -// Debug: - -//#define VERBOSEDEBUG - -// For derivation output (verbosity level 2) -#define L_IND "%-*d" -#define L_ind solver_dlevel(s)*3+3,solver_dlevel(s) -#define L_LIT "%sx%d" -#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) - -// Just like 'assert()' but expression will be evaluated in the release version as well. -static inline void check(int expr) { assert(expr); } - -static void printlits(lit* begin, lit* end) -{ - int i; - for (i = 0; i < end - begin; i++) - printf(L_LIT" ",L_lit(begin[i])); -} - -//================================================================================================= -// Random numbers: - - -// Returns a random float 0 <= x < 1. Seed must never be 0. -static inline double drand(double* seed) { - int q; - *seed *= 1389796; - q = (int)(*seed / 2147483647); - *seed -= (double)q * 2147483647; - return *seed / 2147483647; } - - -// Returns a random integer 0 <= x < size. Seed must never be 0. -static inline int irand(double* seed, int size) { - return (int)(drand(seed) * size); } - - -//================================================================================================= -// Predeclarations: - -void sort(void** array, int size, int(*comp)(const void *, const void *)); - -//================================================================================================= -// Clause datatype + minor functions: - -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 inline int clause_learnt (clause* c) { return c->size_learnt & 1; } -static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } -static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } - -//================================================================================================= -// 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); } - -//================================================================================================= -// Simple helpers: - -static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); } -static inline vec* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; } -static inline void vec_remove(vec* v, void* e) -{ - void** ws = vec_begin(v); - int j = 0; - - for (; ws[j] != e ; j++); - assert(j < vec_size(v)); - for (; j < vec_size(v)-1; j++) ws[j] = ws[j+1]; - vec_resize(v,vec_size(v)-1); -} - -//================================================================================================= -// Variable order functions: - -static inline void order_update(solver* s, int v) // updateorder -{ -// int clk = clock(); - int* orderpos = s->orderpos; - double* activity = s->activity; - int* heap = veci_begin(&s->order); - int i = orderpos[v]; - int x = heap[i]; - int parent = (i - 1) / 2; - - assert(s->orderpos[v] != -1); - - while (i != 0 && activity[x] > activity[heap[parent]]){ - heap[i] = heap[parent]; - orderpos[heap[i]] = i; - i = parent; - parent = (i - 1) / 2; - } - heap[i] = x; - orderpos[x] = i; -// s->timeUpdate += clock() - clk; -} - -static inline void order_assigned(solver* s, int v) -{ -} - -static inline void order_unassigned(solver* s, int v) // undoorder -{ -// int clk = clock(); - int* orderpos = s->orderpos; - if (orderpos[v] == -1){ - orderpos[v] = veci_size(&s->order); - veci_push(&s->order,v); - order_update(s,v); - } -// s->timeUpdate += clock() - clk; -} - -static int order_select(solver* s, float random_var_freq) // selectvar -{ -// int clk = clock(); - static int Counter = 0; - int* heap; - double* activity; - int* orderpos; - - lbool* values = s->assigns; - - // The first decisions - if ( s->pPrefVars && s->nPrefDecNum < s->nPrefVars ) - { - int i; - s->nPrefDecNum++; - for ( i = 0; i < s->nPrefVars; i++ ) - if ( values[s->pPrefVars[i]] == l_Undef ) - return s->pPrefVars[i]; - } - - // Random decision: - if (drand(&s->random_seed) < random_var_freq){ - int next = irand(&s->random_seed,s->size); - assert(next >= 0 && next < s->size); - if (values[next] == l_Undef) - return next; - } - - // Activity based decision: - - heap = veci_begin(&s->order); - activity = s->activity; - orderpos = s->orderpos; - - - while (veci_size(&s->order) > 0){ - int next = heap[0]; - int size = veci_size(&s->order)-1; - int x = heap[size]; - - veci_resize(&s->order,size); - - orderpos[next] = -1; - - if (size > 0){ - double act = activity[x]; - - int i = 0; - int child = 1; - - - while (child < size){ - if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) - child++; - - assert(child < size); - - if (act >= activity[heap[child]]) - break; - - heap[i] = heap[child]; - orderpos[heap[i]] = i; - i = child; - child = 2 * child + 1; - } - heap[i] = x; - orderpos[heap[i]] = i; - } - - if (values[next] == l_Undef) - return next; - } - -// s->timeSelect += clock() - clk; - return var_Undef; -} - -// J-frontier -extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); -extern void Asat_JManUnassign( Asat_JMan_t * p, int Var ); -extern int Asat_JManSelect( Asat_JMan_t * p ); - -//================================================================================================= -// Activity functions: - -static inline void act_var_rescale(solver* s) { - double* activity = s->activity; - int i; - for (i = 0; i < s->size; i++) - activity[i] *= 1e-100; - s->var_inc *= 1e-100; -} - -static inline void act_var_bump(solver* s, int v) { - double* activity = s->activity; - activity[v] += s->var_inc; -// activity[v] += s->var_inc * s->factors[v]; - if (activity[v] > 1e100) - act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); - if ( s->pJMan == NULL && 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_clause_rescale(solver* s) { - clause** cs = (clause**)vec_begin(&s->learnts); - int i; - for (i = 0; i < vec_size(&s->learnts); i++){ - float a = clause_activity(cs[i]); - clause_setactivity(cs[i], a * (float)1e-20); - } - s->cla_inc *= (float)1e-20; -} - - -static inline void act_clause_bump(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; } - - -//================================================================================================= -// Clause functions: - -/* pre: size > 1 && no variable occurs twice - */ -static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) -{ - int size; - clause* c; - int i; - - assert(end - begin > 1); - assert(learnt >= 0 && learnt < 2); - size = end - begin; - -// 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); - - for (i = 0; i < size; i++) - { - assert(begin[i] >= 0); - c->lits[i] = begin[i]; - } - - if (learnt) - *((float*)&c->lits[size]) = 0.0; - - assert(begin[0] >= 0); - assert(begin[0] < s->size*2); - assert(begin[1] >= 0); - assert(begin[1] < s->size*2); - - assert(neg(begin[0]) < s->size*2); - assert(neg(begin[1]) < s->size*2); - - //vec_push(solver_read_wlist(s,neg(begin[0])),(void*)c); - //vec_push(solver_read_wlist(s,neg(begin[1])),(void*)c); - - vec_push(solver_read_wlist(s,neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); - vec_push(solver_read_wlist(s,neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); - - return c; -} - - -static void clause_remove(solver* s, clause* c) -{ - lit* lits = clause_begin(c); - assert(neg(lits[0]) < s->size*2); - assert(neg(lits[1]) < s->size*2); - assert(lits[0] < s->size*2); - - //vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)c); - //vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)c); - - vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); - - if (clause_learnt(c)){ - s->solver_stats.learnts--; - s->solver_stats.learnts_literals -= clause_size(c); - }else{ - s->solver_stats.clauses--; - 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 - -} - - -static lbool clause_simplify(solver* s, clause* c) -{ - lit* lits = clause_begin(c); - lbool* values = s->assigns; - int i; - - assert(solver_dlevel(s) == 0); - - for (i = 0; i < clause_size(c); i++){ - lbool sig = !lit_sign(lits[i]); sig += sig - 1; - if (values[lit_var(lits[i])] == sig) - return l_True; - } - return l_False; -} - -//================================================================================================= -// Minor (solver) functions: - -static void solver_setnvars(solver* s,int n) -{ - int var; - if (s->cap < n){ - - while (s->cap < n) s->cap = s->cap*2+1; - - s->wlists = (vec*) realloc(s->wlists, sizeof(vec)*s->cap*2); - s->activity = (double*) realloc(s->activity, 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); - s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); - s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); - s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); - } - - for (var = s->size; var < n; var++){ - vec_new(&s->wlists[2*var]); - vec_new(&s->wlists[2*var+1]); - s->activity [var] = 0; - s->assigns [var] = l_Undef; - s->orderpos [var] = var; - s->reasons [var] = (clause*)0; - s->levels [var] = 0; - s->tags [var] = l_Undef; - - assert(veci_size(&s->order) == var); - veci_push(&s->order,var); - order_update(s,var); - } - - s->size = n > s->size ? n : s->size; -} - - -static inline bool enqueue(solver* s, lit l, clause* from) -{ - lbool* values = s->assigns; - int v = lit_var(l); - lbool val = values[v]; - lbool sig = !lit_sign(l); sig += sig - 1; -#ifdef VERBOSEDEBUG - printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); -#endif - if (val != l_Undef){ - return val == sig; - }else{ - // New fact -- store it. - int* levels = s->levels; - clause** reasons = s->reasons; -#ifdef VERBOSEDEBUG - printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); -#endif - - values [v] = sig; - levels [v] = solver_dlevel(s); - reasons[v] = from; - s->trail[s->qtail++] = l; - - if ( s->pJMan ) - Asat_JManAssign( s->pJMan, v ); - else - order_assigned(s, v); - return 1; - } -} - - -static inline void assume(solver* s, lit l){ - assert(s->qtail == s->qhead); - assert(s->assigns[lit_var(l)] == l_Undef); -#ifdef VERBOSEDEBUG - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); -#endif - veci_push(&s->trail_lim,s->qtail); - enqueue(s,l,(clause*)0); -} - - -static inline void solver_canceluntil(solver* s, int level) { - lit* trail; - lbool* values; - clause** reasons; - int bound; - int c; - - if (solver_dlevel(s) <= level) - return; - - trail = s->trail; - values = s->assigns; - reasons = s->reasons; - bound = veci_begin(&s->trail_lim)[level]; - - for (c = s->qtail-1; c >= bound; c--) { - int x = lit_var(trail[c]); - values [x] = l_Undef; - reasons[x] = (clause*)0; - } - - if ( s->pJMan ) - for (c = s->qtail-1; c >= bound; c--) - Asat_JManUnassign( s->pJMan, lit_var(trail[c]) ); - else - for (c = s->qhead-1; c >= bound; c--) - order_unassigned( s, lit_var(trail[c]) ); - - s->qhead = s->qtail = bound; - veci_resize(&s->trail_lim,level); -} - -static void solver_record(solver* s, veci* cls) -{ - lit* begin = veci_begin(cls); - lit* end = begin + veci_size(cls); - clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; - enqueue(s,*begin,c); - -Sat_SolverTraceWrite( s, begin, end, 0 ); - - assert(veci_size(cls) > 0); - - if (c != 0) { - vec_push(&s->learnts,(void*)c); - act_clause_bump(s,c); - s->solver_stats.learnts++; - s->solver_stats.learnts_literals += veci_size(cls); - } -} - - -static double solver_progress(solver* s) -{ - lbool* values = s->assigns; - int* levels = s->levels; - int i; - - double progress = 0; - double F = 1.0 / s->size; - for (i = 0; i < s->size; i++) - if (values[i] != l_Undef) - progress += pow(F, levels[i]); - return progress / s->size; -} - -//================================================================================================= -// Major methods: - -static bool solver_lit_removable(solver* s, lit l, int minl) -{ - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int top = veci_size(&s->tagged); - - assert(lit_var(l) >= 0 && lit_var(l) < s->size); - assert(reasons[lit_var(l)] != 0); - veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - - while (veci_size(&s->stack) > 0){ - clause* c; - int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; - assert(v >= 0 && v < s->size); - veci_resize(&s->stack,veci_size(&s->stack)-1); - assert(reasons[v] != 0); - c = reasons[v]; - - if (clause_is_lit(c)){ - int v = lit_var(clause_read_lit(c)); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - veci_push(&s->stack,v); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - int j; - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return 0; - } - } - }else{ - lit* lits = clause_begin(c); - int i, j; - - for (i = 1; i < clause_size(c); i++){ - int v = lit_var(lits[i]); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - - veci_push(&s->stack,lit_var(lits[i])); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return 0; - } - } - } - } - } - - return 1; -} - -static void solver_analyze(solver* s, clause* c, veci* learnt) -{ - lit* trail = s->trail; - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int cnt = 0; - lit p = lit_Undef; - int ind = s->qtail-1; - lit* lits; - int i, j, minl; - int* tagged; - - veci_push(learnt,lit_Undef); - - do{ - assert(c != 0); - - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - 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)) - cnt++; - else - veci_push(learnt,q); - } - }else{ - - if (clause_learnt(c)) - act_clause_bump(s,c); - - lits = clause_begin(c); - //printlits(lits,lits+clause_size(c)); printf("\n"); - for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ - lit q = lits[j]; - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - 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)) - cnt++; - else - veci_push(learnt,q); - } - } - } - - while (tags[lit_var(trail[ind--])] == l_Undef); - - p = trail[ind+1]; - c = reasons[lit_var(p)]; - cnt--; - - }while (cnt > 0); - -// *veci_begin(learnt) = neg(p); - - lits = veci_begin(learnt); - lits[0] = neg(p); - - minl = 0; - for (i = 1; i < veci_size(learnt); i++){ - int lev = levels[lit_var(lits[i])]; - minl |= 1 << (lev & 31); - } - - // 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)) - lits[j++] = lits[i]; - } -// j = veci_size(learnt); - - // update size of learnt + statistics - s->solver_stats.max_literals += veci_size(learnt); - veci_resize(learnt,j); - s->solver_stats.tot_literals += j; - - // clear tags - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - tags[tagged[i]] = l_Undef; - veci_resize(&s->tagged,0); - -#ifdef DEBUG - for (i = 0; i < s->size; i++) - assert(tags[i] == l_Undef); -#endif - -#ifdef VERBOSEDEBUG - printf(L_IND"Learnt {", L_ind); - for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); -#endif - if (veci_size(learnt) > 1){ - int max_i = 1; - int max = levels[lit_var(lits[1])]; - lit tmp; - - for (i = 2; i < veci_size(learnt); i++) - if (levels[lit_var(lits[i])] > max){ - max = levels[lit_var(lits[i])]; - max_i = i; - } - - tmp = lits[1]; - lits[1] = lits[max_i]; - lits[max_i] = tmp; - } -#ifdef VERBOSEDEBUG - { - int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; - printf(" } at level %d\n", lev); - } -#endif -} - - -clause* solver_propagate(solver* s) -{ - lbool* values = s->assigns; - clause* confl = (clause*)0; - lit* lits; - - //printf("solver_propagate\n"); - while (confl == 0 && s->qtail - s->qhead > 0){ - lit p = s->trail[s->qhead++]; - vec* ws = solver_read_wlist(s,p); - clause **begin = (clause**)vec_begin(ws); - clause **end = begin + vec_size(ws); - clause **i, **j; - - s->solver_stats.propagations++; - s->simpdb_props--; - - //printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p)); - for (i = j = begin; i < end; ){ - if (clause_is_lit(*i)){ - *j++ = *i; - if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ - confl = s->binary; - (clause_begin(confl))[1] = neg(p); - (clause_begin(confl))[0] = clause_read_lit(*i++); - - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - }else{ - lit false_lit; - lbool sig; - - lits = clause_begin(*i); - - // Make sure the false literal is data[1]: - false_lit = neg(p); - if (lits[0] == false_lit){ - lits[0] = lits[1]; - lits[1] = false_lit; - } - assert(lits[1] == false_lit); - //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); - - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig){ - *j++ = *i; - }else{ - // Look for new watch: - lit* stop = lits + clause_size(*i); - lit* k; - for (k = lits + 2; k < stop; k++){ - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig){ - lits[1] = *k; - *k = false_lit; - vec_push(solver_read_wlist(s,neg(lits[1])),*i); - goto next; } - } - - *j++ = *i; - // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)){ - confl = *i++; - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - } - } - next: - i++; - } - - s->solver_stats.inspects += j - (clause**)vec_begin(ws); - vec_resize(ws,j - (clause**)vec_begin(ws)); - } - - return confl; -} - -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) -{ - int i, j; - double extra_lim = s->cla_inc / vec_size(&s->learnts); // Remove any clause below this activity - clause** learnts = (clause**)vec_begin(&s->learnts); - clause** reasons = s->reasons; - - sort(vec_begin(&s->learnts), vec_size(&s->learnts), &clause_cmp); - - for (i = j = 0; i < vec_size(&s->learnts) / 2; i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - for (; i < vec_size(&s->learnts); i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - - //printf("reducedb deleted %d\n", vec_size(&s->learnts) - j); - - - vec_resize(&s->learnts,j); -} - -static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) -{ - int* levels = s->levels; - double var_decay = 0.95; - double clause_decay = 0.999; - double random_var_freq = 0.0;//0.02; - - int conflictC = 0; - veci learnt_clause; - int i; - - assert(s->root_level == solver_dlevel(s)); - - s->solver_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); - - // reset the activities - if ( s->factors ) - { - s->var_inc = 1.0; - for ( i = 0; i < s->size; i++ ) - { - s->activity[i] = (double)s->factors[i]; -// if ( s->orderpos[i] != -1 ) -// order_update(s, i ); - } -// s->activity[i] = 1.0; - } - - for (;;){ - clause* confl = solver_propagate(s); - if (confl != 0){ - // CONFLICT - int blevel; - -#ifdef VERBOSEDEBUG - printf(L_IND"**CONFLICT**\n", L_ind); -#endif - s->solver_stats.conflicts++; conflictC++; - if (solver_dlevel(s) == s->root_level){ - veci_delete(&learnt_clause); - return l_False; - } - - veci_resize(&learnt_clause,0); - solver_analyze(s, confl, &learnt_clause); - blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; - solver_canceluntil(s,blevel); - solver_record(s,&learnt_clause); - act_var_decay(s); - act_clause_decay(s); - - }else{ - // NO CONFLICT - int next; - - 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); - veci_delete(&learnt_clause); - return l_Undef; - } - - if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit || - s->nInsLimit && s->solver_stats.inspects > s->nInsLimit ) - { - // Reached bound on number of conflicts: - s->progress_estimate = solver_progress(s); - solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; - } - - if (solver_dlevel(s) == 0) - // Simplify the set of problem clauses: - solver_simplify(s); - - if (nof_learnts >= 0 && vec_size(&s->learnts) - s->qtail >= nof_learnts) - // Reduce the set of learnt clauses: - solver_reducedb(s); - - // New variable decision: - s->solver_stats.decisions++; - if ( s->pJMan ) - next = Asat_JManSelect( s->pJMan ); - else - next = order_select(s,(float)random_var_freq); - - if (next == var_Undef){ - // 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_delete(&learnt_clause); - return l_True; - } - - assume(s,neg(toLit(next))); - } - } - - return l_Undef; // cannot happen -} - -//================================================================================================= -// External solver functions: - -solver* solver_new(void) -{ - solver* s = (solver*)malloc(sizeof(solver)); - memset( s, 0, sizeof(solver) ); - - // initialize vectors - vec_new(&s->clauses); - vec_new(&s->learnts); - veci_new(&s->order); - veci_new(&s->trail_lim); - veci_new(&s->tagged); - veci_new(&s->stack); - veci_new(&s->model); - - // initialize arrays - s->wlists = 0; - s->activity = 0; - s->factors = 0; - s->assigns = 0; - s->orderpos = 0; - s->reasons = 0; - s->levels = 0; - s->tags = 0; - s->trail = 0; - - - // initialize other vars - s->size = 0; - s->cap = 0; - s->qhead = 0; - s->qtail = 0; - s->cla_inc = 1; - s->cla_decay = 1; - s->var_inc = 1; - s->var_decay = 1; - s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; - s->random_seed = 91648253; - s->progress_estimate = 0; - s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); - s->binary->size_learnt = (2 << 1); - s->verbosity = 0; - - s->solver_stats.starts = 0; - s->solver_stats.decisions = 0; - s->solver_stats.propagations = 0; - s->solver_stats.inspects = 0; - s->solver_stats.conflicts = 0; - s->solver_stats.clauses = 0; - s->solver_stats.clauses_literals = 0; - s->solver_stats.learnts = 0; - s->solver_stats.learnts_literals = 0; - 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 - s->pJMan = NULL; - s->pPrefVars = NULL; - s->nPrefVars = 0; - s->timeTotal = clock(); - s->timeSelect = 0; - s->timeUpdate = 0; - 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); - vec_delete(&s->learnts); - veci_delete(&s->order); - veci_delete(&s->trail_lim); - veci_delete(&s->tagged); - veci_delete(&s->stack); - veci_delete(&s->model); - free(s->binary); - - // delete arrays - if (s->wlists != 0){ - int i; - for (i = 0; i < s->size*2; i++) - vec_delete(&s->wlists[i]); - - // if one is different from null, all are - free(s->wlists); - free(s->activity ); - free(s->assigns ); - free(s->orderpos ); - free(s->reasons ); - free(s->levels ); - free(s->trail ); - free(s->tags ); - } - if ( s->pJMan ) Asat_JManStop( s ); - if ( s->pPrefVars ) free( s->pPrefVars ); - if ( s->factors ) free( s->factors ); - free(s); -} - - -bool solver_addclause(solver* s, lit* begin, lit* end) -{ - lit *i,*j; - int maxvar; - lbool* values; - lit last; - - if (begin == end) return 0; - - //printlits(begin,end); printf("\n"); - // insertion sort - maxvar = lit_var(*begin); - for (i = begin + 1; i < end; i++){ - lit l = *i; - maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; - for (j = i; j > begin && *(j-1) > l; j--) - *j = *(j-1); - *j = l; - } - solver_setnvars(s,maxvar+1); - - //printlits(begin,end); printf("\n"); - values = s->assigns; - - // delete duplicates - last = lit_Undef; - for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); - lbool sig = !lit_sign(*i); sig += sig - 1; - if (*i == neg(last) || sig == values[lit_var(*i)]) - return 1; // tautology - else if (*i != last && values[lit_var(*i)] == l_Undef) - last = *j++ = *i; - } - - //printf("final: "); printlits(begin,j); printf("\n"); - - if (j == begin) // empty clause - return 0; - -Sat_SolverTraceWrite( s, begin, end, 1 ); - - if (j - begin == 1) // unit clause - return enqueue(s,*begin,(clause*)0); - - // create new clause - vec_push(&s->clauses,clause_new(s,begin,j,0)); - - - s->solver_stats.clauses++; - s->solver_stats.clauses_literals += j - begin; - - return 1; -} - - -bool solver_simplify(solver* s) -{ - clause** reasons; - int type; - - assert(solver_dlevel(s) == 0); - - if (solver_propagate(s) != 0) - return 0; - - if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return 1; - - reasons = s->reasons; - for (type = 0; type < 2; type++){ - vec* cs = type ? &s->learnts : &s->clauses; - clause** cls = (clause**)vec_begin(cs); - - int i, j; - for (j = i = 0; i < vec_size(cs); i++){ - if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && - clause_simplify(s,cls[i]) == l_True) - clause_remove(s,cls[i]); - else - cls[j++] = cls[i]; - } - vec_resize(cs,j); - } - - s->simpdb_assigns = s->qhead; - // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals); - - return 1; -} - - -bool solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit ) -{ - double nof_conflicts = 100; -// double nof_conflicts = 1000000; - double nof_learnts = solver_nclauses(s) / 3; - lbool status = l_Undef; - lbool* values = s->assigns; - lit* i; - - // set the external limits - s->nConfLimit = nConfLimit; // external limit on the number of conflicts - s->nInsLimit = nInsLimit; // 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)){ - solver_canceluntil(s,0); - return l_False; } - - s->root_level = solver_dlevel(s); - - if (s->verbosity >= 1){ - printf("==================================[MINISAT]===================================\n"); - printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); - printf("==============================================================================\n"); - } - - while (status == l_Undef){ - double Ratio = (s->solver_stats.learnts == 0)? 0.0 : - s->solver_stats.learnts_literals / (double)s->solver_stats.learnts; - - if (s->verbosity >= 1){ - printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", - (double)s->solver_stats.conflicts, - (double)s->solver_stats.clauses, - (double)s->solver_stats.clauses_literals, - (double)nof_learnts, - (double)s->solver_stats.learnts, - (double)s->solver_stats.learnts_literals, - Ratio, - s->progress_estimate*100); - fflush(stdout); - } - s->nPrefDecNum = 0; - status = 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->solver_stats.conflicts > s->nConfLimit ) - { -// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); - break; - } - if ( s->nInsLimit && s->solver_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); - s->timeTotal = clock() - s->timeTotal; - return status; -} - - -int solver_nvars(solver* s) -{ - return s->size; -} - - -int solver_nclauses(solver* s) -{ - return vec_size(&s->clauses); -} - -//================================================================================================= -// Sorting functions (sigh): - -static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) -{ - int i, j, best_i; - void* tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (comp(array[j], array[best_i]) < 0) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - - -static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) -{ - if (size <= 15) - selectionsort(array, size, comp); - - else{ - void* pivot = array[irand(seed, size)]; - void* tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(comp(array[i], pivot)<0); - do j--; while(comp(pivot, array[j])<0); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sortrnd(array , i , comp, seed); - sortrnd(&array[i], size-i, comp, seed); - } -} - -void 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/solver.h b/src/sat/asat/solver.h deleted file mode 100644 index 83066f41..00000000 --- a/src/sat/asat/solver.h +++ /dev/null @@ -1,189 +0,0 @@ -/************************************************************************************************** -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 solver_h -#define solver_h - -#ifdef __cplusplus -extern "C" { -#endif - -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 -#endif - -#include "solver_vec.h" -#include "asatmem.h" - -//================================================================================================= -// Simple types: - -//typedef int bool; -#ifndef __cplusplus -#ifndef bool -#define bool int -#endif -#endif - -typedef int lit; -typedef char lbool; - -#ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 -#else -typedef long long sint64; -#endif - -static const int var_Undef = -1; -static const lit lit_Undef = -2; - -static const lbool l_Undef = 0; -static const lbool l_True = 1; -static const lbool l_False = -1; - -static inline lit neg (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 + (int)(c != 0); } - -//================================================================================================= -// Public interface: - -typedef struct Asat_JMan_t_ Asat_JMan_t; - -struct solver_t; -typedef struct solver_t solver; - -extern solver* solver_new(void); -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, sint64 nConfLimit, sint64 nInsLimit); -extern int * solver_get_model( solver * p, int * pVars, int nVars ); - -extern int solver_nvars(solver* s); -extern int solver_nclauses(solver* s); - - -// additional procedures -extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, - lit* assumptionsBegin, lit* assumptionsEnd, - int incrementVars); -extern void Asat_SatPrintStats( FILE * pFile, solver * p ); -extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); -extern void Asat_SolverSetFactors( solver * s, float * pFactors ); - -// trace recording -extern void Sat_SolverTraceStart( solver * pSat, char * pName ); -extern void Sat_SolverTraceStop( solver * pSat ); -extern void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ); - -// J-frontier support -extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); -extern void Asat_JManStop( solver * pSat ); - - -struct stats_t -{ - sint64 starts, decisions, propagations, inspects, conflicts; - sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; -}; -typedef struct stats_t stats; - -//================================================================================================= -// Solver representation: - -struct clause_t; -typedef struct clause_t clause; - -struct solver_t -{ - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. - - // clauses - vec clauses; // List of problem constraints. (contains: clause*) - vec learnts; // List of learnt clauses. (contains: clause*) - - // activities - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - float cla_inc; // Amount to bump next clause with. - float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - - vec* wlists; // - double* activity; // A heuristic measurement of the activity of a variable. - float * factors; // the factor of variable activity - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - - clause* binary; // A temporary binary clause - lbool* tags; // - veci tagged; // (contains: var) - veci stack; // (contains: var) - - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci model; // If problem is solved, this vector contains the model (contains: lbool). - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - - sint64 nConfLimit; // external limit on the number of conflicts - sint64 nInsLimit; // external limit on the number of implications - - // the memory manager - Asat_MmStep_t * pMem; - - // J-frontier - Asat_JMan_t * pJMan; - - // for making decisions on some variables first - int nPrefDecNum; - int * pPrefVars; - int nPrefVars; - - // solver statistics - stats solver_stats; - int timeTotal; - int timeSelect; - int timeUpdate; - - // trace recording - FILE * pFile; - int nClauses; - int nRoots; -}; - -#ifdef __cplusplus -} -#endif - -#endif diff --git a/src/sat/asat/solver_vec.h b/src/sat/asat/solver_vec.h deleted file mode 100644 index 1ae30b0a..00000000 --- a/src/sat/asat/solver_vec.h +++ /dev/null @@ -1,83 +0,0 @@ -/************************************************************************************************** -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 vec_h -#define vec_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 vec_t { - int size; - int cap; - void** ptr; -}; -typedef struct vec_t vec; - -static inline void vec_new (vec* v) { - v->size = 0; - v->cap = 4; - v->ptr = (void**)malloc(sizeof(void*)*v->cap); -} - -static inline void vec_delete (vec* v) { free(v->ptr); } -static inline void** vec_begin (vec* v) { return v->ptr; } -static inline int vec_size (vec* v) { return v->size; } -static inline void vec_resize (vec* v, int k) { v->size = k; } // only safe to shrink !! -static inline void vec_push (vec* 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 |