luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly.

This commit is contained in:
Alan Mishchenko 2016-12-13 10:34:17 +08:00
parent 81af996fee
commit cb49c5d006
2 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/sat/xsat/xsatHeap.h
View File

@ -48,7 +48,7 @@ struct xSAT_Heap_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
inline int xSAT_HeapSize( xSAT_Heap_t * h ) static inline int xSAT_HeapSize( xSAT_Heap_t * h )
{ {
return Vec_IntSize( h->vHeap ); return Vec_IntSize( h->vHeap );
} }
@ -64,7 +64,7 @@ inline int xSAT_HeapSize( xSAT_Heap_t * h )
SeeAlso [] 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 ); return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 );
} }

3
src/sat/xsat/xsatSolver.c
View File

@ -503,7 +503,6 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit ); ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
begin = xSAT_WatchListArray( ws ); begin = xSAT_WatchListArray( ws );
end = begin + xSAT_WatchListSize( ws ); end = begin + xSAT_WatchListSize( ws );
pWatcher;
nb = 0; nb = 0;
for ( pWatcher = begin; pWatcher < end; pWatcher++ ) 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++ ) for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
if ( (unsigned) 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 ) )] ) ); xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, (unsigned *)&( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
pArray = ( unsigned * ) Vec_IntArray( s->vLearnts ); pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ ) for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )