summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/xsat/xsatBQueue.h15
-rw-r--r--src/sat/xsat/xsatClause.h8
-rw-r--r--src/sat/xsat/xsatHeap.h4
-rw-r--r--src/sat/xsat/xsatMemory.h10
-rw-r--r--src/sat/xsat/xsatSolver.c176
-rw-r--r--src/sat/xsat/xsatSolver.h26
-rw-r--r--src/sat/xsat/xsatSolverAPI.c2
-rw-r--r--src/sat/xsat/xsatWatchList.h14
8 files changed, 119 insertions, 136 deletions
diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h
index 6c170c93..560f75c0 100644
--- a/src/sat/xsat/xsatBQueue.h
+++ b/src/sat/xsat/xsatBQueue.h
@@ -24,7 +24,6 @@
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
@@ -32,7 +31,6 @@ ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
typedef struct xSAT_BQueue_t_ xSAT_BQueue_t;
struct xSAT_BQueue_t_
{
@@ -41,13 +39,12 @@ struct xSAT_BQueue_t_
int iFirst;
int iEmpty;
word nSum;
- word * pData;
+ unsigned * pData;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-
/**Function*************************************************************
Synopsis []
@@ -63,7 +60,7 @@ static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap )
{
xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 );
p->nCap = nCap;
- p->pData = ABC_CALLOC( word, nCap );
+ p->pData = ABC_CALLOC( unsigned, nCap );
return p;
}
@@ -95,7 +92,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p )
SeeAlso []
***********************************************************************/
-static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
+static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, unsigned Value )
{
if ( p->nSize == p->nCap )
{
@@ -128,8 +125,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
***********************************************************************/
static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
{
- int RetValue = p->pData[p->iFirst];
assert( p->nSize >= 1 );
+ int RetValue = p->pData[p->iFirst];
p->nSum -= RetValue;
p->iFirst = ( p->iFirst + 1 ) % p->nCap;
p->nSize--;
@@ -147,9 +144,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
SeeAlso []
***********************************************************************/
-static inline word xSAT_BQueueAvg( xSAT_BQueue_t * p )
+static inline unsigned xSAT_BQueueAvg( xSAT_BQueue_t * p )
{
- return ( word )( p->nSum / ( ( word ) p->nSize ) );
+ return ( unsigned )( p->nSum / ( ( word ) p->nSize ) );
}
/**Function*************************************************************
diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h
index d05eb6de..ef353198 100644
--- a/src/sat/xsat/xsatClause.h
+++ b/src/sat/xsat/xsatClause.h
@@ -39,7 +39,7 @@ struct xSAT_Clause_t_
unsigned fReallocd : 1;
unsigned fCanBeDel : 1;
unsigned nLBD : 28;
- unsigned nSize;
+ int nSize;
union {
int Lit;
unsigned Act;
@@ -60,7 +60,7 @@ struct xSAT_Clause_t_
SeeAlso []
***********************************************************************/
-static int xSAT_ClauseCompare( const void * p1, const void * p2 )
+static inline int xSAT_ClauseCompare( const void * p1, const void * p2 )
{
xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1;
xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2;
@@ -91,12 +91,12 @@ static int xSAT_ClauseCompare( const void * p1, const void * p2 )
SeeAlso []
***********************************************************************/
-static void xSAT_ClausePrint( xSAT_Clause_t * pCla )
+static inline void xSAT_ClausePrint( xSAT_Clause_t * pCla )
{
int i;
printf("{ ");
- for ( i = 0; i < (int)pCla->nSize; i++ )
+ for ( i = 0; i < pCla->nSize; i++ )
printf("%d ", pCla->pData[i].Lit );
printf("}\n");
}
diff --git a/src/sat/xsat/xsatHeap.h b/src/sat/xsat/xsatHeap.h
index 409ce460..2e873e59 100644
--- a/src/sat/xsat/xsatHeap.h
+++ b/src/sat/xsat/xsatHeap.h
@@ -48,7 +48,7 @@ struct xSAT_Heap_t_
SeeAlso []
***********************************************************************/
-static inline int xSAT_HeapSize( xSAT_Heap_t * h )
+inline int xSAT_HeapSize( xSAT_Heap_t * h )
{
return Vec_IntSize( h->vHeap );
}
@@ -64,7 +64,7 @@ static inline int xSAT_HeapSize( xSAT_Heap_t * h )
SeeAlso []
***********************************************************************/
-static inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
+inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
{
return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 );
}
diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h
index 3324a563..129c2f50 100644
--- a/src/sat/xsat/xsatMemory.h
+++ b/src/sat/xsat/xsatMemory.h
@@ -77,16 +77,14 @@ static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap )
unsigned nPrevCap = p->nCap;
if ( p->nCap >= nCap )
return;
-
while (p->nCap < nCap)
{
- unsigned delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1;
+ unsigned delta = ( ( p->nCap >> 1 ) + ( p->nCap >> 3 ) + 2 ) & ~1;
p->nCap += delta;
assert(p->nCap >= nPrevCap);
}
-
assert(p->nCap > 0);
- p->pData = ABC_REALLOC(unsigned, p->pData, p->nCap);
+ p->pData = ABC_REALLOC( unsigned, p->pData, p->nCap );
}
/**Function*************************************************************
@@ -160,12 +158,10 @@ static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
{
unsigned nPrevSize;
assert(nSize > 0);
- xSAT_MemGrow(p, p->nSize + nSize);
-
+ xSAT_MemGrow( p, p->nSize + nSize );
nPrevSize = p->nSize;
p->nSize += nSize;
assert(p->nSize > nPrevSize);
-
return nPrevSize;
}
diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c
index 5806409e..467f5f8d 100644
--- a/src/sat/xsat/xsatSolver.c
+++ b/src/sat/xsat/xsatSolver.c
@@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-static inline int xSAT_SolverDecide( xSAT_Solver_t* s )
+static inline int xSAT_SolverDecide( xSAT_Solver_t * s )
{
int NextVar = VarUndef;
@@ -74,7 +74,7 @@ static inline int xSAT_SolverDecide( xSAT_Solver_t* s )
SeeAlso []
***********************************************************************/
-void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s )
+void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t * s )
{
Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) );
int Var;
@@ -100,14 +100,14 @@ void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s )
***********************************************************************/
static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
{
- unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
int i;
+ unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );
for ( i = 0; i < Vec_IntSize( s->vActivity ); i++ )
pActivity[i] >>= 19;
s->nVarActInc >>= 19;
- s->nVarActInc = Abc_MaxInt( s->nVarActInc, (1 << 5) );
+ s->nVarActInc = Abc_MaxInt( s->nVarActInc, ( 1 << 5 ) );
}
/**Function*************************************************************
@@ -121,9 +121,9 @@ static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
SeeAlso []
***********************************************************************/
-static inline void xSAT_SolverVarActBump( xSAT_Solver_t* s, int Var )
+static inline void xSAT_SolverVarActBump( xSAT_Solver_t * s, int Var )
{
- unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
+ unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );
pActivity[Var] += s->nVarActInc;
if ( pActivity[Var] & 0x80000000 )
@@ -167,7 +167,7 @@ static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s )
Vec_IntForEachEntry( s->vLearnts, CRef, i )
{
- pC = xSAT_SolverReadClause( s, (unsigned) CRef );
+ pC = xSAT_SolverReadClause( s, ( unsigned ) CRef );
pC->pData[pC->nSize].Act >>= 14;
}
s->nClaActInc >>= 14;
@@ -221,16 +221,16 @@ static inline void xSAT_SolverClaActDecay( xSAT_Solver_t * s )
***********************************************************************/
static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
{
- int nLBD = 0;
int i;
+ int nLBD = 0;
s->nStamp++;
- for ( i = 0; i < (int)pCla->nSize; i++ )
+ for ( i = 0; i < pCla->nSize; i++ )
{
int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) );
- if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+ if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
{
- Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+ Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
nLBD++;
}
}
@@ -239,16 +239,16 @@ static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla
static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits )
{
- int nLBD = 0;
int i;
+ int nLBD = 0;
s->nStamp++;
for ( i = 0; i < Vec_IntSize( vLits ); i++ )
{
int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Vec_IntEntry( vLits, i ) ) );
- if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+ if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
{
- Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+ Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
nLBD++;
}
}
@@ -330,13 +330,13 @@ unsigned xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
SeeAlso []
***********************************************************************/
-int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason )
+int xSAT_SolverEnqueue( xSAT_Solver_t * s, int Lit, unsigned Reason )
{
int Var = xSAT_Lit2Var( Lit );
- Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) );
+ Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) );
Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
- Vec_IntWriteEntry( s->vReasons, Var, (int) Reason );
+ Vec_IntWriteEntry( s->vReasons, Var, ( int ) Reason );
Vec_IntPush( s->vTrail, Lit );
return true;
@@ -353,7 +353,7 @@ int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason )
SeeAlso []
***********************************************************************/
-static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit )
+static inline void xSAT_SolverNewDecision( xSAT_Solver_t * s, int Lit )
{
assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX );
s->Stats.nDecisions++;
@@ -375,6 +375,7 @@ static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit )
void xSAT_SolverCancelUntil( xSAT_Solver_t * s, int Level )
{
int c;
+
if ( xSAT_SolverDecisionLevel( s ) <= Level )
return;
@@ -410,30 +411,30 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
{
int top = Vec_IntSize( s->vTagged );
- assert( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
+ assert( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
Vec_IntClear( s->vStack );
Vec_IntPush( s->vStack, xSAT_Lit2Var( Lit ) );
while ( Vec_IntSize( s->vStack ) )
{
+ int i;
int v = Vec_IntPop( s->vStack );
xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( unsigned ) Vec_IntEntry( s->vReasons, v ) );
- int* Lits = &( c->pData[0].Lit );
- int i;
- assert( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
+ int * Lits = &( c->pData[0].Lit );
+ assert( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
{
assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
ABC_SWAP( int, Lits[0], Lits[1] );
}
- for (i = 1; i < (int)c->nSize; i++)
+ for ( i = 1; i < c->nSize; i++ )
{
int v = xSAT_Lit2Var( Lits[i] );
if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) )
{
- if ( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ((1 << (Vec_IntEntry( s->vLevels, v ) & 31)) & MinLevel))
+ if ( ( unsigned ) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ( ( 1 << (Vec_IntEntry( s->vLevels, v ) & 31 ) ) & MinLevel ) )
{
Vec_IntPush( s->vStack, v );
Vec_IntPush( s->vTagged, Lits[i] );
@@ -443,7 +444,7 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
{
int Lit;
Vec_IntForEachEntryStart( s->vTagged, Lit, i, top )
- Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var(Lit), 0 );
+ Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
Vec_IntShrink( s->vTagged, top );
return 0;
}
@@ -479,40 +480,34 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
/* Remove reduntant literals */
Vec_IntAppend( s->vTagged, vLits );
for ( i = j = 1; i < Vec_IntSize( vLits ); i++ )
- if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
+ if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
pLits[j++] = pLits[i];
Vec_IntShrink( vLits, j );
/* Binary Resolution */
if( Vec_IntSize( vLits ) <= 30 && xSAT_SolverClaCalcLBD2( s, vLits ) <= 6 )
{
+ int nb, l;
int Lit;
int FlaseLit = xSAT_NegLit( pLits[0] );
- int nb;
- int l;
-
- xSAT_WatchList_t * ws;
- xSAT_Watcher_t * begin;
- xSAT_Watcher_t * end;
+ xSAT_WatchList_t * ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
+ xSAT_Watcher_t * begin = xSAT_WatchListArray( ws );
+ xSAT_Watcher_t * end = begin + xSAT_WatchListSize( ws );
xSAT_Watcher_t * pWatcher;
s->nStamp++;
Vec_IntForEachEntry( vLits, Lit, i )
- Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp );
-
- ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
- begin = xSAT_WatchListArray( ws );
- end = begin + xSAT_WatchListSize( ws );
+ Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), ( int ) s->nStamp );
nb = 0;
for ( pWatcher = begin; pWatcher < end; pWatcher++ )
{
int ImpLit = pWatcher->Blocker;
- if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == (int)s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
+ if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
{
nb++;
- Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 );
+ Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), ( int )( s->nStamp - 1 ) );
}
}
@@ -520,7 +515,7 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
if ( nb > 0 )
{
for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ )
- if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != (int)s->nStamp )
+ if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp )
{
int TempLit = pLits[l];
pLits[l] = pLits[i];
@@ -546,43 +541,44 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
***********************************************************************/
static void xSAT_SolverAnalyze( xSAT_Solver_t* s, unsigned ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD )
{
- int* trail = Vec_IntArray( s->vTrail );
- int Count = 0;
+ int * trail = Vec_IntArray( s->vTrail );
+ int Count = 0;
int p = LitUndef;
int Idx = Vec_IntSize( s->vTrail ) - 1;
- int* Lits;
+ int * Lits;
int Lit;
int i, j;
Vec_IntPush( vLearnt, LitUndef );
do
{
- xSAT_Clause_t * c;
+ xSAT_Clause_t * pCla;
+
assert( ConfCRef != CRefUndef );
- c = xSAT_SolverReadClause(s, ConfCRef);
- Lits = &( c->pData[0].Lit );
+ pCla = xSAT_SolverReadClause(s, ConfCRef);
+ Lits = &( pCla->pData[0].Lit );
- if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
+ if( p != LitUndef && pCla->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
{
assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
ABC_SWAP( int, Lits[0], Lits[1] );
}
- if ( c->fLearnt )
- xSAT_SolverClaActBump( s, c );
+ if ( pCla->fLearnt )
+ xSAT_SolverClaActBump( s, pCla );
- if ( c->fLearnt && c->nLBD > 2 )
+ if ( pCla->fLearnt && pCla->nLBD > 2 )
{
- unsigned int nblevels = xSAT_SolverClaCalcLBD(s, c);
- if ( nblevels + 1 < c->nLBD )
+ unsigned int nLevels = xSAT_SolverClaCalcLBD( s, pCla );
+ if ( nLevels + 1 < pCla->nLBD )
{
- if (c->nLBD <= s->Config.nLBDFrozenClause)
- c->fCanBeDel = 0;
- c->nLBD = nblevels;
+ if ( pCla->nLBD <= s->Config.nLBDFrozenClause )
+ pCla->fCanBeDel = 0;
+ pCla->nLBD = nLevels;
}
}
- for ( j = ( p == LitUndef ? 0 : 1 ); j < (int)c->nSize; j++ )
+ for ( j = ( p == LitUndef ? 0 : 1 ); j < pCla->nSize; j++ )
{
int Var = xSAT_Lit2Var( Lits[j] );
@@ -605,14 +601,13 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, unsigned ConfCRef, Vec_Int_t *
// Next clause to look at
p = trail[Idx+1];
- ConfCRef = (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
+ ConfCRef = ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( p ), 0 );
Count--;
} while ( Count > 0 );
Vec_IntArray( vLearnt )[0] = xSAT_NegLit( p );
-
xSAT_SolverClaMinimisation( s, vLearnt );
// Find the backtrack level
@@ -677,41 +672,38 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
while ( s->iQhead < Vec_IntSize( s->vTrail ) )
{
int p = Vec_IntEntry( s->vTrail, s->iQhead++ );
-
xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p );
xSAT_Watcher_t* begin = xSAT_WatchListArray( ws );
xSAT_Watcher_t* end = begin + xSAT_WatchListSize( ws );
xSAT_Watcher_t *i, *j;
nProp++;
- for (i = begin; i < end; i++)
+ for ( i = begin; i < end; i++ )
{
- if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == xSAT_LitSign(xSAT_NegLit(i->Blocker)))
+ if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) )
{
return i->CRef;
}
- else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == VarX)
- xSAT_SolverEnqueue(s, i->Blocker, i->CRef);
+ else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
+ xSAT_SolverEnqueue( s, i->Blocker, i->CRef );
}
-
- ws = xSAT_VecWatchListEntry( s->vWatches, p);
+ ws = xSAT_VecWatchListEntry( s->vWatches, p );
begin = xSAT_WatchListArray( ws );
end = begin + xSAT_WatchListSize( ws );
for ( i = j = begin; i < end; )
{
- xSAT_Clause_t* c;
+ xSAT_Clause_t * pCla;
xSAT_Watcher_t w;
-
if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
{
*j++ = *i++;
continue;
}
- c = xSAT_SolverReadClause( s, i->CRef );
- Lits = &( c->pData[0].Lit );
+ pCla = xSAT_SolverReadClause( s, i->CRef );
+ Lits = &( pCla->pData[0].Lit );
// Make sure the false literal is data[1]:
NegLit = xSAT_NegLit( p );
@@ -731,8 +723,8 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
else
{
// Look for new watch:
- int* stop = Lits + c->nSize;
- int* k;
+ int * stop = Lits + pCla->nSize;
+ int * k;
for ( k = Lits + 2; k < stop; k++ )
{
if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) )
@@ -791,7 +783,7 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
int nLearnedOld = Vec_IntSize( s->vLearnts );
int i, limit;
unsigned CRef;
- xSAT_Clause_t * c;
+ xSAT_Clause_t * pCla;
xSAT_Clause_t ** learnts_cls;
learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld );
@@ -812,21 +804,22 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
for ( i = 0; i < nLearnedOld; i++ )
{
unsigned CRef;
- c = learnts_cls[i];
- CRef = xSAT_MemCRef( s->pMemory, (unsigned * ) c );
- assert(c->fMark == 0);
- if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) )
+
+ pCla = learnts_cls[i];
+ CRef = xSAT_MemCRef( s->pMemory, ( unsigned * ) pCla );
+ assert( pCla->fMark == 0 );
+ if ( pCla->fCanBeDel && pCla->nLBD > 2 && pCla->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pCla->pData[0].Lit ) ) != CRef && ( i < limit ) )
{
- c->fMark = 1;
- s->Stats.nLearntLits -= c->nSize;
- xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[0].Lit ) ), CRef );
- xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[1].Lit ) ), CRef );
+ pCla->fMark = 1;
+ s->Stats.nLearntLits -= pCla->nSize;
+ xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), CRef );
+ xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), CRef );
}
else
{
- if (!c->fCanBeDel)
+ if ( !pCla->fCanBeDel )
limit++;
- c->fCanBeDel = 1;
+ pCla->fCanBeDel = 1;
Vec_IntPush( s->vLearnts, CRef );
}
}
@@ -876,7 +869,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
return LBoolFalse;
xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) );
- if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * (iword)xSAT_BQueueAvg( s->bqTrail ) ) ) )
+ if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * ( iword ) xSAT_BQueueAvg( s->bqTrail ) ) ) )
xSAT_BQueueClean(s->bqLBD);
Vec_IntClear( s->vLearntClause );
@@ -896,7 +889,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
{
/* No conflict */
int NextVar;
- if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( (iword)xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / (iword)s->Stats.nConflicts ) ) )
+ if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( ( iword )xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
{
xSAT_BQueueClean( s->bqLBD );
xSAT_SolverCancelUntil( s, 0 );
@@ -942,23 +935,20 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
***********************************************************************/
void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, unsigned * pCRef )
{
- xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
unsigned nNewCRef;
xSAT_Clause_t * pNewCla;
+ xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
if ( pOldCla->fReallocd )
{
- *pCRef = (unsigned) pOldCla->nSize;
+ *pCRef = ( unsigned ) pOldCla->nSize;
return;
}
-
nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
-
memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
-
pOldCla->fReallocd = 1;
- pOldCla->nSize = (unsigned) nNewCRef;
+ pOldCla->nSize = ( unsigned ) nNewCRef;
*pCRef = nNewCRef;
}
@@ -997,14 +987,14 @@ void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
}
for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
- if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
- xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, (unsigned *)&( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
+ if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
+ xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, ( unsigned * ) &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
- pArray = (unsigned *) Vec_IntArray( s->vClauses );
+ pArray = ( unsigned * ) Vec_IntArray( s->vClauses );
for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ )
xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
diff --git a/src/sat/xsat/xsatSolver.h b/src/sat/xsat/xsatSolver.h
index 2bcd93b7..bf8bf419 100644
--- a/src/sat/xsat/xsatSolver.h
+++ b/src/sat/xsat/xsatSolver.h
@@ -81,9 +81,9 @@ struct xSAT_SolverOptions_t_
char fVerbose;
// Limits
- word nConfLimit; // external limit on the number of conflicts
- word nInsLimit; // external limit on the number of implications
- abctime nRuntimeLimit; // external limit on runtime
+ iword nConfLimit; // external limit on the number of conflicts
+ iword nInsLimit; // external limit on the number of implications
+ abctime nRuntimeLimit; // external limit on runtime
// Constants used for restart heuristic
double K; // Forces a restart
@@ -105,13 +105,13 @@ struct xSAT_Stats_t_
unsigned nStarts;
unsigned nReduceDB;
- word nDecisions;
- word nPropagations;
- word nInspects;
- word nConflicts;
+ iword nDecisions;
+ iword nPropagations;
+ iword nInspects;
+ iword nConflicts;
- word nClauseLits;
- word nLearntLits;
+ iword nClauseLits;
+ iword nLearntLits;
};
struct xSAT_Solver_t_
@@ -143,7 +143,7 @@ struct xSAT_Solver_t_
int nAssignSimplify; /* Number of top-level assignments since last
* execution of 'simplify()'. */
- word nPropSimplify; /* Remaining number of propagations that must be
+ int64_t nPropSimplify; /* Remaining number of propagations that must be
* made before next execution of 'simplify()'. */
/* Temporary data used by Search method */
@@ -203,10 +203,10 @@ static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned
static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
{
int i;
- int * lits = &( pCla->pData[0].Lit );
+ int * Lits = &( pCla->pData[0].Lit );
- for ( i = 0; i < (int)pCla->nSize; i++ )
- if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) )
+ for ( i = 0; i < pCla->nSize; i++ )
+ if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[i] ) ) == xSAT_LitSign( ( Lits[i] ) ) )
return true;
return false;
diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c
index 43c2d06e..7746dc0b 100644
--- a/src/sat/xsat/xsatSolverAPI.c
+++ b/src/sat/xsat/xsatSolverAPI.c
@@ -51,6 +51,7 @@ xSAT_SolverOptions_t DefaultConfig =
30 //.nLBDFrozenClause = 30
};
+
/**Function*************************************************************
Synopsis []
@@ -125,7 +126,6 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s )
xSAT_VecWatchListFree( s->vWatches );
xSAT_VecWatchListFree( s->vBinWatches );
- // delete vectors
xSAT_HeapFree(s->hOrder);
Vec_IntFree( s->vTrailLim );
Vec_IntFree( s->vTrail );
diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h
index 2ba13c24..284be100 100644
--- a/src/sat/xsat/xsatWatchList.h
+++ b/src/sat/xsat/xsatWatchList.h
@@ -118,9 +118,9 @@ static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k )
static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e )
{
assert( v );
- if (v->nSize == v->nCap)
+ if ( v->nSize == v->nCap )
{
- int newsize = (v->nCap < 4) ? 4 : (v->nCap / 2) * 3;
+ int newsize = ( v->nCap < 4 ) ? 4 : ( v->nCap / 2 ) * 3;
v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize );
if ( v->pArray == NULL )
@@ -167,9 +167,9 @@ static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef )
xSAT_Watcher_t* ws = xSAT_WatchListArray(v);
int j = 0;
- for (; ws[j].CRef != CRef; j++);
- assert(j < xSAT_WatchListSize(v));
- memmove(v->pArray + j, v->pArray + j + 1, (v->nSize - j - 1) * sizeof(xSAT_Watcher_t));
+ for ( ; ws[j].CRef != CRef; j++ );
+ assert( j < xSAT_WatchListSize( v ) );
+ memmove( v->pArray + j, v->pArray + j + 1, ( v->nSize - j - 1 ) * sizeof( xSAT_Watcher_t ) );
v->nSize -= 1;
}
@@ -190,7 +190,7 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap )
v->nCap = 4;
v->nSize = 0;
- v->pArray = (xSAT_WatchList_t *) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
+ v->pArray = ( xSAT_WatchList_t * ) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
return v;
}
@@ -233,7 +233,7 @@ static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v )
int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3;
v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize );
- memset( v->pArray + v->nCap, 0, sizeof(xSAT_WatchList_t) * (newsize - v->nCap) );
+ memset( v->pArray + v->nCap, 0, sizeof( xSAT_WatchList_t ) * ( newsize - v->nCap ) );
if ( v->pArray == NULL )
{
printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n",
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 22:05:18 +0000