src/sat/msat/msatClause.c

Go to the documentation of this file.

#include "msatInt.h"


struct Msat_Clause_t_
{
    int           Num;              // unique number of the clause
    unsigned      fLearned   :  1;  // 1 if the clause is learned
    unsigned      fMark      :  1;  // used to mark visited clauses during proof recording
    unsigned      fTypeA     :  1;  // used to mark clauses belonging to A for interpolant computation
    unsigned      nSize      : 14;  // the number of literals in the clause
    unsigned      nSizeAlloc : 15;  // the number of bytes allocated for the clause
    Msat_Lit_t     pData[0];
};


bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out )
{
    int * pAssigns = Msat_SolverReadAssignsArray(p);
    Msat_ClauseVec_t ** pvWatched;
    Msat_Clause_t * pC;
    int * pLits;
    int nLits, i, j;
    int nBytes;
    Msat_Var_t Var;
    bool Sign;

    *pClause_out = NULL;

    nLits = Msat_IntVecReadSize(vLits);
    pLits = Msat_IntVecReadArray(vLits);

    if ( !fLearned ) 
    {
        int * pSeen = Msat_SolverReadSeenArray( p );
        int nSeenId;
        assert( Msat_SolverReadDecisionLevel(p) == 0 );
        // sorting literals makes the code trace-equivalent 
        // with to the original C++ solver
        Msat_IntVecSort( vLits, 0 );
        // increment the counter of seen twice
        nSeenId = Msat_SolverIncrementSeenId( p );
        nSeenId = Msat_SolverIncrementSeenId( p );
        // nSeenId - 1 stands for negative
        // nSeenId     stands for positive
        // Remove false literals

        // there is a bug here!!!!
        // when the same var in opposite polarities is given, it drops one polarity!!!

        for ( i = j = 0; i < nLits; i++ ) {
            // get the corresponding variable
            Var  = MSAT_LIT2VAR(pLits[i]);
            Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
            // check if we already saw this variable in the this clause
            if ( pSeen[Var] >= nSeenId - 1 )
            {
                if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
                    continue;
                return 1; // two opposite polarity lits -- don't add the clause
            }
            // mark the variable as seen
            pSeen[Var] = nSeenId - !Sign;

            // analize the value of this literal
            if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
            {
                if ( pAssigns[Var] == pLits[i] )
                    return 1;  // the clause is always true -- don't add anything
                // the literal has no impact - skip it
                continue;
            }
            // otherwise, add this literal to the clause
            pLits[j++] = pLits[i];
        }
        Msat_IntVecShrink( vLits, j );
        nLits = j;
/*
        // the problem with this code is that performance is very
        // sensitive to the ordering of adjacency lits
        // the best ordering requires fanins first, next fanouts
        // this ordering is more convenient to make from FRAIG

        // create the adjacency information
        if ( nLits > 2 )
        {
            Msat_Var_t VarI, VarJ;
            Msat_IntVec_t * pAdjI, * pAdjJ;

            for ( i = 0; i < nLits; i++ )
            {
                VarI = MSAT_LIT2VAR(pLits[i]);
                pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];

                for ( j = i+1; j < nLits; j++ )
                {
                    VarJ = MSAT_LIT2VAR(pLits[j]);
                    pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];

                    Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
                    Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
                }
            }
        }
*/
    }
    // 'vLits' is now the (possibly) reduced vector of literals.
    if ( nLits == 0 )
        return 0;
    if ( nLits == 1 )
        return Msat_SolverEnqueue( p, pLits[0], NULL );

    // Allocate clause:
//    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
    nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
    pC = (Msat_Clause_t *)ALLOC( char, nBytes );
#else
    pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
#endif
    pC->Num        = p->nClauses++;
    pC->fTypeA     = 0;
    pC->fMark      = 0;
    pC->fLearned   = fLearned;
    pC->nSize      = nLits;
    pC->nSizeAlloc = nBytes;
    memcpy( pC->pData, pLits, sizeof(int)*nLits );

    // For learnt clauses only:
    if ( fLearned )
    {
        int * pLevel = Msat_SolverReadDecisionLevelArray( p );
        int iLevelMax, iLevelCur, iLitMax;

        // Put the second watch on the literal with highest decision level:
        iLitMax = 1;
        iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
        for ( i = 2; i < nLits; i++ )
        {
            iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
            assert( iLevelCur != -1 );
            if ( iLevelMax < iLevelCur )
            // this is very strange - shouldn't it be???
            // if ( iLevelMax > iLevelCur )
                iLevelMax = iLevelCur, iLitMax = i;
        }
        pC->pData[1]       = pLits[iLitMax];
        pC->pData[iLitMax] = pLits[1];

        // Bumping:
        // (newly learnt clauses should be considered active)
        Msat_ClauseWriteActivity( pC, 0.0 );
        Msat_SolverClaBumpActivity( p, pC ); 
//        if ( nLits < 20 )
        for ( i = 0; i < nLits; i++ )
        {
            Msat_SolverVarBumpActivity( p, pLits[i] );
//            Msat_SolverVarBumpActivity( p, pLits[i] );
//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
        }
    }

    // Store clause:
    pvWatched = Msat_SolverReadWatchedArray( p );
    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
    *pClause_out = pC;
    return 1;
}

void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched )
{
    if ( fRemoveWatched )
    {
        Msat_Lit_t Lit;
        Msat_ClauseVec_t ** pvWatched;
        pvWatched = Msat_SolverReadWatchedArray( p );
        Lit = MSAT_LITNOT( pC->pData[0] );
        Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
        Lit = MSAT_LITNOT( pC->pData[1] );
        Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
    }

#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
    free( pC );
#else
    Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
#endif

}

bool  Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
int   Msat_ClauseReadSize( Msat_Clause_t * pC )     {  return pC->nSize;    }
int * Msat_ClauseReadLits( Msat_Clause_t * pC )     {  return pC->pData;    }
bool  Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
int   Msat_ClauseReadNum( Msat_Clause_t * pC )      {  return pC->Num;      }
bool  Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }

void  Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark )   {  pC->fMark = fMark;   }
void  Msat_ClauseSetNum( Msat_Clause_t * pC, int Num )       {  pC->Num = Num;       }
void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTypeA; }

bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
{
    Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
    return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
}

float Msat_ClauseReadActivity( Msat_Clause_t * pC )
{
    return *((float *)(pC->pData + pC->nSize));
}

void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
{
    *((float *)(pC->pData + pC->nSize)) = Num;
}

bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
{
    // make sure the false literal is pC->pData[1]
    Msat_Lit_t LitF = MSAT_LITNOT(Lit);
    if ( pC->pData[0] == LitF )
         pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
    assert( pC->pData[1] == LitF );
    // if the 0-th watch is true, clause is already satisfied
    if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
        return 1; 
    // look for a new watch
    if ( pC->nSize > 2 )
    {
        int i;
        for ( i = 2; i < (int)pC->nSize; i++ )
            if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
            {
                pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
                *pLit_out = MSAT_LITNOT(pC->pData[1]);
                return 1; 
            }
    }
    // clause is unit under assignment
    *pLit_out = pC->pData[0];
    return 0;
}

bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
{
    Msat_Var_t Var;
    int i, j;
    for ( i = j = 0; i < (int)pC->nSize; i++ )
    {
        Var = MSAT_LIT2VAR(pC->pData[i]);
        if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
        {
            pC->pData[j++] = pC->pData[i];
            continue;
        }
        if ( pAssigns[Var] == pC->pData[i] )
            return 1;
        // otherwise, the value of the literal is false
        // make sure, this literal is not watched
        assert( i >= 2 );
    }
    // if the size has changed, update it and move activity
    if ( j < (int)pC->nSize )
    {
        float Activ = Msat_ClauseReadActivity(pC);
        pC->nSize = j;
        Msat_ClauseWriteActivity(pC, Activ);
    }
    return 0;
}

void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out )
{
    int i;
    // clear the reason
    Msat_IntVecClear( vLits_out );
    assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
    for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
    {
        assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
        Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
    }
    if ( pC->fLearned ) 
        Msat_SolverClaBumpActivity( p, pC );
}

void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC )
{
    Msat_Clause_t ** pClauses;
    int nClauses, i;
    nClauses = Msat_ClauseVecReadSize( vClauses );
    pClauses = Msat_ClauseVecReadArray( vClauses );
    for ( i = 0; pClauses[i] != pC; i++ )
        assert( i < nClauses );
    for (      ; i < nClauses - 1; i++ )
        pClauses[i] = pClauses[i+1];
    Msat_ClauseVecPop( vClauses );
}

void Msat_ClausePrint( Msat_Clause_t * pC )
{
    int i;
    if ( pC == NULL )
        printf( "NULL pointer" );
    else 
    {
        if ( pC->fLearned )
            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
        for ( i = 0; i < (int)pC->nSize; i++ )
            printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
    }
    printf( "\n" );
}

void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement )
{
    int i;
    for ( i = 0; i < (int)pC->nSize; i++ )
        fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
    if ( fIncrement )
        fprintf( pFile, "0" );
    fprintf( pFile, "\n" );
}

void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
{
    int i;
    if ( pC == NULL )
        printf( "NULL pointer" );
    else 
    {
//        if ( pC->fLearned )
//            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
        for ( i = 0; i < (int)pC->nSize; i++ )
            printf(" "L_LIT, L_lit(pC->pData[i]));
    }
    printf( "\n" );
}

---