src/sat/msat/msatInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include <math.h>
#include "msat.h"
Include dependency graph for msatInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Msat_SolverStats_t_
struct  Msat_SearchParams_t_
struct  Msat_Solver_t_
struct  Msat_ClauseVec_t_
struct  Msat_IntVec_t_

Defines

#define PRT(a, t)   printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
#define ALLOC(type, num)   ((type *) malloc(sizeof(type) * (num)))
#define REALLOC(type, obj, num)
#define FREE(obj)   ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
#define MSAT_VAR_UNASSIGNED   (-1)
#define MSAT_LIT_UNASSIGNED   (-2)
#define MSAT_ORDER_UNKNOWN   (-3)
#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

Typedefs

typedef long long int64
typedef struct Msat_Clause_t_ Msat_Clause_t
typedef struct Msat_Queue_t_ Msat_Queue_t
typedef struct Msat_Order_t_ Msat_Order_t
typedef struct Msat_MmFixed_t_ Msat_MmFixed_t
typedef struct Msat_MmFlex_t_ Msat_MmFlex_t
typedef struct Msat_MmStep_t_ Msat_MmStep_t
typedef int Msat_Lit_t
typedef int Msat_Var_t
typedef struct Msat_SolverStats_t_ Msat_SolverStats_t
typedef struct Msat_SearchParams_t_ Msat_SearchParams_t

Functions

void Msat_SolverVarDecayActivity (Msat_Solver_t *p)
void Msat_SolverVarRescaleActivity (Msat_Solver_t *p)
void Msat_SolverClaDecayActivity (Msat_Solver_t *p)
void Msat_SolverClaRescaleActivity (Msat_Solver_t *p)
Msat_Clause_t * Msat_SolverReadClause (Msat_Solver_t *p, int Num)
int Msat_SolverReadDecisionLevel (Msat_Solver_t *p)
int * Msat_SolverReadDecisionLevelArray (Msat_Solver_t *p)
Msat_Clause_t ** Msat_SolverReadReasonArray (Msat_Solver_t *p)
Msat_Type_t Msat_SolverReadVarValue (Msat_Solver_t *p, Msat_Var_t Var)
Msat_ClauseVec_t * Msat_SolverReadLearned (Msat_Solver_t *p)
Msat_ClauseVec_t ** Msat_SolverReadWatchedArray (Msat_Solver_t *p)
int * Msat_SolverReadSeenArray (Msat_Solver_t *p)
int Msat_SolverIncrementSeenId (Msat_Solver_t *p)
Msat_MmStep_t * Msat_SolverReadMem (Msat_Solver_t *p)
void Msat_SolverClausesIncrement (Msat_Solver_t *p)
void Msat_SolverClausesDecrement (Msat_Solver_t *p)
void Msat_SolverClausesIncrementL (Msat_Solver_t *p)
void Msat_SolverClausesDecrementL (Msat_Solver_t *p)
void Msat_SolverVarBumpActivity (Msat_Solver_t *p, Msat_Lit_t Lit)
void Msat_SolverClaBumpActivity (Msat_Solver_t *p, Msat_Clause_t *pC)
bool Msat_SolverEnqueue (Msat_Solver_t *p, Msat_Lit_t Lit, Msat_Clause_t *pC)
double Msat_SolverProgressEstimate (Msat_Solver_t *p)
bool Msat_SolverAssume (Msat_Solver_t *p, Msat_Lit_t Lit)
Msat_Clause_t * Msat_SolverPropagate (Msat_Solver_t *p)
void Msat_SolverCancelUntil (Msat_Solver_t *p, int Level)
Msat_Type_t Msat_SolverSearch (Msat_Solver_t *p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t *pPars)
Msat_Queue_t * Msat_QueueAlloc (int nVars)
void Msat_QueueFree (Msat_Queue_t *p)
int Msat_QueueReadSize (Msat_Queue_t *p)
void Msat_QueueInsert (Msat_Queue_t *p, int Lit)
int Msat_QueueExtract (Msat_Queue_t *p)
void Msat_QueueClear (Msat_Queue_t *p)
Msat_Order_t * Msat_OrderAlloc (Msat_Solver_t *pSat)
void Msat_OrderSetBounds (Msat_Order_t *p, int nVarsMax)
void Msat_OrderClean (Msat_Order_t *p, Msat_IntVec_t *vCone)
int Msat_OrderCheck (Msat_Order_t *p)
void Msat_OrderFree (Msat_Order_t *p)
int Msat_OrderVarSelect (Msat_Order_t *p)
void Msat_OrderVarAssigned (Msat_Order_t *p, int Var)
void Msat_OrderVarUnassigned (Msat_Order_t *p, int Var)
void Msat_OrderUpdate (Msat_Order_t *p, int Var)
bool Msat_ClauseCreate (Msat_Solver_t *p, Msat_IntVec_t *vLits, bool fLearnt, Msat_Clause_t **pClause_out)
Msat_Clause_t * Msat_ClauseCreateFake (Msat_Solver_t *p, Msat_IntVec_t *vLits)
Msat_Clause_t * Msat_ClauseCreateFakeLit (Msat_Solver_t *p, Msat_Lit_t Lit)
bool Msat_ClauseReadLearned (Msat_Clause_t *pC)
int Msat_ClauseReadSize (Msat_Clause_t *pC)
int * Msat_ClauseReadLits (Msat_Clause_t *pC)
bool Msat_ClauseReadMark (Msat_Clause_t *pC)
void Msat_ClauseSetMark (Msat_Clause_t *pC, bool fMark)
int Msat_ClauseReadNum (Msat_Clause_t *pC)
void Msat_ClauseSetNum (Msat_Clause_t *pC, int Num)
bool Msat_ClauseReadTypeA (Msat_Clause_t *pC)
void Msat_ClauseSetTypeA (Msat_Clause_t *pC, bool fTypeA)
bool Msat_ClauseIsLocked (Msat_Solver_t *p, Msat_Clause_t *pC)
float Msat_ClauseReadActivity (Msat_Clause_t *pC)
void Msat_ClauseWriteActivity (Msat_Clause_t *pC, float Num)
void Msat_ClauseFree (Msat_Solver_t *p, Msat_Clause_t *pC, bool fRemoveWatched)
bool Msat_ClausePropagate (Msat_Clause_t *pC, Msat_Lit_t Lit, int *pAssigns, Msat_Lit_t *pLit_out)
bool Msat_ClauseSimplify (Msat_Clause_t *pC, int *pAssigns)
void Msat_ClauseCalcReason (Msat_Solver_t *p, Msat_Clause_t *pC, Msat_Lit_t Lit, Msat_IntVec_t *vLits_out)
void Msat_ClauseRemoveWatch (Msat_ClauseVec_t *vClauses, Msat_Clause_t *pC)
void Msat_ClausePrint (Msat_Clause_t *pC)
void Msat_ClausePrintSymbols (Msat_Clause_t *pC)
void Msat_ClauseWriteDimacs (FILE *pFile, Msat_Clause_t *pC, bool fIncrement)
unsigned Msat_ClauseComputeTruth (Msat_Solver_t *p, Msat_Clause_t *pC)
void Msat_SolverSortDB (Msat_Solver_t *p)
Msat_ClauseVec_t * Msat_ClauseVecAlloc (int nCap)
void Msat_ClauseVecFree (Msat_ClauseVec_t *p)
Msat_Clause_t ** Msat_ClauseVecReadArray (Msat_ClauseVec_t *p)
int Msat_ClauseVecReadSize (Msat_ClauseVec_t *p)
void Msat_ClauseVecGrow (Msat_ClauseVec_t *p, int nCapMin)
void Msat_ClauseVecShrink (Msat_ClauseVec_t *p, int nSizeNew)
void Msat_ClauseVecClear (Msat_ClauseVec_t *p)
void Msat_ClauseVecPush (Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
Msat_Clause_t * Msat_ClauseVecPop (Msat_ClauseVec_t *p)
void Msat_ClauseVecWriteEntry (Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
Msat_Clause_t * Msat_ClauseVecReadEntry (Msat_ClauseVec_t *p, int i)
Msat_MmFixed_t * Msat_MmFixedStart (int nEntrySize)
void Msat_MmFixedStop (Msat_MmFixed_t *p, int fVerbose)
char * Msat_MmFixedEntryFetch (Msat_MmFixed_t *p)
void Msat_MmFixedEntryRecycle (Msat_MmFixed_t *p, char *pEntry)
void Msat_MmFixedRestart (Msat_MmFixed_t *p)
int Msat_MmFixedReadMemUsage (Msat_MmFixed_t *p)
Msat_MmFlex_t * Msat_MmFlexStart ()
void Msat_MmFlexStop (Msat_MmFlex_t *p, int fVerbose)
char * Msat_MmFlexEntryFetch (Msat_MmFlex_t *p, int nBytes)
int Msat_MmFlexReadMemUsage (Msat_MmFlex_t *p)
Msat_MmStep_t * Msat_MmStepStart (int nSteps)
void Msat_MmStepStop (Msat_MmStep_t *p, int fVerbose)
char * Msat_MmStepEntryFetch (Msat_MmStep_t *p, int nBytes)
void Msat_MmStepEntryRecycle (Msat_MmStep_t *p, char *pEntry, int nBytes)
int Msat_MmStepReadMemUsage (Msat_MmStep_t *p)

Define Documentation

#define ALLOC ( type,
num   )     ((type *) malloc(sizeof(type) * (num)))

Definition at line 56 of file msatInt.h.

#define FREE ( obj   )     ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)

Definition at line 61 of file msatInt.h.

#define L_ind   Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)

Definition at line 89 of file msatInt.h.

#define L_IND   "%-*d"

Definition at line 88 of file msatInt.h.

#define L_lit ( Lit   )     MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1

Definition at line 91 of file msatInt.h.

#define L_LIT   "%s%d"

Definition at line 90 of file msatInt.h.

#define MSAT_LIT_UNASSIGNED   (-2)

Definition at line 84 of file msatInt.h.

#define MSAT_ORDER_UNKNOWN   (-3)

Definition at line 85 of file msatInt.h.

#define MSAT_VAR_UNASSIGNED   (-1)

Definition at line 83 of file msatInt.h.

#define PRT ( a,
t   )     printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )

Definition at line 52 of file msatInt.h.

#define REALLOC ( type,
obj,
num   ) 
Value:
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
            ((type *) malloc(sizeof(type) * (num))))

Definition at line 58 of file msatInt.h.

Typedef Documentation

typedef long long int64

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

FileName [msatInt.c]

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

Synopsis [Internal definitions of the solver.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

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

Definition at line 48 of file msatInt.h.

typedef struct Msat_Clause_t_ Msat_Clause_t

Definition at line 72 of file msatInt.h.

typedef int Msat_Lit_t

Definition at line 80 of file msatInt.h.

typedef struct Msat_MmFixed_t_ Msat_MmFixed_t

Definition at line 76 of file msatInt.h.

typedef struct Msat_MmFlex_t_ Msat_MmFlex_t

Definition at line 77 of file msatInt.h.

typedef struct Msat_MmStep_t_ Msat_MmStep_t

Definition at line 78 of file msatInt.h.

typedef struct Msat_Order_t_ Msat_Order_t

Definition at line 74 of file msatInt.h.

typedef struct Msat_Queue_t_ Msat_Queue_t

Definition at line 73 of file msatInt.h.

typedef struct Msat_SearchParams_t_ Msat_SearchParams_t

Definition at line 104 of file msatInt.h.

typedef struct Msat_SolverStats_t_ Msat_SolverStats_t

Definition at line 93 of file msatInt.h.

typedef int Msat_Var_t

Definition at line 81 of file msatInt.h.

Function Documentation

void Msat_ClauseCalcReason ( Msat_Solver_t *  p,
Msat_Clause_t *  pC,
Msat_Lit_t  Lit,
Msat_IntVec_t *  vLits_out 
)

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

Definition at line 412 of file msatClause.c.

00413 {
00414     int i;
00415     // clear the reason
00416     Msat_IntVecClear( vLits_out );
00417     assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
00418     for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
00419     {
00420         assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
00421         Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
00422     }
00423     if ( pC->fLearned ) 
00424         Msat_SolverClaBumpActivity( p, pC );
00425 }

unsigned Msat_ClauseComputeTruth ( Msat_Solver_t *  p,
Msat_Clause_t *  pC 
)
bool Msat_ClauseCreate ( Msat_Solver_t *  p,
Msat_IntVec_t *  vLits,
bool  fLearned,
Msat_Clause_t **  pClause_out 
)

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

Synopsis [Creates a new clause.]

Description [Returns FALSE if top-level conflict detected (must be handled); TRUE otherwise. 'pClause_out' may be set to NULL if clause is already satisfied by the top-level assignment.]

SideEffects []

SeeAlso []

Definition at line 55 of file msatClause.c.

00056 {
00057     int * pAssigns = Msat_SolverReadAssignsArray(p);
00058     Msat_ClauseVec_t ** pvWatched;
00059     Msat_Clause_t * pC;
00060     int * pLits;
00061     int nLits, i, j;
00062     int nBytes;
00063     Msat_Var_t Var;
00064     bool Sign;
00065 
00066     *pClause_out = NULL;
00067 
00068     nLits = Msat_IntVecReadSize(vLits);
00069     pLits = Msat_IntVecReadArray(vLits);
00070 
00071     if ( !fLearned ) 
00072     {
00073         int * pSeen = Msat_SolverReadSeenArray( p );
00074         int nSeenId;
00075         assert( Msat_SolverReadDecisionLevel(p) == 0 );
00076         // sorting literals makes the code trace-equivalent 
00077         // with to the original C++ solver
00078         Msat_IntVecSort( vLits, 0 );
00079         // increment the counter of seen twice
00080         nSeenId = Msat_SolverIncrementSeenId( p );
00081         nSeenId = Msat_SolverIncrementSeenId( p );
00082         // nSeenId - 1 stands for negative
00083         // nSeenId     stands for positive
00084         // Remove false literals
00085 
00086         // there is a bug here!!!!
00087         // when the same var in opposite polarities is given, it drops one polarity!!!
00088 
00089         for ( i = j = 0; i < nLits; i++ ) {
00090             // get the corresponding variable
00091             Var  = MSAT_LIT2VAR(pLits[i]);
00092             Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
00093             // check if we already saw this variable in the this clause
00094             if ( pSeen[Var] >= nSeenId - 1 )
00095             {
00096                 if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
00097                     continue;
00098                 return 1; // two opposite polarity lits -- don't add the clause
00099             }
00100             // mark the variable as seen
00101             pSeen[Var] = nSeenId - !Sign;
00102 
00103             // analize the value of this literal
00104             if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
00105             {
00106                 if ( pAssigns[Var] == pLits[i] )
00107                     return 1;  // the clause is always true -- don't add anything
00108                 // the literal has no impact - skip it
00109                 continue;
00110             }
00111             // otherwise, add this literal to the clause
00112             pLits[j++] = pLits[i];
00113         }
00114         Msat_IntVecShrink( vLits, j );
00115         nLits = j;
00116 /*
00117         // the problem with this code is that performance is very
00118         // sensitive to the ordering of adjacency lits
00119         // the best ordering requires fanins first, next fanouts
00120         // this ordering is more convenient to make from FRAIG
00121 
00122         // create the adjacency information
00123         if ( nLits > 2 )
00124         {
00125             Msat_Var_t VarI, VarJ;
00126             Msat_IntVec_t * pAdjI, * pAdjJ;
00127 
00128             for ( i = 0; i < nLits; i++ )
00129             {
00130                 VarI = MSAT_LIT2VAR(pLits[i]);
00131                 pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];
00132 
00133                 for ( j = i+1; j < nLits; j++ )
00134                 {
00135                     VarJ = MSAT_LIT2VAR(pLits[j]);
00136                     pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];
00137 
00138                     Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
00139                     Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
00140                 }
00141             }
00142         }
00143 */
00144     }
00145     // 'vLits' is now the (possibly) reduced vector of literals.
00146     if ( nLits == 0 )
00147         return 0;
00148     if ( nLits == 1 )
00149         return Msat_SolverEnqueue( p, pLits[0], NULL );
00150 
00151     // Allocate clause:
00152 //    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
00153     nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
00154 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
00155     pC = (Msat_Clause_t *)ALLOC( char, nBytes );
00156 #else
00157     pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
00158 #endif
00159     pC->Num        = p->nClauses++;
00160     pC->fTypeA     = 0;
00161     pC->fMark      = 0;
00162     pC->fLearned   = fLearned;
00163     pC->nSize      = nLits;
00164     pC->nSizeAlloc = nBytes;
00165     memcpy( pC->pData, pLits, sizeof(int)*nLits );
00166 
00167     // For learnt clauses only:
00168     if ( fLearned )
00169     {
00170         int * pLevel = Msat_SolverReadDecisionLevelArray( p );
00171         int iLevelMax, iLevelCur, iLitMax;
00172 
00173         // Put the second watch on the literal with highest decision level:
00174         iLitMax = 1;
00175         iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
00176         for ( i = 2; i < nLits; i++ )
00177         {
00178             iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
00179             assert( iLevelCur != -1 );
00180             if ( iLevelMax < iLevelCur )
00181             // this is very strange - shouldn't it be???
00182             // if ( iLevelMax > iLevelCur )
00183                 iLevelMax = iLevelCur, iLitMax = i;
00184         }
00185         pC->pData[1]       = pLits[iLitMax];
00186         pC->pData[iLitMax] = pLits[1];
00187 
00188         // Bumping:
00189         // (newly learnt clauses should be considered active)
00190         Msat_ClauseWriteActivity( pC, 0.0 );
00191         Msat_SolverClaBumpActivity( p, pC ); 
00192 //        if ( nLits < 20 )
00193         for ( i = 0; i < nLits; i++ )
00194         {
00195             Msat_SolverVarBumpActivity( p, pLits[i] );
00196 //            Msat_SolverVarBumpActivity( p, pLits[i] );
00197 //            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
00198         }
00199     }
00200 
00201     // Store clause:
00202     pvWatched = Msat_SolverReadWatchedArray( p );
00203     Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
00204     Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
00205     *pClause_out = pC;
00206     return 1;
00207 }

Msat_Clause_t* Msat_ClauseCreateFake ( Msat_Solver_t *  p,
Msat_IntVec_t *  vLits 
)
Msat_Clause_t* Msat_ClauseCreateFakeLit ( Msat_Solver_t *  p,
Msat_Lit_t  Lit 
)
void Msat_ClauseFree ( Msat_Solver_t *  p,
Msat_Clause_t *  pC,
bool  fRemoveWatched 
)

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

Synopsis [Deallocates the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file msatClause.c.

00221 {
00222     if ( fRemoveWatched )
00223     {
00224         Msat_Lit_t Lit;
00225         Msat_ClauseVec_t ** pvWatched;
00226         pvWatched = Msat_SolverReadWatchedArray( p );
00227         Lit = MSAT_LITNOT( pC->pData[0] );
00228         Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
00229         Lit = MSAT_LITNOT( pC->pData[1] );
00230         Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
00231     }
00232 
00233 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
00234     free( pC );
00235 #else
00236     Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
00237 #endif
00238 
00239 }

bool Msat_ClauseIsLocked ( Msat_Solver_t *  p,
Msat_Clause_t *  pC 
)

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

Definition at line 275 of file msatClause.c.

00276 {
00277     Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
00278     return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
00279 }

void Msat_ClausePrint ( Msat_Clause_t *  pC  ) 

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

Synopsis [Prints the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 462 of file msatClause.c.

00463 {
00464     int i;
00465     if ( pC == NULL )
00466         printf( "NULL pointer" );
00467     else 
00468     {
00469         if ( pC->fLearned )
00470             printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
00471         for ( i = 0; i < (int)pC->nSize; i++ )
00472             printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
00473     }
00474     printf( "\n" );
00475 }

void Msat_ClausePrintSymbols ( Msat_Clause_t *  pC  ) 

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

Synopsis [Prints the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 509 of file msatClause.c.

00510 {
00511     int i;
00512     if ( pC == NULL )
00513         printf( "NULL pointer" );
00514     else 
00515     {
00516 //        if ( pC->fLearned )
00517 //            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
00518         for ( i = 0; i < (int)pC->nSize; i++ )
00519             printf(" "L_LIT, L_lit(pC->pData[i]));
00520     }
00521     printf( "\n" );
00522 }

bool Msat_ClausePropagate ( Msat_Clause_t *  pC,
Msat_Lit_t  Lit,
int *  pAssigns,
Msat_Lit_t *  pLit_out 
)

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

Definition at line 329 of file msatClause.c.

00330 {
00331     // make sure the false literal is pC->pData[1]
00332     Msat_Lit_t LitF = MSAT_LITNOT(Lit);
00333     if ( pC->pData[0] == LitF )
00334          pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
00335     assert( pC->pData[1] == LitF );
00336     // if the 0-th watch is true, clause is already satisfied
00337     if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
00338         return 1; 
00339     // look for a new watch
00340     if ( pC->nSize > 2 )
00341     {
00342         int i;
00343         for ( i = 2; i < (int)pC->nSize; i++ )
00344             if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
00345             {
00346                 pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
00347                 *pLit_out = MSAT_LITNOT(pC->pData[1]);
00348                 return 1; 
00349             }
00350     }
00351     // clause is unit under assignment
00352     *pLit_out = pC->pData[0];
00353     return 0;
00354 }

float Msat_ClauseReadActivity ( Msat_Clause_t *  pC  ) 

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

Synopsis [Reads the activity of the given clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file msatClause.c.

00293 {
00294     return *((float *)(pC->pData + pC->nSize));
00295 }

bool Msat_ClauseReadLearned ( Msat_Clause_t *  pC  ) 

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

Synopsis [Access the data field of the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file msatClause.c.

00252 {  return pC->fLearned; }

int* Msat_ClauseReadLits ( Msat_Clause_t *  pC  ) 

Definition at line 254 of file msatClause.c.

00254 {  return pC->pData;    }

bool Msat_ClauseReadMark ( Msat_Clause_t *  pC  ) 

Definition at line 255 of file msatClause.c.

00255 {  return pC->fMark;    }

int Msat_ClauseReadNum ( Msat_Clause_t *  pC  ) 

Definition at line 256 of file msatClause.c.

00256 {  return pC->Num;      }

int Msat_ClauseReadSize ( Msat_Clause_t *  pC  ) 

Definition at line 253 of file msatClause.c.

00253 {  return pC->nSize;    }

bool Msat_ClauseReadTypeA ( Msat_Clause_t *  pC  ) 

Definition at line 257 of file msatClause.c.

00257 {  return pC->fTypeA;    }

void Msat_ClauseRemoveWatch ( Msat_ClauseVec_t *  vClauses,
Msat_Clause_t *  pC 
)

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

Synopsis [Removes the given clause from the watched list.]

Description []

SideEffects []

SeeAlso []

Definition at line 438 of file msatClause.c.

00439 {
00440     Msat_Clause_t ** pClauses;
00441     int nClauses, i;
00442     nClauses = Msat_ClauseVecReadSize( vClauses );
00443     pClauses = Msat_ClauseVecReadArray( vClauses );
00444     for ( i = 0; pClauses[i] != pC; i++ )
00445         assert( i < nClauses );
00446     for (      ; i < nClauses - 1; i++ )
00447         pClauses[i] = pClauses[i+1];
00448     Msat_ClauseVecPop( vClauses );
00449 }

void Msat_ClauseSetMark ( Msat_Clause_t *  pC,
bool  fMark 
)

Definition at line 259 of file msatClause.c.

00259 {  pC->fMark = fMark;   }

void Msat_ClauseSetNum ( Msat_Clause_t *  pC,
int  Num 
)

Definition at line 260 of file msatClause.c.

00260 {  pC->Num = Num;       }

void Msat_ClauseSetTypeA ( Msat_Clause_t *  pC,
bool  fTypeA 
)

Definition at line 261 of file msatClause.c.

00261 {  pC->fTypeA = fTypeA; }

bool Msat_ClauseSimplify ( Msat_Clause_t *  pC,
int *  pAssigns 
)

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

Synopsis [Simplifies the clause.]

Description [Assumes everything has been propagated! (esp. watches in clauses are NOT unsatisfied)]

SideEffects []

SeeAlso []

Definition at line 368 of file msatClause.c.

00369 {
00370     Msat_Var_t Var;
00371     int i, j;
00372     for ( i = j = 0; i < (int)pC->nSize; i++ )
00373     {
00374         Var = MSAT_LIT2VAR(pC->pData[i]);
00375         if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
00376         {
00377             pC->pData[j++] = pC->pData[i];
00378             continue;
00379         }
00380         if ( pAssigns[Var] == pC->pData[i] )
00381             return 1;
00382         // otherwise, the value of the literal is false
00383         // make sure, this literal is not watched
00384         assert( i >= 2 );
00385     }
00386     // if the size has changed, update it and move activity
00387     if ( j < (int)pC->nSize )
00388     {
00389         float Activ = Msat_ClauseReadActivity(pC);
00390         pC->nSize = j;
00391         Msat_ClauseWriteActivity(pC, Activ);
00392     }
00393     return 0;
00394 }

Msat_ClauseVec_t* Msat_ClauseVecAlloc ( int  nCap  ) 

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

FileName [msatClauseVec.c]

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

Synopsis [Procedures working with arrays of SAT clauses.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

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

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file msatClauseVec.c.

00043 {
00044     Msat_ClauseVec_t * p;
00045     p = ALLOC( Msat_ClauseVec_t, 1 );
00046     if ( nCap > 0 && nCap < 16 )
00047         nCap = 16;
00048     p->nSize  = 0;
00049     p->nCap   = nCap;
00050     p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
00051     return p;
00052 }

void Msat_ClauseVecClear ( Msat_ClauseVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file msatClauseVec.c.

00151 {
00152     p->nSize = 0;
00153 }

void Msat_ClauseVecFree ( Msat_ClauseVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file msatClauseVec.c.

00066 {
00067     FREE( p->pArray );
00068     FREE( p );
00069 }

void Msat_ClauseVecGrow ( Msat_ClauseVec_t *  p,
int  nCapMin 
)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file msatClauseVec.c.

00115 {
00116     if ( p->nCap >= nCapMin )
00117         return;
00118     p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
00119     p->nCap   = nCapMin;
00120 }

Msat_Clause_t* Msat_ClauseVecPop ( Msat_ClauseVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file msatClauseVec.c.

00190 {
00191     return p->pArray[--p->nSize];
00192 }

void Msat_ClauseVecPush ( Msat_ClauseVec_t *  p,
Msat_Clause_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file msatClauseVec.c.

00167 {
00168     if ( p->nSize == p->nCap )
00169     {
00170         if ( p->nCap < 16 )
00171             Msat_ClauseVecGrow( p, 16 );
00172         else
00173             Msat_ClauseVecGrow( p, 2 * p->nCap );
00174     }
00175     p->pArray[p->nSize++] = Entry;
00176 }

Msat_Clause_t** Msat_ClauseVecReadArray ( Msat_ClauseVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file msatClauseVec.c.

00083 {
00084     return p->pArray;
00085 }

Msat_Clause_t* Msat_ClauseVecReadEntry ( Msat_ClauseVec_t *  p,
int  i 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file msatClauseVec.c.

00223 {
00224     assert( i >= 0 && i < p->nSize );
00225     return p->pArray[i];
00226 }

int Msat_ClauseVecReadSize ( Msat_ClauseVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file msatClauseVec.c.

00099 {
00100     return p->nSize;
00101 }

void Msat_ClauseVecShrink ( Msat_ClauseVec_t *  p,
int  nSizeNew 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatClauseVec.c.

00134 {
00135     assert( p->nSize >= nSizeNew );
00136     p->nSize = nSizeNew;
00137 }

void Msat_ClauseVecWriteEntry ( Msat_ClauseVec_t *  p,
int  i,
Msat_Clause_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file msatClauseVec.c.

00206 {
00207     assert( i >= 0 && i < p->nSize );
00208     p->pArray[i] = Entry;
00209 }

void Msat_ClauseWriteActivity ( Msat_Clause_t *  pC,
float  Num 
)

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

Synopsis [Sets the activity of the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file msatClause.c.

00309 {
00310     *((float *)(pC->pData + pC->nSize)) = Num;
00311 }

void Msat_ClauseWriteDimacs ( FILE *  pFile,
Msat_Clause_t *  pC,
bool  fIncrement 
)

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

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file msatClause.c.

00489 {
00490     int i;
00491     for ( i = 0; i < (int)pC->nSize; i++ )
00492         fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
00493     if ( fIncrement )
00494         fprintf( pFile, "0" );
00495     fprintf( pFile, "\n" );
00496 }

char* Msat_MmFixedEntryFetch ( Msat_MmFixed_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file msatMem.c.

00159 {
00160     char * pTemp;
00161     int i;
00162 
00163     // check if there are still free entries
00164     if ( p->nEntriesUsed == p->nEntriesAlloc )
00165     { // need to allocate more entries
00166         assert( p->pEntriesFree == NULL );
00167         if ( p->nChunks == p->nChunksAlloc )
00168         {
00169             p->nChunksAlloc *= 2;
00170             p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
00171         }
00172         p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
00173         p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
00174         // transform these entries into a linked list
00175         pTemp = p->pEntriesFree;
00176         for ( i = 1; i < p->nChunkSize; i++ )
00177         {
00178             *((char **)pTemp) = pTemp + p->nEntrySize;
00179             pTemp += p->nEntrySize;
00180         }
00181         // set the last link
00182         *((char **)pTemp) = NULL;
00183         // add the chunk to the chunk storage
00184         p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
00185         // add to the number of entries allocated
00186         p->nEntriesAlloc += p->nChunkSize;
00187     }
00188     // incrememt the counter of used entries
00189     p->nEntriesUsed++;
00190     if ( p->nEntriesMax < p->nEntriesUsed )
00191         p->nEntriesMax = p->nEntriesUsed;
00192     // return the first entry in the free entry list
00193     pTemp = p->pEntriesFree;
00194     p->pEntriesFree = *((char **)pTemp);
00195     return pTemp;
00196 }

void Msat_MmFixedEntryRecycle ( Msat_MmFixed_t *  p,
char *  pEntry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file msatMem.c.

00210 {
00211     // decrement the counter of used entries
00212     p->nEntriesUsed--;
00213     // add the entry to the linked list of free entries
00214     *((char **)pEntry) = p->pEntriesFree;
00215     p->pEntriesFree = pEntry;
00216 }

int Msat_MmFixedReadMemUsage ( Msat_MmFixed_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file msatMem.c.

00268 {
00269     return p->nMemoryAlloc;
00270 }

void Msat_MmFixedRestart ( Msat_MmFixed_t *  p  ) 

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

Synopsis []

Description [Relocates all the memory except the first chunk.]

SideEffects []

SeeAlso []

Definition at line 229 of file msatMem.c.

00230 {
00231     int i;
00232     char * pTemp;
00233 
00234     // deallocate all chunks except the first one
00235     for ( i = 1; i < p->nChunks; i++ )
00236         free( p->pChunks[i] );
00237     p->nChunks = 1;
00238     // transform these entries into a linked list
00239     pTemp = p->pChunks[0];
00240     for ( i = 1; i < p->nChunkSize; i++ )
00241     {
00242         *((char **)pTemp) = pTemp + p->nEntrySize;
00243         pTemp += p->nEntrySize;
00244     }
00245     // set the last link
00246     *((char **)pTemp) = NULL;
00247     // set the free entry list
00248     p->pEntriesFree  = p->pChunks[0];
00249     // set the correct statistics
00250     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
00251     p->nMemoryUsed   = 0;
00252     p->nEntriesAlloc = p->nChunkSize;
00253     p->nEntriesUsed  = 0;
00254 }

Msat_MmFixed_t* Msat_MmFixedStart ( int  nEntrySize  ) 

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

Synopsis [Allocates memory pieces of fixed size.]

Description [The size of the chunk is computed as the minimum of 1024 entries and 64K. Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 90 of file msatMem.c.

00091 {
00092     Msat_MmFixed_t * p;
00093 
00094     p = ALLOC( Msat_MmFixed_t, 1 );
00095     memset( p, 0, sizeof(Msat_MmFixed_t) );
00096 
00097     p->nEntrySize    = nEntrySize;
00098     p->nEntriesAlloc = 0;
00099     p->nEntriesUsed  = 0;
00100     p->pEntriesFree  = NULL;
00101 
00102     if ( nEntrySize * (1 << 10) < (1<<16) )
00103         p->nChunkSize = (1 << 10);
00104     else
00105         p->nChunkSize = (1<<16) / nEntrySize;
00106     if ( p->nChunkSize < 8 )
00107         p->nChunkSize = 8;
00108 
00109     p->nChunksAlloc  = 64;
00110     p->nChunks       = 0;
00111     p->pChunks       = ALLOC( char *, p->nChunksAlloc );
00112 
00113     p->nMemoryUsed   = 0;
00114     p->nMemoryAlloc  = 0;
00115     return p;
00116 }

void Msat_MmFixedStop ( Msat_MmFixed_t *  p,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file msatMem.c.

00130 {
00131     int i;
00132     if ( p == NULL )
00133         return;
00134     if ( fVerbose )
00135     {
00136         printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
00137             p->nEntrySize, p->nChunkSize, p->nChunks );
00138         printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
00139             p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
00140     }
00141     for ( i = 0; i < p->nChunks; i++ )
00142         free( p->pChunks[i] );
00143     free( p->pChunks );
00144     free( p );
00145 }

char* Msat_MmFlexEntryFetch ( Msat_MmFlex_t *  p,
int  nBytes 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file msatMem.c.

00347 {
00348     char * pTemp;
00349     // check if there are still free entries
00350     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
00351     { // need to allocate more entries
00352         if ( p->nChunks == p->nChunksAlloc )
00353         {
00354             p->nChunksAlloc *= 2;
00355             p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
00356         }
00357         if ( nBytes > p->nChunkSize )
00358         {
00359             // resize the chunk size if more memory is requested than it can give
00360             // (ideally, this should never happen)
00361             p->nChunkSize = 2 * nBytes;
00362         }
00363         p->pCurrent = ALLOC( char, p->nChunkSize );
00364         p->pEnd     = p->pCurrent + p->nChunkSize;
00365         p->nMemoryAlloc += p->nChunkSize;
00366         // add the chunk to the chunk storage
00367         p->pChunks[ p->nChunks++ ] = p->pCurrent;
00368     }
00369     assert( p->pCurrent + nBytes <= p->pEnd );
00370     // increment the counter of used entries
00371     p->nEntriesUsed++;
00372     // keep track of the memory used
00373     p->nMemoryUsed += nBytes;
00374     // return the next entry
00375     pTemp = p->pCurrent;
00376     p->pCurrent += nBytes;
00377     return pTemp;
00378 }

int Msat_MmFlexReadMemUsage ( Msat_MmFlex_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file msatMem.c.

00392 {
00393     return p->nMemoryAlloc;
00394 }

Msat_MmFlex_t* Msat_MmFlexStart (  ) 

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

Synopsis [Allocates entries of flexible size.]

Description [Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 285 of file msatMem.c.

00286 {
00287     Msat_MmFlex_t * p;
00288 
00289     p = ALLOC( Msat_MmFlex_t, 1 );
00290     memset( p, 0, sizeof(Msat_MmFlex_t) );
00291 
00292     p->nEntriesUsed  = 0;
00293     p->pCurrent      = NULL;
00294     p->pEnd          = NULL;
00295 
00296     p->nChunkSize    = (1 << 12);
00297     p->nChunksAlloc  = 64;
00298     p->nChunks       = 0;
00299     p->pChunks       = ALLOC( char *, p->nChunksAlloc );
00300 
00301     p->nMemoryUsed   = 0;
00302     p->nMemoryAlloc  = 0;
00303     return p;
00304 }

void Msat_MmFlexStop ( Msat_MmFlex_t *  p,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file msatMem.c.

00318 {
00319     int i;
00320     if ( p == NULL )
00321         return;
00322     if ( fVerbose )
00323     {
00324         printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
00325             p->nChunkSize, p->nChunks );
00326         printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
00327             p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
00328     }
00329     for ( i = 0; i < p->nChunks; i++ )
00330         free( p->pChunks[i] );
00331     free( p->pChunks );
00332     free( p );
00333 }

char* Msat_MmStepEntryFetch ( Msat_MmStep_t *  p,
int  nBytes 
)

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

Synopsis [Creates the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file msatMem.c.

00477 {
00478     if ( nBytes == 0 )
00479         return NULL;
00480     if ( nBytes > p->nMapSize )
00481     {
00482 //        printf( "Allocating %d bytes.\n", nBytes );
00483         return ALLOC( char, nBytes );
00484     }
00485     return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
00486 }

void Msat_MmStepEntryRecycle ( Msat_MmStep_t *  p,
char *  pEntry,
int  nBytes 
)

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

Synopsis [Recycles the entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file msatMem.c.

00501 {
00502     if ( nBytes == 0 )
00503         return;
00504     if ( nBytes > p->nMapSize )
00505     {
00506         free( pEntry );
00507         return;
00508     }
00509     Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
00510 }

int Msat_MmStepReadMemUsage ( Msat_MmStep_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file msatMem.c.

00524 {
00525     int i, nMemTotal = 0;
00526     for ( i = 0; i < p->nMems; i++ )
00527         nMemTotal += p->pMems[i]->nMemoryAlloc;
00528     return nMemTotal;
00529 }

Msat_MmStep_t* Msat_MmStepStart ( int  nSteps  ) 

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

Definition at line 420 of file msatMem.c.

00421 {
00422     Msat_MmStep_t * p;
00423     int i, k;
00424     p = ALLOC( Msat_MmStep_t, 1 );
00425     p->nMems = nSteps;
00426     // start the fixed memory managers
00427     p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems );
00428     for ( i = 0; i < p->nMems; i++ )
00429         p->pMems[i] = Msat_MmFixedStart( (8<<i) );
00430     // set up the mapping of the required memory size into the corresponding manager
00431     p->nMapSize = (4<<p->nMems);
00432     p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
00433     p->pMap[0] = NULL;
00434     for ( k = 1; k <= 4; k++ )
00435         p->pMap[k] = p->pMems[0];
00436     for ( i = 0; i < p->nMems; i++ )
00437         for ( k = (4<<i)+1; k <= (8<<i); k++ )
00438             p->pMap[k] = p->pMems[i];
00439 //for ( i = 1; i < 100; i ++ )
00440 //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
00441     return p;
00442 }

void Msat_MmStepStop ( Msat_MmStep_t *  p,
int  fVerbose 
)

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

Synopsis [Stops the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file msatMem.c.

00456 {
00457     int i;
00458     for ( i = 0; i < p->nMems; i++ )
00459         Msat_MmFixedStop( p->pMems[i], fVerbose );
00460     free( p->pMems );
00461     free( p->pMap );
00462     free( p );
00463 }

Msat_Order_t* Msat_OrderAlloc ( Msat_Solver_t *  pSat  ) 

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

Synopsis [Allocates the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file msatOrderH.c.

00076 {
00077     Msat_Order_t * p;
00078     p = ALLOC( Msat_Order_t, 1 );
00079     memset( p, 0, sizeof(Msat_Order_t) );
00080     p->pSat   = pSat;
00081     p->vIndex = Msat_IntVecAlloc( 0 );
00082     p->vHeap  = Msat_IntVecAlloc( 0 );
00083     Msat_OrderSetBounds( p, pSat->nVarsAlloc );
00084     return p;
00085 }

int Msat_OrderCheck ( Msat_Order_t *  p  ) 

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

Synopsis [Checks that the J-boundary is okay.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file msatOrderH.c.

00145 {
00146     return Msat_HeapCheck_rec( p, 1 );
00147 }

void Msat_OrderClean ( Msat_Order_t *  p,
Msat_IntVec_t *  vCone 
)

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

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatOrderH.c.

00118 {
00119     int i;
00120     for ( i = 0; i < p->vIndex->nSize; i++ )
00121         p->vIndex->pArray[i] = 0;
00122     for ( i = 0; i < vCone->nSize; i++ )
00123     {
00124         assert( i+1 < p->vHeap->nCap );
00125         p->vHeap->pArray[i+1] = vCone->pArray[i];
00126 
00127         assert( vCone->pArray[i] < p->vIndex->nSize );
00128         p->vIndex->pArray[vCone->pArray[i]] = i+1;
00129     }
00130     p->vHeap->nSize = vCone->nSize + 1;
00131 }

void Msat_OrderFree ( Msat_Order_t *  p  ) 

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

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file msatOrderH.c.

00161 {
00162     Msat_IntVecFree( p->vHeap );
00163     Msat_IntVecFree( p->vIndex );
00164     free( p );
00165 }

void Msat_OrderSetBounds ( Msat_Order_t *  p,
int  nVarsMax 
)

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

Synopsis [Sets the bound of the ordering structure.]

Description [Should be called whenever the SAT solver is resized.]

SideEffects []

SeeAlso []

Definition at line 98 of file msatOrderH.c.

00099 {
00100     Msat_IntVecGrow( p->vIndex, nVarsMax );
00101     Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
00102     p->vIndex->nSize = nVarsMax;
00103     p->vHeap->nSize = 0;
00104 }

void Msat_OrderUpdate ( Msat_Order_t *  p,
int  Var 
)

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

Synopsis [Updates the order after a variable changed weight.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file msatOrderH.c.

00255 {
00256 //    if (heap.inHeap(x))
00257 //        heap.increase(x);
00258 
00259     int clk = clock();
00260     if ( HINHEAP(p,Var) )
00261         Msat_HeapIncrease( p, Var );
00262 timeSelect += clock() - clk;
00263 }

void Msat_OrderVarAssigned ( Msat_Order_t *  p,
int  Var 
)

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

Synopsis [Updates J-boundary when the variable is assigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file msatOrderH.c.

00218 {
00219 }

int Msat_OrderVarSelect ( Msat_Order_t *  p  ) 

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

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file msatOrderH.c.

00181 {
00182     // Activity based decision:
00183 //    while (!heap.empty()){
00184 //        Var next = heap.getmin();
00185 //        if (toLbool(assigns[next]) == l_Undef)
00186 //            return next;
00187 //    }
00188 //    return var_Undef;
00189 
00190     int Var;
00191     int clk = clock();
00192 
00193     while ( !HEMPTY(p) )
00194     {
00195         Var = Msat_HeapGetTop(p);
00196         if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
00197         {
00198 //assert( Msat_OrderCheck(p) );
00199 timeSelect += clock() - clk;
00200             return Var;
00201         }
00202     }
00203     return MSAT_ORDER_UNKNOWN;
00204 }

void Msat_OrderVarUnassigned ( Msat_Order_t *  p,
int  Var 
)

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

Synopsis [Updates the order after a variable is unassigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file msatOrderH.c.

00233 {
00234 //    if (!heap.inHeap(x))
00235 //        heap.insert(x);
00236 
00237     int clk = clock();
00238     if ( !HINHEAP(p,Var) )
00239         Msat_HeapInsert( p, Var );
00240 timeSelect += clock() - clk;
00241 }

Msat_Queue_t* Msat_QueueAlloc ( int  nVars  ) 

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

Synopsis [Allocates the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file msatQueue.c.

00051 {
00052     Msat_Queue_t * p;
00053     p = ALLOC( Msat_Queue_t, 1 );
00054     memset( p, 0, sizeof(Msat_Queue_t) );
00055     p->nVars  = nVars;
00056     p->pVars  = ALLOC( int, nVars );
00057     return p;
00058 }

void Msat_QueueClear ( Msat_Queue_t *  p  ) 

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

Synopsis [Resets the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file msatQueue.c.

00147 {
00148     p->iFirst = 0;
00149     p->iLast  = 0;
00150 }

int Msat_QueueExtract ( Msat_Queue_t *  p  ) 

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

Synopsis [Extracts an entry from the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file msatQueue.c.

00129 {
00130     if ( p->iFirst == p->iLast )
00131         return -1;
00132     return p->pVars[p->iFirst++];
00133 }

void Msat_QueueFree ( Msat_Queue_t *  p  ) 

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

Synopsis [Deallocate the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file msatQueue.c.

00072 {
00073     free( p->pVars );
00074     free( p );
00075 }

void Msat_QueueInsert ( Msat_Queue_t *  p,
int  Lit 
)

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

Synopsis [Insert an entry into the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file msatQueue.c.

00105 {
00106     if ( p->iLast == p->nVars )
00107     {
00108         int i;
00109         assert( 0 );
00110         for ( i = 0; i < p->iLast; i++ )
00111             printf( "entry = %2d  lit = %2d  var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
00112     }
00113     assert( p->iLast < p->nVars );
00114     p->pVars[p->iLast++] = Lit;
00115 }

int Msat_QueueReadSize ( Msat_Queue_t *  p  ) 

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

Synopsis [Reads the queue size.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file msatQueue.c.

00089 {
00090     return p->iLast - p->iFirst;
00091 }

bool Msat_SolverAssume ( Msat_Solver_t *  p,
Msat_Lit_t  Lit 
)

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

Synopsis [Makes the next assumption (Lit).]

Description [Returns FALSE if immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 48 of file msatSolverSearch.c.

00049 {
00050     assert( Msat_QueueReadSize(p->pQueue) == 0 );
00051     if ( p->fVerbose )
00052         printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit));
00053     Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
00054 //    assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
00055 //    assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
00056     return Msat_SolverEnqueue( p, Lit, NULL );
00057 }

void Msat_SolverCancelUntil ( Msat_Solver_t *  p,
int  Level 
)

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

Synopsis [Reverts to the state at given level.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file msatSolverSearch.c.

00126 {
00127     while ( Msat_IntVecReadSize(p->vTrailLim) > Level )
00128         Msat_SolverCancel(p);
00129 }

void Msat_SolverClaBumpActivity ( Msat_Solver_t *  p,
Msat_Clause_t *  pC 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file msatActivity.c.

00103 {
00104     float Activ;
00105     Activ = Msat_ClauseReadActivity(pC);
00106     if ( Activ + p->dClaInc > 1e20 )
00107     {
00108         Msat_SolverClaRescaleActivity( p );
00109         Activ = Msat_ClauseReadActivity( pC );
00110     }
00111     Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc );
00112 }

void Msat_SolverClaDecayActivity ( Msat_Solver_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file msatActivity.c.

00126 {
00127     p->dClaInc *= p->dClaDecay;
00128 }

void Msat_SolverClaRescaleActivity ( Msat_Solver_t *  p  ) 

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

Synopsis [Divide all constraint activities by 1e20.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file msatActivity.c.

00142 {
00143     Msat_Clause_t ** pLearned;
00144     int nLearned, i;
00145     float Activ;
00146     nLearned = Msat_ClauseVecReadSize( p->vLearned );
00147     pLearned = Msat_ClauseVecReadArray( p->vLearned );
00148     for ( i = 0; i < nLearned; i++ )
00149     {
00150         Activ = Msat_ClauseReadActivity( pLearned[i] );
00151         Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 );
00152     }
00153     p->dClaInc *= 1e-20;
00154 }

void Msat_SolverClausesDecrement ( Msat_Solver_t *  p  ) 

Definition at line 62 of file msatSolverApi.c.

00062 { p->nClausesAlloc--;   }

void Msat_SolverClausesDecrementL ( Msat_Solver_t *  p  ) 

Definition at line 64 of file msatSolverApi.c.

00064 { p->nClausesAllocL--;  }

void Msat_SolverClausesIncrement ( Msat_Solver_t *  p  ) 

Definition at line 61 of file msatSolverApi.c.

00061 { p->nClausesAlloc++;   }

void Msat_SolverClausesIncrementL ( Msat_Solver_t *  p  ) 

Definition at line 63 of file msatSolverApi.c.

00063 { p->nClausesAllocL++;  }

bool Msat_SolverEnqueue ( Msat_Solver_t *  p,
Msat_Lit_t  Lit,
Msat_Clause_t *  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 []

Definition at line 170 of file msatSolverSearch.c.

00171 {
00172     Msat_Var_t Var = MSAT_LIT2VAR(Lit);
00173 
00174     // skip literals that are not in the current cone
00175     if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) )
00176         return 1;
00177 
00178 //    assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) );
00179     // if the literal is assigned
00180     // return 1 if the assignment is consistent
00181     // return 0 if the assignment is inconsistent (conflict)
00182     if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED )
00183         return p->pAssigns[Var] == Lit;
00184     // new fact - store it
00185     if ( p->fVerbose )
00186     {
00187 //        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
00188         printf(L_IND"bind("L_LIT")  ", L_ind, L_lit(Lit));
00189         Msat_ClausePrintSymbols( pC );
00190     }
00191     p->pAssigns[Var] = Lit;
00192     p->pLevel[Var]   = Msat_IntVecReadSize(p->vTrailLim);
00193 //    p->pReasons[Var] = p->pLevel[Var]? pC: NULL;
00194     p->pReasons[Var] = pC;
00195     Msat_IntVecPush( p->vTrail, Lit );
00196     Msat_QueueInsert( p->pQueue, Lit );
00197 
00198     Msat_OrderVarAssigned( p->pOrder, Var );
00199     return 1;
00200 }

int Msat_SolverIncrementSeenId ( Msat_Solver_t *  p  ) 

Definition at line 59 of file msatSolverApi.c.

00059 { return ++p->nSeenId;  }

double Msat_SolverProgressEstimate ( Msat_Solver_t *  p  ) 

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

Synopsis [Returns search-space coverage. Not extremely reliable.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file msatSolverCore.c.

00086 {
00087     double dProgress = 0.0;
00088     double dF = 1.0 / p->nVars;
00089     int i;
00090     for ( i = 0; i < p->nVars; i++ )
00091         if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
00092             dProgress += pow( dF, p->pLevel[i] );
00093     return dProgress / p->nVars;
00094 }

Msat_Clause_t* Msat_SolverPropagate ( Msat_Solver_t *  p  ) 

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

Definition at line 214 of file msatSolverSearch.c.

00215 {
00216     Msat_ClauseVec_t ** pvWatched = p->pvWatched;
00217     Msat_Clause_t ** pClauses;
00218     Msat_Clause_t * pConflict;
00219     Msat_Lit_t Lit, Lit_out;
00220     int i, j, nClauses;
00221 
00222     // propagate all the literals in the queue
00223     while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 )
00224     {
00225         p->Stats.nPropagations++;
00226         // get the clauses watched by this literal
00227         nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] );
00228         pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] );
00229         // go through the watched clauses and decide what to do with them
00230         for ( i = j = 0; i < nClauses; i++ )
00231         {
00232             p->Stats.nInspects++;
00233             // clear the returned literal
00234             Lit_out = -1;
00235             // propagate the clause
00236             if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) )
00237             {   // the clause is unit
00238                 // "Lit_out" contains the new assignment to be enqueued
00239                 if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) 
00240                 { // consistent assignment 
00241                     // no changes to the implication queue; the watch is the same too
00242                     pClauses[j++] = pClauses[i];
00243                     continue;
00244                 }
00245                 // remember the reason of conflict (will be returned)
00246                 pConflict = pClauses[i];
00247                 // leave the remaning clauses in the same watched list
00248                 for ( ; i < nClauses; i++ )
00249                     pClauses[j++] = pClauses[i];
00250                 Msat_ClauseVecShrink( pvWatched[Lit], j );
00251                 // clear the propagation queue
00252                 Msat_QueueClear( p->pQueue );
00253                 return pConflict;
00254             }
00255             // the clause is not unit
00256             // in this case "Lit_out" contains the new watch if it has changed
00257             if ( Lit_out >= 0 )
00258                 Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] );
00259             else // the watch did not change
00260                 pClauses[j++] = pClauses[i];
00261         }
00262         Msat_ClauseVecShrink( pvWatched[Lit], j );
00263     }
00264     return NULL;
00265 }

Msat_Clause_t* Msat_SolverReadClause ( Msat_Solver_t *  p,
int  Num 
)

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

Synopsis [Reads the clause with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file msatSolverApi.c.

00081 {
00082     int nClausesP;
00083     assert( Num < p->nClauses );
00084     nClausesP = Msat_ClauseVecReadSize( p->vClauses );
00085     if ( Num < nClausesP )
00086         return Msat_ClauseVecReadEntry( p->vClauses, Num );
00087     return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
00088 }

int Msat_SolverReadDecisionLevel ( Msat_Solver_t *  p  ) 

Definition at line 47 of file msatSolverApi.c.

00047 { return Msat_IntVecReadSize(p->vTrailLim); }

int* Msat_SolverReadDecisionLevelArray ( Msat_Solver_t *  p  ) 

Definition at line 48 of file msatSolverApi.c.

00048 { return p->pLevel;     }

Msat_ClauseVec_t* Msat_SolverReadLearned ( Msat_Solver_t *  p  ) 

Definition at line 51 of file msatSolverApi.c.

00051 { return p->vLearned;   }

Msat_MmStep_t* Msat_SolverReadMem ( Msat_Solver_t *  p  ) 

Definition at line 57 of file msatSolverApi.c.

00057 { return p->pMem;       }

Msat_Clause_t** Msat_SolverReadReasonArray ( Msat_Solver_t *  p  ) 

Definition at line 49 of file msatSolverApi.c.

00049 { return p->pReasons;   }

int* Msat_SolverReadSeenArray ( Msat_Solver_t *  p  ) 

Definition at line 58 of file msatSolverApi.c.

00058 { return p->pSeen;      }

Msat_Type_t Msat_SolverReadVarValue ( Msat_Solver_t *  p,
Msat_Var_t  Var 
)

Definition at line 50 of file msatSolverApi.c.

00050 { return p->pAssigns[Var]; }

Msat_ClauseVec_t** Msat_SolverReadWatchedArray ( Msat_Solver_t *  p  ) 

Definition at line 52 of file msatSolverApi.c.

00052 { return p->pvWatched;  }

Msat_Type_t Msat_SolverSearch ( Msat_Solver_t *  p,
int  nConfLimit,
int  nLearnedLimit,
int  nBackTrackLimit,
Msat_SearchParams_t *  pPars 
)

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

Definition at line 532 of file msatSolverSearch.c.

00533 {
00534     Msat_Clause_t * pConf;
00535     Msat_Var_t Var;
00536     int nLevelBack, nConfs, nAssigns, Value;
00537     int i;
00538 
00539     assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
00540     p->Stats.nStarts++;
00541     p->dVarDecay = 1 / pPars->dVarDecay;
00542     p->dClaDecay = 1 / pPars->dClaDecay;
00543 
00544     // reset the activities
00545     for ( i = 0; i < p->nVars; i++ )
00546        p->pdActivity[i] = (double)p->pFactors[i];
00547 //       p->pdActivity[i] = 0.0;
00548 
00549     nConfs = 0;
00550     while ( 1 )
00551     {
00552         pConf = Msat_SolverPropagate( p );
00553         if ( pConf != NULL ){
00554             // CONFLICT
00555             if ( p->fVerbose )
00556             {
00557 //                printf(L_IND"**CONFLICT**\n", L_ind);
00558                 printf(L_IND"**CONFLICT**  ", L_ind);
00559                 Msat_ClausePrintSymbols( pConf );
00560             }
00561             // count conflicts
00562             p->Stats.nConflicts++;
00563             nConfs++;
00564 
00565             // if top level, return UNSAT
00566             if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot )
00567                 return MSAT_FALSE;
00568 
00569             // perform conflict analysis
00570             Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack );
00571             Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack );
00572             Msat_SolverRecord( p, p->vTemp );
00573 
00574             // it is important that recording is done after cancelling
00575             // because canceling cleans the queue while recording adds to it
00576             Msat_SolverVarDecayActivity( p );
00577             Msat_SolverClaDecayActivity( p );
00578 
00579         }
00580         else{
00581             // NO CONFLICT
00582             if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) {
00583                 // Simplify the set of problem clauses:
00584 //                Value = Msat_SolverSimplifyDB(p);
00585 //                assert( Value );
00586             }
00587             nAssigns = Msat_IntVecReadSize( p->vTrail );
00588             if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) {
00589                 // Reduce the set of learnt clauses:
00590                 Msat_SolverReduceDB(p);
00591             }
00592 
00593             Var = Msat_OrderVarSelect( p->pOrder );
00594             if ( Var == MSAT_ORDER_UNKNOWN ) {
00595                 // Model found and stored in p->pAssigns
00596                 memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars );
00597                 Msat_QueueClear( p->pQueue );
00598                 Msat_SolverCancelUntil( p, p->nLevelRoot );
00599                 return MSAT_TRUE;
00600             }
00601             if ( nConfLimit > 0 && nConfs > nConfLimit ) {
00602                 // Reached bound on number of conflicts:
00603                 p->dProgress = Msat_SolverProgressEstimate( p );
00604                 Msat_QueueClear( p->pQueue );
00605                 Msat_SolverCancelUntil( p, p->nLevelRoot );
00606                 return MSAT_UNKNOWN; 
00607             }
00608             else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
00609                 // Reached bound on number of conflicts:
00610                 Msat_QueueClear( p->pQueue );
00611                 Msat_SolverCancelUntil( p, p->nLevelRoot );
00612                 return MSAT_UNKNOWN; 
00613             }
00614             else{
00615                 // New variable decision:
00616                 p->Stats.nDecisions++;
00617                 assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars );
00618                 Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) );
00619                 assert( Value );
00620             }
00621         }
00622     }
00623 }

void Msat_SolverSortDB ( Msat_Solver_t *  p  ) 

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

Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file msatSort.c.

00059 {
00060     Msat_ClauseVec_t * pVecClauses;
00061     Msat_Clause_t ** pLearned;
00062     int nLearned;
00063     // read the parameters
00064     pVecClauses = Msat_SolverReadLearned( p );
00065     nLearned    = Msat_ClauseVecReadSize( pVecClauses );
00066     pLearned    = Msat_ClauseVecReadArray( pVecClauses );
00067     // Msat_SolverSort the array
00068 //    qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 
00069 //            (int (*)(const void *, const void *)) Msat_SolverSortCompare );
00070 //    printf( "Msat_SolverSorting.\n" );
00071     Msat_SolverSort( pLearned, nLearned, 91648253 );
00072 /*
00073     if ( nLearned > 2 )
00074     {
00075     printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
00076     printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
00077     printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
00078     }
00079 */
00080 }

void Msat_SolverVarBumpActivity ( Msat_Solver_t *  p,
Msat_Lit_t  Lit 
)

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

FileName [msatActivity.c]

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

Synopsis [Procedures controlling activity of variables and clauses.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
msatActivity.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file msatActivity.c.

00043 {
00044     Msat_Var_t Var;
00045     if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
00046         return;
00047     Var = MSAT_LIT2VAR(Lit);
00048     p->pdActivity[Var] += p->dVarInc;
00049 //    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
00050     if ( p->pdActivity[Var] > 1e100 )
00051         Msat_SolverVarRescaleActivity( p );
00052     Msat_OrderUpdate( p->pOrder, Var );
00053 }

void Msat_SolverVarDecayActivity ( Msat_Solver_t *  p  ) 

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file msatActivity.c.

00067 {
00068     if ( p->dVarDecay >= 0 )
00069         p->dVarInc *= p->dVarDecay;
00070 }

void Msat_SolverVarRescaleActivity ( Msat_Solver_t *  p  ) 

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

Synopsis [Divide all variable activities by 1e100.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file msatActivity.c.

00084 {
00085     int i;
00086     for ( i = 0; i < p->nVars; i++ )
00087         p->pdActivity[i] *= 1e-100;
00088     p->dVarInc *= 1e-100;
00089 }

Generated on Tue Jan 5 12:19:39 2010 for abc70930 by  doxygen 1.6.1