src/sat/msat/msat.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Defines

#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)

Typedefs

typedef int bool
typedef struct Msat_Solver_t_ Msat_Solver_t
typedef struct Msat_IntVec_t_ Msat_IntVec_t
typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t
typedef struct Msat_VarHeap_t_ Msat_VarHeap_t

Enumerations

enum  Msat_Type_t { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 }

Functions

bool Msat_SolverParseDimacs (FILE *pFile, Msat_Solver_t **p, int fVerbose)
bool Msat_SolverAddVar (Msat_Solver_t *p, int Level)
bool Msat_SolverAddClause (Msat_Solver_t *p, Msat_IntVec_t *pLits)
bool Msat_SolverSimplifyDB (Msat_Solver_t *p)
bool Msat_SolverSolve (Msat_Solver_t *p, Msat_IntVec_t *pVecAssumps, int nBackTrackLimit, int nTimeLimit)
void Msat_SolverPrintStats (Msat_Solver_t *p)
void Msat_SolverPrintAssignment (Msat_Solver_t *p)
void Msat_SolverPrintClauses (Msat_Solver_t *p)
void Msat_SolverWriteDimacs (Msat_Solver_t *p, char *pFileName)
int Msat_SolverReadVarNum (Msat_Solver_t *p)
int Msat_SolverReadClauseNum (Msat_Solver_t *p)
int Msat_SolverReadVarAllocNum (Msat_Solver_t *p)
int * Msat_SolverReadAssignsArray (Msat_Solver_t *p)
int * Msat_SolverReadModelArray (Msat_Solver_t *p)
unsigned Msat_SolverReadTruth (Msat_Solver_t *p)
int Msat_SolverReadBackTracks (Msat_Solver_t *p)
int Msat_SolverReadInspects (Msat_Solver_t *p)
void Msat_SolverSetVerbosity (Msat_Solver_t *p, int fVerbose)
void Msat_SolverSetProofWriting (Msat_Solver_t *p, int fProof)
void Msat_SolverSetVarTypeA (Msat_Solver_t *p, int Var)
void Msat_SolverSetVarMap (Msat_Solver_t *p, Msat_IntVec_t *vVarMap)
void Msat_SolverMarkLastClauseTypeA (Msat_Solver_t *p)
void Msat_SolverMarkClausesStart (Msat_Solver_t *p)
float * Msat_SolverReadFactors (Msat_Solver_t *p)
int Msat_SolverReadSolutions (Msat_Solver_t *p)
int * Msat_SolverReadSolutionsArray (Msat_Solver_t *p)
Msat_ClauseVec_t * Msat_SolverReadAdjacents (Msat_Solver_t *p)
Msat_IntVec_t * Msat_SolverReadConeVars (Msat_Solver_t *p)
Msat_IntVec_t * Msat_SolverReadVarsUsed (Msat_Solver_t *p)
void Msat_SolverRemoveLearned (Msat_Solver_t *p)
void Msat_SolverRemoveMarked (Msat_Solver_t *p)
Msat_Solver_t * Msat_SolverAlloc (int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose)
void Msat_SolverResize (Msat_Solver_t *pMan, int nVarsAlloc)
void Msat_SolverClean (Msat_Solver_t *p, int nVars)
void Msat_SolverPrepare (Msat_Solver_t *pSat, Msat_IntVec_t *vVars)
void Msat_SolverFree (Msat_Solver_t *p)
Msat_IntVec_t * Msat_IntVecAlloc (int nCap)
Msat_IntVec_t * Msat_IntVecAllocArray (int *pArray, int nSize)
Msat_IntVec_t * Msat_IntVecAllocArrayCopy (int *pArray, int nSize)
Msat_IntVec_t * Msat_IntVecDup (Msat_IntVec_t *pVec)
Msat_IntVec_t * Msat_IntVecDupArray (Msat_IntVec_t *pVec)
void Msat_IntVecFree (Msat_IntVec_t *p)
void Msat_IntVecFill (Msat_IntVec_t *p, int nSize, int Entry)
int * Msat_IntVecReleaseArray (Msat_IntVec_t *p)
int * Msat_IntVecReadArray (Msat_IntVec_t *p)
int Msat_IntVecReadSize (Msat_IntVec_t *p)
int Msat_IntVecReadEntry (Msat_IntVec_t *p, int i)
int Msat_IntVecReadEntryLast (Msat_IntVec_t *p)
void Msat_IntVecWriteEntry (Msat_IntVec_t *p, int i, int Entry)
void Msat_IntVecGrow (Msat_IntVec_t *p, int nCapMin)
void Msat_IntVecShrink (Msat_IntVec_t *p, int nSizeNew)
void Msat_IntVecClear (Msat_IntVec_t *p)
void Msat_IntVecPush (Msat_IntVec_t *p, int Entry)
int Msat_IntVecPushUnique (Msat_IntVec_t *p, int Entry)
void Msat_IntVecPushUniqueOrder (Msat_IntVec_t *p, int Entry, int fIncrease)
int Msat_IntVecPop (Msat_IntVec_t *p)
void Msat_IntVecSort (Msat_IntVec_t *p, int fReverse)
Msat_VarHeap_t * Msat_VarHeapAlloc ()
void Msat_VarHeapSetActivity (Msat_VarHeap_t *p, double *pActivity)
void Msat_VarHeapStart (Msat_VarHeap_t *p, int *pVars, int nVars, int nVarsAlloc)
void Msat_VarHeapGrow (Msat_VarHeap_t *p, int nSize)
void Msat_VarHeapStop (Msat_VarHeap_t *p)
void Msat_VarHeapPrint (FILE *pFile, Msat_VarHeap_t *p)
void Msat_VarHeapCheck (Msat_VarHeap_t *p)
void Msat_VarHeapCheckOne (Msat_VarHeap_t *p, int iVar)
int Msat_VarHeapContainsVar (Msat_VarHeap_t *p, int iVar)
void Msat_VarHeapInsert (Msat_VarHeap_t *p, int iVar)
void Msat_VarHeapUpdate (Msat_VarHeap_t *p, int iVar)
void Msat_VarHeapDelete (Msat_VarHeap_t *p, int iVar)
double Msat_VarHeapReadMaxWeight (Msat_VarHeap_t *p)
int Msat_VarHeapCountNodes (Msat_VarHeap_t *p, double WeightLimit)
int Msat_VarHeapReadMax (Msat_VarHeap_t *p)
int Msat_VarHeapGetMax (Msat_VarHeap_t *p)

Define Documentation

#define MSAT_LIT2VAR ( l   )     ((l)>>1)

Definition at line 65 of file msat.h.

#define MSAT_LITNOT ( l   )     ((l)^1)

Definition at line 63 of file msat.h.

#define MSAT_LITSIGN ( l   )     ((l)&1)

Definition at line 64 of file msat.h.

#define MSAT_VAR2LIT ( v,
s   )     (2*(v)+(s))

Definition at line 62 of file msat.h.

Typedef Documentation

typedef int bool

CFile****************************************************************

FileName [msat.h]

PackageName [A C version of SAT solver MINISAT, originally developed in C++ by Niklas Een and Niklas Sorensson, Chalmers University of Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]

Synopsis [External definitions of the solver.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id
msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp

] INCLUDES /// PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 45 of file msat.h.

typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t

Definition at line 52 of file msat.h.

typedef struct Msat_IntVec_t_ Msat_IntVec_t

Definition at line 51 of file msat.h.

typedef struct Msat_Solver_t_ Msat_Solver_t

Definition at line 48 of file msat.h.

typedef struct Msat_VarHeap_t_ Msat_VarHeap_t

Definition at line 53 of file msat.h.

Enumeration Type Documentation

enum Msat_Type_t
Enumerator:
MSAT_FALSE 
MSAT_UNKNOWN 
MSAT_TRUE 

Definition at line 56 of file msat.h.

00056 { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;

Function Documentation

Msat_IntVec_t* Msat_IntVecAlloc ( int  nCap  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatVec.c.

00046 {
00047     Msat_IntVec_t * p;
00048     p = ALLOC( Msat_IntVec_t, 1 );
00049     if ( nCap > 0 && nCap < 16 )
00050         nCap = 16;
00051     p->nSize  = 0;
00052     p->nCap   = nCap;
00053     p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
00054     return p;
00055 }

Msat_IntVec_t* Msat_IntVecAllocArray ( int *  pArray,
int  nSize 
)

Function*************************************************************

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file msatVec.c.

00069 {
00070     Msat_IntVec_t * p;
00071     p = ALLOC( Msat_IntVec_t, 1 );
00072     p->nSize  = nSize;
00073     p->nCap   = nSize;
00074     p->pArray = pArray;
00075     return p;
00076 }

Msat_IntVec_t* Msat_IntVecAllocArrayCopy ( int *  pArray,
int  nSize 
)

Function*************************************************************

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file msatVec.c.

00090 {
00091     Msat_IntVec_t * p;
00092     p = ALLOC( Msat_IntVec_t, 1 );
00093     p->nSize  = nSize;
00094     p->nCap   = nSize;
00095     p->pArray = ALLOC( int, nSize );
00096     memcpy( p->pArray, pArray, sizeof(int) * nSize );
00097     return p;
00098 }

void Msat_IntVecClear ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 332 of file msatVec.c.

00333 {
00334     p->nSize = 0;
00335 }

Msat_IntVec_t* Msat_IntVecDup ( Msat_IntVec_t *  pVec  ) 

Function*************************************************************

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file msatVec.c.

00112 {
00113     Msat_IntVec_t * p;
00114     p = ALLOC( Msat_IntVec_t, 1 );
00115     p->nSize  = pVec->nSize;
00116     p->nCap   = pVec->nCap;
00117     p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
00118     memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
00119     return p;
00120 }

Msat_IntVec_t* Msat_IntVecDupArray ( Msat_IntVec_t *  pVec  ) 

Function*************************************************************

Synopsis [Transfers the array into another vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatVec.c.

00134 {
00135     Msat_IntVec_t * p;
00136     p = ALLOC( Msat_IntVec_t, 1 );
00137     p->nSize  = pVec->nSize;
00138     p->nCap   = pVec->nCap;
00139     p->pArray = pVec->pArray;
00140     pVec->nSize  = 0;
00141     pVec->nCap   = 0;
00142     pVec->pArray = NULL;
00143     return p;
00144 }

void Msat_IntVecFill ( Msat_IntVec_t *  p,
int  nSize,
int  Entry 
)

Function*************************************************************

Synopsis [Fills the vector with given number of entries.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file msatVec.c.

00175 {
00176     int i;
00177     Msat_IntVecGrow( p, nSize );
00178     p->nSize = nSize;
00179     for ( i = 0; i < p->nSize; i++ )
00180         p->pArray[i] = Entry;
00181 }

void Msat_IntVecFree ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file msatVec.c.

00158 {
00159     FREE( p->pArray );
00160     FREE( p );
00161 }

void Msat_IntVecGrow ( Msat_IntVec_t *  p,
int  nCapMin 
)

Function*************************************************************

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 296 of file msatVec.c.

00297 {
00298     if ( p->nCap >= nCapMin )
00299         return;
00300     p->pArray = REALLOC( int, p->pArray, nCapMin ); 
00301     p->nCap   = nCapMin;
00302 }

int Msat_IntVecPop ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis [Returns the last entry and removes it from the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file msatVec.c.

00423 {
00424     assert( p->nSize > 0 );
00425     return p->pArray[--p->nSize];
00426 }

void Msat_IntVecPush ( Msat_IntVec_t *  p,
int  Entry 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file msatVec.c.

00349 {
00350     if ( p->nSize == p->nCap )
00351     {
00352         if ( p->nCap < 16 )
00353             Msat_IntVecGrow( p, 16 );
00354         else
00355             Msat_IntVecGrow( p, 2 * p->nCap );
00356     }
00357     p->pArray[p->nSize++] = Entry;
00358 }

int Msat_IntVecPushUnique ( Msat_IntVec_t *  p,
int  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 []

Definition at line 371 of file msatVec.c.

00372 {
00373     int i;
00374     for ( i = 0; i < p->nSize; i++ )
00375         if ( p->pArray[i] == Entry )
00376             return 1;
00377     Msat_IntVecPush( p, Entry );
00378     return 0;
00379 }

void Msat_IntVecPushUniqueOrder ( Msat_IntVec_t *  p,
int  Entry,
int  fIncrease 
)

Function*************************************************************

Synopsis [Inserts the element while sorting in the increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 392 of file msatVec.c.

00393 {
00394     int Entry1, Entry2;
00395     int i;
00396     Msat_IntVecPushUnique( p, Entry );
00397     // find the p of the node
00398     for ( i = p->nSize-1; i > 0; i-- )
00399     {
00400         Entry1 = p->pArray[i  ];
00401         Entry2 = p->pArray[i-1];
00402         if ( fIncrease && Entry1 >= Entry2 || 
00403             !fIncrease && Entry1 <= Entry2 )
00404             break;
00405         p->pArray[i  ] = Entry2;
00406         p->pArray[i-1] = Entry1;
00407     }
00408 }

int* Msat_IntVecReadArray ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file msatVec.c.

00215 {
00216     return p->pArray;
00217 }

int Msat_IntVecReadEntry ( Msat_IntVec_t *  p,
int  i 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file msatVec.c.

00247 {
00248     assert( i >= 0 && i < p->nSize );
00249     return p->pArray[i];
00250 }

int Msat_IntVecReadEntryLast ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file msatVec.c.

00281 {
00282     return p->pArray[p->nSize-1];
00283 }

int Msat_IntVecReadSize ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file msatVec.c.

00231 {
00232     return p->nSize;
00233 }

int* Msat_IntVecReleaseArray ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file msatVec.c.

00195 {
00196     int * pArray = p->pArray;
00197     p->nCap = 0;
00198     p->nSize = 0;
00199     p->pArray = NULL;
00200     return pArray;
00201 }

void Msat_IntVecShrink ( Msat_IntVec_t *  p,
int  nSizeNew 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file msatVec.c.

00316 {
00317     assert( p->nSize >= nSizeNew );
00318     p->nSize = nSizeNew;
00319 }

void Msat_IntVecSort ( Msat_IntVec_t *  p,
int  fReverse 
)

Function*************************************************************

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file msatVec.c.

00440 {
00441     if ( fReverse ) 
00442         qsort( (void *)p->pArray, p->nSize, sizeof(int), 
00443                 (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
00444     else
00445         qsort( (void *)p->pArray, p->nSize, sizeof(int), 
00446                 (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
00447 }

void Msat_IntVecWriteEntry ( Msat_IntVec_t *  p,
int  i,
int  Entry 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file msatVec.c.

00264 {
00265     assert( i >= 0 && i < p->nSize );
00266     p->pArray[i] = Entry;
00267 }

bool Msat_SolverAddClause ( Msat_Solver_t *  p,
Msat_IntVec_t *  vLits 
)

Function*************************************************************

Synopsis [Adds one clause to the solver's clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file msatSolverCore.c.

00063 {
00064     Msat_Clause_t * pC; 
00065     bool Value;
00066     Value = Msat_ClauseCreate( p, vLits, 0, &pC );
00067     if ( pC != NULL )
00068         Msat_ClauseVecPush( p->vClauses, pC );
00069 //    else if ( p->fProof )
00070 //        Msat_ClauseCreateFake( p, vLits );
00071     return Value;
00072 }

bool Msat_SolverAddVar ( Msat_Solver_t *  p,
int  Level 
)

CFile****************************************************************

FileName [msatSolverCore.c]

PackageName [A C version of SAT solver MINISAT, originally developed in C++ by Niklas Een and Niklas Sorensson, Chalmers University of Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]

Synopsis [The SAT solver core procedures.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id
msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Adds one variable to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file msatSolverCore.c.

00043 {
00044     if ( p->nVars == p->nVarsAlloc )
00045         Msat_SolverResize( p, 2 * p->nVarsAlloc );
00046     p->pLevel[p->nVars] = Level;
00047     p->nVars++;
00048     return 1;
00049 }

Msat_Solver_t* Msat_SolverAlloc ( int  nVarsAlloc,
double  dClaInc,
double  dClaDecay,
double  dVarInc,
double  dVarDecay,
bool  fVerbose 
)

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 []

Definition at line 151 of file msatSolverApi.c.

00155 {
00156     Msat_Solver_t * p;
00157     int i;
00158 
00159     assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
00160     assert(sizeof(float)     == sizeof(unsigned));
00161 
00162     p = ALLOC( Msat_Solver_t, 1 );
00163     memset( p, 0, sizeof(Msat_Solver_t) );
00164 
00165     p->nVarsAlloc = nVarsAlloc;
00166     p->nVars     = 0;
00167 
00168     p->nClauses  = 0;
00169     p->vClauses  = Msat_ClauseVecAlloc( 512 );
00170     p->vLearned  = Msat_ClauseVecAlloc( 512 );
00171 
00172     p->dClaInc   = dClaInc;
00173     p->dClaDecay = dClaDecay;
00174     p->dVarInc   = dVarInc;
00175     p->dVarDecay = dVarDecay;
00176 
00177     p->pdActivity = ALLOC( double, p->nVarsAlloc );
00178     p->pFactors   = ALLOC( float, p->nVarsAlloc );
00179     for ( i = 0; i < p->nVarsAlloc; i++ )
00180     {
00181         p->pdActivity[i] = 0.0;
00182         p->pFactors[i]   = 1.0;
00183     }
00184 
00185     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
00186     p->pModel    = ALLOC( int, p->nVarsAlloc ); 
00187     for ( i = 0; i < p->nVarsAlloc; i++ )
00188         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00189 //    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
00190     p->pOrder    = Msat_OrderAlloc( p );
00191 
00192     p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
00193     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
00194         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
00195     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
00196 
00197     p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
00198     p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
00199     p->pReasons  = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
00200     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
00201     p->pLevel = ALLOC( int, p->nVarsAlloc );
00202     for ( i = 0; i < p->nVarsAlloc; i++ )
00203         p->pLevel[i] = -1;
00204     p->dRandSeed = 91648253;
00205     p->fVerbose  = fVerbose;
00206     p->dProgress = 0.0;
00207 //    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
00208     p->pMem = Msat_MmStepStart( 10 );
00209 
00210     p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
00211     p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
00212     for ( i = 0; i < p->nVarsAlloc; i++ )
00213         Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
00214     p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
00215     Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
00216 
00217 
00218     p->pSeen     = ALLOC( int, p->nVarsAlloc );
00219     memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
00220     p->nSeenId   = 1;
00221     p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
00222     p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
00223     return p;
00224 }

void Msat_SolverClean ( Msat_Solver_t *  p,
int  nVars 
)

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 []

Definition at line 304 of file msatSolverApi.c.

00305 {
00306     int i;
00307     // free the clauses
00308     int nClauses;
00309     Msat_Clause_t ** pClauses;
00310 
00311     assert( p->nVarsAlloc >= nVars );
00312     p->nVars    = nVars;
00313     p->nClauses = 0;
00314 
00315     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00316     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00317     for ( i = 0; i < nClauses; i++ )
00318         Msat_ClauseFree( p, pClauses[i], 0 );
00319 //    Msat_ClauseVecFree( p->vClauses );
00320     Msat_ClauseVecClear( p->vClauses );
00321 
00322     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00323     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00324     for ( i = 0; i < nClauses; i++ )
00325         Msat_ClauseFree( p, pClauses[i], 0 );
00326 //    Msat_ClauseVecFree( p->vLearned );
00327     Msat_ClauseVecClear( p->vLearned );
00328 
00329 //    FREE( p->pdActivity );
00330     for ( i = 0; i < p->nVars; i++ )
00331         p->pdActivity[i] = 0;
00332 
00333 //    Msat_OrderFree( p->pOrder );
00334 //    Msat_OrderClean( p->pOrder, p->nVars, NULL );
00335     Msat_OrderSetBounds( p->pOrder, p->nVars );
00336 
00337     for ( i = 0; i < 2 * p->nVars; i++ )
00338 //        Msat_ClauseVecFree( p->pvWatched[i] );
00339         Msat_ClauseVecClear( p->pvWatched[i] );
00340 //    FREE( p->pvWatched );
00341 //    Msat_QueueFree( p->pQueue );
00342     Msat_QueueClear( p->pQueue );
00343 
00344 //    FREE( p->pAssigns );
00345     for ( i = 0; i < p->nVars; i++ )
00346         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00347 //    Msat_IntVecFree( p->vTrail );
00348     Msat_IntVecClear( p->vTrail );
00349 //    Msat_IntVecFree( p->vTrailLim );
00350     Msat_IntVecClear( p->vTrailLim );
00351 //    FREE( p->pReasons );
00352     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
00353 //    FREE( p->pLevel );
00354     for ( i = 0; i < p->nVars; i++ )
00355         p->pLevel[i] = -1;
00356 //    Msat_IntVecFree( p->pModel );
00357 //    Msat_MmStepStop( p->pMem, 0 );
00358     p->dRandSeed = 91648253;
00359     p->dProgress = 0.0;
00360 
00361 //    FREE( p->pSeen );
00362     memset( p->pSeen, 0, sizeof(int) * p->nVars );
00363     p->nSeenId = 1;
00364 //    Msat_IntVecFree( p->vReason );
00365     Msat_IntVecClear( p->vReason );
00366 //    Msat_IntVecFree( p->vTemp );
00367     Msat_IntVecClear( p->vTemp );
00368 //    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
00369 //    FREE( p );
00370 }

void Msat_SolverFree ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Frees the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file msatSolverApi.c.

00384 {
00385     int i;
00386 
00387     // free the clauses
00388     int nClauses;
00389     Msat_Clause_t ** pClauses;
00390 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
00391 //                                         Msat_ClauseVecReadSize( p->vLearned ) );
00392 
00393     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00394     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00395     for ( i = 0; i < nClauses; i++ )
00396         Msat_ClauseFree( p, pClauses[i], 0 );
00397     Msat_ClauseVecFree( p->vClauses );
00398 
00399     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00400     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00401     for ( i = 0; i < nClauses; i++ )
00402         Msat_ClauseFree( p, pClauses[i], 0 );
00403     Msat_ClauseVecFree( p->vLearned );
00404 
00405     FREE( p->pdActivity );
00406     FREE( p->pFactors );
00407     Msat_OrderFree( p->pOrder );
00408 
00409     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
00410         Msat_ClauseVecFree( p->pvWatched[i] );
00411     FREE( p->pvWatched );
00412     Msat_QueueFree( p->pQueue );
00413 
00414     FREE( p->pAssigns );
00415     FREE( p->pModel );
00416     Msat_IntVecFree( p->vTrail );
00417     Msat_IntVecFree( p->vTrailLim );
00418     FREE( p->pReasons );
00419     FREE( p->pLevel );
00420 
00421     Msat_MmStepStop( p->pMem, 0 );
00422 
00423     nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
00424     pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
00425     for ( i = 0; i < nClauses; i++ )
00426         Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
00427     Msat_ClauseVecFree( p->vAdjacents );
00428     Msat_IntVecFree( p->vConeVars );
00429     Msat_IntVecFree( p->vVarsUsed );
00430 
00431     FREE( p->pSeen );
00432     Msat_IntVecFree( p->vReason );
00433     Msat_IntVecFree( p->vTemp );
00434     FREE( p );
00435 }

void Msat_SolverMarkClausesStart ( Msat_Solver_t *  p  ) 

Definition at line 66 of file msatSolverApi.c.

00066 { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }

void Msat_SolverMarkLastClauseTypeA ( Msat_Solver_t *  p  ) 

Definition at line 65 of file msatSolverApi.c.

00065 { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }

bool Msat_SolverParseDimacs ( FILE *  pFile,
Msat_Solver_t **  p,
int  fVerbose 
)

GLOBAL VARIABLES /// MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

Function*************************************************************

Synopsis [Starts the solver and reads the DIMAC file.]

Description [Returns FALSE upon immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 254 of file msatRead.c.

00255 {
00256     char * pText;
00257     bool Value;
00258     pText = Msat_FileRead( pFile );
00259     Value = Msat_ReadDimacs( pText, p, fVerbose );
00260     free( pText );
00261     return Value;
00262 }

void Msat_SolverPrepare ( Msat_Solver_t *  p,
Msat_IntVec_t *  vVars 
)

Function*************************************************************

Synopsis [Prepares the solver to run on a subset of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file msatSolverApi.c.

00449 {
00450 
00451     int i;
00452     // undo the previous data
00453     for ( i = 0; i < p->nVarsAlloc; i++ )
00454     {
00455         p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
00456         p->pReasons[i]   = NULL;
00457         p->pLevel[i]     = -1;
00458         p->pdActivity[i] = 0.0;
00459     }
00460 
00461     // set the new variable order
00462     Msat_OrderClean( p->pOrder, vVars );
00463 
00464     Msat_QueueClear( p->pQueue );
00465     Msat_IntVecClear( p->vTrail );
00466     Msat_IntVecClear( p->vTrailLim );
00467     p->dProgress = 0.0;
00468 }

void Msat_SolverPrintAssignment ( Msat_Solver_t *  p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file msatSolverIo.c.

00045 {
00046     int i;
00047     printf( "Current assignments are: \n" );
00048     for ( i = 0; i < p->nVars; i++ )
00049         printf( "%d", i % 10 );
00050     printf( "\n" );
00051     for ( i = 0; i < p->nVars; i++ )
00052         if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
00053             printf( "." );
00054         else
00055         {
00056             assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
00057             if ( MSAT_LITSIGN(p->pAssigns[i]) )
00058                 printf( "0" );
00059             else 
00060                 printf( "1" );
00061         }
00062     printf( "\n" );
00063 }

void Msat_SolverPrintClauses ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file msatSolverIo.c.

00077 {
00078     Msat_Clause_t ** pClauses;
00079     int nClauses, i;
00080 
00081     printf( "Original clauses: \n" );
00082     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00083     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00084     for ( i = 0; i < nClauses; i++ )
00085     {
00086         printf( "%3d: ", i );
00087         Msat_ClausePrint( pClauses[i] );
00088     }
00089 
00090     printf( "Learned clauses: \n" );
00091     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00092     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00093     for ( i = 0; i < nClauses; i++ )
00094     {
00095         printf( "%3d: ", i );
00096         Msat_ClausePrint( pClauses[i] );
00097     }
00098 
00099     printf( "Variable activity: \n" );
00100     for ( i = 0; i < p->nVars; i++ )
00101         printf( "%3d : %.4f\n", i, p->pdActivity[i] );
00102 }

void Msat_SolverPrintStats ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Prints statistics about the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file msatSolverCore.c.

00108 {
00109     printf("C solver (%d vars; %d clauses; %d learned):\n", 
00110         p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
00111     printf("starts        : %lld\n", p->Stats.nStarts);
00112     printf("conflicts     : %lld\n", p->Stats.nConflicts);
00113     printf("decisions     : %lld\n", p->Stats.nDecisions);
00114     printf("propagations  : %lld\n", p->Stats.nPropagations);
00115     printf("inspects      : %lld\n", p->Stats.nInspects);
00116 }

Msat_ClauseVec_t* Msat_SolverReadAdjacents ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file msatSolverApi.c.

00102 {
00103     return p->vAdjacents;
00104 }

int* Msat_SolverReadAssignsArray ( Msat_Solver_t *  p  ) 

Definition at line 53 of file msatSolverApi.c.

00053 { return p->pAssigns;   }

int Msat_SolverReadBackTracks ( Msat_Solver_t *  p  ) 

Definition at line 55 of file msatSolverApi.c.

00055 { return (int)p->Stats.nConflicts; }

int Msat_SolverReadClauseNum ( Msat_Solver_t *  p  ) 

Definition at line 45 of file msatSolverApi.c.

00045 { return p->nClauses;   }

Msat_IntVec_t* Msat_SolverReadConeVars ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatSolverApi.c.

00118 {
00119     return p->vConeVars;
00120 }

float* Msat_SolverReadFactors ( Msat_Solver_t *  p  ) 

Definition at line 67 of file msatSolverApi.c.

00067 { return p->pFactors;   }

int Msat_SolverReadInspects ( Msat_Solver_t *  p  ) 

Definition at line 56 of file msatSolverApi.c.

00056 { return (int)p->Stats.nInspects;  }

int* Msat_SolverReadModelArray ( Msat_Solver_t *  p  ) 

Definition at line 54 of file msatSolverApi.c.

00054 { return p->pModel;     }

int Msat_SolverReadSolutions ( Msat_Solver_t *  p  ) 
int* Msat_SolverReadSolutionsArray ( Msat_Solver_t *  p  ) 
unsigned Msat_SolverReadTruth ( Msat_Solver_t *  p  ) 
int Msat_SolverReadVarAllocNum ( Msat_Solver_t *  p  ) 

Definition at line 46 of file msatSolverApi.c.

00046 { return p->nVarsAlloc; }

int Msat_SolverReadVarNum ( Msat_Solver_t *  p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Simple SAT solver APIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file msatSolverApi.c.

00044 { return p->nVars;      }

Msat_IntVec_t* Msat_SolverReadVarsUsed ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatSolverApi.c.

00134 {
00135     return p->vVarsUsed;
00136 }

void Msat_SolverRemoveLearned ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Removes the learned clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file msatSolverSearch.c.

00369 {
00370     Msat_Clause_t ** pLearned;
00371     int nLearned, i;
00372 
00373     // discard the learned clauses
00374     nLearned = Msat_ClauseVecReadSize( p->vLearned );
00375     pLearned = Msat_ClauseVecReadArray( p->vLearned );
00376     for ( i = 0; i < nLearned; i++ )
00377     {
00378         assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
00379         
00380         Msat_ClauseFree( p, pLearned[i], 1 );
00381     }
00382     Msat_ClauseVecShrink( p->vLearned, 0 );
00383     p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
00384 
00385     for ( i = 0; i < p->nVarsAlloc; i++ )
00386         p->pReasons[i] = NULL;
00387 }

void Msat_SolverRemoveMarked ( Msat_Solver_t *  p  ) 

Function*************************************************************

Synopsis [Removes the recently added clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 400 of file msatSolverSearch.c.

00401 {
00402     Msat_Clause_t ** pLearned, ** pClauses;
00403     int nLearned, nClauses, i;
00404 
00405     // discard the learned clauses
00406     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00407     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00408     for ( i = p->nClausesStart; i < nClauses; i++ )
00409     {
00410 //        assert( !Msat_ClauseIsLocked( p, pClauses[i]) );
00411         Msat_ClauseFree( p, pClauses[i], 1 );
00412     }
00413     Msat_ClauseVecShrink( p->vClauses, p->nClausesStart );
00414 
00415     // discard the learned clauses
00416     nLearned = Msat_ClauseVecReadSize( p->vLearned );
00417     pLearned = Msat_ClauseVecReadArray( p->vLearned );
00418     for ( i = 0; i < nLearned; i++ )
00419     {
00420 //        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
00421         Msat_ClauseFree( p, pLearned[i], 1 );
00422     }
00423     Msat_ClauseVecShrink( p->vLearned, 0 );
00424     p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
00425 /*
00426     // undo the previous data
00427     for ( i = 0; i < p->nVarsAlloc; i++ )
00428     {
00429         p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
00430         p->pReasons[i]   = NULL;
00431         p->pLevel[i]     = -1;
00432         p->pdActivity[i] = 0.0;
00433     }
00434     Msat_OrderClean( p->pOrder, p->nVars, NULL );
00435     Msat_QueueClear( p->pQueue );
00436 */
00437 }

void Msat_SolverResize ( Msat_Solver_t *  p,
int  nVarsAlloc 
)

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 []

Definition at line 239 of file msatSolverApi.c.

00240 {
00241     int nVarsAllocOld, i;
00242 
00243     nVarsAllocOld = p->nVarsAlloc;
00244     p->nVarsAlloc = nVarsAlloc;
00245 
00246     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
00247     p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
00248     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00249     {
00250         p->pdActivity[i] = 0.0;
00251         p->pFactors[i]   = 1.0;
00252     }
00253 
00254     p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
00255     p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
00256     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00257         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
00258 
00259 //    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
00260     Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
00261 
00262     p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
00263     for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
00264         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
00265 
00266     Msat_QueueFree( p->pQueue );
00267     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
00268 
00269     p->pReasons  = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
00270     p->pLevel    = REALLOC( int, p->pLevel, p->nVarsAlloc );
00271     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00272     {
00273         p->pReasons[i] = NULL;
00274         p->pLevel[i] = -1;
00275     }
00276 
00277     p->pSeen     = REALLOC( int, p->pSeen, p->nVarsAlloc );
00278     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
00279         p->pSeen[i] = 0;
00280 
00281     Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
00282     Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
00283 
00284     // make sure the array of adjucents has room to store the variable numbers
00285     for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
00286         Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
00287     Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
00288 }

void Msat_SolverSetProofWriting ( Msat_Solver_t *  p,
int  fProof 
)
void Msat_SolverSetVarMap ( Msat_Solver_t *  p,
Msat_IntVec_t *  vVarMap 
)
void Msat_SolverSetVarTypeA ( Msat_Solver_t *  p,
int  Var 
)
void Msat_SolverSetVerbosity ( Msat_Solver_t *  p,
int  fVerbose 
)

Definition at line 60 of file msatSolverApi.c.

00060 { p->fVerbose = fVerbose; }

bool Msat_SolverSimplifyDB ( Msat_Solver_t *  p  ) 

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 []

Definition at line 279 of file msatSolverSearch.c.

00280 {
00281     Msat_ClauseVec_t * vClauses;
00282     Msat_Clause_t ** pClauses;
00283     int nClauses, Type, i, j;
00284     int * pAssigns;
00285     int Counter;
00286 
00287     assert( Msat_SolverReadDecisionLevel(p) == 0 );
00288     if ( Msat_SolverPropagate(p) != NULL )
00289         return 0;
00290 //Msat_SolverPrintClauses( p );
00291 //Msat_SolverPrintAssignment( p );
00292 //printf( "Simplification\n" );
00293 
00294     // simplify and reassign clause numbers
00295     Counter = 0;
00296     pAssigns = Msat_SolverReadAssignsArray( p );
00297     for ( Type = 0; Type < 2; Type++ )
00298     {
00299         vClauses = Type? p->vLearned : p->vClauses;
00300         nClauses = Msat_ClauseVecReadSize( vClauses );
00301         pClauses = Msat_ClauseVecReadArray( vClauses );
00302         for ( i = j = 0; i < nClauses; i++ )
00303             if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) )
00304                 Msat_ClauseFree( p, pClauses[i], 1 );
00305             else
00306             {
00307                 pClauses[j++] = pClauses[i];
00308                 Msat_ClauseSetNum( pClauses[i], Counter++ );
00309             }
00310         Msat_ClauseVecShrink( vClauses, j );
00311     }
00312     p->nClauses = Counter;
00313     return 1;
00314 }

bool Msat_SolverSolve ( Msat_Solver_t *  p,
Msat_IntVec_t *  vAssumps,
int  nBackTrackLimit,
int  nTimeLimit 
)

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 []

Definition at line 135 of file msatSolverCore.c.

00136 {
00137     Msat_SearchParams_t Params = { 0.95, 0.999 };
00138     double nConflictsLimit, nLearnedLimit;
00139     Msat_Type_t Status;
00140     int timeStart = clock();
00141     int64 nConflictsOld = p->Stats.nConflicts;
00142     int64 nDecisionsOld = p->Stats.nDecisions;
00143 
00144 //    p->pFreq = ALLOC( int, p->nVarsAlloc );
00145 //    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
00146  
00147     if ( vAssumps )
00148     {
00149         int * pAssumps, nAssumps, i;
00150 
00151         assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );
00152 
00153         nAssumps = Msat_IntVecReadSize( vAssumps );
00154         pAssumps = Msat_IntVecReadArray( vAssumps );
00155         for ( i = 0; i < nAssumps; i++ )
00156         {
00157             if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
00158             {
00159                 Msat_QueueClear( p->pQueue );
00160                 Msat_SolverCancelUntil( p, 0 );
00161                 return MSAT_FALSE;
00162             }
00163         }
00164     }
00165     p->nLevelRoot   = Msat_SolverReadDecisionLevel(p);
00166     p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );    
00167     nConflictsLimit = 100;
00168     nLearnedLimit   = Msat_ClauseVecReadSize(p->vClauses) / 3;
00169     Status = MSAT_UNKNOWN;
00170     p->nBackTracks = (int)p->Stats.nConflicts;
00171     while ( Status == MSAT_UNKNOWN )
00172     {
00173         if ( p->fVerbose )
00174             printf("Solving -- conflicts=%d   learnts=%d   progress=%.4f %%\n", 
00175                 (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
00176         Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
00177         nConflictsLimit *= 1.5;
00178         nLearnedLimit   *= 1.1;
00179         // if the limit on the number of backtracks is given, quit the restart loop
00180         if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
00181             break;
00182         // if the runtime limit is exceeded, quit the restart loop
00183         if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
00184             break;
00185     }
00186     Msat_SolverCancelUntil( p, 0 );
00187     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
00188 /*
00189     PRT( "True solver runtime", clock() - timeStart );
00190     // print the statistics
00191     {
00192         int i, Counter = 0;
00193         for ( i = 0; i < p->nVars; i++ )
00194             if ( p->pFreq[i] > 0 )
00195             {
00196                 printf( "%d ", p->pFreq[i] );
00197                 Counter++;
00198             }
00199         if ( Counter )
00200             printf( "\n" );
00201         printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
00202         PRT( "Time", clock() - timeStart );
00203     }
00204 */
00205     return Status;
00206 }

void Msat_SolverWriteDimacs ( Msat_Solver_t *  p,
char *  pFileName 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file msatSolverIo.c.

00116 {
00117     FILE * pFile;
00118     Msat_Clause_t ** pClauses;
00119     int nClauses, i;
00120 
00121     nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
00122     for ( i = 0; i < p->nVars; i++ )
00123         nClauses += ( p->pLevel[i] == 0 );
00124 
00125     pFile = fopen( pFileName, "wb" );
00126     fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
00127     fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );
00128 
00129     nClauses = Msat_ClauseVecReadSize( p->vClauses );
00130     pClauses = Msat_ClauseVecReadArray( p->vClauses );
00131     for ( i = 0; i < nClauses; i++ )
00132         Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
00133 
00134     nClauses = Msat_ClauseVecReadSize( p->vLearned );
00135     pClauses = Msat_ClauseVecReadArray( p->vLearned );
00136     for ( i = 0; i < nClauses; i++ )
00137         Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
00138 
00139     // write zero-level assertions
00140     for ( i = 0; i < p->nVars; i++ )
00141         if ( p->pLevel[i] == 0 )
00142             fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );
00143 
00144     fprintf( pFile, "\n" );
00145     fclose( pFile );
00146 }

Msat_VarHeap_t* Msat_VarHeapAlloc (  ) 
void Msat_VarHeapCheck ( Msat_VarHeap_t *  p  ) 
void Msat_VarHeapCheckOne ( Msat_VarHeap_t *  p,
int  iVar 
)
int Msat_VarHeapContainsVar ( Msat_VarHeap_t *  p,
int  iVar 
)
int Msat_VarHeapCountNodes ( Msat_VarHeap_t *  p,
double  WeightLimit 
)
void Msat_VarHeapDelete ( Msat_VarHeap_t *  p,
int  iVar 
)
int Msat_VarHeapGetMax ( Msat_VarHeap_t *  p  ) 
void Msat_VarHeapGrow ( Msat_VarHeap_t *  p,
int  nSize 
)
void Msat_VarHeapInsert ( Msat_VarHeap_t *  p,
int  iVar 
)
void Msat_VarHeapPrint ( FILE *  pFile,
Msat_VarHeap_t *  p 
)
int Msat_VarHeapReadMax ( Msat_VarHeap_t *  p  ) 
double Msat_VarHeapReadMaxWeight ( Msat_VarHeap_t *  p  ) 
void Msat_VarHeapSetActivity ( Msat_VarHeap_t *  p,
double *  pActivity 
)
void Msat_VarHeapStart ( Msat_VarHeap_t *  p,
int *  pVars,
int  nVars,
int  nVarsAlloc 
)
void Msat_VarHeapStop ( Msat_VarHeap_t *  p  ) 
void Msat_VarHeapUpdate ( Msat_VarHeap_t *  p,
int  iVar 
)
Generated on Tue Jan 5 12:19:39 2010 for abc70930 by  doxygen 1.6.1