diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-13 10:34:17 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-13 10:34:17 +0800 |
| commit | cb49c5d0067bc2630c86d258bba5bfbbc5a5d916 (patch) | |
| tree | c57108762b34e2360a329ac36a0a47e7db8f0b74 | |
| parent | 81af996fee2626daf45936e892ab34f26bea2ada (diff) | |
| download | abc-cb49c5d0067bc2630c86d258bba5bfbbc5a5d916.tar.gz abc-cb49c5d0067bc2630c86d258bba5bfbbc5a5d916.tar.bz2 abc-cb49c5d0067bc2630c86d258bba5bfbbc5a5d916.zip | |
Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly.
| -rw-r--r-- | src/sat/xsat/xsatHeap.h | 4 | ||||
| -rw-r--r-- | src/sat/xsat/xsatSolver.c | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/sat/xsat/xsatHeap.h b/src/sat/xsat/xsatHeap.h index 2e873e59..409ce460 100644 --- a/src/sat/xsat/xsatHeap.h +++ b/src/sat/xsat/xsatHeap.h @@ -48,7 +48,7 @@ struct xSAT_Heap_t_ SeeAlso [] ***********************************************************************/ -inline int xSAT_HeapSize( xSAT_Heap_t * h ) +static inline int xSAT_HeapSize( xSAT_Heap_t * h ) { return Vec_IntSize( h->vHeap ); } @@ -64,7 +64,7 @@ inline int xSAT_HeapSize( xSAT_Heap_t * h ) SeeAlso [] ***********************************************************************/ -inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var ) +static 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/xsatSolver.c b/src/sat/xsat/xsatSolver.c index 91b0c595..5806409e 100644 --- a/src/sat/xsat/xsatSolver.c +++ b/src/sat/xsat/xsatSolver.c @@ -503,7 +503,6 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits ) ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit ); begin = xSAT_WatchListArray( ws ); end = begin + xSAT_WatchListSize( ws ); - pWatcher; nb = 0; for ( pWatcher = begin; pWatcher < end; pWatcher++ ) @@ -999,7 +998,7 @@ 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, &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) ); + 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++ ) |