summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/asat/added.c234
-rw-r--r--src/sat/asat/asatmem.c527
-rw-r--r--src/sat/asat/asatmem.h78
-rw-r--r--src/sat/asat/jfront.c514
-rw-r--r--src/sat/asat/main.c195
-rw-r--r--src/sat/asat/module.make4
-rw-r--r--src/sat/asat/solver.c1290
-rw-r--r--src/sat/asat/solver.h189
-rw-r--r--src/sat/asat/solver_vec.h83
-rw-r--r--src/sat/bsat/satInter.c980
-rw-r--r--src/sat/bsat/satSolver.c79
-rw-r--r--src/sat/bsat/satSolver.h33
-rw-r--r--src/sat/bsat/satStore.c437
-rw-r--r--src/sat/bsat/satStore.h135
-rw-r--r--src/sat/bsat/satTrace.c (renamed from src/sat/asat/satTrace.c)15
-rw-r--r--src/sat/bsat/satUtil.c71
-rw-r--r--src/sat/csat/csat_apis.c2
-rw-r--r--src/sat/fraig/fraig.h6
-rw-r--r--src/sat/proof/pr.c62
19 files changed, 1790 insertions, 3144 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/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
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
new file mode 100644
index 00000000..e22b309c
--- /dev/null
+++ b/src/sat/bsat/satInter.c
@@ -0,0 +1,980 @@
+/**CFile****************************************************************
+
+ FileName [satInter.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT sat_solver.]
+
+ Synopsis [Interpolation package.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments
+static const lit LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Int_Man_t_
+{
+ // clauses of the problems
+ Sto_Man_t * pCnf; // the set of CNF clauses for A and B
+ // various parameters
+ int fVerbose; // verbosiness flag
+ int fProofVerif; // verifies the proof
+ int fProofWrite; // writes the proof file
+ int nVarsAlloc; // the allocated size of var arrays
+ int nClosAlloc; // the allocated size of clause arrays
+ // internal BCP
+ int nRootSize; // the number of root level assignments
+ int nTrailSize; // the number of assignments made
+ lit * pTrail; // chronological order of assignments (size nVars)
+ lit * pAssigns; // assignments by variable (size nVars)
+ char * pSeens; // temporary mark (size nVars)
+ Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars)
+ Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars)
+ // interpolation data
+ int nVarsAB; // the number of global variables
+ char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
+ unsigned * pInters; // storage for interpolants as truth tables (size nClauses)
+ int nIntersAlloc; // the allocated size of truth table array
+ int nWords; // the number of words in the truth table
+ // proof recording
+ int Counter; // counter of resolved clauses
+ int * pProofNums; // the proof numbers for each clause (size nClauses)
+ FILE * pFile; // the file for proof recording
+ // internal verification
+ lit * pResLits; // the literals of the resolvent
+ int nResLits; // the number of literals of the resolvent
+ int nResLitsAlloc;// the number of literals of the resolvent
+ // runtime stats
+ int timeBcp; // the runtime for BCP
+ int timeTrace; // the runtime of trace construction
+ int timeTotal; // the total runtime of interpolation
+};
+
+// procedure to get hold of the clauses' truth table
+static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; }
+static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; }
+static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; }
+static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
+static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
+static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
+static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
+
+// reading/writing the proof for a clause
+static inline int Int_ManProofRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
+static inline void Int_ManProofWrite( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Int_Man_t * Int_ManAlloc( int nVarsAlloc )
+{
+ Int_Man_t * p;
+ // allocate the manager
+ p = (Int_Man_t *)malloc( sizeof(Int_Man_t) );
+ memset( p, 0, sizeof(Int_Man_t) );
+ // verification
+ p->nResLitsAlloc = (1<<16);
+ p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+ // parameters
+ p->fProofWrite = 0;
+ p->fProofVerif = 0;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count common variables in the clauses of A and B.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Int_ManCommonVars( Int_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ int Var, nVarsAB, v;
+
+ // mark the variable encountered in the clauses of A
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( !pClause->fA )
+ break;
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
+ }
+
+ // check variables that appear in clauses of B
+ nVarsAB = 0;
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( pClause->fA )
+ continue;
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ Var = lit_var(pClause->pLits[v]);
+ if ( p->pVarTypes[Var] == 1 ) // var of A
+ {
+ // change it into a global variable
+ nVarsAB++;
+ p->pVarTypes[Var] = -1;
+ }
+ }
+ }
+
+ // order global variables
+ nVarsAB = 0;
+ for ( v = 0; v < p->pCnf->nVars; v++ )
+ if ( p->pVarTypes[v] == -1 )
+ p->pVarTypes[v] -= p->nVarsAB++;
+printf( "There are %d global variables.\n", nVarsAB );
+ return nVarsAB;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resize proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManResize( Int_Man_t * p )
+{
+ // check if resizing is needed
+ if ( p->nVarsAlloc < p->pCnf->nVars )
+ {
+ int nVarsAllocOld = p->nVarsAlloc;
+ // find the new size
+ if ( p->nVarsAlloc == 0 )
+ p->nVarsAlloc = 1;
+ while ( p->nVarsAlloc < p->pCnf->nVars )
+ p->nVarsAlloc *= 2;
+ // resize the arrays
+ p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
+ p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
+ p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
+ p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
+ p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc );
+ p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+ }
+
+ // clean the free space
+ memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
+ memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars );
+ memset( p->pVarTypes, 0, sizeof(char) * p->pCnf->nVars );
+ memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars );
+ memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
+
+ // compute the number of common variables
+ p->nVarsAB = Int_ManCommonVars( p );
+ // compute the number of words in the truth table
+ p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
+
+ // check if resizing of clauses is needed
+ if ( p->nClosAlloc < p->pCnf->nClauses )
+ {
+ // find the new size
+ if ( p->nClosAlloc == 0 )
+ p->nClosAlloc = 1;
+ while ( p->nClosAlloc < p->pCnf->nClauses )
+ p->nClosAlloc *= 2;
+ // resize the arrays
+ p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc );
+ }
+ memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
+
+ // check if resizing of truth tables is needed
+ if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
+ {
+ p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
+ p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
+ }
+ memset( p->pInters, 0, sizeof(unsigned) * p->nIntersAlloc );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManFree( Int_Man_t * p )
+{
+ printf( "Runtime stats:\n" );
+PRT( "BCP ", p->timeBcp );
+PRT( "Trace ", p->timeTrace );
+PRT( "TOTAL ", p->timeTotal );
+
+ free( p->pInters );
+ free( p->pProofNums );
+ free( p->pTrail );
+ free( p->pAssigns );
+ free( p->pSeens );
+ free( p->pVarTypes );
+ free( p->pReasons );
+ free( p->pWatches );
+ free( p->pResLits );
+ free( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+ int i;
+ printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofRead(p, pClause) );
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ printf( " %d", pClause->pLits[i] );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the resolvent.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+ int i;
+ printf( "Resolvent: {" );
+ for ( i = 0; i < nResLits; i++ )
+ printf( " %d", pResLits[i] );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records the proof.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits )
+{
+ int Remainder, nWords;
+ int w, i;
+
+ Remainder = (nBits%(sizeof(unsigned)*8));
+ nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+ for ( w = nWords-1; w >= 0; w-- )
+ for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
+ fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the interpolant for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+ printf( "Clause %2d : ", pClause->Id );
+ Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) );
+ printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Adds one clause to the watcher list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit )
+{
+ assert( lit_check(Lit, p->pCnf->nVars) );
+ if ( pClause->pLits[0] == Lit )
+ pClause->pNext0 = p->pWatches[lit_neg(Lit)];
+ else
+ {
+ assert( pClause->pLits[1] == Lit );
+ pClause->pNext1 = p->pWatches[lit_neg(Lit)];
+ }
+ p->pWatches[lit_neg(Lit)] = pClause;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Records implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason )
+{
+ int Var = lit_var(Lit);
+ if ( p->pAssigns[Var] != LIT_UNDEF )
+ return p->pAssigns[Var] == Lit;
+ p->pAssigns[Var] = Lit;
+ p->pReasons[Var] = pReason;
+ p->pTrail[p->nTrailSize++] = Lit;
+//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Int_ManCancelUntil( Int_Man_t * p, int Level )
+{
+ lit Lit;
+ int i, Var;
+ for ( i = p->nTrailSize - 1; i >= Level; i-- )
+ {
+ Lit = p->pTrail[i];
+ Var = lit_var( Lit );
+ p->pReasons[Var] = NULL;
+ p->pAssigns[Var] = LIT_UNDEF;
+//printf( "cancelling var %d\n", Var );
+ }
+ p->nTrailSize = Level;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate one assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit )
+{
+ Sto_Cls_t ** ppPrev, * pCur, * pTemp;
+ lit LitF = lit_neg(Lit);
+ int i;
+ // iterate through the literals
+ ppPrev = p->pWatches + Lit;
+ for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
+ {
+ // make sure the false literal is in the second literal of the clause
+ if ( pCur->pLits[0] == LitF )
+ {
+ pCur->pLits[0] = pCur->pLits[1];
+ pCur->pLits[1] = LitF;
+ pTemp = pCur->pNext0;
+ pCur->pNext0 = pCur->pNext1;
+ pCur->pNext1 = pTemp;
+ }
+ assert( pCur->pLits[1] == LitF );
+
+ // if the first literal is true, the clause is satisfied
+ if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
+ {
+ ppPrev = &pCur->pNext1;
+ continue;
+ }
+
+ // look for a new literal to watch
+ for ( i = 2; i < (int)pCur->nLits; i++ )
+ {
+ // skip the case when the literal is false
+ if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
+ continue;
+ // the literal is either true or unassigned - watch it
+ pCur->pLits[1] = pCur->pLits[i];
+ pCur->pLits[i] = LitF;
+ // remove this clause from the watch list of Lit
+ *ppPrev = pCur->pNext1;
+ // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
+ Int_ManWatchClause( p, pCur, pCur->pLits[1] );
+ break;
+ }
+ if ( i < (int)pCur->nLits ) // found new watch
+ continue;
+
+ // clause is unit - enqueue new implication
+ if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) )
+ {
+ ppPrev = &pCur->pNext1;
+ continue;
+ }
+
+ // conflict detected - return the conflict clause
+ return pCur;
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate the current assignments.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
+{
+ Sto_Cls_t * pClause;
+ int i;
+ int clk = clock();
+ for ( i = Start; i < p->nTrailSize; i++ )
+ {
+ pClause = Int_ManPropagateOne( p, p->pTrail[i] );
+ if ( pClause )
+ {
+p->timeBcp += clock() - clk;
+ return pClause;
+ }
+ }
+p->timeBcp += clock() - clk;
+ return NULL;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes one root clause into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+ Int_ManProofWrite( p, pClause, ++p->Counter );
+
+ if ( p->fProofWrite )
+ {
+ int v;
+ fprintf( p->pFile, "%d", Int_ManProofRead(p, pClause) );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
+ fprintf( p->pFile, " 0 0\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Traces the proof for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
+{
+ Sto_Cls_t * pReason;
+ int i, v, Var, PrevId;
+ int fPrint = 0;
+ int clk = clock();
+
+ // collect resolvent literals
+ if ( p->fProofVerif )
+ {
+ assert( (int)pConflict->nLits <= p->nResLitsAlloc );
+ memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
+ p->nResLits = pConflict->nLits;
+ }
+
+ // mark all the variables in the conflict as seen
+ for ( v = 0; v < (int)pConflict->nLits; v++ )
+ p->pSeens[lit_var(pConflict->pLits[v])] = 1;
+
+ // start the anticedents
+// pFinal->pAntis = Vec_PtrAlloc( 32 );
+// Vec_PtrPush( pFinal->pAntis, pConflict );
+
+ if ( p->pCnf->nClausesA )
+ Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
+
+ // follow the trail backwards
+ PrevId = Int_ManProofRead(p, pConflict);
+ for ( i = p->nTrailSize - 1; i >= 0; i-- )
+ {
+ // skip literals that are not involved
+ Var = lit_var(p->pTrail[i]);
+ if ( !p->pSeens[Var] )
+ continue;
+ p->pSeens[Var] = 0;
+
+ // skip literals of the resulting clause
+ pReason = p->pReasons[Var];
+ if ( pReason == NULL )
+ continue;
+ assert( p->pTrail[i] == pReason->pLits[0] );
+
+ // add the variables to seen
+ for ( v = 1; v < (int)pReason->nLits; v++ )
+ p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+
+ // record the reason clause
+ assert( Int_ManProofRead(p, pReason) > 0 );
+ p->Counter++;
+ if ( p->fProofWrite )
+ fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofRead(p, pReason) );
+ PrevId = p->Counter;
+
+ if ( p->pCnf->nClausesA )
+ {
+ if ( p->pVarTypes[Var] == 1 ) // var of A
+ Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
+ else
+ Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
+ }
+
+ // resolve the temporary resolvent with the reason clause
+ if ( p->fProofVerif )
+ {
+ int v1, v2;
+ if ( fPrint )
+ Int_ManPrintResolvent( p->pResLits, p->nResLits );
+ // check that the var is present in the resolvent
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ if ( lit_var(p->pResLits[v1]) == Var )
+ break;
+ if ( v1 == p->nResLits )
+ printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
+ if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
+ printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
+ // remove this variable from the resolvent
+ assert( lit_var(p->pResLits[v1]) == Var );
+ p->nResLits--;
+ for ( ; v1 < p->nResLits; v1++ )
+ p->pResLits[v1] = p->pResLits[v1+1];
+ // add variables of the reason clause
+ for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
+ {
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
+ break;
+ // if it is a new variable, add it to the resolvent
+ if ( v1 == p->nResLits )
+ {
+ if ( p->nResLits == p->nResLitsAlloc )
+ printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" );
+ p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
+ continue;
+ }
+ // if the variable is the same, the literal should be the same too
+ if ( p->pResLits[v1] == pReason->pLits[v2] )
+ continue;
+ // the literal is different
+ printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
+ }
+ }
+
+// Vec_PtrPush( pFinal->pAntis, pReason );
+ }
+
+ // unmark all seen variables
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// p->pSeens[lit_var(p->pTrail[i])] = 0;
+ // check that the literals are unmarked
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
+
+ // use the resulting clause to check the correctness of resolution
+ if ( p->fProofVerif )
+ {
+ int v1, v2;
+ if ( fPrint )
+ Int_ManPrintResolvent( p->pResLits, p->nResLits );
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ {
+ for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
+ if ( pFinal->pLits[v2] == p->pResLits[v1] )
+ break;
+ if ( v2 < (int)pFinal->nLits )
+ continue;
+ break;
+ }
+ if ( v1 < p->nResLits )
+ {
+ printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
+ Int_ManPrintClause( p, pConflict );
+ Int_ManPrintResolvent( p->pResLits, p->nResLits );
+ Int_ManPrintClause( p, pFinal );
+ }
+ }
+p->timeTrace += clock() - clk;
+
+ // return the proof pointer
+ if ( p->pCnf->nClausesA )
+ {
+// Int_ManPrintInterOne( p, pFinal );
+ }
+ Int_ManProofWrite( p, pFinal, p->Counter );
+ return p->Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records the proof for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+ Sto_Cls_t * pConflict;
+ int i;
+
+ // empty clause never ends up there
+ assert( pClause->nLits > 0 );
+ if ( pClause->nLits == 0 )
+ printf( "Error: Empty clause is attempted.\n" );
+
+ // add assumptions to the trail
+ assert( !pClause->fRoot );
+ assert( p->nTrailSize == p->nRootSize );
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+ {
+ assert( 0 ); // impossible
+ return 0;
+ }
+
+ // propagate the assumptions
+ pConflict = Int_ManPropagate( p, p->nRootSize );
+ if ( pConflict == NULL )
+ {
+ assert( 0 ); // cannot prove
+ return 0;
+ }
+
+ // construct the proof
+ Int_ManProofTraceOne( p, pConflict, pClause );
+
+ // undo to the root level
+ Int_ManCancelUntil( p, p->nRootSize );
+
+ // add large clauses to the watched lists
+ if ( pClause->nLits > 1 )
+ {
+ Int_ManWatchClause( p, pClause, pClause->pLits[0] );
+ Int_ManWatchClause( p, pClause, pClause->pLits[1] );
+ return 1;
+ }
+ assert( pClause->nLits == 1 );
+
+ // if the clause proved is unit, add it and propagate
+ if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
+ {
+ assert( 0 ); // impossible
+ return 0;
+ }
+
+ // propagate the assumption
+ pConflict = Int_ManPropagate( p, p->nRootSize );
+ if ( pConflict )
+ {
+ // construct the proof
+ Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
+ printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+ return 0;
+ }
+
+ // update the root level
+ p->nRootSize = p->nTrailSize;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate the root clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Int_ManProcessRoots( Int_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ int Counter;
+
+ // make sure the root clauses are preceeding the learnt clauses
+ Counter = 0;
+ Sto_ManForEachClause( p->pCnf, pClause )
+ {
+ assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) );
+ assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) );
+ Counter++;
+ }
+ assert( p->pCnf->nClauses == Counter );
+
+ // make sure the last clause if empty
+ assert( p->pCnf->pTail->nLits == 0 );
+
+ // go through the root unit clauses
+ p->nTrailSize = 0;
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ // create watcher lists for the root clauses
+ if ( pClause->nLits > 1 )
+ {
+ Int_ManWatchClause( p, pClause, pClause->pLits[0] );
+ Int_ManWatchClause( p, pClause, pClause->pLits[1] );
+ }
+ // empty clause and large clauses
+ if ( pClause->nLits != 1 )
+ continue;
+ // unit clause
+ assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
+ if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
+ {
+ // detected root level conflict
+ printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
+ assert( 0 );
+ return 0;
+ }
+ }
+
+ // propagate the root unit clauses
+ pClause = Int_ManPropagate( p, 0 );
+ if ( pClause )
+ {
+ // detected root level conflict
+ printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
+ assert( 0 );
+ return 0;
+ }
+
+ // set the root level
+ p->nRootSize = p->nTrailSize;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records the proof.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Int_ManPrepareInter( Int_Man_t * p )
+{
+ // elementary truth tables
+ unsigned uTruths[8][8] = {
+ { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+ { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+ { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+ { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+ { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
+ { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
+ { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
+ { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
+ };
+ Sto_Cls_t * pClause;
+ int Var, v;
+ assert( p->nVarsAB <= 8 );
+
+ // set interpolants for root clauses
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( !pClause->fA ) // clause of B
+ {
+ Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords );
+// Int_ManPrintInterOne( p, pClause );
+ continue;
+ }
+ // clause of A
+ Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ Var = lit_var(pClause->pLits[v]);
+ if ( p->pVarTypes[Var] < 0 ) // global var
+ {
+ if ( lit_sign(pClause->pLits[v]) ) // negative var
+ Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords );
+ else
+ Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords );
+ }
+ }
+// Int_ManPrintInterOne( p, pClause );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes interpolant for the given CNF.]
+
+ Description [Returns the number of common variable found and interpolant.
+ Returns 0, if something did not work.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult )
+{
+ Sto_Cls_t * pClause;
+ int RetValue = 1;
+ int clkTotal = clock();
+
+ // check that the CNF makes sense
+ assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
+
+ // adjust the manager
+ Int_ManResize( p );
+
+ // propagate root level assignments
+ Int_ManProcessRoots( p );
+
+ // prepare the interpolant computation
+ Int_ManPrepareInter( p );
+
+ // construct proof for each clause
+ // start the proof
+ if ( p->fProofWrite )
+ {
+ p->pFile = fopen( "proof.cnf_", "w" );
+ p->Counter = 0;
+ }
+
+ // write the root clauses
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ Int_ManProofWriteOne( p, pClause );
+
+ // consider each learned clause
+ Sto_ManForEachClause( p->pCnf, pClause )
+ {
+ if ( pClause->fRoot )
+ continue;
+ if ( !Int_ManProofRecordOne( p, pClause ) )
+ {
+ RetValue = 0;
+ break;
+ }
+ }
+
+ // stop the proof
+ if ( p->fProofWrite )
+ {
+ fclose( p->pFile );
+ p->pFile = NULL;
+ }
+
+ printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
+ p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
+ 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
+ 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
+
+p->timeTotal += clock() - clkTotal;
+ Int_ManFree( p );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1dd40155..6aafc187 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -477,6 +477,16 @@ static void sat_solver_record(sat_solver* s, veci* cls)
clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
enqueue(s,*begin,c);
+ ///////////////////////////////////
+ // add clause to internal storage
+ if ( s->pStore )
+ {
+ extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+ int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+ assert( RetValue );
+ }
+ ///////////////////////////////////
+
assert(veci_size(cls) > 0);
if (c != 0) {
@@ -1022,6 +1032,7 @@ void sat_solver_delete(sat_solver* s)
free(s->tags );
}
+ sat_solver_store_free(s);
free(s);
}
@@ -1046,6 +1057,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
*j = l;
}
sat_solver_setnvars(s,maxvar+1);
+// sat_solver_setnvars(s, lit_var(*(end-1))+1 );
//printlits(begin,end); printf("\n");
values = s->assigns;
@@ -1065,7 +1077,18 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
if (j == begin) // empty clause
return false;
- else if (j - begin == 1) // unit clause
+
+ ///////////////////////////////////
+ // add clause to internal storage
+ if ( s->pStore )
+ {
+ extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+ int RetValue = Sto_ManAddClause( s->pStore, begin, j );
+ assert( RetValue );
+ }
+ ///////////////////////////////////
+
+ if (j - begin == 1) // unit clause
return enqueue(s,*begin,(clause*)0);
// create new clause
@@ -1198,6 +1221,15 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
printf("==============================================================================\n");
sat_solver_canceluntil(s,0);
+
+ ////////////////////////////////////////////////
+ if ( status == l_Undef && s->pStore )
+ {
+ extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+ int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+ assert( RetValue );
+ }
+ ////////////////////////////////////////////////
return status;
}
@@ -1220,6 +1252,51 @@ int sat_solver_nconflicts(sat_solver* s)
}
//=================================================================================================
+// Clause storage functions:
+
+void sat_solver_store_alloc( sat_solver * s )
+{
+ extern void * Sto_ManAlloc();
+ assert( s->pStore == NULL );
+ s->pStore = Sto_ManAlloc();
+}
+
+void sat_solver_store_write( sat_solver * s, char * pFileName )
+{
+ extern void Sto_ManDumpClauses( void * p, char * pFileName );
+ Sto_ManDumpClauses( s->pStore, pFileName );
+}
+
+void sat_solver_store_free( sat_solver * s )
+{
+ extern void Sto_ManFree( void * p );
+ if ( s->pStore ) Sto_ManFree( s->pStore );
+ s->pStore = NULL;
+}
+
+void sat_solver_store_mark_roots( sat_solver * s )
+{
+ extern void Sto_ManMarkRoots( void * p );
+ if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
+}
+
+void sat_solver_store_mark_clauses_a( sat_solver * s )
+{
+ extern void Sto_ManMarkClausesA( void * p );
+ if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
+}
+
+void * sat_solver_store_release( sat_solver * s )
+{
+ void * pTemp;
+ if ( s->pStore == NULL )
+ return NULL;
+ pTemp = s->pStore;
+ s->pStore = NULL;
+ return pTemp;
+}
+
+//=================================================================================================
// Sorting functions (sigh):
static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 6c05a14a..8f71370f 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -33,7 +33,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
// Simple types:
// does not work for c++
-typedef int bool;
+//typedef int bool;
+#ifndef __cplusplus
+#ifndef bool
+#define bool int
+#endif
+#endif
+
static const bool true = 1;
static const bool false = 0;
@@ -58,6 +64,8 @@ static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
static inline lit lit_neg (lit l) { return l ^ 1; }
static inline int lit_var (lit l) { return l >> 1; }
static inline int lit_sign (lit l) { return l & 1; }
+static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
//=================================================================================================
@@ -88,6 +96,21 @@ typedef struct stats_t stats;
extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
+extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar );
+
+// trace recording
+extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName );
+extern void Sat_SolverTraceStop( sat_solver * pSat );
+extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void sat_solver_store_alloc( sat_solver * s );
+extern void sat_solver_store_write( sat_solver * s, char * pFileName );
+extern void sat_solver_store_free( sat_solver * s );
+extern void sat_solver_store_mark_roots( sat_solver * s );
+extern void sat_solver_store_mark_clauses_a( sat_solver * s );
+extern void * sat_solver_store_release( sat_solver * s );
//=================================================================================================
// Solver representation:
@@ -146,6 +169,14 @@ struct sat_solver_t
int nRestarts; // the number of local restarts
Sat_MmStep_t * pMem;
+
+ // clause store
+ void * pStore;
+
+ // trace recording
+ FILE * pFile;
+ int nClauses;
+ int nRoots;
};
#endif
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
new file mode 100644
index 00000000..33cba6a7
--- /dev/null
+++ b/src/sat/bsat/satStore.c
@@ -0,0 +1,437 @@
+/**CFile****************************************************************
+
+ FileName [satStore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT 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: satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Fetches memory.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes )
+{
+ char * pMem;
+ if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
+ {
+ pMem = (char *)malloc( p->nChunkSize );
+ *(char **)pMem = p->pChunkLast;
+ p->pChunkLast = pMem;
+ p->nChunkUsed = sizeof(char *);
+ }
+ pMem = p->pChunkLast + p->nChunkUsed;
+ p->nChunkUsed += nBytes;
+ return pMem;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees memory manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sto_ManMemoryStop( Sto_Man_t * p )
+{
+ char * pMem, * pNext;
+ if ( p->pChunkLast == NULL )
+ return;
+ for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+ free( pMem );
+ free( pMem );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports memory usage in bytes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sto_ManMemoryReport( Sto_Man_t * p )
+{
+ int Total;
+ char * pMem, * pNext;
+ if ( p->pChunkLast == NULL )
+ return 0;
+ Total = p->nChunkUsed;
+ for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+ Total += p->nChunkSize;
+ return Total;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sto_Man_t * Sto_ManAlloc()
+{
+ Sto_Man_t * p;
+ // allocate the manager
+ p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
+ memset( p, 0, sizeof(Sto_Man_t) );
+ // memory management
+ p->nChunkSize = (1<<16); // use 64K chunks
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sto_ManFree( Sto_Man_t * p )
+{
+ Sto_ManMemoryStop( p );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one clause to the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd )
+{
+ Sto_Cls_t * pClause;
+ lit Lit, * i, * j;
+ int nSize;
+
+ // process the literals
+ if ( pBeg < pEnd )
+ {
+ // insertion sort
+ for ( i = pBeg + 1; i < pEnd; i++ )
+ {
+ Lit = *i;
+ for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
+ *j = *(j-1);
+ *j = Lit;
+ }
+ // make sure there is no duplicated variables
+ for ( i = pBeg + 1; i < pEnd; i++ )
+ if ( lit_var(*(i-1)) == lit_var(*i) )
+ {
+ printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
+ return 0;
+ }
+ // check the largest var size
+ p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
+ }
+
+ // get memory for the clause
+ nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
+ pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
+ memset( pClause, 0, sizeof(Sto_Cls_t) );
+
+ // assign the clause
+ pClause->Id = p->nClauses++;
+ pClause->nLits = pEnd - pBeg;
+ memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
+
+ // add the clause to the list
+ if ( p->pHead == NULL )
+ p->pHead = pClause;
+ if ( p->pTail == NULL )
+ p->pTail = pClause;
+ else
+ {
+ p->pTail->pNext = pClause;
+ p->pTail = pClause;
+ }
+
+ // add the empty clause
+ if ( pClause->nLits == 0 )
+ {
+ if ( p->pEmpty )
+ {
+ printf( "More than one empty clause!\n" );
+ return 0;
+ }
+ p->pEmpty = pClause;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Mark all clauses added so far as root clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sto_ManMarkRoots( Sto_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ p->nRoots = 0;
+ Sto_ManForEachClause( p, pClause )
+ {
+ pClause->fRoot = 1;
+ p->nRoots++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Mark all clauses added so far as clause of A.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sto_ManMarkClausesA( Sto_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ p->nClausesA = 0;
+ Sto_ManForEachClause( p, pClause )
+ {
+ pClause->fA = 1;
+ p->nClausesA++;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the stored clauses into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
+{
+ FILE * pFile;
+ Sto_Cls_t * pClause;
+ int i;
+ // start the file
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Error: Cannot open output file (%s).\n", pFileName );
+ return;
+ }
+ // write the data
+ fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
+ Sto_ManForEachClause( p, pClause )
+ {
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
+ fprintf( pFile, "\n" );
+ }
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads one literal from file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sto_ManLoadNumber( FILE * pFile, int * pNumber )
+{
+ int Char, Number = 0, Sign = 0;
+ // skip space-like chars
+ do {
+ Char = fgetc( pFile );
+ if ( Char == EOF )
+ return 0;
+ } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' );
+ // read the literal
+ while ( 1 )
+ {
+ // get the next character
+ Char = fgetc( pFile );
+ if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' )
+ break;
+ // check that the char is a digit
+ if ( (Char < '0' || Char > '9') && Char != '-' )
+ {
+ printf( "Error: Wrong char (%c) in the input file.\n", Char );
+ return 0;
+ }
+ // check if this is a minus
+ if ( Char == '-' )
+ Sign = 1;
+ else
+ Number = 10 * Number + Char;
+ }
+ // return the number
+ *pNumber = Sign? -Number : Number;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads CNF from file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
+{
+ FILE * pFile;
+ Sto_Man_t * p;
+ Sto_Cls_t * pClause;
+ char pBuffer[1024];
+ int nLits, nLitsAlloc, Counter, Number;
+ lit * pLits;
+
+ // start the file
+ pFile = fopen( pFileName, "r" );
+ if ( pFile == NULL )
+ {
+ printf( "Error: Cannot open input file (%s).\n", pFileName );
+ return NULL;
+ }
+
+ // create the manager
+ p = Sto_ManAlloc();
+
+ // alloc the array of literals
+ nLitsAlloc = 1024;
+ pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );
+
+ // read file header
+ p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
+ while ( fgets( pBuffer, 1024, pFile ) )
+ {
+ if ( pBuffer[0] == 'c' )
+ continue;
+ if ( pBuffer[0] == 'p' )
+ {
+ sscanf( pBuffer + 1, "%d %d %d %d", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
+ break;
+ }
+ printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
+ }
+
+ // read the clauses
+ nLits = 0;
+ while ( Sto_ManLoadNumber(pFile, &Number) )
+ {
+ if ( Number == 0 )
+ {
+ int RetValue;
+ RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
+ assert( RetValue );
+ nLits = 0;
+ continue;
+ }
+ if ( nLits == nLitsAlloc )
+ {
+ nLitsAlloc *= 2;
+ pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
+ }
+ pLits[ nLits++ ] = lit_read(Number);
+ }
+ if ( nLits > 0 )
+ printf( "Error: The last clause was not saved.\n" );
+
+ // count clauses
+ Counter = 0;
+ Sto_ManForEachClause( p, pClause )
+ Counter++;
+
+ // check the number of clauses
+ if ( p->nClauses != Counter )
+ {
+ printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
+ Sto_ManFree( p );
+ return NULL;
+ }
+
+ free( pLits );
+ fclose( pFile );
+ return p;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
new file mode 100644
index 00000000..3db52ada
--- /dev/null
+++ b/src/sat/bsat/satStore.h
@@ -0,0 +1,135 @@
+/**CFile****************************************************************
+
+ FileName [pr.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Proof recording.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __PR_H__
+#define __PR_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>
+*/
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#ifndef PRT
+#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+#define STO_MAX(a,b) ((a) > (b) ? (a) : (b))
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef unsigned lit;
+
+typedef struct Sto_Cls_t_ Sto_Cls_t;
+struct Sto_Cls_t_
+{
+ Sto_Cls_t * pNext; // the next clause
+ Sto_Cls_t * pNext0; // the next 0-watch
+ Sto_Cls_t * pNext1; // the next 0-watch
+ int Id; // the clause ID
+ unsigned fA : 1; // belongs to A
+ unsigned fRoot : 1; // original clause
+ unsigned fVisit : 1; // visited clause
+ unsigned nLits : 24; // the number of literals
+ lit pLits[0]; // literals of this clause
+};
+
+typedef struct Sto_Man_t_ Sto_Man_t;
+struct Sto_Man_t_
+{
+ // general data
+ int nVars; // the number of variables
+ int nRoots; // the number of root clauses
+ int nClauses; // the number of all clauses
+ int nClausesA; // the number of clauses of A
+ Sto_Cls_t * pHead; // the head clause
+ Sto_Cls_t * pTail; // the tail clause
+ Sto_Cls_t * pEmpty; // the empty clause
+ // memory management
+ int nChunkSize; // the number of bytes in a chunk
+ int nChunkUsed; // the number of bytes used in the last chunk
+ char * pChunkLast; // the last memory chunk
+};
+
+// variable/literal conversions (taken from MiniSat)
+static inline lit toLit (int v) { return v + v; }
+static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit lit_neg (lit l) { return l ^ 1; }
+static inline int lit_var (lit l) { return l >> 1; }
+static inline int lit_sign (lit l) { return l & 1; }
+static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
+
+// iterators through the clauses
+#define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext )
+#define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== satStore.c ==========================================================*/
+extern Sto_Man_t * Sto_ManAlloc();
+extern void Sto_ManFree( Sto_Man_t * p );
+extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
+extern int Sto_ManMemoryReport( Sto_Man_t * p );
+extern void Sto_ManMarkRoots( Sto_Man_t * p );
+extern void Sto_ManMarkClausesA( Sto_Man_t * p );
+
+/*=== satInter.c ==========================================================*/
+typedef struct Int_Man_t_ Int_Man_t;
+extern Int_Man_t * Int_ManAlloc( int nVarsAlloc );
+extern void Int_ManFree( Int_Man_t * p );
+extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/asat/satTrace.c b/src/sat/bsat/satTrace.c
index 3318933a..111e8dfb 100644
--- a/src/sat/asat/satTrace.c
+++ b/src/sat/bsat/satTrace.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [C-language MiniSat solver.]
+ PackageName [SAT sat_solver.]
Synopsis [Records the trace of SAT solving in the CNF form.]
@@ -20,7 +20,7 @@
#include <stdio.h>
#include <assert.h>
-#include "solver.h"
+#include "satSolver.h"
/*
The trace of SAT solving contains the original clause of the problem
@@ -33,9 +33,6 @@
/// 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 ///
@@ -52,7 +49,7 @@ static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 :
SeeAlso []
***********************************************************************/
-void Sat_SolverTraceStart( solver * pSat, char * pName )
+void Sat_SolverTraceStart( sat_solver * pSat, char * pName )
{
assert( pSat->pFile == NULL );
pSat->pFile = fopen( pName, "w" );
@@ -72,12 +69,12 @@ void Sat_SolverTraceStart( solver * pSat, char * pName )
SeeAlso []
***********************************************************************/
-void Sat_SolverTraceStop( solver * pSat )
+void Sat_SolverTraceStop( sat_solver * pSat )
{
if ( pSat->pFile == NULL )
return;
rewind( pSat->pFile );
- fprintf( pSat->pFile, "p %d %d %d", solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
+ fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
fclose( pSat->pFile );
pSat->pFile = NULL;
}
@@ -94,7 +91,7 @@ void Sat_SolverTraceStop( solver * pSat )
SeeAlso []
***********************************************************************/
-void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot )
+void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )
{
if ( pSat->pFile == NULL )
return;
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index f2b78fe6..76cb2dc2 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -153,6 +153,77 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
printf( "inspects : %d\n", (int)p->stats.inspects );
}
+/**Function*************************************************************
+
+ Synopsis [Returns a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Sat_SolverGetModel( sat_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 [Duplicates all clauses, complements unit clause of the given var.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
+{
+ clause ** pClauses;
+ lit Lit, * pLits;
+ int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
+ // get the number of variables
+ nVarsOld = p->size;
+ nLitsOld = 2 * p->size;
+ // extend the solver to depend on two sets of variables
+ sat_solver_setnvars( p, 2 * p->size );
+ // duplicate implications
+ for ( v = 0; v < nVarsOld; v++ )
+ if ( p->assigns[v] != l_Undef )
+ {
+ Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
+ if ( v == iVar )
+ Lit = lit_neg(Lit);
+ RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
+ assert( RetValue );
+ }
+ // duplicate clauses
+ nClauses = vecp_size(&p->clauses);
+ pClauses = (clause**)vecp_begin(&p->clauses);
+ for ( c = 0; c < nClauses; c++ )
+ {
+ nLits = clause_size(pClauses[c]);
+ pLits = clause_begin(pClauses[c]);
+ for ( v = 0; v < nLits; v++ )
+ pLits[v] += nLitsOld;
+ RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
+ assert( RetValue );
+ for ( v = 0; v < nLits; v++ )
+ pLits[v] -= nLitsOld;
+ }
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index e45b1b81..c7340824 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -612,7 +612,7 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
// try to prove the miter using a number of techniques
if ( mng->mode )
- RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
+ RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
else
// RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 7f15c58f..7e595390 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -27,7 +27,11 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-#include "solver.h"
+#ifdef _WIN32
+typedef signed __int64 sint64; // compatible with MS VS 6.0
+#else
+typedef long long sint64;
+#endif
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
index 4e8a3522..2d1ab2d1 100644
--- a/src/sat/proof/pr.c
+++ b/src/sat/proof/pr.c
@@ -23,7 +23,7 @@
#include <string.h>
#include <assert.h>
#include <time.h>
-#include "vec.h"
+//#include "vec.h"
#include "pr.h"
////////////////////////////////////////////////////////////////////////
@@ -150,7 +150,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
// set the starting number of variables
p->nVars = 0;
// memory management
- p->nChunkSize = (1<<18); // use 256K chunks
+ p->nChunkSize = (1<<16); // use 64K chunks
// verification
p->nResLitsAlloc = (1<<16);
p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
@@ -329,13 +329,6 @@ int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClaus
printf( "More than one empty clause!\n" );
p->pEmpty = pClause;
}
-
- // create watcher lists for the root clauses
- if ( fRoot && pClause->nLits > 1 )
- {
- Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
- Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
- }
return 1;
}
@@ -388,6 +381,29 @@ void Pr_ManMemoryStop( Pr_Man_t * p )
/**Function*************************************************************
+ Synopsis [Reports memory usage in bytes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pr_ManMemoryReport( Pr_Man_t * p )
+{
+ int Total;
+ char * pMem, * pNext;
+ if ( p->pChunkLast == NULL )
+ return 0;
+ Total = p->nChunkUsed;
+ for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+ Total += p->nChunkSize;
+ return Total;
+}
+
+/**Function*************************************************************
+
Synopsis [Records the proof.]
Description []
@@ -688,6 +704,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
Var = lit_var(p->pTrail[i]);
if ( !p->pSeens[Var] )
continue;
+ p->pSeens[Var] = 0;
// skip literals of the resulting clause
pReason = p->pReasons[Var];
@@ -695,6 +712,11 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
continue;
assert( p->pTrail[i] == pReason->pLits[0] );
+ // add the variables to seen
+ for ( v = 1; v < (int)pReason->nLits; v++ )
+ p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+
// record the reason clause
assert( pReason->pProof > 0 );
p->Counter++;
@@ -751,16 +773,15 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
}
}
- // add the variables to seen
- for ( v = 1; v < (int)pReason->nLits; v++ )
- p->pSeens[lit_var(pReason->pLits[v])] = 1;
-
// Vec_PtrPush( pFinal->pAntis, pReason );
}
// unmark all seen variables
- for ( i = p->nTrailSize - 1; i >= 0; i-- )
- p->pSeens[lit_var(p->pTrail[i])] = 0;
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// p->pSeens[lit_var(p->pTrail[i])] = 0;
+ // check that the literals are unmarked
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
// use the resulting clause to check the correctness of resolution
if ( p->fProofVerif )
@@ -904,6 +925,12 @@ int Pr_ManProcessRoots( Pr_Man_t * p )
p->nTrailSize = 0;
Pr_ManForEachClauseRoot( p, pClause )
{
+ // create watcher lists for the root clauses
+ if ( pClause->nLits > 1 )
+ {
+ Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
+ Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
+ }
// empty clause and large clauses
if ( pClause->nLits != 1 )
continue;
@@ -1218,9 +1245,10 @@ p->timeRead = clock() - clk;
1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) );
*/
- printf( "Vars = %d. Roots = %d. Learned = %d. Resolution steps = %d. Ave = %.2f.\n",
+ printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter,
- 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots) );
+ 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
+ 1.0*Pr_ManMemoryReport(p)/(1<<20) );
p->timeTotal = clock() - clkTotal;
Pr_ManFree( p );
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-06 15:08:37 +0000