diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/msat | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/sat/msat')
-rw-r--r-- | src/sat/msat/module.make | 13 | ||||
-rw-r--r-- | src/sat/msat/msat.h | 172 | ||||
-rw-r--r-- | src/sat/msat/msatActivity.c | 160 | ||||
-rw-r--r-- | src/sat/msat/msatClause.c | 529 | ||||
-rw-r--r-- | src/sat/msat/msatClauseVec.c | 232 | ||||
-rw-r--r-- | src/sat/msat/msatInt.h | 306 | ||||
-rw-r--r-- | src/sat/msat/msatMem.c | 529 | ||||
-rw-r--r-- | src/sat/msat/msatOrderH.c | 405 | ||||
-rw-r--r-- | src/sat/msat/msatOrderJ.c | 472 | ||||
-rw-r--r-- | src/sat/msat/msatQueue.c | 157 | ||||
-rw-r--r-- | src/sat/msat/msatRead.c | 268 | ||||
-rw-r--r-- | src/sat/msat/msatSolverApi.c | 500 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 212 | ||||
-rw-r--r-- | src/sat/msat/msatSolverIo.c | 177 | ||||
-rw-r--r-- | src/sat/msat/msatSolverSearch.c | 629 | ||||
-rw-r--r-- | src/sat/msat/msatSort.c | 173 | ||||
-rw-r--r-- | src/sat/msat/msatVec.c | 495 |
17 files changed, 0 insertions, 5429 deletions
diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make deleted file mode 100644 index 0dadfbe1..00000000 --- a/src/sat/msat/module.make +++ /dev/null @@ -1,13 +0,0 @@ -SRC += src/sat/msat/msatActivity.c \ - src/sat/msat/msatClause.c \ - src/sat/msat/msatClauseVec.c \ - src/sat/msat/msatMem.c \ - src/sat/msat/msatOrderJ.c \ - src/sat/msat/msatQueue.c \ - src/sat/msat/msatRead.c \ - src/sat/msat/msatSolverApi.c \ - src/sat/msat/msatSolverCore.c \ - src/sat/msat/msatSolverIo.c \ - src/sat/msat/msatSolverSearch.c \ - src/sat/msat/msatSort.c \ - src/sat/msat/msatVec.c diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h deleted file mode 100644 index 53353ba6..00000000 --- a/src/sat/msat/msat.h +++ /dev/null @@ -1,172 +0,0 @@ -/**CFile**************************************************************** - - FileName [msat.h] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [External definitions of the solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $] - -***********************************************************************/ - -#ifndef __MSAT_H__ -#define __MSAT_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#ifdef bool -#undef bool -#endif - -#ifndef __MVTYPES_H__ -typedef int bool; -#endif - -typedef struct Msat_Solver_t_ Msat_Solver_t; - -// the vector of intergers and of clauses -typedef struct Msat_IntVec_t_ Msat_IntVec_t; -typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t; -typedef struct Msat_VarHeap_t_ Msat_VarHeap_t; - -// the return value of the solver -typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; - -// representation of variables and literals -// the literal (l) is the variable (v) and the sign (s) -// s = 0 the variable is positive -// s = 1 the variable is negative -#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) -#define MSAT_LITNOT(l) ((l)^1) -#define MSAT_LITSIGN(l) ((l)&1) -#define MSAT_LIT2VAR(l) ((l)>>1) - -//////////////////////////////////////////////////////////////////////// -/// GLOBAL VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== satRead.c ============================================================*/ -extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ); -/*=== satSolver.c ===========================================================*/ -// adding vars, clauses, simplifying the database, and solving -extern bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ); -extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); -extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p ); -extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); -// printing stats, assignments, and clauses -extern void Msat_SolverPrintStats( Msat_Solver_t * p ); -extern void Msat_SolverPrintAssignment( Msat_Solver_t * p ); -extern void Msat_SolverPrintClauses( Msat_Solver_t * p ); -extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ); -// access to the solver internal data -extern int Msat_SolverReadVarNum( Msat_Solver_t * p ); -extern int Msat_SolverReadClauseNum( Msat_Solver_t * p ); -extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ); -extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ); -extern int * Msat_SolverReadModelArray( Msat_Solver_t * p ); -extern unsigned Msat_SolverReadTruth( Msat_Solver_t * p ); -extern int Msat_SolverReadBackTracks( Msat_Solver_t * p ); -extern int Msat_SolverReadInspects( Msat_Solver_t * p ); -extern void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ); -extern void Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof ); -extern void Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var ); -extern void Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap ); -extern void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ); -extern void Msat_SolverMarkClausesStart( Msat_Solver_t * p ); -extern float * Msat_SolverReadFactors( Msat_Solver_t * p ); -// returns the solution after incremental solving -extern int Msat_SolverReadSolutions( Msat_Solver_t * p ); -extern int * Msat_SolverReadSolutionsArray( Msat_Solver_t * p ); -extern Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p ); -extern Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p ); -extern Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p ); -/*=== satSolverSearch.c ===========================================================*/ -extern void Msat_SolverRemoveLearned( Msat_Solver_t * p ); -extern void Msat_SolverRemoveMarked( Msat_Solver_t * p ); -/*=== satSolverApi.c ===========================================================*/ -// allocation, cleaning, and freeing the solver -extern Msat_Solver_t * Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose ); -extern void Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc ); -extern void Msat_SolverClean( Msat_Solver_t * p, int nVars ); -extern void Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars ); -extern void Msat_SolverFree( Msat_Solver_t * p ); -/*=== satVec.c ===========================================================*/ -extern Msat_IntVec_t * Msat_IntVecAlloc( int nCap ); -extern Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ); -extern Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ); -extern Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ); -extern Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ); -extern void Msat_IntVecFree( Msat_IntVec_t * p ); -extern void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry ); -extern int * Msat_IntVecReleaseArray( Msat_IntVec_t * p ); -extern int * Msat_IntVecReadArray( Msat_IntVec_t * p ); -extern int Msat_IntVecReadSize( Msat_IntVec_t * p ); -extern int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i ); -extern int Msat_IntVecReadEntryLast( Msat_IntVec_t * p ); -extern void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry ); -extern void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ); -extern void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew ); -extern void Msat_IntVecClear( Msat_IntVec_t * p ); -extern void Msat_IntVecPush( Msat_IntVec_t * p, int Entry ); -extern int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry ); -extern void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease ); -extern int Msat_IntVecPop( Msat_IntVec_t * p ); -extern void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse ); -/*=== satHeap.c ===========================================================*/ -extern Msat_VarHeap_t * Msat_VarHeapAlloc(); -extern void Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity ); -extern void Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc ); -extern void Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize ); -extern void Msat_VarHeapStop( Msat_VarHeap_t * p ); -extern void Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p ); -extern void Msat_VarHeapCheck( Msat_VarHeap_t * p ); -extern void Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar ); -extern int Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar ); -extern void Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar ); -extern void Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar ); -extern void Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar ); -extern double Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p ); -extern int Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit ); -extern int Msat_VarHeapReadMax( Msat_VarHeap_t * p ); -extern int Msat_VarHeapGetMax( Msat_VarHeap_t * p ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c deleted file mode 100644 index 1cd795bd..00000000 --- a/src/sat/msat/msatActivity.c +++ /dev/null @@ -1,160 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatActivity.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Procedures controlling activity of variables and clauses.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatActivity.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) -{ - Msat_Var_t Var; - if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump) - return; - Var = MSAT_LIT2VAR(Lit); - p->pdActivity[Var] += p->dVarInc; -// p->pdActivity[Var] += p->dVarInc * p->pFactors[Var]; - if ( p->pdActivity[Var] > 1e100 ) - Msat_SolverVarRescaleActivity( p ); - Msat_OrderUpdate( p->pOrder, Var ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverVarDecayActivity( Msat_Solver_t * p ) -{ - if ( p->dVarDecay >= 0 ) - p->dVarInc *= p->dVarDecay; -} - -/**Function************************************************************* - - Synopsis [Divide all variable activities by 1e100.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverVarRescaleActivity( Msat_Solver_t * p ) -{ - int i; - for ( i = 0; i < p->nVars; i++ ) - p->pdActivity[i] *= 1e-100; - p->dVarInc *= 1e-100; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC ) -{ - float Activ; - Activ = Msat_ClauseReadActivity(pC); - if ( Activ + p->dClaInc > 1e20 ) - { - Msat_SolverClaRescaleActivity( p ); - Activ = Msat_ClauseReadActivity( pC ); - } - Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverClaDecayActivity( Msat_Solver_t * p ) -{ - p->dClaInc *= p->dClaDecay; -} - -/**Function************************************************************* - - Synopsis [Divide all constraint activities by 1e20.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverClaRescaleActivity( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned; - int nLearned, i; - float Activ; - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nLearned; i++ ) - { - Activ = Msat_ClauseReadActivity( pLearned[i] ); - Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 ); - } - p->dClaInc *= 1e-20; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c deleted file mode 100644 index 2ba8cd32..00000000 --- a/src/sat/msat/msatClause.c +++ /dev/null @@ -1,529 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatClause.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Procedures working with SAT clauses.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatClause.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Msat_Clause_t_ -{ - int Num; // unique number of the clause - unsigned fLearned : 1; // 1 if the clause is learned - unsigned fMark : 1; // used to mark visited clauses during proof recording - unsigned fTypeA : 1; // used to mark clauses belonging to A for interpolant computation - unsigned nSize : 14; // the number of literals in the clause - unsigned nSizeAlloc : 15; // the number of bytes allocated for the clause - Msat_Lit_t pData[0]; -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates a new clause.] - - Description [Returns FALSE if top-level conflict detected (must be handled); - TRUE otherwise. 'pClause_out' may be set to NULL if clause is already - satisfied by the top-level assignment.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out ) -{ - int * pAssigns = Msat_SolverReadAssignsArray(p); - Msat_ClauseVec_t ** pvWatched; - Msat_Clause_t * pC; - int * pLits; - int nLits, i, j; - int nBytes; - Msat_Var_t Var; - bool Sign; - - *pClause_out = NULL; - - nLits = Msat_IntVecReadSize(vLits); - pLits = Msat_IntVecReadArray(vLits); - - if ( !fLearned ) - { - int * pSeen = Msat_SolverReadSeenArray( p ); - int nSeenId; - assert( Msat_SolverReadDecisionLevel(p) == 0 ); - // sorting literals makes the code trace-equivalent - // with to the original C++ solver - Msat_IntVecSort( vLits, 0 ); - // increment the counter of seen twice - nSeenId = Msat_SolverIncrementSeenId( p ); - nSeenId = Msat_SolverIncrementSeenId( p ); - // nSeenId - 1 stands for negative - // nSeenId stands for positive - // Remove false literals - - // there is a bug here!!!! - // when the same var in opposite polarities is given, it drops one polarity!!! - - for ( i = j = 0; i < nLits; i++ ) { - // get the corresponding variable - Var = MSAT_LIT2VAR(pLits[i]); - Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive - // check if we already saw this variable in the this clause - if ( pSeen[Var] >= nSeenId - 1 ) - { - if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit - continue; - return 1; // two opposite polarity lits -- don't add the clause - } - // mark the variable as seen - pSeen[Var] = nSeenId - !Sign; - - // analize the value of this literal - if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED ) - { - if ( pAssigns[Var] == pLits[i] ) - return 1; // the clause is always true -- don't add anything - // the literal has no impact - skip it - continue; - } - // otherwise, add this literal to the clause - pLits[j++] = pLits[i]; - } - Msat_IntVecShrink( vLits, j ); - nLits = j; -/* - // the problem with this code is that performance is very - // sensitive to the ordering of adjacency lits - // the best ordering requires fanins first, next fanouts - // this ordering is more convenient to make from FRAIG - - // create the adjacency information - if ( nLits > 2 ) - { - Msat_Var_t VarI, VarJ; - Msat_IntVec_t * pAdjI, * pAdjJ; - - for ( i = 0; i < nLits; i++ ) - { - VarI = MSAT_LIT2VAR(pLits[i]); - pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI]; - - for ( j = i+1; j < nLits; j++ ) - { - VarJ = MSAT_LIT2VAR(pLits[j]); - pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ]; - - Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 ); - Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 ); - } - } - } -*/ - } - // 'vLits' is now the (possibly) reduced vector of literals. - if ( nLits == 0 ) - return 0; - if ( nLits == 1 ) - return Msat_SolverEnqueue( p, pLits[0], NULL ); - - // Allocate clause: -// nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned); - nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned); -#ifdef USE_SYSTEM_MEMORY_MANAGEMENT - pC = (Msat_Clause_t *)ALLOC( char, nBytes ); -#else - pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes ); -#endif - pC->Num = p->nClauses++; - pC->fTypeA = 0; - pC->fMark = 0; - pC->fLearned = fLearned; - pC->nSize = nLits; - pC->nSizeAlloc = nBytes; - memcpy( pC->pData, pLits, sizeof(int)*nLits ); - - // For learnt clauses only: - if ( fLearned ) - { - int * pLevel = Msat_SolverReadDecisionLevelArray( p ); - int iLevelMax, iLevelCur, iLitMax; - - // Put the second watch on the literal with highest decision level: - iLitMax = 1; - iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ]; - for ( i = 2; i < nLits; i++ ) - { - iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ]; - assert( iLevelCur != -1 ); - if ( iLevelMax < iLevelCur ) - // this is very strange - shouldn't it be??? - // if ( iLevelMax > iLevelCur ) - iLevelMax = iLevelCur, iLitMax = i; - } - pC->pData[1] = pLits[iLitMax]; - pC->pData[iLitMax] = pLits[1]; - - // Bumping: - // (newly learnt clauses should be considered active) - Msat_ClauseWriteActivity( pC, 0.0 ); - Msat_SolverClaBumpActivity( p, pC ); -// if ( nLits < 20 ) - for ( i = 0; i < nLits; i++ ) - { - Msat_SolverVarBumpActivity( p, pLits[i] ); -// Msat_SolverVarBumpActivity( p, pLits[i] ); -// p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; - } - } - - // Store clause: - pvWatched = Msat_SolverReadWatchedArray( p ); - Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC ); - Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC ); - *pClause_out = pC; - return 1; -} - -/**Function************************************************************* - - Synopsis [Deallocates the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ) -{ - if ( fRemoveWatched ) - { - Msat_Lit_t Lit; - Msat_ClauseVec_t ** pvWatched; - pvWatched = Msat_SolverReadWatchedArray( p ); - Lit = MSAT_LITNOT( pC->pData[0] ); - Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); - Lit = MSAT_LITNOT( pC->pData[1] ); - Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); - } - -#ifdef USE_SYSTEM_MEMORY_MANAGEMENT - free( pC ); -#else - Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc ); -#endif - -} - -/**Function************************************************************* - - Synopsis [Access the data field of the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_ClauseReadLearned( Msat_Clause_t * pC ) { return pC->fLearned; } -int Msat_ClauseReadSize( Msat_Clause_t * pC ) { return pC->nSize; } -int * Msat_ClauseReadLits( Msat_Clause_t * pC ) { return pC->pData; } -bool Msat_ClauseReadMark( Msat_Clause_t * pC ) { return pC->fMark; } -int Msat_ClauseReadNum( Msat_Clause_t * pC ) { return pC->Num; } -bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ) { return pC->fTypeA; } - -void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ) { pC->fMark = fMark; } -void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ) { pC->Num = Num; } -void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) { pC->fTypeA = fTypeA; } - -/**Function************************************************************* - - Synopsis [Checks whether the learned clause is locked.] - - Description [The clause may be locked if it is the reason of a - recent conflict. Such clause cannot be removed from the database.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ) -{ - Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p ); - return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC); -} - -/**Function************************************************************* - - Synopsis [Reads the activity of the given clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float Msat_ClauseReadActivity( Msat_Clause_t * pC ) -{ - return *((float *)(pC->pData + pC->nSize)); -} - -/**Function************************************************************* - - Synopsis [Sets the activity of the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ) -{ - *((float *)(pC->pData + pC->nSize)) = Num; -} - -/**Function************************************************************* - - Synopsis [Propages the assignment.] - - Description [The literal that has become true (Lit) is given to this - procedure. The array of current variable assignments is given for - efficiency. The output literal (pLit_out) can be the second watched - literal (if TRUE is returned) or the conflict literal (if FALSE is - returned). This messy interface is used to improve performance. - This procedure accounts for ~50% of the runtime of the solver.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ) -{ - // make sure the false literal is pC->pData[1] - Msat_Lit_t LitF = MSAT_LITNOT(Lit); - if ( pC->pData[0] == LitF ) - pC->pData[0] = pC->pData[1], pC->pData[1] = LitF; - assert( pC->pData[1] == LitF ); - // if the 0-th watch is true, clause is already satisfied - if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] ) - return 1; - // look for a new watch - if ( pC->nSize > 2 ) - { - int i; - for ( i = 2; i < (int)pC->nSize; i++ ) - if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) ) - { - pC->pData[1] = pC->pData[i], pC->pData[i] = LitF; - *pLit_out = MSAT_LITNOT(pC->pData[1]); - return 1; - } - } - // clause is unit under assignment - *pLit_out = pC->pData[0]; - return 0; -} - -/**Function************************************************************* - - Synopsis [Simplifies the clause.] - - Description [Assumes everything has been propagated! (esp. watches - in clauses are NOT unsatisfied)] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ) -{ - Msat_Var_t Var; - int i, j; - for ( i = j = 0; i < (int)pC->nSize; i++ ) - { - Var = MSAT_LIT2VAR(pC->pData[i]); - if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED ) - { - pC->pData[j++] = pC->pData[i]; - continue; - } - if ( pAssigns[Var] == pC->pData[i] ) - return 1; - // otherwise, the value of the literal is false - // make sure, this literal is not watched - assert( i >= 2 ); - } - // if the size has changed, update it and move activity - if ( j < (int)pC->nSize ) - { - float Activ = Msat_ClauseReadActivity(pC); - pC->nSize = j; - Msat_ClauseWriteActivity(pC, Activ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Computes reason of conflict in the given clause.] - - Description [If the literal is unassigned, finds the reason by - complementing literals in the given cluase (pC). If the literal is - assigned, makes sure that this literal is the first one in the clause - and computes the complement of all other literals in the clause. - Returns the reason in the given array (vLits_out). If the clause is - learned, bumps its activity.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ) -{ - int i; - // clear the reason - Msat_IntVecClear( vLits_out ); - assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] ); - for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ ) - { - assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) ); - Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) ); - } - if ( pC->fLearned ) - Msat_SolverClaBumpActivity( p, pC ); -} - -/**Function************************************************************* - - Synopsis [Removes the given clause from the watched list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ) -{ - Msat_Clause_t ** pClauses; - int nClauses, i; - nClauses = Msat_ClauseVecReadSize( vClauses ); - pClauses = Msat_ClauseVecReadArray( vClauses ); - for ( i = 0; pClauses[i] != pC; i++ ) - assert( i < nClauses ); - for ( ; i < nClauses - 1; i++ ) - pClauses[i] = pClauses[i+1]; - Msat_ClauseVecPop( vClauses ); -} - -/**Function************************************************************* - - Synopsis [Prints the given clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClausePrint( Msat_Clause_t * pC ) -{ - int i; - if ( pC == NULL ) - printf( "NULL pointer" ); - else - { - if ( pC->fLearned ) - printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); - for ( i = 0; i < (int)pC->nSize; i++ ) - printf( " %s%d", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + 1 ); - } - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ) -{ - int i; - for ( i = 0; i < (int)pC->nSize; i++ ) - fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + (int)(fIncrement>0) ); - if ( fIncrement ) - fprintf( pFile, "0" ); - fprintf( pFile, "\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints the given clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClausePrintSymbols( Msat_Clause_t * pC ) -{ - int i; - if ( pC == NULL ) - printf( "NULL pointer" ); - else - { -// if ( pC->fLearned ) -// printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); - for ( i = 0; i < (int)pC->nSize; i++ ) - printf(" "L_LIT, L_lit(pC->pData[i])); - } - printf( "\n" ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c deleted file mode 100644 index 04691cf2..00000000 --- a/src/sat/msat/msatClauseVec.c +++ /dev/null @@ -1,232 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatClauseVec.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Procedures working with arrays of SAT clauses.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates a vector with the given capacity.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) -{ - Msat_ClauseVec_t * p; - p = ALLOC( Msat_ClauseVec_t, 1 ); - if ( nCap > 0 && nCap < 16 ) - nCap = 16; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecFree( Msat_ClauseVec_t * p ) -{ - FREE( p->pArray ); - FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p ) -{ - return p->pArray; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p ) -{ - return p->nSize; -} - -/**Function************************************************************* - - Synopsis [Resizes the vector to the given capacity.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); - p->nCap = nCapMin; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew ) -{ - assert( p->nSize >= nSizeNew ); - p->nSize = nSizeNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecClear( Msat_ClauseVec_t * p ) -{ - p->nSize = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry ) -{ - if ( p->nSize == p->nCap ) - { - if ( p->nCap < 16 ) - Msat_ClauseVecGrow( p, 16 ); - else - Msat_ClauseVecGrow( p, 2 * p->nCap ); - } - p->pArray[p->nSize++] = Entry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p ) -{ - return p->pArray[--p->nSize]; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry ) -{ - assert( i >= 0 && i < p->nSize ); - p->pArray[i] = Entry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray[i]; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h deleted file mode 100644 index 03903abe..00000000 --- a/src/sat/msat/msatInt.h +++ /dev/null @@ -1,306 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatInt.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Internal definitions of the solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __MSAT_INT_H__ -#define __MSAT_INT_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//#include "leaks.h" -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> -#include <time.h> -#include <math.h> -#include "msat.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#ifdef _MSC_VER -typedef __int64 int64; -#else -typedef long long int64; -#endif - -// outputs the runtime in seconds -#define PRT(a,t) \ - printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) - -// memory management macros -#define ALLOC(type, num) \ - ((type *) malloc(sizeof(type) * (num))) -#define REALLOC(type, obj, num) \ - ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ - ((type *) malloc(sizeof(type) * (num)))) -#define FREE(obj) \ - ((obj) ? (free((char *)(obj)), (obj) = 0) : 0) - -// By default, custom memory management is used -// which guarantees constant time allocation/deallocation -// for SAT clauses and other frequently modified objects. -// For debugging, it is possible use system memory management -// directly. In which case, uncomment the macro below. -//#define USE_SYSTEM_MEMORY_MANAGEMENT - -// internal data structures -typedef struct Msat_Clause_t_ Msat_Clause_t; -typedef struct Msat_Queue_t_ Msat_Queue_t; -typedef struct Msat_Order_t_ Msat_Order_t; -// memory managers (duplicated from Extra for stand-aloneness) -typedef struct Msat_MmFixed_t_ Msat_MmFixed_t; -typedef struct Msat_MmFlex_t_ Msat_MmFlex_t; -typedef struct Msat_MmStep_t_ Msat_MmStep_t; -// variables and literals -typedef int Msat_Lit_t; -typedef int Msat_Var_t; -// the type of return value -#define MSAT_VAR_UNASSIGNED (-1) -#define MSAT_LIT_UNASSIGNED (-2) -#define MSAT_ORDER_UNKNOWN (-3) - -// printing the search tree -#define L_IND "%-*d" -#define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p) -#define L_LIT "%s%d" -#define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1 - -typedef struct Msat_SolverStats_t_ Msat_SolverStats_t; -struct Msat_SolverStats_t_ -{ - int64 nStarts; // the number of restarts - int64 nDecisions; // the number of decisions - int64 nPropagations; // the number of implications - int64 nInspects; // the number of times clauses are vising while watching them - int64 nConflicts; // the number of conflicts - int64 nSuccesses; // the number of sat assignments found -}; - -typedef struct Msat_SearchParams_t_ Msat_SearchParams_t; -struct Msat_SearchParams_t_ -{ - double dVarDecay; - double dClaDecay; -}; - -// sat solver data structure visible through all the internal files -struct Msat_Solver_t_ -{ - int nClauses; // the total number of clauses - int nClausesStart; // the number of clauses before adding - Msat_ClauseVec_t * vClauses; // problem clauses - Msat_ClauseVec_t * vLearned; // learned clauses - double dClaInc; // Amount to bump next clause with. - double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. - - double * pdActivity; // A heuristic measurement of the activity of a variable. - float * pFactors; // the multiplicative factors of variable activity - double dVarInc; // Amount to bump next variable with. - double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. - Msat_Order_t * pOrder; // Keeps track of the decision variable order. - - Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). - Msat_Queue_t * pQueue; // Propagation queue. - - int nVars; // the current number of variables - int nVarsAlloc; // the maximum allowed number of variables - int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN) - int * pModel; // The satisfying assignment - Msat_IntVec_t * vTrail; // List of assignments made. - Msat_IntVec_t * vTrailLim; // Separator indices for different decision levels in 'trail'. - Msat_Clause_t ** pReasons; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. - int * pLevel; // 'level[var]' is the decision level at which assignment was made. - int nLevelRoot; // Level of first proper decision. - - double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms). - - bool fVerbose; // the verbosity flag - double dProgress; // Set by 'search()'. - - // the variable cone and variable connectivity - Msat_IntVec_t * vConeVars; - Msat_IntVec_t * vVarsUsed; - Msat_ClauseVec_t * vAdjacents; - - // internal data used during conflict analysis - int * pSeen; // time when a lit was seen for the last time - int nSeenId; // the id of current seeing - Msat_IntVec_t * vReason; // the temporary array of literals - Msat_IntVec_t * vTemp; // the temporary array of literals - int * pFreq; // the number of times each var participated in conflicts - - // the memory manager - Msat_MmStep_t * pMem; - - // statistics - Msat_SolverStats_t Stats; - int nTwoLits; - int nTwoLitsL; - int nClausesInit; - int nClausesAlloc; - int nClausesAllocL; - int nBackTracks; -}; - -struct Msat_ClauseVec_t_ -{ - Msat_Clause_t ** pArray; - int nSize; - int nCap; -}; - -struct Msat_IntVec_t_ -{ - int * pArray; - int nSize; - int nCap; -}; - -//////////////////////////////////////////////////////////////////////// -/// GLOBAL VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== satActivity.c ===========================================================*/ -extern void Msat_SolverVarDecayActivity( Msat_Solver_t * p ); -extern void Msat_SolverVarRescaleActivity( Msat_Solver_t * p ); -extern void Msat_SolverClaDecayActivity( Msat_Solver_t * p ); -extern void Msat_SolverClaRescaleActivity( Msat_Solver_t * p ); -/*=== satSolverApi.c ===========================================================*/ -extern Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num ); -/*=== satSolver.c ===========================================================*/ -extern int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ); -extern int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ); -extern Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ); -extern Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ); -extern Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ); -extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ); -extern int * Msat_SolverReadSeenArray( Msat_Solver_t * p ); -extern int Msat_SolverIncrementSeenId( Msat_Solver_t * p ); -extern Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ); -extern void Msat_SolverClausesIncrement( Msat_Solver_t * p ); -extern void Msat_SolverClausesDecrement( Msat_Solver_t * p ); -extern void Msat_SolverClausesIncrementL( Msat_Solver_t * p ); -extern void Msat_SolverClausesDecrementL( Msat_Solver_t * p ); -extern void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ); -extern void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC ); -extern bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ); -extern double Msat_SolverProgressEstimate( Msat_Solver_t * p ); -/*=== satSolverSearch.c ===========================================================*/ -extern bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ); -extern Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ); -extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ); -extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ); -/*=== satQueue.c ===========================================================*/ -extern Msat_Queue_t * Msat_QueueAlloc( int nVars ); -extern void Msat_QueueFree( Msat_Queue_t * p ); -extern int Msat_QueueReadSize( Msat_Queue_t * p ); -extern void Msat_QueueInsert( Msat_Queue_t * p, int Lit ); -extern int Msat_QueueExtract( Msat_Queue_t * p ); -extern void Msat_QueueClear( Msat_Queue_t * p ); -/*=== satOrder.c ===========================================================*/ -extern Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ); -extern void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ); -extern void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ); -extern int Msat_OrderCheck( Msat_Order_t * p ); -extern void Msat_OrderFree( Msat_Order_t * p ); -extern int Msat_OrderVarSelect( Msat_Order_t * p ); -extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ); -extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ); -extern void Msat_OrderUpdate( Msat_Order_t * p, int Var ); -/*=== satClause.c ===========================================================*/ -extern bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out ); -extern Msat_Clause_t * Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits ); -extern Msat_Clause_t * Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit ); -extern bool Msat_ClauseReadLearned( Msat_Clause_t * pC ); -extern int Msat_ClauseReadSize( Msat_Clause_t * pC ); -extern int * Msat_ClauseReadLits( Msat_Clause_t * pC ); -extern bool Msat_ClauseReadMark( Msat_Clause_t * pC ); -extern void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ); -extern int Msat_ClauseReadNum( Msat_Clause_t * pC ); -extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ); -extern bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ); -extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ); -extern bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ); -extern float Msat_ClauseReadActivity( Msat_Clause_t * pC ); -extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ); -extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ); -extern bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); -extern bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ); -extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ); -extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ); -extern void Msat_ClausePrint( Msat_Clause_t * pC ); -extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC ); -extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ); -extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC ); -/*=== satSort.c ===========================================================*/ -extern void Msat_SolverSortDB( Msat_Solver_t * p ); -/*=== satClauseVec.c ===========================================================*/ -extern Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ); -extern void Msat_ClauseVecFree( Msat_ClauseVec_t * p ); -extern Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p ); -extern int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p ); -extern void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ); -extern void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew ); -extern void Msat_ClauseVecClear( Msat_ClauseVec_t * p ); -extern void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry ); -extern Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p ); -extern void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry ); -extern Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ); - -/*=== satMem.c ===========================================================*/ -// fixed-size-block memory manager -extern Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ); -extern void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose ); -extern char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ); -extern void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ); -extern void Msat_MmFixedRestart( Msat_MmFixed_t * p ); -extern int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p ); -// flexible-size-block memory manager -extern Msat_MmFlex_t * Msat_MmFlexStart(); -extern void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ); -extern char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ); -extern int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p ); -// hierarchical memory manager -extern Msat_MmStep_t * Msat_MmStepStart( int nSteps ); -extern void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ); -extern char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes ); -extern void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ); -extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c deleted file mode 100644 index 30bf4a96..00000000 --- a/src/sat/msat/msatMem.c +++ /dev/null @@ -1,529 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatMem.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Memory managers borrowed from Extra.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Msat_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 Msat_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 Msat_MmStep_t_ -{ - int nMems; // the number of fixed memory managers employed - Msat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc - int nMapSize; // the size of the memory array - Msat_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 [] - -***********************************************************************/ -Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ) -{ - Msat_MmFixed_t * p; - - p = ALLOC( Msat_MmFixed_t, 1 ); - memset( p, 0, sizeof(Msat_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 Msat_MmFixedStop( Msat_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 * Msat_MmFixedEntryFetch( Msat_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 Msat_MmFixedEntryRecycle( Msat_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 Msat_MmFixedRestart( Msat_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 Msat_MmFixedReadMemUsage( Msat_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 [] - -***********************************************************************/ -Msat_MmFlex_t * Msat_MmFlexStart() -{ - Msat_MmFlex_t * p; - - p = ALLOC( Msat_MmFlex_t, 1 ); - memset( p, 0, sizeof(Msat_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 Msat_MmFlexStop( Msat_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 * Msat_MmFlexEntryFetch( Msat_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 Msat_MmFlexReadMemUsage( Msat_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 [] - -***********************************************************************/ -Msat_MmStep_t * Msat_MmStepStart( int nSteps ) -{ - Msat_MmStep_t * p; - int i, k; - p = ALLOC( Msat_MmStep_t, 1 ); - p->nMems = nSteps; - // start the fixed memory managers - p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems ); - for ( i = 0; i < p->nMems; i++ ) - p->pMems[i] = Msat_MmFixedStart( (8<<i) ); - // set up the mapping of the required memory size into the corresponding manager - p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Msat_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 Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ) -{ - int i; - for ( i = 0; i < p->nMems; i++ ) - Msat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Creates the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Msat_MmStepEntryFetch( Msat_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 Msat_MmFixedEntryFetch( p->pMap[nBytes] ); -} - - -/**Function************************************************************* - - Synopsis [Recycles the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ) -{ - if ( nBytes == 0 ) - return; - if ( nBytes > p->nMapSize ) - { - free( pEntry ); - return; - } - Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_MmStepReadMemUsage( Msat_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/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c deleted file mode 100644 index 956e7fc6..00000000 --- a/src/sat/msat/msatOrderH.c +++ /dev/null @@ -1,405 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatOrder.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The manager of variable assignment.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// the variable package data structure -struct Msat_Order_t_ -{ - Msat_Solver_t * pSat; // the SAT solver - Msat_IntVec_t * vIndex; // the heap - Msat_IntVec_t * vHeap; // the mapping of var num into its heap num -}; - -//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 (pSat->vConeVars) -//- the array of arrays of variables adjucent to each(pSat->vAdjacents) - -#define HLEFT(i) ((i)<<1) -#define HRIGHT(i) (((i)<<1)+1) -#define HPARENT(i) ((i)>>1) -#define HCOMPARE(p, i, j) ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j]) -#define HHEAP(p, i) ((p)->vHeap->pArray[i]) -#define HSIZE(p) ((p)->vHeap->nSize) -#define HOKAY(p, i) ((i) >= 0 && (i) < (p)->vIndex->nSize) -#define HINHEAP(p, i) (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0) -#define HEMPTY(p) (HSIZE(p) == 1) - -static int Msat_HeapCheck_rec( Msat_Order_t * p, int i ); -static int Msat_HeapGetTop( Msat_Order_t * p ); -static void Msat_HeapInsert( Msat_Order_t * p, int n ); -static void Msat_HeapIncrease( Msat_Order_t * p, int n ); -static void Msat_HeapPercolateUp( Msat_Order_t * p, int i ); -static void Msat_HeapPercolateDown( Msat_Order_t * p, int i ); - -extern int timeSelect; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) -{ - Msat_Order_t * p; - p = ALLOC( Msat_Order_t, 1 ); - memset( p, 0, sizeof(Msat_Order_t) ); - p->pSat = pSat; - p->vIndex = Msat_IntVecAlloc( 0 ); - p->vHeap = Msat_IntVecAlloc( 0 ); - Msat_OrderSetBounds( p, pSat->nVarsAlloc ); - return p; -} - -/**Function************************************************************* - - Synopsis [Sets the bound of the ordering structure.] - - Description [Should be called whenever the SAT solver is resized.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ) -{ - Msat_IntVecGrow( p->vIndex, nVarsMax ); - Msat_IntVecGrow( p->vHeap, nVarsMax + 1 ); - p->vIndex->nSize = nVarsMax; - p->vHeap->nSize = 0; -} - -/**Function************************************************************* - - Synopsis [Cleans the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ) -{ - int i; - for ( i = 0; i < p->vIndex->nSize; i++ ) - p->vIndex->pArray[i] = 0; - for ( i = 0; i < vCone->nSize; i++ ) - { - assert( i+1 < p->vHeap->nCap ); - p->vHeap->pArray[i+1] = vCone->pArray[i]; - - assert( vCone->pArray[i] < p->vIndex->nSize ); - p->vIndex->pArray[vCone->pArray[i]] = i+1; - } - p->vHeap->nSize = vCone->nSize + 1; -} - -/**Function************************************************************* - - Synopsis [Checks that the J-boundary is okay.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderCheck( Msat_Order_t * p ) -{ - return Msat_HeapCheck_rec( p, 1 ); -} - -/**Function************************************************************* - - Synopsis [Frees the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderFree( Msat_Order_t * p ) -{ - Msat_IntVecFree( p->vHeap ); - Msat_IntVecFree( p->vIndex ); - free( p ); -} - - - -/**Function************************************************************* - - Synopsis [Selects the next variable to assign.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderVarSelect( Msat_Order_t * p ) -{ - // Activity based decision: -// while (!heap.empty()){ -// Var next = heap.getmin(); -// if (toLbool(assigns[next]) == l_Undef) -// return next; -// } -// return var_Undef; - - int Var; - int clk = clock(); - - while ( !HEMPTY(p) ) - { - Var = Msat_HeapGetTop(p); - if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED ) - { -//assert( Msat_OrderCheck(p) ); -timeSelect += clock() - clk; - return Var; - } - } - return MSAT_ORDER_UNKNOWN; -} - -/**Function************************************************************* - - Synopsis [Updates J-boundary when the variable is assigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) -{ -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable is unassigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) -{ -// if (!heap.inHeap(x)) -// heap.insert(x); - - int clk = clock(); - if ( !HINHEAP(p,Var) ) - Msat_HeapInsert( p, Var ); -timeSelect += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable changed weight.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderUpdate( Msat_Order_t * p, int Var ) -{ -// if (heap.inHeap(x)) -// heap.increase(x); - - int clk = clock(); - if ( HINHEAP(p,Var) ) - Msat_HeapIncrease( p, Var ); -timeSelect += clock() - clk; -} - - - - -/**Function************************************************************* - - Synopsis [Checks the heap property recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_HeapCheck_rec( Msat_Order_t * p, int i ) -{ - return i >= HSIZE(p) || - ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) && - Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) ); -} - -/**Function************************************************************* - - Synopsis [Retrieves the minimum element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_HeapGetTop( Msat_Order_t * p ) -{ - int Result, NewTop; - Result = HHEAP(p, 1); - NewTop = Msat_IntVecPop( p->vHeap ); - p->vHeap->pArray[1] = NewTop; - p->vIndex->pArray[NewTop] = 1; - p->vIndex->pArray[Result] = 0; - if ( p->vHeap->nSize > 1 ) - Msat_HeapPercolateDown( p, 1 ); - return Result; -} - -/**Function************************************************************* - - Synopsis [Inserts the new element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapInsert( Msat_Order_t * p, int n ) -{ - assert( HOKAY(p, n) ); - p->vIndex->pArray[n] = HSIZE(p); - Msat_IntVecPush( p->vHeap, n ); - Msat_HeapPercolateUp( p, p->vIndex->pArray[n] ); -} - -/**Function************************************************************* - - Synopsis [Inserts the new element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapIncrease( Msat_Order_t * p, int n ) -{ - Msat_HeapPercolateUp( p, p->vIndex->pArray[n] ); -} - -/**Function************************************************************* - - Synopsis [Moves the entry up.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapPercolateUp( Msat_Order_t * p, int i ) -{ - int x = HHEAP(p, i); - while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) ) - { - p->vHeap->pArray[i] = HHEAP(p, HPARENT(i)); - p->vIndex->pArray[HHEAP(p, i)] = i; - i = HPARENT(i); - } - p->vHeap->pArray[i] = x; - p->vIndex->pArray[x] = i; -} - -/**Function************************************************************* - - Synopsis [Moves the entry down.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapPercolateDown( Msat_Order_t * p, int i ) -{ - int x = HHEAP(p, i); - int Child; - while ( HLEFT(i) < HSIZE(p) ) - { - if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) ) - Child = HRIGHT(i); - else - Child = HLEFT(i); - if ( !HCOMPARE(p, HHEAP(p, Child), x) ) - break; - p->vHeap->pArray[i] = HHEAP(p, Child); - p->vIndex->pArray[HHEAP(p, i)] = i; - i = Child; - } - p->vHeap->pArray[i] = x; - p->vIndex->pArray[x] = i; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c deleted file mode 100644 index 4db7ff7b..00000000 --- a/src/sat/msat/msatOrderJ.c +++ /dev/null @@ -1,472 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatOrder.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The manager of variable assignment.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -/* -The J-boundary (justification boundary) is defined as a set of unassigned -variables belonging to the cone of interest, such that for each of them, -there exist an adjacent assigned variable in the cone of interest. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Msat_OrderVar_t_ Msat_OrderVar_t; -typedef struct Msat_OrderRing_t_ Msat_OrderRing_t; - -// the variable data structure -struct Msat_OrderVar_t_ -{ - Msat_OrderVar_t * pNext; - Msat_OrderVar_t * pPrev; - int Num; -}; - -// the ring of variables data structure (J-boundary) -struct Msat_OrderRing_t_ -{ - Msat_OrderVar_t * pRoot; - int nItems; -}; - -// the variable package data structure -struct Msat_Order_t_ -{ - Msat_Solver_t * pSat; // the SAT solver - Msat_OrderVar_t * pVars; // the storage for variables - int nVarsAlloc; // the number of variables allocated - Msat_OrderRing_t rVars; // the J-boundary as a ring of variables -}; - -//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 (pSat->vConeVars) -//- the array of arrays of variables adjucent to each(pSat->vAdjacents) - -#define Msat_OrderVarIsInBoundary( p, i ) ((p)->pVars[i].pNext) -#define Msat_OrderVarIsAssigned( p, i ) ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED) -#define Msat_OrderVarIsUsedInCone( p, i ) ((p)->pSat->vVarsUsed->pArray[i]) - -// iterator through the entries in J-boundary -#define Msat_OrderRingForEachEntry( pRing, pVar, pNext ) \ - for ( pVar = pRing, \ - pNext = pVar? pVar->pNext : NULL; \ - pVar; \ - pVar = (pNext != pRing)? pNext : NULL, \ - pNext = pVar? pVar->pNext : NULL ) - -static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); -static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); - -extern int timeSelect; -extern int timeAssign; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) -{ - Msat_Order_t * p; - p = ALLOC( Msat_Order_t, 1 ); - memset( p, 0, sizeof(Msat_Order_t) ); - p->pSat = pSat; - Msat_OrderSetBounds( p, pSat->nVarsAlloc ); - return p; -} - -/**Function************************************************************* - - Synopsis [Sets the bound of the ordering structure.] - - Description [Should be called whenever the SAT solver is resized.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ) -{ - int i; - // add variables if they are missing - if ( p->nVarsAlloc < nVarsMax ) - { - p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax ); - for ( i = p->nVarsAlloc; i < nVarsMax; i++ ) - { - p->pVars[i].pNext = p->pVars[i].pPrev = NULL; - p->pVars[i].Num = i; - } - p->nVarsAlloc = nVarsMax; - } -} - -/**Function************************************************************* - - Synopsis [Cleans the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ) -{ - Msat_OrderVar_t * pVar, * pNext; - // quickly undo the ring - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - pVar->pNext = pVar->pPrev = NULL; - p->rVars.pRoot = NULL; - p->rVars.nItems = 0; -} - -/**Function************************************************************* - - Synopsis [Checks that the J-boundary is okay.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderCheck( Msat_Order_t * p ) -{ - Msat_OrderVar_t * pVar, * pNext; - Msat_IntVec_t * vRound; - int * pRound, nRound; - int * pVars, nVars, i, k; - int Counter = 0; - - // go through all the variables in the boundary - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - { - assert( !Msat_OrderVarIsAssigned(p, pVar->Num) ); - // 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++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, pRound[i]) ) - break; - } -// assert( i != nRound ); -// if ( i == nRound ) -// return 0; - if ( i == nRound ) - 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++ ) - { - assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) ); - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Msat_OrderVarIsAssigned(p, pVars[i]) || - Msat_OrderVarIsInBoundary(p, pVars[i]) ) - 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 ( k = 0; k < nRound; k++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, pRound[k]) ) - break; - } -// assert( k == nRound ); -// if ( k != nRound ) -// return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Frees the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderFree( Msat_Order_t * p ) -{ - free( p->pVars ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Selects the next variable to assign.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderVarSelect( Msat_Order_t * p ) -{ - Msat_OrderVar_t * pVar, * pNext, * pVarBest; - double * pdActs = p->pSat->pdActivity; - double dfActBest; -// int clk = clock(); - - pVarBest = NULL; - dfActBest = -1.0; - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - { - if ( dfActBest < pdActs[pVar->Num] ) - { - dfActBest = pdActs[pVar->Num]; - pVarBest = pVar; - } - } -//timeSelect += clock() - clk; -//timeAssign += clock() - clk; - -//if ( pVarBest && pVarBest->Num % 1000 == 0 ) -//printf( "%d ", p->rVars.nItems ); - -// Msat_OrderCheck( p ); - if ( pVarBest ) - { - assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) ); - return pVarBest->Num; - } - return MSAT_ORDER_UNKNOWN; -} - -/**Function************************************************************* - - Synopsis [Updates J-boundary when the variable is assigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) -{ - Msat_IntVec_t * vRound; - int i;//, clk = clock(); - - // make sure the variable is in the boundary - assert( Var < p->nVarsAlloc ); - // if it is not in the boundary (initial decision, random decision), do not remove - if ( Msat_OrderVarIsInBoundary( p, Var ) ) - Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] ); - // 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++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) - continue; - if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) - continue; - Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -//timeSelect += clock() - clk; -// Msat_OrderCheck( p ); -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable is unassigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) -{ - Msat_IntVec_t * vRound, * vRound2; - int i, k;//, clk = clock(); - - // make sure the variable is not in the boundary - assert( Var < p->nVarsAlloc ); - assert( !Msat_OrderVarIsInBoundary( p, Var ) ); - // 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 ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) - break; - if ( i != vRound->nSize ) - Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] ); - - // unassigning a variable may lead to its adjacents dropping from the boundary - for ( i = 0; i < vRound->nSize; i++ ) - if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) - { // the neighbor is in the J-boundary (and unassigned) - assert( !Msat_OrderVarIsAssigned(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 ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) - break; - if ( k == vRound2->nSize ) // there is no assigned vars, delete this one - Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -//timeSelect += clock() - clk; -// Msat_OrderCheck( p ); -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable changed weight.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderUpdate( Msat_Order_t * p, int Var ) -{ -} - - -/**Function************************************************************* - - Synopsis [Adds node to the end of the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) -{ -//printf( "adding %d\n", pVar->Num ); - // check that the node is not in a ring - assert( pVar->pPrev == NULL ); - assert( pVar->pNext == NULL ); - // if the ring is empty, make the node point to itself - pRing->nItems++; - if ( pRing->pRoot == NULL ) - { - pRing->pRoot = pVar; - pVar->pPrev = pVar; - pVar->pNext = pVar; - return; - } - // if the ring is not empty, add it as the last entry - pVar->pPrev = pRing->pRoot->pPrev; - pVar->pNext = pRing->pRoot; - pVar->pPrev->pNext = pVar; - pVar->pNext->pPrev = pVar; - - // move the root so that it points to the new entry -// pRing->pRoot = pRing->pRoot->pPrev; -} - -/**Function************************************************************* - - Synopsis [Removes the node from the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) -{ -//printf( "removing %d\n", pVar->Num ); - // check that the var is in a ring - assert( pVar->pPrev ); - assert( pVar->pNext ); - pRing->nItems--; - if ( pRing->nItems == 0 ) - { - assert( pRing->pRoot == pVar ); - pVar->pPrev = NULL; - pVar->pNext = NULL; - pRing->pRoot = NULL; - return; - } - // move the root if needed - if ( pRing->pRoot == pVar ) - pRing->pRoot = pVar->pNext; - // move the root to the next entry after pVar - // this way all the additions to the list will be traversed first -// pRing->pRoot = pVar->pPrev; - // delete the node - pVar->pPrev->pNext = pVar->pNext; - pVar->pNext->pPrev = pVar->pPrev; - pVar->pPrev = NULL; - pVar->pNext = NULL; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c deleted file mode 100644 index 5938e042..00000000 --- a/src/sat/msat/msatQueue.c +++ /dev/null @@ -1,157 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatQueue.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The manager of the assignment propagation queue.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatQueue.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Msat_Queue_t_ -{ - int nVars; - int * pVars; - int iFirst; - int iLast; -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the variable propagation queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Queue_t * Msat_QueueAlloc( int nVars ) -{ - Msat_Queue_t * p; - p = ALLOC( Msat_Queue_t, 1 ); - memset( p, 0, sizeof(Msat_Queue_t) ); - p->nVars = nVars; - p->pVars = ALLOC( int, nVars ); - return p; -} - -/**Function************************************************************* - - Synopsis [Deallocate the variable propagation queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_QueueFree( Msat_Queue_t * p ) -{ - free( p->pVars ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Reads the queue size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_QueueReadSize( Msat_Queue_t * p ) -{ - return p->iLast - p->iFirst; -} - -/**Function************************************************************* - - Synopsis [Insert an entry into the queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_QueueInsert( Msat_Queue_t * p, int Lit ) -{ - if ( p->iLast == p->nVars ) - { - int i; - assert( 0 ); - for ( i = 0; i < p->iLast; i++ ) - printf( "entry = %2d lit = %2d var = %2d \n", i, p->pVars[i], p->pVars[i]/2 ); - } - assert( p->iLast < p->nVars ); - p->pVars[p->iLast++] = Lit; -} - -/**Function************************************************************* - - Synopsis [Extracts an entry from the queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_QueueExtract( Msat_Queue_t * p ) -{ - if ( p->iFirst == p->iLast ) - return -1; - return p->pVars[p->iFirst++]; -} - -/**Function************************************************************* - - Synopsis [Resets the queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_QueueClear( Msat_Queue_t * p ) -{ - p->iFirst = 0; - p->iLast = 0; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c deleted file mode 100644 index 738562ef..00000000 --- a/src/sat/msat/msatRead.c +++ /dev/null @@ -1,268 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatRead.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The reader of the CNF formula in DIMACS format.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatRead.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static char * Msat_FileRead( FILE * pFile ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Read the file into the internal buffer.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Msat_FileRead( FILE * pFile ) -{ - int nFileSize; - char * pBuffer; - // get the file size, in bytes - fseek( pFile, 0, SEEK_END ); - nFileSize = ftell( pFile ); - // move the file current reading position to the beginning - rewind( pFile ); - // load the contents of the file into memory - pBuffer = ALLOC( char, nFileSize + 3 ); - fread( pBuffer, nFileSize, 1, pFile ); - // terminate the string with '\0' - pBuffer[ nFileSize + 0] = '\n'; - pBuffer[ nFileSize + 1] = '\0'; - return pBuffer; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Msat_ReadWhitespace( char ** pIn ) -{ - while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32) - (*pIn)++; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Msat_ReadNotWhitespace( char ** pIn ) -{ - while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) ) - (*pIn)++; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void skipLine( char ** pIn ) -{ - while ( 1 ) - { - if (**pIn == 0) - return; - if (**pIn == '\n') - { - (*pIn)++; - return; - } - (*pIn)++; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Msat_ReadInt( char ** pIn ) -{ - int val = 0; - bool neg = 0; - - Msat_ReadWhitespace( pIn ); - if ( **pIn == '-' ) - neg = 1, - (*pIn)++; - else if ( **pIn == '+' ) - (*pIn)++; - if ( **pIn < '0' || **pIn > '9' ) - fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn), - exit(1); - while ( **pIn >= '0' && **pIn <= '9' ) - val = val*10 + (**pIn - '0'), - (*pIn)++; - return neg ? -val : val; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLits ) -{ - int nVars = Msat_SolverReadVarNum( p ); - int parsed_lit, var, sign; - - Msat_IntVecClear( pLits ); - while ( 1 ) - { - parsed_lit = Msat_ReadInt(pIn); - if ( parsed_lit == 0 ) - break; - var = abs(parsed_lit) - 1; - sign = (parsed_lit > 0); - if ( var >= nVars ) - { - printf( "Variable %d is larger than the number of allocated variables (%d).\n", var+1, nVars ); - exit(1); - } - Msat_IntVecPush( pLits, MSAT_VAR2LIT(var, !sign) ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) -{ - Msat_Solver_t * p; - Msat_IntVec_t * pLits; - char * pIn = pText; - int nVars, nClas; - while ( 1 ) - { - Msat_ReadWhitespace( &pIn ); - if ( *pIn == 0 ) - break; - else if ( *pIn == 'c' ) - skipLine( &pIn ); - else if ( *pIn == 'p' ) - { - pIn++; - Msat_ReadWhitespace( &pIn ); - Msat_ReadNotWhitespace( &pIn ); - - nVars = Msat_ReadInt( &pIn ); - nClas = Msat_ReadInt( &pIn ); - skipLine( &pIn ); - // start the solver - p = Msat_SolverAlloc( nVars, 1, 1, 1, 1, 0 ); - Msat_SolverClean( p, nVars ); - Msat_SolverSetVerbosity( p, fVerbose ); - // allocate the vector - pLits = Msat_IntVecAlloc( nVars ); - } - else - { - if ( p == NULL ) - { - printf( "There is no parameter line.\n" ); - exit(1); - } - Msat_ReadClause( &pIn, p, pLits ); - if ( !Msat_SolverAddClause( p, pLits ) ) - return 0; - } - } - Msat_IntVecFree( pLits ); - *pS = p; - return Msat_SolverSimplifyDB( p ); -} - -/**Function************************************************************* - - Synopsis [Starts the solver and reads the DIMAC file.] - - Description [Returns FALSE upon immediate conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) -{ - char * pText; - bool Value; - pText = Msat_FileRead( pFile ); - Value = Msat_ReadDimacs( pText, p, fVerbose ); - free( pText ); - return Value; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c deleted file mode 100644 index ee3507a6..00000000 --- a/src/sat/msat/msatSolverApi.c +++ /dev/null @@ -1,500 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverApi.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [APIs of the SAT solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Simple SAT solver APIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } -int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; } -int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc; } -int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } -int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } -Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; } -Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; } -Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; } -Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; } -int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; } -int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; } -int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; } -int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; } -Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; } -int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; } -int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; } -void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; } -void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; } -void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; } -void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; } -void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; } -void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); } -void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); } -float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; } - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num ) -{ - int nClausesP; - assert( Num < p->nClauses ); - nClausesP = Msat_ClauseVecReadSize( p->vClauses ); - if ( Num < nClausesP ) - return Msat_ClauseVecReadEntry( p->vClauses, Num ); - return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP ); -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p ) -{ - return p->vAdjacents; -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p ) -{ - return p->vConeVars; -} - -/**Function************************************************************* - - Synopsis [Reads the clause with the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p ) -{ - return p->vVarsUsed; -} - - -/**Function************************************************************* - - Synopsis [Allocates the solver.] - - Description [After the solver is allocated, the procedure - Msat_SolverClean() should be called to set the number of variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, - double dClaInc, double dClaDecay, - double dVarInc, double dVarDecay, - bool fVerbose ) -{ - Msat_Solver_t * p; - int i; - - assert(sizeof(Msat_Lit_t) == sizeof(unsigned)); - assert(sizeof(float) == sizeof(unsigned)); - - p = ALLOC( Msat_Solver_t, 1 ); - memset( p, 0, sizeof(Msat_Solver_t) ); - - p->nVarsAlloc = nVarsAlloc; - p->nVars = 0; - - p->nClauses = 0; - p->vClauses = Msat_ClauseVecAlloc( 512 ); - p->vLearned = Msat_ClauseVecAlloc( 512 ); - - p->dClaInc = dClaInc; - p->dClaDecay = dClaDecay; - p->dVarInc = dVarInc; - p->dVarDecay = dVarDecay; - - p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pFactors = ALLOC( float, p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - { - p->pdActivity[i] = 0.0; - p->pFactors[i] = 1.0; - } - - p->pAssigns = ALLOC( int, p->nVarsAlloc ); - p->pModel = ALLOC( int, p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; -// p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc ); - p->pOrder = Msat_OrderAlloc( p ); - - p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); - for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) - p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); - p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); - - p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc ); - p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc ); - p->pReasons = ALLOC( Msat_Clause_t *, p->nVarsAlloc ); - memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc ); - p->pLevel = ALLOC( int, p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pLevel[i] = -1; - p->dRandSeed = 91648253; - p->fVerbose = fVerbose; - p->dProgress = 0.0; -// p->pModel = Msat_IntVecAlloc( p->nVarsAlloc ); - p->pMem = Msat_MmStepStart( 10 ); - - p->vConeVars = Msat_IntVecAlloc( p->nVarsAlloc ); - p->vAdjacents = Msat_ClauseVecAlloc( p->nVarsAlloc ); - for ( i = 0; i < p->nVarsAlloc; i++ ) - Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) ); - p->vVarsUsed = Msat_IntVecAlloc( p->nVarsAlloc ); - Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); - - - p->pSeen = ALLOC( int, p->nVarsAlloc ); - memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc ); - p->nSeenId = 1; - p->vReason = Msat_IntVecAlloc( p->nVarsAlloc ); - p->vTemp = Msat_IntVecAlloc( p->nVarsAlloc ); - return p; -} - -/**Function************************************************************* - - Synopsis [Resizes the solver.] - - Description [Assumes that the solver contains some clauses, and that - it is currently between the calls. Resizes the solver to accomodate - more variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) -{ - int nVarsAllocOld, i; - - nVarsAllocOld = p->nVarsAlloc; - p->nVarsAlloc = nVarsAlloc; - - p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - { - p->pdActivity[i] = 0.0; - p->pFactors[i] = 1.0; - } - - p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc ); - p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; - -// Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc ); - Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc ); - - p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); - for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ ) - p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); - - Msat_QueueFree( p->pQueue ); - p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); - - p->pReasons = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc ); - p->pLevel = REALLOC( int, p->pLevel, p->nVarsAlloc ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - { - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - } - - p->pSeen = REALLOC( int, p->pSeen, p->nVarsAlloc ); - for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - p->pSeen[i] = 0; - - Msat_IntVecGrow( p->vTrail, p->nVarsAlloc ); - Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc ); - - // make sure the array of adjucents has room to store the variable numbers - for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ ) - Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) ); - Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); -} - -/**Function************************************************************* - - Synopsis [Prepares the solver.] - - Description [Cleans the solver assuming that the problem will involve - the given number of variables (nVars). This procedure is useful - for many small (incremental) SAT problems, to prevent the solver - from being reallocated each time.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverClean( Msat_Solver_t * p, int nVars ) -{ - int i; - // free the clauses - int nClauses; - Msat_Clause_t ** pClauses; - - assert( p->nVarsAlloc >= nVars ); - p->nVars = nVars; - p->nClauses = 0; - - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); -// Msat_ClauseVecFree( p->vClauses ); - Msat_ClauseVecClear( p->vClauses ); - - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); -// Msat_ClauseVecFree( p->vLearned ); - Msat_ClauseVecClear( p->vLearned ); - -// FREE( p->pdActivity ); - for ( i = 0; i < p->nVars; i++ ) - p->pdActivity[i] = 0; - -// Msat_OrderFree( p->pOrder ); -// Msat_OrderClean( p->pOrder, p->nVars, NULL ); - Msat_OrderSetBounds( p->pOrder, p->nVars ); - - for ( i = 0; i < 2 * p->nVars; i++ ) -// Msat_ClauseVecFree( p->pvWatched[i] ); - Msat_ClauseVecClear( p->pvWatched[i] ); -// FREE( p->pvWatched ); -// Msat_QueueFree( p->pQueue ); - Msat_QueueClear( p->pQueue ); - -// FREE( p->pAssigns ); - for ( i = 0; i < p->nVars; i++ ) - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; -// Msat_IntVecFree( p->vTrail ); - Msat_IntVecClear( p->vTrail ); -// Msat_IntVecFree( p->vTrailLim ); - Msat_IntVecClear( p->vTrailLim ); -// FREE( p->pReasons ); - memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars ); -// FREE( p->pLevel ); - for ( i = 0; i < p->nVars; i++ ) - p->pLevel[i] = -1; -// Msat_IntVecFree( p->pModel ); -// Msat_MmStepStop( p->pMem, 0 ); - p->dRandSeed = 91648253; - p->dProgress = 0.0; - -// FREE( p->pSeen ); - memset( p->pSeen, 0, sizeof(int) * p->nVars ); - p->nSeenId = 1; -// Msat_IntVecFree( p->vReason ); - Msat_IntVecClear( p->vReason ); -// Msat_IntVecFree( p->vTemp ); - Msat_IntVecClear( p->vTemp ); -// printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL ); -// FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Frees the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverFree( Msat_Solver_t * p ) -{ - int i; - - // free the clauses - int nClauses; - Msat_Clause_t ** pClauses; -//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), -// Msat_ClauseVecReadSize( p->vLearned ) ); - - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); - Msat_ClauseVecFree( p->vClauses ); - - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseFree( p, pClauses[i], 0 ); - Msat_ClauseVecFree( p->vLearned ); - - FREE( p->pdActivity ); - FREE( p->pFactors ); - Msat_OrderFree( p->pOrder ); - - for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) - Msat_ClauseVecFree( p->pvWatched[i] ); - FREE( p->pvWatched ); - Msat_QueueFree( p->pQueue ); - - FREE( p->pAssigns ); - FREE( p->pModel ); - Msat_IntVecFree( p->vTrail ); - Msat_IntVecFree( p->vTrailLim ); - FREE( p->pReasons ); - FREE( p->pLevel ); - - Msat_MmStepStop( p->pMem, 0 ); - - nClauses = Msat_ClauseVecReadSize( p->vAdjacents ); - pClauses = Msat_ClauseVecReadArray( p->vAdjacents ); - for ( i = 0; i < nClauses; i++ ) - Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] ); - Msat_ClauseVecFree( p->vAdjacents ); - Msat_IntVecFree( p->vConeVars ); - Msat_IntVecFree( p->vVarsUsed ); - - FREE( p->pSeen ); - Msat_IntVecFree( p->vReason ); - Msat_IntVecFree( p->vTemp ); - FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Prepares the solver to run on a subset of variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars ) -{ - - int i; - // undo the previous data - for ( i = 0; i < p->nVarsAlloc; i++ ) - { - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - p->pdActivity[i] = 0.0; - } - - // set the new variable order - Msat_OrderClean( p->pOrder, vVars ); - - Msat_QueueClear( p->pQueue ); - Msat_IntVecClear( p->vTrail ); - Msat_IntVecClear( p->vTrailLim ); - p->dProgress = 0.0; -} - -/**Function************************************************************* - - Synopsis [Sets up the truth tables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ) -{ - int m, v; - // set up the truth tables - for ( m = 0; m < 32; m++ ) - for ( v = 0; v < 5; v++ ) - if ( m & (1 << v) ) - uTruths[v][0] |= (1 << m); - // make adjustments for the case of 6 variables - for ( v = 0; v < 5; v++ ) - uTruths[v][1] = uTruths[v][0]; - uTruths[5][0] = 0; - uTruths[5][1] = ~((unsigned)0); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c deleted file mode 100644 index f9fee73c..00000000 --- a/src/sat/msat/msatSolverCore.c +++ /dev/null @@ -1,212 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverCore.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The SAT solver core procedures.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Adds one variable to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ) -{ - if ( p->nVars == p->nVarsAlloc ) - Msat_SolverResize( p, 2 * p->nVarsAlloc ); - p->pLevel[p->nVars] = Level; - p->nVars++; - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds one clause to the solver's clause database.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits ) -{ - Msat_Clause_t * pC; - bool Value; - Value = Msat_ClauseCreate( p, vLits, 0, &pC ); - if ( pC != NULL ) - Msat_ClauseVecPush( p->vClauses, pC ); -// else if ( p->fProof ) -// Msat_ClauseCreateFake( p, vLits ); - return Value; -} - -/**Function************************************************************* - - Synopsis [Returns search-space coverage. Not extremely reliable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -double Msat_SolverProgressEstimate( Msat_Solver_t * p ) -{ - double dProgress = 0.0; - double dF = 1.0 / p->nVars; - int i; - for ( i = 0; i < p->nVars; i++ ) - if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED ) - dProgress += pow( dF, p->pLevel[i] ); - return dProgress / p->nVars; -} - -/**Function************************************************************* - - Synopsis [Prints statistics about the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverPrintStats( Msat_Solver_t * p ) -{ - printf("C solver (%d vars; %d clauses; %d learned):\n", - p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) ); - printf("starts : %lld\n", p->Stats.nStarts); - printf("conflicts : %lld\n", p->Stats.nConflicts); - printf("decisions : %lld\n", p->Stats.nDecisions); - printf("propagations : %lld\n", p->Stats.nPropagations); - printf("inspects : %lld\n", p->Stats.nInspects); -} - -/**Function************************************************************* - - Synopsis [Top-level solve.] - - Description [If using assumptions (non-empty 'assumps' vector), you must - call 'simplifyDB()' first to see that no top-level conflict is present - (which would put the solver in an undefined state. If the last argument - is given (vProj), the solver enumerates through the satisfying solutions, - which are projected on the variables listed in this array. Note that the - variables in the array may be complemented, in which case the derived - assignment for the variable is complemented.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit ) -{ - Msat_SearchParams_t Params = { 0.95, 0.999 }; - double nConflictsLimit, nLearnedLimit; - Msat_Type_t Status; - int timeStart = clock(); - int64 nConflictsOld = p->Stats.nConflicts; - int64 nDecisionsOld = p->Stats.nDecisions; - -// p->pFreq = ALLOC( int, p->nVarsAlloc ); -// memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); - - if ( vAssumps ) - { - int * pAssumps, nAssumps, i; - - assert( Msat_IntVecReadSize(p->vTrailLim) == 0 ); - - nAssumps = Msat_IntVecReadSize( vAssumps ); - pAssumps = Msat_IntVecReadArray( vAssumps ); - for ( i = 0; i < nAssumps; i++ ) - { - if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) ) - { - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, 0 ); - return MSAT_FALSE; - } - } - } - p->nLevelRoot = Msat_SolverReadDecisionLevel(p); - p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses ); - nConflictsLimit = 100; - nLearnedLimit = Msat_ClauseVecReadSize(p->vClauses) / 3; - Status = MSAT_UNKNOWN; - p->nBackTracks = (int)p->Stats.nConflicts; - while ( Status == MSAT_UNKNOWN ) - { - if ( p->fVerbose ) - printf("Solving -- conflicts=%d learnts=%d progress=%.4f %%\n", - (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100); - Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params ); - nConflictsLimit *= 1.5; - nLearnedLimit *= 1.1; - // if the limit on the number of backtracks is given, quit the restart loop - if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) - break; - // if the runtime limit is exceeded, quit the restart loop - if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) - break; - } - Msat_SolverCancelUntil( p, 0 ); - p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; -/* - PRT( "True solver runtime", clock() - timeStart ); - // print the statistics - { - int i, Counter = 0; - for ( i = 0; i < p->nVars; i++ ) - if ( p->pFreq[i] > 0 ) - { - printf( "%d ", p->pFreq[i] ); - Counter++; - } - if ( Counter ) - printf( "\n" ); - printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); - PRT( "Time", clock() - timeStart ); - } -*/ - return Status; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c deleted file mode 100644 index 05b7f6a9..00000000 --- a/src/sat/msat/msatSolverIo.c +++ /dev/null @@ -1,177 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverIo.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Input/output of CNFs.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverIo.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static char * Msat_TimeStamp(); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverPrintAssignment( Msat_Solver_t * p ) -{ - int i; - printf( "Current assignments are: \n" ); - for ( i = 0; i < p->nVars; i++ ) - printf( "%d", i % 10 ); - printf( "\n" ); - for ( i = 0; i < p->nVars; i++ ) - if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED ) - printf( "." ); - else - { - assert( i == MSAT_LIT2VAR(p->pAssigns[i]) ); - if ( MSAT_LITSIGN(p->pAssigns[i]) ) - printf( "0" ); - else - printf( "1" ); - } - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverPrintClauses( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pClauses; - int nClauses, i; - - printf( "Original clauses: \n" ); - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - { - printf( "%3d: ", i ); - Msat_ClausePrint( pClauses[i] ); - } - - printf( "Learned clauses: \n" ); - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - { - printf( "%3d: ", i ); - Msat_ClausePrint( pClauses[i] ); - } - - printf( "Variable activity: \n" ); - for ( i = 0; i < p->nVars; i++ ) - printf( "%3d : %.4f\n", i, p->pdActivity[i] ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ) -{ - FILE * pFile; - Msat_Clause_t ** pClauses; - int nClauses, i; - - nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned); - for ( i = 0; i < p->nVars; i++ ) - nClauses += ( p->pLevel[i] == 0 ); - - pFile = fopen( pFileName, "wb" ); - fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() ); - fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses ); - - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); - - nClauses = Msat_ClauseVecReadSize( p->vLearned ); - pClauses = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nClauses; i++ ) - Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); - - // write zero-level assertions - for ( i = 0; i < p->nVars; i++ ) - if ( p->pLevel[i] == 0 ) - fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 ); - - fprintf( pFile, "\n" ); - fclose( pFile ); -} - - -/**Function************************************************************* - - Synopsis [Returns the time stamp.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Msat_TimeStamp() -{ - static char Buffer[100]; - time_t ltime; - char * TimeStamp; - // get the current time - time( <ime ); - TimeStamp = asctime( localtime( <ime ) ); - TimeStamp[ strlen(TimeStamp) - 1 ] = 0; - strcpy( Buffer, TimeStamp ); - return Buffer; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c deleted file mode 100644 index 11a6540c..00000000 --- a/src/sat/msat/msatSolverSearch.c +++ /dev/null @@ -1,629 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverSearch.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The search part of the solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Msat_SolverUndoOne( Msat_Solver_t * p ); -static void Msat_SolverCancel( Msat_Solver_t * p ); -static Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ); -static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ); -static void Msat_SolverReduceDB( Msat_Solver_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Makes the next assumption (Lit).] - - Description [Returns FALSE if immediate conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) -{ - assert( Msat_QueueReadSize(p->pQueue) == 0 ); - if ( p->fVerbose ) - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit)); - Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) ); -// assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 ); -// assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars ); - return Msat_SolverEnqueue( p, Lit, NULL ); -} - -/**Function************************************************************* - - Synopsis [Reverts one variable binding on the trail.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverUndoOne( Msat_Solver_t * p ) -{ - Msat_Lit_t Lit; - Msat_Var_t Var; - Lit = Msat_IntVecPop( p->vTrail ); - Var = MSAT_LIT2VAR(Lit); - p->pAssigns[Var] = MSAT_VAR_UNASSIGNED; - p->pReasons[Var] = NULL; - p->pLevel[Var] = -1; -// Msat_OrderUndo( p->pOrder, Var ); - Msat_OrderVarUnassigned( p->pOrder, Var ); - - if ( p->fVerbose ) - printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); -} - -/**Function************************************************************* - - Synopsis [Reverts to the state before last Msat_SolverAssume().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverCancel( Msat_Solver_t * p ) -{ - int c; - assert( Msat_QueueReadSize(p->pQueue) == 0 ); - if ( p->fVerbose ) - { - if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) ) - { - Msat_Lit_t Lit; - Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); - printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit)); - } - } - for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- ) - Msat_SolverUndoOne( p ); -} - -/**Function************************************************************* - - Synopsis [Reverts to the state at given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ) -{ - while ( Msat_IntVecReadSize(p->vTrailLim) > Level ) - Msat_SolverCancel(p); -} - - -/**Function************************************************************* - - Synopsis [Record a clause and drive backtracking.] - - Description [vLits[0] must contain the asserting literal.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ) -{ - Msat_Clause_t * pC; - int Value; - assert( Msat_IntVecReadSize(vLits) != 0 ); - Value = Msat_ClauseCreate( p, vLits, 1, &pC ); - assert( Value ); - Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC ); - assert( Value ); - if ( pC ) - Msat_ClauseVecPush( p->vLearned, pC ); - return pC; -} - -/**Function************************************************************* - - Synopsis [Enqueues one variable assignment.] - - Description [Puts a new fact on the propagation queue and immediately - updates the variable value. Should a conflict arise, FALSE is returned. - Otherwise returns TRUE.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) -{ - Msat_Var_t Var = MSAT_LIT2VAR(Lit); - - // skip literals that are not in the current cone - if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) ) - return 1; - -// assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) ); - // if the literal is assigned - // return 1 if the assignment is consistent - // return 0 if the assignment is inconsistent (conflict) - if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED ) - return p->pAssigns[Var] == Lit; - // new fact - store it - if ( p->fVerbose ) - { -// printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit)); - printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit)); - Msat_ClausePrintSymbols( pC ); - } - p->pAssigns[Var] = Lit; - p->pLevel[Var] = Msat_IntVecReadSize(p->vTrailLim); -// p->pReasons[Var] = p->pLevel[Var]? pC: NULL; - p->pReasons[Var] = pC; - Msat_IntVecPush( p->vTrail, Lit ); - Msat_QueueInsert( p->pQueue, Lit ); - - Msat_OrderVarAssigned( p->pOrder, Var ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagates the assignments in the queue.] - - Description [Propagates all enqueued facts. If a conflict arises, - the conflicting clause is returned, otherwise NULL.] - - SideEffects [The propagation queue is empty, even if there was a conflict.] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ) -{ - Msat_ClauseVec_t ** pvWatched = p->pvWatched; - Msat_Clause_t ** pClauses; - Msat_Clause_t * pConflict; - Msat_Lit_t Lit, Lit_out; - int i, j, nClauses; - - // propagate all the literals in the queue - while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 ) - { - p->Stats.nPropagations++; - // get the clauses watched by this literal - nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] ); - pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] ); - // go through the watched clauses and decide what to do with them - for ( i = j = 0; i < nClauses; i++ ) - { - p->Stats.nInspects++; - // clear the returned literal - Lit_out = -1; - // propagate the clause - if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) ) - { // the clause is unit - // "Lit_out" contains the new assignment to be enqueued - if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) - { // consistent assignment - // no changes to the implication queue; the watch is the same too - pClauses[j++] = pClauses[i]; - continue; - } - // remember the reason of conflict (will be returned) - pConflict = pClauses[i]; - // leave the remaning clauses in the same watched list - for ( ; i < nClauses; i++ ) - pClauses[j++] = pClauses[i]; - Msat_ClauseVecShrink( pvWatched[Lit], j ); - // clear the propagation queue - Msat_QueueClear( p->pQueue ); - return pConflict; - } - // the clause is not unit - // in this case "Lit_out" contains the new watch if it has changed - if ( Lit_out >= 0 ) - Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] ); - else // the watch did not change - pClauses[j++] = pClauses[i]; - } - Msat_ClauseVecShrink( pvWatched[Lit], j ); - } - return NULL; -} - -/**Function************************************************************* - - Synopsis [Simplifies the data base.] - - Description [Simplify all constraints according to the current top-level - assigment (redundant constraints may be removed altogether).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverSimplifyDB( Msat_Solver_t * p ) -{ - Msat_ClauseVec_t * vClauses; - Msat_Clause_t ** pClauses; - int nClauses, Type, i, j; - int * pAssigns; - int Counter; - - assert( Msat_SolverReadDecisionLevel(p) == 0 ); - if ( Msat_SolverPropagate(p) != NULL ) - return 0; -//Msat_SolverPrintClauses( p ); -//Msat_SolverPrintAssignment( p ); -//printf( "Simplification\n" ); - - // simplify and reassign clause numbers - Counter = 0; - pAssigns = Msat_SolverReadAssignsArray( p ); - for ( Type = 0; Type < 2; Type++ ) - { - vClauses = Type? p->vLearned : p->vClauses; - nClauses = Msat_ClauseVecReadSize( vClauses ); - pClauses = Msat_ClauseVecReadArray( vClauses ); - for ( i = j = 0; i < nClauses; i++ ) - if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) ) - Msat_ClauseFree( p, pClauses[i], 1 ); - else - { - pClauses[j++] = pClauses[i]; - Msat_ClauseSetNum( pClauses[i], Counter++ ); - } - Msat_ClauseVecShrink( vClauses, j ); - } - p->nClauses = Counter; - return 1; -} - -/**Function************************************************************* - - Synopsis [Cleans the clause databased from the useless learnt clauses.] - - Description [Removes half of the learnt clauses, minus the clauses locked - by the current assignment. Locked clauses are clauses that are reason - to a some assignment.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverReduceDB( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned; - int nLearned, i, j; - double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned); - // Remove any clause below this activity - - // sort the learned clauses in the increasing order of activity - Msat_SolverSortDB( p ); - - // discard the first half the clauses (the less active ones) - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = j = 0; i < nLearned / 2; i++ ) - if ( !Msat_ClauseIsLocked( p, pLearned[i]) ) - Msat_ClauseFree( p, pLearned[i], 1 ); - else - pLearned[j++] = pLearned[i]; - // filter the more active clauses and leave those above the limit - for ( ; i < nLearned; i++ ) - if ( !Msat_ClauseIsLocked( p, pLearned[i] ) && - Msat_ClauseReadActivity(pLearned[i]) < dExtraLim ) - Msat_ClauseFree( p, pLearned[i], 1 ); - else - pLearned[j++] = pLearned[i]; - Msat_ClauseVecShrink( p->vLearned, j ); -} - -/**Function************************************************************* - - Synopsis [Removes the learned clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverRemoveLearned( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned; - int nLearned, i; - - // discard the learned clauses - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nLearned; i++ ) - { - assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); - - Msat_ClauseFree( p, pLearned[i], 1 ); - } - Msat_ClauseVecShrink( p->vLearned, 0 ); - p->nClauses = Msat_ClauseVecReadSize(p->vClauses); - - for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pReasons[i] = NULL; -} - -/**Function************************************************************* - - Synopsis [Removes the recently added clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverRemoveMarked( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned, ** pClauses; - int nLearned, nClauses, i; - - // discard the learned clauses - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = p->nClausesStart; i < nClauses; i++ ) - { -// assert( !Msat_ClauseIsLocked( p, pClauses[i]) ); - Msat_ClauseFree( p, pClauses[i], 1 ); - } - Msat_ClauseVecShrink( p->vClauses, p->nClausesStart ); - - // discard the learned clauses - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nLearned; i++ ) - { -// assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); - Msat_ClauseFree( p, pLearned[i], 1 ); - } - Msat_ClauseVecShrink( p->vLearned, 0 ); - p->nClauses = Msat_ClauseVecReadSize(p->vClauses); -/* - // undo the previous data - for ( i = 0; i < p->nVarsAlloc; i++ ) - { - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - p->pdActivity[i] = 0.0; - } - Msat_OrderClean( p->pOrder, p->nVars, NULL ); - Msat_QueueClear( p->pQueue ); -*/ -} - - - -/**Function************************************************************* - - Synopsis [Analyze conflict and produce a reason clause.] - - Description [Current decision level must be greater than root level.] - - SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ) -{ - Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED; - Msat_Var_t VarQ, Var; - int * pReasonArray, nReasonSize; - int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim); - int iStep = Msat_IntVecReadSize(p->vTrail) - 1; - - // increment the seen counter - p->nSeenId++; - // empty the vector array - Msat_IntVecClear( vLits_out ); - Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal) - *pLevel_out = 0; - do { - assert( pC != NULL ); // (otherwise should be UIP) - // get the reason of conflict - Msat_ClauseCalcReason( p, pC, Lit, p->vReason ); - nReasonSize = Msat_IntVecReadSize( p->vReason ); - pReasonArray = Msat_IntVecReadArray( p->vReason ); - for ( j = 0; j < nReasonSize; j++ ) { - LitQ = pReasonArray[j]; - VarQ = MSAT_LIT2VAR(LitQ); - if ( p->pSeen[VarQ] != p->nSeenId ) { - p->pSeen[VarQ] = p->nSeenId; - - // added to better fine-tune the search - Msat_SolverVarBumpActivity( p, LitQ ); - - // skip all the literals on this decision level - if ( p->pLevel[VarQ] == nLevelCur ) - pathC++; - else if ( p->pLevel[VarQ] > 0 ) { - // add the literals on other decision levels but - // exclude variables from decision level 0 - Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) ); - if ( *pLevel_out < p->pLevel[VarQ] ) - *pLevel_out = p->pLevel[VarQ]; - } - } - } - // Select next clause to look at: - do { -// Lit = Msat_IntVecReadEntryLast(p->vTrail); - Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- ); - Var = MSAT_LIT2VAR(Lit); - pC = p->pReasons[Var]; -// Msat_SolverUndoOne( p ); - } while ( p->pSeen[Var] != p->nSeenId ); - pathC--; - } while ( pathC > 0 ); - // we do not unbind the variables above - // this will be done after conflict analysis - - Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) ); - if ( p->fVerbose ) - { - printf( L_IND"Learnt {", L_ind ); - nReasonSize = Msat_IntVecReadSize( vLits_out ); - pReasonArray = Msat_IntVecReadArray( vLits_out ); - for ( j = 0; j < nReasonSize; j++ ) - printf(" "L_LIT, L_lit(pReasonArray[j])); - printf(" } at level %d\n", *pLevel_out); - } -} - -/**Function************************************************************* - - Synopsis [The search procedure called between the restarts.] - - Description [Search for a satisfying solution as long as the number of - conflicts does not exceed the limit (nConfLimit) while keeping the number - of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use - negative value for nConfLimit or nLearnedLimit to indicate infinity.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ) -{ - Msat_Clause_t * pConf; - Msat_Var_t Var; - int nLevelBack, nConfs, nAssigns, Value; - int i; - - assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); - p->Stats.nStarts++; - p->dVarDecay = 1 / pPars->dVarDecay; - p->dClaDecay = 1 / pPars->dClaDecay; - - // reset the activities - for ( i = 0; i < p->nVars; i++ ) - p->pdActivity[i] = (double)p->pFactors[i]; -// p->pdActivity[i] = 0.0; - - nConfs = 0; - while ( 1 ) - { - pConf = Msat_SolverPropagate( p ); - if ( pConf != NULL ){ - // CONFLICT - if ( p->fVerbose ) - { -// printf(L_IND"**CONFLICT**\n", L_ind); - printf(L_IND"**CONFLICT** ", L_ind); - Msat_ClausePrintSymbols( pConf ); - } - // count conflicts - p->Stats.nConflicts++; - nConfs++; - - // if top level, return UNSAT - if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ) - return MSAT_FALSE; - - // perform conflict analysis - Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack ); - Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack ); - Msat_SolverRecord( p, p->vTemp ); - - // it is important that recording is done after cancelling - // because canceling cleans the queue while recording adds to it - Msat_SolverVarDecayActivity( p ); - Msat_SolverClaDecayActivity( p ); - - } - else{ - // NO CONFLICT - if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) { - // Simplify the set of problem clauses: -// Value = Msat_SolverSimplifyDB(p); -// assert( Value ); - } - nAssigns = Msat_IntVecReadSize( p->vTrail ); - if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) { - // Reduce the set of learnt clauses: - Msat_SolverReduceDB(p); - } - - Var = Msat_OrderVarSelect( p->pOrder ); - if ( Var == MSAT_ORDER_UNKNOWN ) { - // Model found and stored in p->pAssigns - memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars ); - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_TRUE; - } - if ( nConfLimit > 0 && nConfs > nConfLimit ) { - // Reached bound on number of conflicts: - p->dProgress = Msat_SolverProgressEstimate( p ); - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_UNKNOWN; - } - else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) { - // Reached bound on number of conflicts: - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_UNKNOWN; - } - else{ - // New variable decision: - p->Stats.nDecisions++; - assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars ); - Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) ); - assert( Value ); - } - } - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c deleted file mode 100644 index 3b89d102..00000000 --- a/src/sat/msat/msatSort.c +++ /dev/null @@ -1,173 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSort.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Sorting clauses.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSort.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 ); - -// Returns a random float 0 <= x < 1. Seed must never be 0. -static 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 int irand(double seed, int size) { - return (int)(drand(seed) * size); } - -static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverSortDB( Msat_Solver_t * p ) -{ - Msat_ClauseVec_t * pVecClauses; - Msat_Clause_t ** pLearned; - int nLearned; - // read the parameters - pVecClauses = Msat_SolverReadLearned( p ); - nLearned = Msat_ClauseVecReadSize( pVecClauses ); - pLearned = Msat_ClauseVecReadArray( pVecClauses ); - // Msat_SolverSort the array -// qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), -// (int (*)(const void *, const void *)) Msat_SolverSortCompare ); -// printf( "Msat_SolverSorting.\n" ); - Msat_SolverSort( pLearned, nLearned, 91648253 ); -/* - if ( nLearned > 2 ) - { - printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) ); - printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) ); - printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) ); - } -*/ -} - -/**Function************************************************************* - - Synopsis [Comparison procedure for two clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 ) -{ - float Value1 = Msat_ClauseReadActivity( *ppC1 ); - float Value2 = Msat_ClauseReadActivity( *ppC2 ); - if ( Value1 < Value2 ) - return -1; - if ( Value1 > Value2 ) - return 1; - return 0; -} - - -/**Function************************************************************* - - Synopsis [Selection sort for small array size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverSortSelection( Msat_Clause_t ** array, int size ) -{ - Msat_Clause_t * tmp; - int i, j, best_i; - for ( i = 0; i < size-1; i++ ) - { - best_i = i; - for (j = i+1; j < size; j++) - { - if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) ) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - -/**Function************************************************************* - - Synopsis [The original MiniSat sorting procedure.] - - Description [This procedure is used to preserve trace-equivalence - with the orignal C++ implemenation of the solver.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed ) -{ - if (size <= 15) - Msat_SolverSortSelection( array, size ); - else - { - Msat_Clause_t * pivot = array[irand(seed, size)]; - Msat_Clause_t * tmp; - int i = -1; - int j = size; - - for(;;) - { - do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) ); - do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) ); - - if ( i >= j ) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - Msat_SolverSort(array , i , seed); - Msat_SolverSort(&array[i], size-i, seed); - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c deleted file mode 100644 index 75f53047..00000000 --- a/src/sat/msat/msatVec.c +++ /dev/null @@ -1,495 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatVec.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [Integer vector borrowed from Extra.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Msat_IntVecSortCompare1( int * pp1, int * pp2 ); -static int Msat_IntVecSortCompare2( int * pp1, int * pp2 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates a vector with the given capacity.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) -{ - Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); - if ( nCap > 0 && nCap < 16 ) - nCap = 16; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; - return p; -} - -/**Function************************************************************* - - Synopsis [Creates the vector from an integer array of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) -{ - Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); - p->nSize = nSize; - p->nCap = nSize; - p->pArray = pArray; - return p; -} - -/**Function************************************************************* - - Synopsis [Creates the vector from an integer array of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) -{ - Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); - p->nSize = nSize; - p->nCap = nSize; - p->pArray = ALLOC( int, nSize ); - memcpy( p->pArray, pArray, sizeof(int) * nSize ); - return p; -} - -/**Function************************************************************* - - Synopsis [Duplicates the integer array.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) -{ - Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); - p->nSize = pVec->nSize; - p->nCap = pVec->nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; - memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize ); - return p; -} - -/**Function************************************************************* - - Synopsis [Transfers the array into another vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) -{ - Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); - p->nSize = pVec->nSize; - p->nCap = pVec->nCap; - p->pArray = pVec->pArray; - pVec->nSize = 0; - pVec->nCap = 0; - pVec->pArray = NULL; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecFree( Msat_IntVec_t * p ) -{ - FREE( p->pArray ); - FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Fills the vector with given number of entries.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry ) -{ - int i; - Msat_IntVecGrow( p, nSize ); - p->nSize = nSize; - for ( i = 0; i < p->nSize; i++ ) - p->pArray[i] = Entry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Msat_IntVecReleaseArray( Msat_IntVec_t * p ) -{ - int * pArray = p->pArray; - p->nCap = 0; - p->nSize = 0; - p->pArray = NULL; - return pArray; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Msat_IntVecReadArray( Msat_IntVec_t * p ) -{ - return p->pArray; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecReadSize( Msat_IntVec_t * p ) -{ - return p->nSize; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray[i]; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry ) -{ - assert( i >= 0 && i < p->nSize ); - p->pArray[i] = Entry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecReadEntryLast( Msat_IntVec_t * p ) -{ - return p->pArray[p->nSize-1]; -} - -/**Function************************************************************* - - Synopsis [Resizes the vector to the given capacity.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = REALLOC( int, p->pArray, nCapMin ); - p->nCap = nCapMin; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew ) -{ - assert( p->nSize >= nSizeNew ); - p->nSize = nSizeNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecClear( Msat_IntVec_t * p ) -{ - p->nSize = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecPush( Msat_IntVec_t * p, int Entry ) -{ - if ( p->nSize == p->nCap ) - { - if ( p->nCap < 16 ) - Msat_IntVecGrow( p, 16 ); - else - Msat_IntVecGrow( p, 2 * p->nCap ); - } - p->pArray[p->nSize++] = Entry; -} - -/**Function************************************************************* - - Synopsis [Add the element while ensuring uniqueness.] - - Description [Returns 1 if the element was found, and 0 if it was new. ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry ) -{ - int i; - for ( i = 0; i < p->nSize; i++ ) - if ( p->pArray[i] == Entry ) - return 1; - Msat_IntVecPush( p, Entry ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Inserts the element while sorting in the increasing order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease ) -{ - int Entry1, Entry2; - int i; - Msat_IntVecPushUnique( p, Entry ); - // find the p of the node - for ( i = p->nSize-1; i > 0; i-- ) - { - Entry1 = p->pArray[i ]; - Entry2 = p->pArray[i-1]; - if ( fIncrease && Entry1 >= Entry2 || - !fIncrease && Entry1 <= Entry2 ) - break; - p->pArray[i ] = Entry2; - p->pArray[i-1] = Entry1; - } -} - - -/**Function************************************************************* - - Synopsis [Returns the last entry and removes it from the list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecPop( Msat_IntVec_t * p ) -{ - assert( p->nSize > 0 ); - return p->pArray[--p->nSize]; -} - -/**Function************************************************************* - - Synopsis [Sorting the entries by their integer value.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse ) -{ - if ( fReverse ) - qsort( (void *)p->pArray, p->nSize, sizeof(int), - (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 ); - else - qsort( (void *)p->pArray, p->nSize, sizeof(int), - (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 ); -} - -/**Function************************************************************* - - Synopsis [Comparison procedure for two clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecSortCompare1( int * pp1, int * pp2 ) -{ - // for some reason commenting out lines (as shown) led to crashing of the release version - if ( *pp1 < *pp2 ) - return -1; - if ( *pp1 > *pp2 ) // - return 1; - return 0; // -} - -/**Function************************************************************* - - Synopsis [Comparison procedure for two clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_IntVecSortCompare2( int * pp1, int * pp2 ) -{ - // for some reason commenting out lines (as shown) led to crashing of the release version - if ( *pp1 > *pp2 ) - return -1; - if ( *pp1 < *pp2 ) // - return 1; - return 0; // -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |