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

Transforming the solver to use different clause representation.

This commit is contained in:
Alan Mishchenko 2011-12-23 21:45:23 -08:00
parent 7facbc3cc9
commit c59e2e9c96
3 changed files with 83 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -59,8 +59,8 @@ struct satset_t
////////////////////////////////////////////////////////////////////////
static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h) { return satset_read( (veci*)p, h ); }
static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); }
//static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
//static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); }
static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; }
static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h) { return (satset*)Vec_RecEntryP(p, h); }
@ -156,15 +156,15 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
SeeAlso []
***********************************************************************/
void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
{
satset * pNext;
int i, hNode;
satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
int i;
if ( pNode->Id )
return;
// start with node
pNode->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNode) << 1 );
Vec_IntPush( vStack, hNode << 1 );
// perform DFS search
while ( Vec_IntSize(vStack) )
{
@ -182,7 +182,7 @@ void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUs
if ( pNext && !pNext->Id )
{
pNext->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNext) << 1 ); // add first time
Vec_IntPush( vStack, (pNode->pEnts[i] >> 2) << 1 ); // add first time
}
}
}
@ -207,13 +207,11 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
vUsed = Vec_IntAlloc( 1000 );
vStack = Vec_IntAlloc( 1000 );
if ( hRoot )
Proof_CollectUsed_iter( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
Proof_CollectUsed_iter( vProof, hRoot, vUsed, vStack );
else
{
satset * pNode;
int i;
Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack );
Vec_IntForEachEntry( vRoots, Entry, i )
Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
}
Vec_IntFree( vStack );
// Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
@ -255,17 +253,17 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
SeeAlso []
***********************************************************************/
void Proof_CollectUsed_rec( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed )
void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
{
satset * pNext;
satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
int i;
if ( pNode->Id )
return;
pNode->Id = 1;
Proof_NodeForeachFanin( vProof, pNode, pNext, i )
if ( pNext && !pNext->Id )
Proof_CollectUsed_rec( vProof, pNext, vUsed );
Vec_IntPush( vUsed, Proof_NodeHandle(vProof, pNode) );
Proof_CollectUsed_rec( vProof, pNode->pEnts[i] >> 2, vUsed );
Vec_IntPush( vUsed, hNode );
}
/**Function*************************************************************
@ -285,13 +283,12 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
assert( (hRoot > 0) ^ (vRoots != NULL) );
vUsed = Vec_IntAlloc( 1000 );
if ( hRoot )
Proof_CollectUsed_rec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
Proof_CollectUsed_rec( vProof, hRoot, vUsed );
else
{
satset * pNode;
int i;
Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
Proof_CollectUsed_rec( vProof, pNode, vUsed );
int i, Entry;
Vec_IntForEachEntry( vRoots, Entry, i )
Proof_CollectUsed_rec( vProof, Entry, vUsed );
}
return vUsed;
}
@ -512,7 +509,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
if ( pFanin && !pFanin->mark )
{
pFanin->mark = 1;
Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) );
Vec_IntPush( vCore, pNode->pEnts[i] >> 2 );
}
}
// clean core clauses and reexpress core in terms of clause IDs
@ -653,7 +650,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
pNode->Id = Aig_ObjToLit(pObj);
}
// save the result
assert( Proof_NodeHandle(vProof, pNode) == hRoot );
// assert( Proof_NodeHandle(vProof, pNode) == hRoot );
Aig_ObjCreatePo( pAig, pObj );
Aig_ManCleanup( pAig );
@ -759,7 +756,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
pNode->Id = Tru_ManInsert( pTru, pRes );
}
// save the result
assert( Proof_NodeHandle(vProof, pNode) == hRoot );
// assert( Proof_NodeHandle(vProof, pNode) == hRoot );
// Aig_ObjCreatePo( pAig, pObj );
// Aig_ManCleanup( pAig );

7
src/sat/bsat/satSolver2.c
View File

@ -1308,15 +1308,16 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
void sat_solver2_delete(sat_solver2* s)
{
// veci * pCore;
veci * pCore;
// report statistics
printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
/*
pCore = Sat_ProofCore( s );
printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
veci_delete( pCore );
ABC_FREE( pCore );
*/
if ( s->fProofLogging )
Sat_ProofCheck( s );

69
src/sat/bsat/vecRec.h
View File

@ -40,14 +40,14 @@ ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
// data-structure for logging entries
// memory is allocated in 2^(p->LogSize+2) byte chunks
// memory is allocated in 'p->Mask+1' int chunks
// the first 'int' of each entry cannot be 0
typedef struct Vec_Rec_t_ Vec_Rec_t;
struct Vec_Rec_t_
{
int LogSize; // the log size of one chunk in 'int'
int Mask; // mask for the log size
int hCurrent; // current position
int hShadow; // current position
int nEntries; // total number of entries
int nChunks; // total number of chunks
int nChunksAlloc; // the number of allocated chunks
@ -89,8 +89,7 @@ static inline Vec_Rec_t * Vec_RecAlloc()
{
Vec_Rec_t * p;
p = ABC_CALLOC( Vec_Rec_t, 1 );
p->LogSize = 15; // chunk size = 2^15 ints = 128 Kb
p->Mask = (1 << p->LogSize) - 1;
p->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
p->hCurrent = (1 << 16);
p->nChunks = 1;
p->nChunksAlloc = 16;
@ -105,8 +104,7 @@ static inline void Vec_RecAlloc_( Vec_Rec_t * p )
// Vec_Rec_t * p;
// p = ABC_CALLOC( Vec_Rec_t, 1 );
memset( p, 0, sizeof(Vec_Rec_t) );
p->LogSize = 15; // chunk size = 2^15 ints = 128 Kb
p->Mask = (1 << p->LogSize) - 1;
p->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
p->hCurrent = (1 << 16);
p->nChunks = 1;
p->nChunksAlloc = 16;
@ -162,7 +160,7 @@ static inline int Vec_RecShift( int i )
***********************************************************************/
static inline int Vec_RecSize( Vec_Rec_t * p )
{
return Vec_RecChunk(p->hCurrent) * (1 << p->LogSize);
return Vec_RecChunk(p->hCurrent) * (p->Mask + 1);
}
/**Function*************************************************************
@ -296,7 +294,6 @@ static inline void Vec_RecFree_( Vec_Rec_t * p )
***********************************************************************/
static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
{
int RetValue;
assert( nSize <= p->Mask );
assert( Vec_RecEntry(p, p->hCurrent) == 0 );
assert( Vec_RecChunk(p->hCurrent) == p->nChunks );
@ -309,15 +306,14 @@ static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
p->nChunksAlloc *= 2;
}
if ( p->pChunks[p->nChunks] == NULL )
p->pChunks[p->nChunks] = ABC_ALLOC( int, (1 << p->LogSize) );
p->pChunks[p->nChunks] = ABC_ALLOC( int, (p->Mask + 1) );
p->pChunks[p->nChunks][0] = 0;
p->hCurrent = p->nChunks << 16;
}
RetValue = p->hCurrent;
p->hCurrent += nSize;
*Vec_RecEntryP(p, p->hCurrent) = 0;
p->nEntries++;
return RetValue;
return p->hCurrent - nSize;
}
/**Function*************************************************************
@ -338,6 +334,57 @@ static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize )
return Handle;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_RecSetShadow( Vec_Rec_t * p, int hShadow )
{
p->hShadow = hShadow;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_RecReadShadow( Vec_Rec_t * p )
{
return p->hShadow;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_RecAppendShadow( Vec_Rec_t * p, int nSize )
{
if ( Vec_RecShift(p->hShadow) + nSize >= p->Mask )
p->hShadow = ((Vec_RecChunk(p->hShadow) + 1) << 16);
p->hShadow += nSize;
return p->hShadow - nSize;
}
ABC_NAMESPACE_HEADER_END