src/sat/msat/msatClause.c File Reference

#include "msatInt.h"
Include dependency graph for msatClause.c:

Go to the source code of this file.

Data Structures

struct  Msat_Clause_t_

Functions

bool Msat_ClauseCreate (Msat_Solver_t *p, Msat_IntVec_t *vLits, bool fLearned, Msat_Clause_t **pClause_out)
void Msat_ClauseFree (Msat_Solver_t *p, Msat_Clause_t *pC, bool fRemoveWatched)
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)
int Msat_ClauseReadNum (Msat_Clause_t *pC)
bool Msat_ClauseReadTypeA (Msat_Clause_t *pC)
void Msat_ClauseSetMark (Msat_Clause_t *pC, bool fMark)
void Msat_ClauseSetNum (Msat_Clause_t *pC, int Num)
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)
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_ClauseWriteDimacs (FILE *pFile, Msat_Clause_t *pC, bool fIncrement)
void Msat_ClausePrintSymbols (Msat_Clause_t *pC)

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 }

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 }

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 }

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 }

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