summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-04-07 13:04:02 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2020-04-07 13:04:02 -0700
commit2dfadb96072d39f358fdd75e97e30acc6830edca (patch)
tree1c8485fe46c0df78ec755ae3e566c2e0af3ac3f2 /src/aig/gia
parent71fd9165e39b5bda06e88d5bb545a3ef38c94e96 (diff)
downloadabc-2dfadb96072d39f358fdd75e97e30acc6830edca.tar.gz
abc-2dfadb96072d39f358fdd75e97e30acc6830edca.tar.bz2
abc-2dfadb96072d39f358fdd75e97e30acc6830edca.zip
Corner-case bug fix in SAT-based sim info generation.
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/giaSimBase.c10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index eb9ba375..1adff0be 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -221,20 +221,22 @@ int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare
}
return (int)(i == iPat);
}
-Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes )
+Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes, int nUnDecs )
{
int c, iCur = 0, iPat = 0;
int nWordsMax = Abc_Bit6WordNum( nCexes );
Vec_Wrd_t * vSimsIn = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWordsMax );
Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax );
Vec_Wrd_t * vSimsRes = NULL;
- for ( c = 0; c < nCexes; c++ )
+ for ( c = 0; c < nCexes + nUnDecs; c++ )
{
int Out = Vec_IntEntry( vCexStore, iCur++ );
int Size = Vec_IntEntry( vCexStore, iCur++ );
+ if ( Size == -1 )
+ continue;
iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
iCur += Size;
- assert( iPat <= nCexes );
+ assert( iPat <= nCexes + nUnDecs );
Out = 0;
}
printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
@@ -430,7 +432,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
printf( "There are no counter-examples. No need for more simulation.\n" );
else
{
- vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] );
+ vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1], Counts[0] );
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = vSimsIn;
Gia_ManSimProfile( p );