diff options
Diffstat (limited to 'src/sat/xsat')
| -rw-r--r-- | src/sat/xsat/xsatBQueue.h | 17 | ||||
| -rw-r--r-- | src/sat/xsat/xsatClause.h | 2 | ||||
| -rw-r--r-- | src/sat/xsat/xsatMemory.h | 31 | ||||
| -rw-r--r-- | src/sat/xsat/xsatSolver.c | 129 | ||||
| -rw-r--r-- | src/sat/xsat/xsatSolver.h | 31 | ||||
| -rw-r--r-- | src/sat/xsat/xsatSolverAPI.c | 29 | ||||
| -rw-r--r-- | src/sat/xsat/xsatWatchList.h | 7 |
7 files changed, 137 insertions, 109 deletions
diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h index 37951684..6c170c93 100644 --- a/src/sat/xsat/xsatBQueue.h +++ b/src/sat/xsat/xsatBQueue.h @@ -24,6 +24,7 @@ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// + #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START @@ -31,6 +32,7 @@ ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + typedef struct xSAT_BQueue_t_ xSAT_BQueue_t; struct xSAT_BQueue_t_ { @@ -38,13 +40,14 @@ struct xSAT_BQueue_t_ int nCap; int iFirst; int iEmpty; - uint64_t nSum; - uint32_t * pData; + word nSum; + word * pData; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + /**Function************************************************************* Synopsis [] @@ -60,7 +63,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( uint32_t, nCap ); + p->pData = ABC_CALLOC( word, nCap ); return p; } @@ -92,7 +95,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p ) SeeAlso [] ***********************************************************************/ -static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value ) +static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value ) { if ( p->nSize == p->nCap ) { @@ -125,8 +128,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value ) ***********************************************************************/ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) { - assert( p->nSize >= 1 ); int RetValue = p->pData[p->iFirst]; + assert( p->nSize >= 1 ); p->nSum -= RetValue; p->iFirst = ( p->iFirst + 1 ) % p->nCap; p->nSize--; @@ -144,9 +147,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) SeeAlso [] ***********************************************************************/ -static inline uint32_t xSAT_BQueueAvg( xSAT_BQueue_t * p ) +static inline word xSAT_BQueueAvg( xSAT_BQueue_t * p ) { - return ( uint32_t )( p->nSum / ( ( uint64_t ) p->nSize ) ); + return ( word )( p->nSum / ( ( word ) p->nSize ) ); } /**Function************************************************************* diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h index 39f0a0c8..d05eb6de 100644 --- a/src/sat/xsat/xsatClause.h +++ b/src/sat/xsat/xsatClause.h @@ -96,7 +96,7 @@ static void xSAT_ClausePrint( xSAT_Clause_t * pCla ) int i; printf("{ "); - for ( i = 0; i < pCla->nSize; i++ ) + for ( i = 0; i < (int)pCla->nSize; i++ ) printf("%d ", pCla->pData[i].Lit ); printf("}\n"); } diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h index 3a961b97..3324a563 100644 --- a/src/sat/xsat/xsatMemory.h +++ b/src/sat/xsat/xsatMemory.h @@ -36,10 +36,10 @@ ABC_NAMESPACE_HEADER_START typedef struct xSAT_Mem_t_ xSAT_Mem_t; struct xSAT_Mem_t_ { - uint32_t nSize; - uint32_t nCap; - uint32_t nWasted; - uint32_t * pData; + unsigned nSize; + unsigned nCap; + unsigned nWasted; + unsigned * pData; }; //////////////////////////////////////////////////////////////////////// @@ -58,7 +58,7 @@ struct xSAT_Mem_t_ ***********************************************************************/ static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h ) { - return h != UINT32_MAX ? ( xSAT_Clause_t * )( p->pData + h ) : NULL; + return h != 0xFFFFFFFF ? ( xSAT_Clause_t * )( p->pData + h ) : NULL; } /**Function************************************************************* @@ -72,21 +72,21 @@ static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h ) SeeAlso [] ***********************************************************************/ -static inline void xSAT_MemGrow( xSAT_Mem_t * p, uint32_t nCap ) +static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap ) { + unsigned nPrevCap = p->nCap; if ( p->nCap >= nCap ) return; - uint32_t nPrevCap = p->nCap; while (p->nCap < nCap) { - uint32_t 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(uint32_t, p->pData, p->nCap); + p->pData = ABC_REALLOC(unsigned, p->pData, p->nCap); } /**Function************************************************************* @@ -156,12 +156,13 @@ static inline void xSAT_MemFree( xSAT_Mem_t * p ) SeeAlso [] ***********************************************************************/ -static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) +static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) { + unsigned nPrevSize; assert(nSize > 0); xSAT_MemGrow(p, p->nSize + nSize); - uint32_t nPrevSize = p->nSize; + nPrevSize = p->nSize; p->nSize += nSize; assert(p->nSize > nPrevSize); @@ -179,9 +180,9 @@ static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) SeeAlso [] ***********************************************************************/ -static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC ) +static inline unsigned xSAT_MemCRef( xSAT_Mem_t * p, unsigned * pC ) { - return ( uint32_t )( pC - &(p->pData[0]) ); + return ( unsigned )( pC - &(p->pData[0]) ); } /**Function************************************************************* @@ -195,7 +196,7 @@ static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC ) SeeAlso [] ***********************************************************************/ -static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p ) +static inline unsigned xSAT_MemCap( xSAT_Mem_t * p ) { return p->nCap; } @@ -211,7 +212,7 @@ static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p ) SeeAlso [] ***********************************************************************/ -static inline uint32_t xSAT_MemWastedCap( xSAT_Mem_t * p ) +static inline unsigned xSAT_MemWastedCap( xSAT_Mem_t * p ) { return p->nWasted; } diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c index d6968a2d..91b0c595 100644 --- a/src/sat/xsat/xsatSolver.c +++ b/src/sat/xsat/xsatSolver.c @@ -101,8 +101,9 @@ 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; - for ( int i = 0; i < Vec_IntSize( s->vActivity ); i++ ) + for ( i = 0; i < Vec_IntSize( s->vActivity ); i++ ) pActivity[i] >>= 19; s->nVarActInc >>= 19; @@ -166,7 +167,7 @@ static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s ) Vec_IntForEachEntry( s->vLearnts, CRef, i ) { - pC = xSAT_SolverReadClause( s, (uint32_t) CRef ); + pC = xSAT_SolverReadClause( s, (unsigned) CRef ); pC->pData[pC->nSize].Act >>= 14; } s->nClaActInc >>= 14; @@ -221,9 +222,10 @@ 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; s->nStamp++; - for ( int i = 0; i < pCla->nSize; i++ ) + for ( i = 0; i < (int)pCla->nSize; i++ ) { int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) ); if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp ) @@ -238,9 +240,10 @@ 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; s->nStamp++; - for ( int i = 0; i < Vec_IntSize( vLits ); i++ ) + 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 ) @@ -263,17 +266,18 @@ static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits ) SeeAlso [] ***********************************************************************/ -uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt ) +unsigned xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt ) { - assert( Vec_IntSize( vLits ) > 1); - assert( fLearnt == 0 || fLearnt == 1 ); - - uint32_t CRef; + unsigned CRef; xSAT_Clause_t * pCla; xSAT_Watcher_t w1; xSAT_Watcher_t w2; + unsigned nWords; - uint32_t nWords = 3 + fLearnt + Vec_IntSize( vLits ); + assert( Vec_IntSize( vLits ) > 1); + assert( fLearnt == 0 || fLearnt == 1 ); + + nWords = 3 + fLearnt + Vec_IntSize( vLits ); CRef = xSAT_MemAppend( s->pMemory, nWords ); pCla = xSAT_SolverReadClause( s, CRef ); pCla->fLearnt = fLearnt; @@ -326,11 +330,11 @@ uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt ) SeeAlso [] ***********************************************************************/ -int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t Reason ) +int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason ) { int Var = xSAT_Lit2Var( Lit ); - Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) ); + Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) ); Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) ); Vec_IntWriteEntry( s->vReasons, Var, (int) Reason ); Vec_IntPush( s->vTrail, Lit ); @@ -370,16 +374,17 @@ 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; - for ( int c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- ) + for ( c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- ) { int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) ); Vec_StrWriteEntry( s->vAssigns, Var, VarX ); Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef ); - Vec_StrWriteEntry( s->vPolarity, Var, xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) ); + Vec_StrWriteEntry( s->vPolarity, Var, ( char )xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) ); if ( !xSAT_HeapInHeap( s->hOrder, Var ) ) xSAT_HeapInsert( s->hOrder, Var ); @@ -405,17 +410,17 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel ) { int top = Vec_IntSize( s->vTagged ); - assert( (uint32_t) 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 v = Vec_IntPop( s->vStack ); - assert( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef); - xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( uint32_t ) Vec_IntEntry( s->vReasons, v ) ); + 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); if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) ) { @@ -423,12 +428,12 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel ) ABC_SWAP( int, Lits[0], Lits[1] ); } - for (i = 1; i < c->nSize; i++) + for (i = 1; i < (int)c->nSize; i++) { int v = xSAT_Lit2Var( Lits[i] ); if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) ) { - if ( (uint32_t) 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] ); @@ -474,7 +479,7 @@ 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 ( (uint32_t) 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 ); @@ -483,33 +488,40 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits ) { 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_Watcher_t * pWatcher; s->nStamp++; Vec_IntForEachEntry( vLits, Lit, i ) Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp ); - 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; + ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit ); + begin = xSAT_WatchListArray( ws ); + end = begin + xSAT_WatchListSize( ws ); + pWatcher; - int nb = 0; + nb = 0; for ( pWatcher = begin; pWatcher < end; pWatcher++ ) { int ImpLit = pWatcher->Blocker; - if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) ) + if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == (int)s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) ) { nb++; Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 ); } } - int l = Vec_IntSize( vLits ) - 1; + l = Vec_IntSize( vLits ) - 1; if ( nb > 0 ) { for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ ) - if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp ) + if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != (int)s->nStamp ) { int TempLit = pLits[l]; pLits[l] = pLits[i]; @@ -533,20 +545,22 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits ) SeeAlso [] ***********************************************************************/ -static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD ) +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 p = LitUndef; int Idx = Vec_IntSize( s->vTrail ) - 1; int* Lits; + int Lit; int i, j; Vec_IntPush( vLearnt, LitUndef ); do { + xSAT_Clause_t * c; assert( ConfCRef != CRefUndef ); - xSAT_Clause_t * c = xSAT_SolverReadClause(s, ConfCRef); + c = xSAT_SolverReadClause(s, ConfCRef); Lits = &( c->pData[0].Lit ); if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) ) @@ -569,7 +583,7 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * } } - for ( j = ( p == LitUndef ? 0 : 1 ); j < c->nSize; j++ ) + for ( j = ( p == LitUndef ? 0 : 1 ); j < (int)c->nSize; j++ ) { int Var = xSAT_Lit2Var( Lits[j] ); @@ -592,7 +606,7 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * // Next clause to look at p = trail[Idx+1]; - ConfCRef = (uint32_t) 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--; @@ -638,7 +652,6 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * Vec_IntClear( s->vLastDLevel ); } - int Lit; Vec_IntForEachEntry( s->vTagged, Lit, i ) Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 ); Vec_IntClear( s->vTagged ); @@ -655,9 +668,9 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * SeeAlso [] ***********************************************************************/ -uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ) +unsigned xSAT_SolverPropagate( xSAT_Solver_t* s ) { - uint32_t hConfl = CRefUndef; + unsigned hConfl = CRefUndef; int * Lits; int NegLit; int nProp = 0; @@ -689,13 +702,16 @@ uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ) for ( i = j = begin; i < end; ) { + xSAT_Clause_t* c; + xSAT_Watcher_t w; + if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) ) { *j++ = *i++; continue; } - xSAT_Clause_t* c = xSAT_SolverReadClause( s, i->CRef ); + c = xSAT_SolverReadClause( s, i->CRef ); Lits = &( c->pData[0].Lit ); // Make sure the false literal is data[1]: @@ -707,8 +723,9 @@ uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ) } assert( Lits[1] == NegLit ); - xSAT_Watcher_t w = { .CRef = i->CRef, - .Blocker = Lits[0] }; + w.CRef = i->CRef; + w.Blocker = Lits[0]; + // If 0th watch is true, then clause is already satisfied. if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) ) *j++ = w; @@ -774,7 +791,7 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s ) abctime clk = Abc_Clock(); int nLearnedOld = Vec_IntSize( s->vLearnts ); int i, limit; - uint32_t CRef; + unsigned CRef; xSAT_Clause_t * c; xSAT_Clause_t ** learnts_cls; @@ -795,10 +812,11 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s ) Vec_IntClear( s->vLearnts ); for ( i = 0; i < nLearnedOld; i++ ) { + unsigned CRef; c = learnts_cls[i]; - uint32_t CRef = xSAT_MemCRef( s->pMemory, (uint32_t * ) c ); + CRef = xSAT_MemCRef( s->pMemory, (unsigned * ) c ); assert(c->fMark == 0); - if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) ) + if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) ) { c->fMark = 1; s->Stats.nLearntLits -= c->nSize; @@ -838,19 +856,19 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s ) ***********************************************************************/ char xSAT_SolverSearch( xSAT_Solver_t * s ) { - ABC_INT64_T conflictC = 0; + iword conflictC = 0; s->Stats.nStarts++; for (;;) { - uint32_t hConfl = xSAT_SolverPropagate( s ); + unsigned hConfl = xSAT_SolverPropagate( s ); if ( hConfl != CRefUndef ) { /* Conflict */ int BacktrackLevel; unsigned nLBD; - uint32_t CRef; + unsigned CRef; s->Stats.nConflicts++; conflictC++; @@ -859,7 +877,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 * 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 ); @@ -879,7 +897,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s ) { /* No conflict */ int NextVar; - if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) ) + if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( (iword)xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / (iword)s->Stats.nConflicts ) ) ) { xSAT_BQueueClean( s->bqLBD ); xSAT_SolverCancelUntil( s, 0 ); @@ -923,17 +941,20 @@ char xSAT_SolverSearch( xSAT_Solver_t * s ) SeeAlso [] ***********************************************************************/ -void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pCRef ) +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; + if ( pOldCla->fReallocd ) { - *pCRef = (uint32_t) pOldCla->nSize; + *pCRef = (unsigned) pOldCla->nSize; return; } - uint32_t nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize ); - xSAT_Clause_t * pNewCla = xSAT_MemClauseHand( pDest, nNewCRef ); + nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize ); + pNewCla = xSAT_MemClauseHand( pDest, nNewCRef ); memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 ); @@ -956,7 +977,7 @@ void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pC void xSAT_SolverGarbageCollect( xSAT_Solver_t * s ) { int i; - uint32_t * pArray; + unsigned * pArray; xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc( xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) ); for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ ) @@ -977,14 +998,14 @@ void xSAT_SolverGarbageCollect( xSAT_Solver_t * s ) } for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ ) - if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef ) + if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef ) xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) ); - pArray = ( uint32_t * ) Vec_IntArray( s->vLearnts ); + pArray = ( unsigned * ) Vec_IntArray( s->vLearnts ); for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ ) xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) ); - pArray = (uint32_t *) 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 a6d646c6..2bcd93b7 100644 --- a/src/sat/xsat/xsatSolver.h +++ b/src/sat/xsat/xsatSolver.h @@ -70,7 +70,7 @@ enum LitUndef = -2 }; -#define CRefUndef UINT32_MAX +#define CRefUndef 0xFFFFFFFF //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// @@ -81,8 +81,8 @@ struct xSAT_SolverOptions_t_ char fVerbose; // Limits - ABC_INT64_T nConfLimit; // external limit on the number of conflicts - ABC_INT64_T nInsLimit; // external limit on the number of implications + word nConfLimit; // external limit on the number of conflicts + word nInsLimit; // external limit on the number of implications abctime nRuntimeLimit; // external limit on runtime // Constants used for restart heuristic @@ -105,13 +105,13 @@ struct xSAT_Stats_t_ unsigned nStarts; unsigned nReduceDB; - ABC_INT64_T nDecisions; - ABC_INT64_T nPropagations; - ABC_INT64_T nInspects; - ABC_INT64_T nConflicts; + word nDecisions; + word nPropagations; + word nInspects; + word nConflicts; - ABC_INT64_T nClauseLits; - ABC_INT64_T nLearntLits; + word nClauseLits; + word 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()'. */ - int64_t nPropSimplify; /* Remaining number of propagations that must be + word nPropSimplify; /* Remaining number of propagations that must be * made before next execution of 'simplify()'. */ /* Temporary data used by Search method */ @@ -195,16 +195,17 @@ static inline int xSAT_SolverDecisionLevel( xSAT_Solver_t * s ) return Vec_IntSize( s->vTrailLim ); } -static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, uint32_t h ) +static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned h ) { return xSAT_MemClauseHand( s->pMemory, h ); } static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla ) { + int i; int * lits = &( pCla->pData[0].Lit ); - for ( int i = 0; i < pCla->nSize; i++ ) + for ( i = 0; i < (int)pCla->nSize; i++ ) if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) ) return true; @@ -232,14 +233,14 @@ static inline void xSAT_SolverPrintState( xSAT_Solver_t * s ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern uint32_t xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt ); +extern unsigned xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt ); extern char xSAT_SolverSearch( xSAT_Solver_t * s ); extern void xSAT_SolverGarbageCollect( xSAT_Solver_t * s ); -extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t From ); +extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned From ); extern void xSAT_SolverCancelUntil( xSAT_Solver_t* s, int Level); -extern uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ); +extern unsigned xSAT_SolverPropagate( xSAT_Solver_t* s ); extern void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c index 7ee817ee..43c2d06e 100644 --- a/src/sat/xsat/xsatSolverAPI.c +++ b/src/sat/xsat/xsatSolverAPI.c @@ -32,23 +32,23 @@ ABC_NAMESPACE_IMPL_START xSAT_SolverOptions_t DefaultConfig = { - .fVerbose = 1, + 1, //.fVerbose = 1, - .nConfLimit = 0, - .nInsLimit = 0, - .nRuntimeLimit = 0, + 0, //.nConfLimit = 0, + 0, //.nInsLimit = 0, + 0, //.nRuntimeLimit = 0, - .K = 0.8, - .R = 1.4, - .nFirstBlockRestart = 10000, - .nSizeLBDQueue = 50, - .nSizeTrailQueue = 5000, + 0.8, //.K = 0.8, + 1.4, //.R = 1.4, + 10000, //.nFirstBlockRestart = 10000, + 50, //.nSizeLBDQueue = 50, + 5000, //.nSizeTrailQueue = 5000, - .nConfFirstReduce = 2000, - .nIncReduce = 300, - .nSpecialIncReduce = 1000, + 2000, //.nConfFirstReduce = 2000, + 300, //.nIncReduce = 300, + 1000, //.nSpecialIncReduce = 1000, - .nLBDFrozenClause = 30 + 30 //.nLBDFrozenClause = 30 }; /**Function************************************************************* @@ -142,6 +142,7 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s ) Vec_StrFree( s->vAssigns ); Vec_IntFree( s->vLevels ); Vec_IntFree( s->vReasons ); + Vec_IntFree( s->vStamp ); xSAT_BQueueFree(s->bqLBD); xSAT_BQueueFree(s->bqTrail); @@ -163,7 +164,7 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s ) int xSAT_SolverSimplify( xSAT_Solver_t * s ) { int i, j; - uint32_t CRef; + unsigned CRef; assert( xSAT_SolverDecisionLevel(s) == 0 ); if ( xSAT_SolverPropagate(s) != CRefUndef ) diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h index 454cfe44..2ba13c24 100644 --- a/src/sat/xsat/xsatWatchList.h +++ b/src/sat/xsat/xsatWatchList.h @@ -34,7 +34,7 @@ ABC_NAMESPACE_HEADER_START typedef struct xSAT_Watcher_t_ xSAT_Watcher_t; struct xSAT_Watcher_t_ { - uint32_t CRef; + unsigned CRef; int Blocker; }; @@ -162,7 +162,7 @@ static inline xSAT_Watcher_t* xSAT_WatchListArray( xSAT_WatchList_t * v ) SeeAlso [] ***********************************************************************/ -static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, uint32_t CRef ) +static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef ) { xSAT_Watcher_t* ws = xSAT_WatchListArray(v); int j = 0; @@ -207,7 +207,8 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap ) ***********************************************************************/ static inline void xSAT_VecWatchListFree( xSAT_VecWatchList_t* v ) { - for( int i = 0; i < v->nSize; i++ ) + int i; + for( i = 0; i < v->nSize; i++ ) xSAT_WatchListFree( v->pArray + i ); ABC_FREE( v->pArray ); |