Version abc70930

1 files changed, 0 insertions, 529 deletions

diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
deleted file mode 100644
index 2ba8cd32..00000000
--- a/src/sat/msat/msatClause.c
+++ /dev/null
@@ -1,529 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [msatClause.c]
-
-  PackageName [A C version of SAT solver MINISAT, originally developed 
-  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
-  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
-
-  Synopsis    [Procedures working with SAT clauses.]
-
-  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2004.]
-
-  Revision    [$Id: msatClause.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Msat_Clause_t_
-{
-    int           Num;              // unique number of the clause
-    unsigned      fLearned   :  1;  // 1 if the clause is learned
-    unsigned      fMark      :  1;  // used to mark visited clauses during proof recording
-    unsigned      fTypeA     :  1;  // used to mark clauses belonging to A for interpolant computation
-    unsigned      nSize      : 14;  // the number of literals in the clause
-    unsigned      nSizeAlloc : 15;  // the number of bytes allocated for the clause
-    Msat_Lit_t     pData[0];
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION 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     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched )
-{
-    if ( fRemoveWatched )
-    {
-        Msat_Lit_t Lit;
-        Msat_ClauseVec_t ** pvWatched;
-        pvWatched = Msat_SolverReadWatchedArray( p );
-        Lit = MSAT_LITNOT( pC->pData[0] );
-        Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
-        Lit = MSAT_LITNOT( pC->pData[1] );
-        Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
-    }
-
-#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    free( pC );
-#else
-    Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
-#endif
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Access the data field of the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool  Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
-int   Msat_ClauseReadSize( Msat_Clause_t * pC )     {  return pC->nSize;    }
-int * Msat_ClauseReadLits( Msat_Clause_t * pC )     {  return pC->pData;    }
-bool  Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
-int   Msat_ClauseReadNum( Msat_Clause_t * pC )      {  return pC->Num;      }
-bool  Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }
-
-void  Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark )   {  pC->fMark = fMark;   }
-void  Msat_ClauseSetNum( Msat_Clause_t * pC, int Num )       {  pC->Num = Num;       }
-void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTypeA; }
-
-/**Function*************************************************************
-
-  Synopsis    [Checks whether the learned clause is locked.]
-
-  Description [The clause may be locked if it is the reason of a
-  recent conflict. Such clause cannot be removed from the database.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
-{
-    Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
-    return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the activity of the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Msat_ClauseReadActivity( Msat_Clause_t * pC )
-{
-    return *((float *)(pC->pData + pC->nSize));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the activity of the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
-{
-    *((float *)(pC->pData + pC->nSize)) = Num;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propages the assignment.]
-
-  Description [The literal that has become true (Lit) is given to this 
-  procedure. The array of current variable assignments is given for
-  efficiency. The output literal (pLit_out) can be the second watched
-  literal (if TRUE is returned) or the conflict literal (if FALSE is 
-  returned). This messy interface is used to improve performance.
-  This procedure accounts for ~50% of the runtime of the solver.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
-{
-    // make sure the false literal is pC->pData[1]
-    Msat_Lit_t LitF = MSAT_LITNOT(Lit);
-    if ( pC->pData[0] == LitF )
-         pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
-    assert( pC->pData[1] == LitF );
-    // if the 0-th watch is true, clause is already satisfied
-    if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
-        return 1; 
-    // look for a new watch
-    if ( pC->nSize > 2 )
-    {
-        int i;
-        for ( i = 2; i < (int)pC->nSize; i++ )
-            if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
-            {
-                pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
-                *pLit_out = MSAT_LITNOT(pC->pData[1]);
-                return 1; 
-            }
-    }
-    // clause is unit under assignment
-    *pLit_out = pC->pData[0];
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simplifies the clause.]
-
-  Description [Assumes everything has been propagated! (esp. watches 
-  in clauses are NOT unsatisfied)]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
-{
-    Msat_Var_t Var;
-    int i, j;
-    for ( i = j = 0; i < (int)pC->nSize; i++ )
-    {
-        Var = MSAT_LIT2VAR(pC->pData[i]);
-        if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
-        {
-            pC->pData[j++] = pC->pData[i];
-            continue;
-        }
-        if ( pAssigns[Var] == pC->pData[i] )
-            return 1;
-        // otherwise, the value of the literal is false
-        // make sure, this literal is not watched
-        assert( i >= 2 );
-    }
-    // if the size has changed, update it and move activity
-    if ( j < (int)pC->nSize )
-    {
-        float Activ = Msat_ClauseReadActivity(pC);
-        pC->nSize = j;
-        Msat_ClauseWriteActivity(pC, Activ);
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes reason of conflict in the given clause.]
-
-  Description [If the literal is unassigned, finds the reason by 
-  complementing literals in the given cluase (pC). If the literal is
-  assigned, makes sure that this literal is the first one in the clause
-  and computes the complement of all other literals in the clause.
-  Returns the reason in the given array (vLits_out). If the clause is
-  learned, bumps its activity.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out )
-{
-    int i;
-    // clear the reason
-    Msat_IntVecClear( vLits_out );
-    assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
-    for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
-    {
-        assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
-        Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
-    }
-    if ( pC->fLearned ) 
-        Msat_SolverClaBumpActivity( p, pC );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes the given clause from the watched list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC )
-{
-    Msat_Clause_t ** pClauses;
-    int nClauses, i;
-    nClauses = Msat_ClauseVecReadSize( vClauses );
-    pClauses = Msat_ClauseVecReadArray( vClauses );
-    for ( i = 0; pClauses[i] != pC; i++ )
-        assert( i < nClauses );
-    for (      ; i < nClauses - 1; i++ )
-        pClauses[i] = pClauses[i+1];
-    Msat_ClauseVecPop( vClauses );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClausePrint( Msat_Clause_t * pC )
-{
-    int i;
-    if ( pC == NULL )
-        printf( "NULL pointer" );
-    else 
-    {
-        if ( pC->fLearned )
-            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
-        for ( i = 0; i < (int)pC->nSize; i++ )
-            printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the given clause in a file in DIMACS format.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement )
-{
-    int i;
-    for ( i = 0; i < (int)pC->nSize; i++ )
-        fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
-    if ( fIncrement )
-        fprintf( pFile, "0" );
-    fprintf( pFile, "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
-{
-    int i;
-    if ( pC == NULL )
-        printf( "NULL pointer" );
-    else 
-    {
-//        if ( pC->fLearned )
-//            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
-        for ( i = 0; i < (int)pC->nSize; i++ )
-            printf(" "L_LIT, L_lit(pC->pData[i]));
-    }
-    printf( "\n" );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-