summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatClause.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat/msatClause.c')
-rw-r--r--src/sat/msat/msatClause.c529
1 files changed, 529 insertions, 0 deletions
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
new file mode 100644
index 00000000..2ba8cd32
--- /dev/null
+++ b/src/sat/msat/msatClause.c
@@ -0,0 +1,529 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:28:12 +0000