From 888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2005 08:01:00 -0700 Subject: Version abc50729 --- src/sat/msat/module.make | 13 + src/sat/msat/msat.h | 160 +++++++++++ src/sat/msat/msatActivity.c | 158 ++++++++++ src/sat/msat/msatClause.c | 524 +++++++++++++++++++++++++++++++++ src/sat/msat/msatClauseVec.c | 232 +++++++++++++++ src/sat/msat/msatInt.h | 304 ++++++++++++++++++++ src/sat/msat/msatMem.c | 529 ++++++++++++++++++++++++++++++++++ src/sat/msat/msatOrderH.c | 405 ++++++++++++++++++++++++++ src/sat/msat/msatOrderJ.c | 466 ++++++++++++++++++++++++++++++ src/sat/msat/msatQueue.c | 157 ++++++++++ src/sat/msat/msatRead.c | 268 +++++++++++++++++ src/sat/msat/msatSolverApi.c | 488 +++++++++++++++++++++++++++++++ src/sat/msat/msatSolverCore.c | 187 ++++++++++++ src/sat/msat/msatSolverIo.c | 177 ++++++++++++ src/sat/msat/msatSolverSearch.c | 623 ++++++++++++++++++++++++++++++++++++++++ src/sat/msat/msatSort.c | 173 +++++++++++ src/sat/msat/msatVec.c | 495 +++++++++++++++++++++++++++++++ 17 files changed, 5359 insertions(+) create mode 100644 src/sat/msat/module.make create mode 100644 src/sat/msat/msat.h create mode 100644 src/sat/msat/msatActivity.c create mode 100644 src/sat/msat/msatClause.c create mode 100644 src/sat/msat/msatClauseVec.c create mode 100644 src/sat/msat/msatInt.h create mode 100644 src/sat/msat/msatMem.c create mode 100644 src/sat/msat/msatOrderH.c create mode 100644 src/sat/msat/msatOrderJ.c create mode 100644 src/sat/msat/msatQueue.c create mode 100644 src/sat/msat/msatRead.c create mode 100644 src/sat/msat/msatSolverApi.c create mode 100644 src/sat/msat/msatSolverCore.c create mode 100644 src/sat/msat/msatSolverIo.c create mode 100644 src/sat/msat/msatSolverSearch.c create mode 100644 src/sat/msat/msatSort.c create mode 100644 src/sat/msat/msatVec.c (limited to 'src/sat/msat') diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make new file mode 100644 index 00000000..0dadfbe1 --- /dev/null +++ b/src/sat/msat/module.make @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..21ddcb81 --- /dev/null +++ b/src/sat/msat/msat.h @@ -0,0 +1,160 @@ +/**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 ] + + 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__ + +//////////////////////////////////////////////////////////////////////// +/// 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// 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 ); +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 ); +// 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_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 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 ); +// 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 ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +#endif diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c new file mode 100644 index 00000000..c9a518ce --- /dev/null +++ b/src/sat/msat/msatActivity.c @@ -0,0 +1,158 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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); + if ( (p->pdActivity[Var] += p->dVarInc) > 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 new file mode 100644 index 00000000..dc39bee6 --- /dev/null +++ b/src/sat/msat/msatClause.c @@ -0,0 +1,524 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 + 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] ); + } + } + + // 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 new file mode 100644 index 00000000..7c24619f --- /dev/null +++ b/src/sat/msat/msatClauseVec.c @@ -0,0 +1,232 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..037616f6 --- /dev/null +++ b/src/sat/msat/msatInt.h @@ -0,0 +1,304 @@ +/**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 ] + + 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 +#include +#include +#include +#include +#include +#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. + 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 + + // 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// 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 new file mode 100644 index 00000000..2d178094 --- /dev/null +++ b/src/sat/msat/msatMem.c @@ -0,0 +1,529 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; + + // delocate 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<nMapSize = (4<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<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 new file mode 100644 index 00000000..ca034233 --- /dev/null +++ b/src/sat/msat/msatOrderH.c @@ -0,0 +1,405 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..6067b40f --- /dev/null +++ b/src/sat/msat/msatOrderJ.c @@ -0,0 +1,466 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; + + // 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; + } + + // 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 ( 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; + } + 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 ); + + 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->pNext; + // 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 new file mode 100644 index 00000000..c12cc75d --- /dev/null +++ b/src/sat/msat/msatQueue.c @@ -0,0 +1,157 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..b8e585a4 --- /dev/null +++ b/src/sat/msat/msatRead.c @@ -0,0 +1,268 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..ba506993 --- /dev/null +++ b/src/sat/msat/msatSolverApi.c @@ -0,0 +1,488 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Simple SAT solver APIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } +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 p->nBackTracks; } +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); } + +/**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 ); + for ( i = 0; i < p->nVarsAlloc; i++ ) + p->pdActivity[i] = 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 ); + for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) + p->pdActivity[i] = 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 ); + 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 new file mode 100644 index 00000000..b8d9f328 --- /dev/null +++ b/src/sat/msat/msatSolverCore.c @@ -0,0 +1,187 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds one variable to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_SolverAddVar( Msat_Solver_t * p ) +{ + if ( p->nVars == p->nVarsAlloc ) + Msat_SolverResize( p, 2 * p->nVarsAlloc ); + 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 ) +{ + Msat_SearchParams_t Params = { 0.95, 0.999 }; + double nConflictsLimit, nLearnedLimit; + Msat_Type_t Status; + int64 nConflictsOld = p->Stats.nConflicts; + int64 nDecisionsOld = p->Stats.nDecisions; + + 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 ) + break; + } + Msat_SolverCancelUntil( p, 0 ); + p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; + return Status; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c new file mode 100644 index 00000000..f17595a7 --- /dev/null +++ b/src/sat/msat/msatSolverIo.c @@ -0,0 +1,177 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..13a0c403 --- /dev/null +++ b/src/sat/msat/msatSolverSearch.c @@ -0,0 +1,623 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; + + assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); + p->Stats.nStarts++; + p->dVarDecay = 1 / pPars->dVarDecay; + p->dClaDecay = 1 / pPars->dClaDecay; + + 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 && nConfs > 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 new file mode 100644 index 00000000..2198d303 --- /dev/null +++ b/src/sat/msat/msatSort.c @@ -0,0 +1,173 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 new file mode 100644 index 00000000..951969cf --- /dev/null +++ b/src/sat/msat/msatVec.c @@ -0,0 +1,495 @@ +/**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 ] + + 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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3