summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaCSat2.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaCSat2.c')
-rw-r--r--src/aig/gia/giaCSat2.c114
1 files changed, 81 insertions, 33 deletions
diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat2.c
index f80c4533..ee0ce311 100644
--- a/src/aig/gia/giaCSat2.c
+++ b/src/aig/gia/giaCSat2.c
@@ -75,6 +75,7 @@ struct Cbs2_Man_t_
Vec_Str_t vMark;
Vec_Int_t vLevReason;
Vec_Int_t vWatches;
+ Vec_Int_t vWatchUpds;
Vec_Int_t vFanoutN;
Vec_Int_t vFanout0;
Vec_Int_t vActivity;
@@ -98,6 +99,7 @@ struct Cbs2_Man_t_
// other statistics
int nPropCalls[3];
int nFails[2];
+ int nClauseConf;
};
static inline int Cbs2_VarUnused( Cbs2_Man_t * p, int iVar ) { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; }
@@ -227,8 +229,9 @@ Cbs2_Man_t * Cbs2_ManAlloc( Gia_Man_t * pGia )
Vec_IntFill( &p->vFanout0, Gia_ManObjNum(pGia), 0 );
Vec_IntFill( &p->vFanoutN, 2*Gia_ManObjNum(pGia), 0 );
Vec_IntFill( &p->vActivity, Gia_ManObjNum(pGia), 0 );
- Vec_IntGrow( &p->vActStore, 1000 );
- Vec_IntGrow( &p->vJStore, 1000 );
+ Vec_IntGrow( &p->vActStore, 1000 );
+ Vec_IntGrow( &p->vJStore, 1000 );
+ Vec_IntGrow( &p->vWatchUpds, 1000 );
return p;
}
@@ -254,6 +257,7 @@ void Cbs2_ManStop( Cbs2_Man_t * p )
Vec_IntErase( &p->vActivity );
Vec_IntErase( &p->vActStore );
Vec_IntErase( &p->vJStore );
+ Vec_IntErase( &p->vWatchUpds );
Vec_IntFree( p->vModel );
Vec_IntFree( p->vTemp );
ABC_FREE( p->pClauses.pData );
@@ -370,6 +374,15 @@ static inline void Cbs2_QuePush( Cbs2_Que_t * p, int iObj )
}
p->pData[p->iTail++] = iObj;
}
+static inline void Cbs2_QueGrow( Cbs2_Que_t * p, int Plus )
+{
+ if ( p->iTail + Plus > p->nSize )
+ {
+ p->nSize *= 2;
+ p->pData = ABC_REALLOC( int, p->pData, p->nSize );
+ }
+ assert( p->iTail + Plus <= p->nSize );
+}
/**Function*************************************************************
@@ -588,14 +601,15 @@ static inline void Cbs2_ManAssign( Cbs2_Man_t * p, int iLit, int Level, int iRes
***********************************************************************/
static inline void Cbs2_ManPrintClause( Cbs2_Man_t * p, int Level, int hClause )
{
- int i, iObj;
+ int i, iLit;
assert( Cbs2_QueIsEmpty( &p->pClauses ) );
printf( "Level %2d : ", Level );
- Cbs2_ClauseForEachEntry( p, hClause, iObj, i )
- printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, iObj), Cbs2_VarDecLevel(p, iObj) );
+ Cbs2_ClauseForEachEntry( p, hClause, iLit, i )
+ printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) );
+// printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, Abc_Lit2Var(iLit)), Cbs2_VarDecLevel(p, Abc_Lit2Var(iLit)) );
printf( "\n" );
}
-static inline void Cbs2_ManPrintClauseNew( Cbs2_Man_t * p, int Level, int hClause )
+static inline void Cbs2_ManPrintCube( Cbs2_Man_t * p, int Level, int hClause )
{
int i, iObj;
assert( Cbs2_QueIsEmpty( &p->pClauses ) );
@@ -633,10 +647,21 @@ static inline void Cbs2_ManBumpClean( Cbs2_Man_t * p )
SeeAlso []
***********************************************************************/
+static inline void Cbs2_ManCleanWatch( Cbs2_Man_t * p )
+{
+ int i, iLit;
+ Vec_IntForEachEntry( &p->vWatchUpds, iLit, i )
+ Vec_IntWriteEntry( &p->vWatches, iLit, 0 );
+ Vec_IntClear( &p->vWatchUpds );
+ //Vec_IntForEachEntry( &p->vWatches, iLit, i )
+ // assert( iLit == 0 );
+}
static inline void Cbs2_ManWatchClause( Cbs2_Man_t * p, int hClause, int Lit )
{
int * pLits = Cbs2_ClauseLits( p, hClause );
int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) );
+ if ( *pPlace == 0 )
+ Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) );
/*
if ( pClause->pLits[0] == Lit )
pClause->pNext0 = p->pWatches[lit_neg(Lit)];
@@ -648,23 +673,36 @@ static inline void Cbs2_ManWatchClause( Cbs2_Man_t * p, int hClause, int Lit )
p->pWatches[lit_neg(Lit)] = pClause;
*/
assert( Lit == pLits[0] || Lit == pLits[1] );
- Cbs2_ClauseSetNext( p, hClause, Lit != pLits[0], *pPlace );
+ Cbs2_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace );
*pPlace = hClause;
}
-static inline int Cbs2_QueFinish( Cbs2_Man_t * p )
+static inline int Cbs2_QueFinish( Cbs2_Man_t * p, int Level )
{
Cbs2_Que_t * pQue = &(p->pClauses);
- int hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
+ int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
assert( pQue->iHead+1 < pQue->iTail );
Cbs2_ClauseSetSize( p, pQue->iHead, Size );
- Cbs2_QuePush( pQue, 0 );
- Cbs2_QuePush( pQue, 0 );
- pQue->iHead = pQue->iTail;
- if ( Size > 1 )
+ hClauseC = pQue->iHead = pQue->iTail;
+ //printf( "Adding cube: " ); Cbs2_ManPrintCube(p, Level, hClause);
+ if ( Size == 1 )
+ return hClause;
+ // create watched clause
+ pQue->iHead = hClause;
+ Cbs2_QueForEachEntry( p->pClauses, iObj, i )
{
- Cbs2_ManWatchClause( p, hClause, Cbs2_ClauseLit(p, hClause, 0) );
- Cbs2_ManWatchClause( p, hClause, Cbs2_ClauseLit(p, hClause, 1) );
+ if ( i == hClauseC )
+ break;
+ else if ( i == hClause ) // nlits
+ Cbs2_QuePush( pQue, iObj );
+ else // literals
+ Cbs2_QuePush( pQue, Abc_Var2Lit(iObj, Cbs2_VarValue(p, iObj)) ); // complement
}
+ Cbs2_QuePush( pQue, 0 ); // next0
+ Cbs2_QuePush( pQue, 0 ); // next1
+ pQue->iHead = pQue->iTail;
+ Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 0) );
+ Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 1) );
+ //printf( "Adding clause %d: ", hClauseC ); Cbs2_ManPrintClause(p, Level, hClauseC);
return hClause;
}
@@ -723,9 +761,10 @@ static inline int Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level )
}
else // clause reason
{
- int i, nLits = Cbs2_ClauseSize( p, pReason[1] );
- int * pLits = Cbs2_ClauseLits( p, pReason[1] );
+ int i, * pLits, nLits = Cbs2_ClauseSize( p, pReason[1] );
assert( pReason[1] );
+ Cbs2_QueGrow( pQue, nLits );
+ pLits = Cbs2_ClauseLits( p, pReason[1] );
assert( iObj == Abc_Lit2Var(pLits[0]) );
for ( i = 1; i < nLits; i++ )
Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
@@ -737,31 +776,33 @@ static inline int Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level )
// clear the marks
Vec_IntForEachEntry( p->vTemp, iObj, i )
Cbs2_VarSetMark0(p, iObj, 0);
- return Cbs2_QueFinish( p );
+ return Cbs2_QueFinish( p, Level );
}
static inline int Cbs2_ManAnalyze( Cbs2_Man_t * p, int Level, int iVar, int iFan0, int iFan1 )
{
Cbs2_Que_t * pQue = &(p->pClauses);
assert( Cbs2_VarIsAssigned(p, iVar) );
- assert( Cbs2_VarIsAssigned(p, iFan0) );
- assert( iFan1 == 0 || Cbs2_VarIsAssigned(p, iFan1) );
assert( Cbs2_QueIsEmpty( pQue ) );
Cbs2_QuePush( pQue, 0 );
Cbs2_QuePush( pQue, 0 );
- Cbs2_QuePush( pQue, iVar );
- if ( iFan0 )
+ if ( iFan0 ) // circuit conflict
{
+ assert( Cbs2_VarIsAssigned(p, iFan0) );
+ assert( iFan1 == 0 || Cbs2_VarIsAssigned(p, iFan1) );
+ Cbs2_QuePush( pQue, iVar );
Cbs2_QuePush( pQue, iFan0 );
if ( iFan1 )
Cbs2_QuePush( pQue, iFan1 );
}
- else
+ else // clause conflict
{
- int i, nLits = Cbs2_ClauseSize( p, iFan1 );
- int * pLits = Cbs2_ClauseLits( p, iFan1 );
+ int i, * pLits, nLits = Cbs2_ClauseSize( p, iFan1 );
assert( iFan1 );
+ Cbs2_QueGrow( pQue, nLits );
+ pLits = Cbs2_ClauseLits( p, iFan1 );
assert( iVar == Abc_Lit2Var(pLits[0]) );
- for ( i = 1; i < nLits; i++ )
+ assert( Cbs2_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) );
+ for ( i = 0; i < nLits; i++ )
Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
}
return Cbs2_ManDeriveReason( p, Level );
@@ -788,6 +829,8 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit )
{
int nLits = Cbs2_ClauseSize( p, Cur );
int * pLits = Cbs2_ClauseLits( p, Cur );
+ p->nPropCalls[1]++;
+//printf( " Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level );
// make sure the false literal is in the second literal of the clause
//if ( pCur->pLits[0] == LitF )
if ( pLits[0] == LitF )
@@ -799,7 +842,7 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit )
//pTemp = pCur->pNext0;
//pCur->pNext0 = pCur->pNext1;
//pCur->pNext1 = pTemp;
- ABC_SWAP( int, pLits[nLits+1], pLits[nLits+2] );
+ ABC_SWAP( int, pLits[nLits], pLits[nLits+1] );
}
//assert( pCur->pLits[1] == LitF );
assert( pLits[1] == LitF );
@@ -855,7 +898,10 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit )
// conflict detected - return the conflict clause
//return pCur;
if ( Value == Abc_LitIsCompl(pLits[0]) )
+ {
+ p->nClauseConf++;
return Cbs2_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur );
+ }
}
return 0;
}
@@ -1086,8 +1132,8 @@ int Cbs2_ManPropagate2( Cbs2_Man_t * p, int Level )
int i, iLit, iFan, hClause;
Cbs2_QueForEachEntry( p->pProp, iLit, i )
{
- //if ( (hClause = Cbs2_ManPropagateClauses(p, Level, iLit)) )
- // return hClause;
+ if ( (hClause = Cbs2_ManPropagateClauses(p, Level, iLit)) )
+ return hClause;
Cbs2_ObjForEachFanout( p, Abc_Lit2Var(iLit), iFan )
{
int iFanout = Abc_Lit2Var(iFan);
@@ -1251,7 +1297,7 @@ int Cbs2_ManSolve1_rec( Cbs2_Man_t * p, int Level )
return hLearn1;
hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 );
Cbs2_ManBumpClause( p, hClause );
-// Cbs2_ManPrintClauseNew( p, Level, hClause );
+// Cbs2_ManPrintCube( p, Level, hClause );
// if ( Level > Cbs2_ClauseDecLevel(p, hClause) )
// p->Pars.nBTThisNc++;
p->Pars.nBTThis++;
@@ -1315,7 +1361,7 @@ int Cbs2_ManSolve2_rec( Cbs2_Man_t * p, int Level )
return hLearn1;
hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 );
Cbs2_ManBumpClause( p, hClause );
- //Cbs2_ManPrintClauseNew( p, Level, hClause );
+ //Cbs2_ManPrintCube( p, Level, hClause );
// if ( Level > Cbs2_ClauseDecLevel(p, hClause) )
// p->Pars.nBTThisNc++;
p->Pars.nBTThis++;
@@ -1353,6 +1399,7 @@ int Cbs2_ManSolve( Cbs2_Man_t * p, int iLit )
else
RetValue = 1;
Cbs2_ManCancelUntil( p, 0 );
+ Cbs2_ManCleanWatch( p );
Cbs2_ManBumpClean( p );
p->pJust.iHead = p->pJust.iTail = 0;
p->pClauses.iHead = p->pClauses.iTail = 1;
@@ -1377,6 +1424,7 @@ int Cbs2_ManSolve2( Cbs2_Man_t * p, int iLit, int iLit2 )
else
RetValue = 1;
Cbs2_ManCancelUntil( p, 0 );
+ Cbs2_ManCleanWatch( p );
Cbs2_ManBumpClean( p );
p->pJust.iHead = p->pJust.iTail = 0;
p->pClauses.iHead = p->pClauses.iTail = 1;
@@ -1538,7 +1586,7 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS
// solve for each output
Gia_ManForEachCo( pAig, pRoot, i )
{
-// printf( "\n" );
+ //printf( "\nOutput %d\n", i );
Vec_IntClear( vCex );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
@@ -1606,7 +1654,7 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS
if ( fVerbose )
Cbs2_ManSatPrintStats( p );
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
- printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nFails[0], p->nFails[1] );
+ printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
Abc_PrintTime( 1, "JFront", p->timeJFront );
Cbs2_ManStop( p );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 01:11:38 +0000