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

Debugging a proof error.

This commit is contained in:
Alan Mishchenko 2012-07-13 18:47:04 -07:00
parent 4ebda996d7
commit bbf4b9a58d
2 changed files with 28 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/misc/vec/vecSet.h
View File

@ -154,25 +154,6 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
Vec_SetWriteLimit( p->pPages[0], 2 );
}
/**Function*************************************************************
Synopsis [Returns memory in bytes occupied by the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline double Vec_ReportMemory( Vec_Set_t * p )
{
double Mem = sizeof(Vec_Set_t);
Mem += p->nPagesAlloc * sizeof(void *);
Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
return Mem;
}
/**Function*************************************************************
Synopsis [Freeing vector.]
@ -197,6 +178,25 @@ static inline void Vec_SetFree( Vec_Set_t * p )
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Returns memory in bytes occupied by the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline double Vec_ReportMemory( Vec_Set_t * p )
{
double Mem = sizeof(Vec_Set_t);
Mem += p->nPagesAlloc * sizeof(void *);
Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
return Mem;
}
/**Function*************************************************************
Synopsis [Appending entries to vector.]
@ -233,19 +233,11 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
}
static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
{
int Before1, Before2, After;
int nWords = Vec_SetWordNum( nSize );
assert( nWords < (1 << p->nPageSize) );
Before1 = Vec_SetLimitS( p->pPages[p->iPageS] );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords >= (1 << p->nPageSize) )
Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 );
Before2 = Vec_SetLimitS( p->pPages[p->iPageS] );
Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
After = Vec_SetLimitS( p->pPages[p->iPageS] );
assert( Vec_SetHandCurrentS(p) - nWords < (1 << p->nPageSize) );
return Vec_SetHandCurrentS(p) - nWords;
}

34
src/sat/bsat/satProof.c
View File

@ -369,6 +369,7 @@ void Sat_ProofReduce2( sat_solver2 * s )
}
*/
void Sat_ProofCheck0( Vec_Set_t * vProof )
{
satset * pNode, * pFanin;
@ -381,6 +382,7 @@ void Sat_ProofCheck0( Vec_Set_t * vProof )
}
}
int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
{
// Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
@ -394,15 +396,13 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
clock_t clk = clock();
static clock_t TimeTotal = 0;
int RetValue;
static int Count = 0;
Count++;
Sat_ProofCheck0( vProof );
// collect visited nodes
nSize = Proof_MarkUsedRec( vProof, vRoots );
vUsed = Vec_PtrAlloc( nSize );
Sat_ProofCheck0( vProof );
// relabel nodes to use smaller space
Vec_SetShrinkS( vProof, 2 );
Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
@ -411,15 +411,13 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
if ( pNode->Id == 0 )
continue;
pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
assert( pNode->Id > 1 );
assert( pNode->Id < (1<<vProof->nPageSize) );
assert( pNode->Id + nSize < (1<<vProof->nPageSize) );
assert( pNode->Id > 0 );
Vec_PtrPush( vUsed, pNode );
// update fanins
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
{
assert( pFanin->Id > 1 );
assert( pFanin->Id > 0 );
pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
}
// else // problem clause
@ -427,40 +425,26 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
}
// update roots
Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
{
assert( pNode->Id > 1 );
Vec_IntWriteEntry( vRoots, i, pNode->Id );
}
// determine new pivot
assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) );
pPivot = Proof_NodeRead( vProof, hProofPivot );
RetValue = Vec_SetHandCurrentS(vProof);
// s->iProofPivot = Vec_PtrSize(vUsed);
Sat_ProofCheck0( vProof );
// compact the nodes
Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
{
int X = Proof_NodeWordNum(pNode->nEnts);
hTemp = pNode->Id; pNode->Id = 0;
assert( hTemp > 1 );
assert( hTemp + Proof_NodeWordNum(pNode->nEnts) < (1<<vProof->nPageSize) );
memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
if ( pPivot && pPivot <= pNode )
{
RetValue = hTemp;
pPivot = NULL;
}
{
satset * pTemp = (satset *)Vec_SetEntry(vProof, hTemp);
assert( pTemp->partA == 0 );
assert( X == Vec_SetWordNum( 2 + pTemp->nEnts ) );
}
}
Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) );
Vec_PtrFree( vUsed );
// report the result
if ( fVerbose )
{
@ -475,7 +459,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
Vec_SetShrinkLimits( vProof );
// Sat_ProofReduceCheck( s );
Sat_ProofCheck0( vProof );
Sat_ProofCheck0( vProof );
return RetValue;
}
@ -644,7 +629,6 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed )
if ( pFanin == NULL )
{
int Entry = (pNode->pEnts[k] >> 2);
assert( Entry <= MaxCla );
if ( Abc_InfoHasBit(pBitMap, Entry) )
continue;
Abc_InfoSetBit(pBitMap, Entry);