summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-12-23 21:45:23 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-12-23 21:45:23 -0800
commitc59e2e9c962590540c2e78ec26f991c0251a47d5 (patch)
tree346b13c434583336faa62b1da7d730b4ebb0eb2a /src/sat
parent7facbc3cc932bf72581d164a0d2d5ea60ab9aa2d (diff)
downloadabc-c59e2e9c962590540c2e78ec26f991c0251a47d5.tar.gz
abc-c59e2e9c962590540c2e78ec26f991c0251a47d5.tar.bz2
abc-c59e2e9c962590540c2e78ec26f991c0251a47d5.zip
Transforming the solver to use different clause representation.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satProof.c45
-rw-r--r--src/sat/bsat/satSolver2.c7
-rw-r--r--src/sat/bsat/vecRec.h69
3 files changed, 83 insertions, 38 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 523de8fe..27fd698c 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -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 );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cb0d7b60..a4166fef 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -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 );
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
index 87a168b0..e92129be 100644
--- a/src/sat/bsat/vecRec.h
+++ b/src/sat/bsat/vecRec.h
@@ -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