summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h4
-rw-r--r--src/aig/gia/giaCSat.c497
-rw-r--r--src/aig/gia/giaCSatOld.c797
-rw-r--r--src/aig/gia/giaRetime.c1
-rw-r--r--src/aig/gia/giaSim.c2
-rw-r--r--src/aig/gia/module.make1
6 files changed, 1148 insertions, 154 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 87c85516..5395f361 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -459,8 +459,10 @@ extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
+/*=== giaCsatOld.c ============================================================*/
+extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/
-extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus );
+extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCof.c =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 5fa9f40f..15faea72 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -32,6 +32,7 @@ struct Cbs_Par_t_
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
+ int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
@@ -48,7 +49,7 @@ struct Cbs_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
- int nSize; // allocated size
+ int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
@@ -59,7 +60,11 @@ struct Cbs_Man_t_
Gia_Man_t * pAig; // AIG manager
Cbs_Que_t pProp; // propagation queue
Cbs_Que_t pJust; // justification queue
+ Cbs_Que_t pClauses; // clause queue
+ Gia_Obj_t ** pIter; // iterator through clause vars
+ Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vModel; // satisfying assignment
+ Vec_Ptr_t * vTemp; // temporary storage
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
@@ -78,16 +83,26 @@ struct Cbs_Man_t_
static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
-static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; }
+static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); }
static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
-#define Cbs_QueForEachEntry( Que, pObj, i ) \
+static inline int Cbs_VarDecLevel( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
+static inline Gia_Obj_t * Cbs_VarReason0( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
+static inline Gia_Obj_t * Cbs_VarReason1( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
+static inline int Cbs_ClauseDecLevel( Cbs_Man_t * p, int hClause ) { return Cbs_VarDecLevel( p, p->pClauses.pData[hClause] ); }
+
+#define Cbs_QueForEachEntry( Que, pObj, i ) \
for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+#define Cbs_ClauseForEachVar( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
+#define Cbs_ClauseForEachVar1( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc()
{
Cbs_Man_t * p;
p = ABC_CALLOC( Cbs_Man_t, 1 );
- p->pProp.nSize = p->pJust.nSize = 10000;
+ p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
- p->vModel = Vec_IntAlloc( 1000 );
+ p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->vModel = Vec_IntAlloc( 1000 );
+ p->vLevReas = Vec_IntAlloc( 1000 );
+ p->vTemp = Vec_PtrAlloc( 1000 );
Cbs_SetDefaultParams( &p->Pars );
return p;
}
@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc()
***********************************************************************/
void Cbs_ManStop( Cbs_Man_t * p )
{
+ Vec_IntFree( p->vLevReas );
Vec_IntFree( p->vModel );
+ Vec_PtrFree( p->vTemp );
+ ABC_FREE( p->pClauses.pData );
ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData );
ABC_FREE( p );
@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld )
p->iTail = iTailOld;
}
+/**Function*************************************************************
+
+ Synopsis [Finalized the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_QueFinish( Cbs_Que_t * p )
+{
+ int iHeadOld = p->iHead;
+ assert( p->iHead < p->iTail );
+ Cbs_QuePush( p, NULL );
+ p->iHead = p->iTail;
+ return iHeadOld;
+}
+
/**Function*************************************************************
@@ -400,7 +442,7 @@ static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p )
pObjMax = pObj;
}
}
- return pObjMax;
+ return pObjMax;
}
@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Cbs_QueForEachEntry( p->pProp, pVar, i )
Cbs_VarUnassign( pVar );
p->pProp.iTail = iBound;
+ Vec_IntShrink( p->vLevReas, 3*iBound );
}
/**Function*************************************************************
@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
SeeAlso []
***********************************************************************/
-static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj )
+static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
{
Gia_Obj_t * pObjR = Gia_Regular(pObj);
assert( Gia_ObjIsCand(pObjR) );
assert( !Cbs_VarIsAssigned(pObjR) );
Cbs_VarAssign( pObjR );
Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ assert( pObjR->Value == ~0 );
+ pObjR->Value = p->pProp.iTail;
Cbs_QuePush( &p->pProp, pObjR );
+ Vec_IntPush( p->vLevReas, Level );
+ Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
+ Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
+ assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns clause size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManClauseSize( Cbs_Man_t * p, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t ** pIter;
+ for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
+ return pIter - pQue->pData - hClause ;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClause( Cbs_Man_t * p, int Level, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs_VarValue(pObj), Cbs_VarDecLevel(p, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClauseNew( Cbs_Man_t * p, int Level, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%c%d ", Cbs_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj, * pReason;
+ int i, k, iLitLevel;
+ assert( pQue->pData[pQue->iHead] == NULL );
+ assert( pQue->iHead + 1 < pQue->iTail );
+/*
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ assert( pObj->fMark0 == 1 );
+ }
+*/
+ // compact literals
+ Vec_PtrClear( p->vTemp );
+ for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Vec_PtrPush( p->vTemp, pObj );
+ // check decision level
+ iLitLevel = Cbs_VarDecLevel( p, pObj );
+ if ( iLitLevel < Level )
+ {
+ pQue->pData[k++] = pObj;
+ continue;
+ }
+ assert( iLitLevel == Level );
+ pReason = Cbs_VarReason0( p, pObj );
+ if ( pReason == pObj ) // no reason
+ {
+ assert( pQue->pData[pQue->iHead] == NULL );
+ pQue->pData[pQue->iHead] = pObj;
+ continue;
+ }
+ Cbs_QuePush( pQue, pReason );
+ pReason = Cbs_VarReason1( p, pObj );
+ if ( pReason != pObj ) // second reason
+ Cbs_QuePush( pQue, pReason );
+ }
+ assert( pQue->pData[pQue->iHead] != NULL );
+ pQue->iTail = k;
+ // clear the marks
+ Vec_PtrForEachEntry( p->vTemp, pObj, i )
+ pObj->fMark0 = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManAnalyze( Cbs_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ assert( Cbs_VarIsAssigned(pVar) );
+ assert( Cbs_VarIsAssigned(pFan0) );
+ assert( pFan1 == NULL || Cbs_VarIsAssigned(pFan1) );
+ assert( Cbs_QueIsEmpty( pQue ) );
+ Cbs_QuePush( pQue, NULL );
+ Cbs_QuePush( pQue, pVar );
+ Cbs_QuePush( pQue, pFan0 );
+ if ( pFan1 )
+ Cbs_QuePush( pQue, pFan1 );
+ Cbs_ManDeriveReason( p, Level );
+ return Cbs_QueFinish( pQue );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs resolution of two clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManResolve( Cbs_Man_t * p, int Level, int hClause0, int hClause1 )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i, LevelMax = -1, LevelCur;
+ assert( pQue->pData[hClause0] != NULL );
+ assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
+/*
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+*/
+ assert( Cbs_QueIsEmpty( pQue ) );
+ Cbs_QuePush( pQue, NULL );
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs_QuePush( pQue, pObj );
+ LevelCur = Cbs_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs_QuePush( pQue, pObj );
+ LevelCur = Cbs_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ pQue->pData[i]->fMark0 = 1;
+ Cbs_ManDeriveReason( p, LevelMax );
+ return Cbs_QueFinish( pQue );
}
/**Function*************************************************************
Synopsis [Propagates a variable.]
- Description [Returns 1 if conflict; 0 if no conflict.]
+ Description [Returns clause handle if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
-static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Cbs_VarValue(pVar) )
{ // value is 1
if ( Value0 == 0 || Value1 == 0 ) // one is 0
- return 1;
+ {
+ if ( Value0 == 0 && Value1 != 0 )
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
+ if ( Value0 != 0 && Value1 == 0 )
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
+ assert( Value0 == 0 && Value1 == 0 );
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ }
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_ObjChild0(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_ObjChild1(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
return 0;
}
// value is 0
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
- return 1;
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
if ( Value0 == 1 || Value1 == 1 ) // one is 1
{
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // second is unassigned
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
assert( Cbs_VarIsJust(pVar) );
@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso []
***********************************************************************/
-static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
@@ -522,12 +788,12 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
- return 1;
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
assert( Value0 == 1 || Value1 == 1 );
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso []
***********************************************************************/
-int Cbs_ManPropagate( Cbs_Man_t * p )
+int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
{
+ int hClause;
Gia_Obj_t * pVar;
int i, k;
while ( 1 )
{
Cbs_QueForEachEntry( p->pProp, pVar, i )
{
- if ( Cbs_ManPropagateOne( p, pVar ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
+ return hClause;
}
p->pProp.iHead = p->pProp.iTail;
k = p->pJust.iHead;
@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
{
if ( Cbs_VarIsJust( pVar ) )
p->pJust.pData[k++] = pVar;
- else if ( Cbs_ManPropagateTwo( p, pVar ) )
- return 1;
+ else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
+ return hClause;
}
if ( k == p->pJust.iTail )
break;
@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
Synopsis [Solve the problem recursively.]
- Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
+ Description [Returns learnt clause if unsat, NULL if sat or undecided.]
SideEffects []
SeeAlso []
-
+
***********************************************************************/
-int Cbs_ManSolve_rec( Cbs_Man_t * p )
-{
- Gia_Obj_t * pVar;
+int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pVar, * pDecVar;
+ int hClause, hLearn0, hLearn1;
int iPropHead, iJustHead, iJustTail;
// propagate assignments
assert( !Cbs_QueIsEmpty(&p->pProp) );
- if ( Cbs_ManPropagate( p ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagate( p, Level )) )
+ return hClause;
// check for satisfying assignment
assert( Cbs_QueIsEmpty(&p->pProp) );
if ( Cbs_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
- p->Pars.nBTThis++;
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs_ManCheckLimits( p ) )
- return 1;
+ return 0;
// remember the state before branching
iPropHead = p->pProp.iHead;
Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
pVar = Cbs_ManDecideMaxFF( p );
else assert( 0 );
assert( Cbs_VarIsJust( pVar ) );
- // decide using fanout count!
- if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
- {
- // decide on first fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- if ( !Cbs_ManSolve_rec( p ) )
- return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- Cbs_ManCancelUntil( p, iPropHead );
- Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
- // decide on second fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
- }
+ // chose decision variable using fanout count
+ if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
else
- {
- // decide on first fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
- if ( !Cbs_ManSolve_rec( p ) )
- return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- Cbs_ManCancelUntil( p, iPropHead );
- Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
- // decide on second fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- }
- if ( !Cbs_ManSolve_rec( p ) )
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+ // decide on first fanin
+ Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+ if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- return 1;
+ if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+ return hLearn0;
+ Cbs_ManCancelUntil( p, iPropHead );
+ Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+ if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+ return hLearn1;
+ hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 );
+// Cbs_ManPrintClauseNew( p, Level, hClause );
+// if ( Level > Cbs_ClauseDecLevel(p, hClause) )
+// p->Pars.nBTThisNc++;
+ p->Pars.nBTThis++;
+ return hClause;
}
/**Function*************************************************************
@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
***********************************************************************/
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{
-// Gia_Obj_t * pTemp;
-// int i;
- int RetValue;
-// Gia_ManForEachObj( p->pAig, pTemp, i )
-// assert( pTemp->fMark0 == 0 );
+ int RetValue = 0;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
- p->Pars.nBTThis = p->Pars.nJustThis = 0;
- Cbs_ManAssign( p, pObj );
- RetValue = Cbs_ManSolve_rec( p );
- if ( RetValue == 0 )
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
Cbs_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
+ p->pClauses.iHead = p->pClauses.iTail = 1;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) )
- return -1;
+ RetValue = -1;
return RetValue;
}
/**Function*************************************************************
- Synopsis [Procedure to test the new SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cbs_ManSolveTest( Gia_Man_t * pGia )
-{
- extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
- int nConfsMax = 1000;
- int CountUnsat, CountSat, CountUndec;
- Cbs_Man_t * p;
- Vec_Int_t * vCex;
- Vec_Int_t * vVisit;
- Gia_Obj_t * pRoot;
- int i, RetValue, clk = clock();
- Gia_ManCreateRefs( pGia );
- // create logic network
- p = Cbs_ManAlloc();
- p->pAig = pGia;
- // prepare AIG
- Gia_ManCleanValue( pGia );
- Gia_ManCleanMark0( pGia );
- Gia_ManCleanMark1( pGia );
-// vCex = Vec_IntAlloc( 100 );
- vVisit = Vec_IntAlloc( 100 );
- // solve for each output
- CountUnsat = CountSat = CountUndec = 0;
- Gia_ManForEachCo( pGia, pRoot, i )
- {
- if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
- continue;
-
-// Gia_ManIncrementTravId( pGia );
-
-//printf( "Output %6d : ", i );
-// iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
-// RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex );
- RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
- if ( RetValue == 1 )
- CountUnsat++;
- else if ( RetValue == -1 )
- CountUndec++;
- else
- {
-// int iLit, k;
- vCex = Cbs_ReadModel( p );
-
-// printf( "complemented = %d. ", Gia_ObjFaninC0(pRoot) );
-//printf( "conflicts = %6d max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis );
-// Vec_IntForEachEntry( vCex, iLit, k )
-// printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) );
-// printf( "\n" );
-
- Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
- assert( RetValue == 0 );
- CountSat++;
- }
-// Gia_ManCheckMark0( p );
-// Gia_ManCheckMark1( p );
- }
- Cbs_ManStop( p );
-// Vec_IntFree( vCex );
- Vec_IntFree( vVisit );
- printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec );
- ABC_PRT( "Time", clock() - clk );
-}
-
-
-/**Function*************************************************************
-
Synopsis [Prints statistics of the manager.]
Description []
@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus )
+Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p;
@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
+ Gia_ManFillValue( pAig ); // maps nodes into trail ids
// create logic network
p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs;
@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
}
else
{
- printf( "Constant 0 output of SRM!!!\n" );
+// printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
@@ -838,12 +1025,15 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+// printf( "\n" );
+/*
if ( status == -1 )
{
p->Pars.fUseHighest = 0;
p->Pars.fUseLowest = 1;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
}
+*/
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
continue;
}
p->nSatSat++;
- p->nConfUnsat += p->Pars.nBTThis;
+ p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
-// Cbs_ManSatPrintStats( p );
+ if ( fVerbose )
+ Cbs_ManSatPrintStats( p );
+// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
Cbs_ManStop( p );
*pvStatus = vStatus;
+
// printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
new file mode 100644
index 00000000..409af56c
--- /dev/null
+++ b/src/aig/gia/giaCSatOld.c
@@ -0,0 +1,797 @@
+/**CFile****************************************************************
+
+ FileName [giaCSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [A simple circuit-based solver.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cbs0_Par_t_ Cbs0_Par_t;
+struct Cbs0_Par_t_
+{
+ // conflict limits
+ int nBTLimit; // limit on the number of conflicts
+ int nJustLimit; // limit on the size of justification queue
+ // current parameters
+ int nBTThis; // number of conflicts
+ int nJustThis; // max size of the frontier
+ int nBTTotal; // total number of conflicts
+ int nJustTotal; // total size of the frontier
+ // decision heuristics
+ int fUseHighest; // use node with the highest ID
+ int fUseLowest; // use node with the highest ID
+ int fUseMaxFF; // use node with the largest fanin fanout
+ // other
+ int fVerbose;
+};
+
+typedef struct Cbs0_Que_t_ Cbs0_Que_t;
+struct Cbs0_Que_t_
+{
+ int iHead; // beginning of the queue
+ int iTail; // end of the queue
+ int nSize; // allocated size
+ Gia_Obj_t ** pData; // nodes stored in the queue
+};
+
+typedef struct Cbs0_Man_t_ Cbs0_Man_t;
+struct Cbs0_Man_t_
+{
+ Cbs0_Par_t Pars; // parameters
+ Gia_Man_t * pAig; // AIG manager
+ Cbs0_Que_t pProp; // propagation queue
+ Cbs0_Que_t pJust; // justification queue
+ Vec_Int_t * vModel; // satisfying assignment
+ // SAT calls statistics
+ int nSatUnsat; // the number of proofs
+ int nSatSat; // the number of failure
+ int nSatUndec; // the number of timeouts
+ int nSatTotal; // the number of calls
+ // conflicts
+ int nConfUnsat; // conflicts in unsat problems
+ int nConfSat; // conflicts in sat problems
+ int nConfUndec; // conflicts in undec problems
+ // runtime stats
+ int timeSatUnsat; // unsat
+ int timeSatSat; // sat
+ int timeSatUndec; // undecided
+ int timeTotal; // total runtime
+};
+
+static inline int Cbs0_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
+static inline void Cbs0_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
+static inline void Cbs0_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; }
+static inline int Cbs0_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
+static inline void Cbs0_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
+static inline int Cbs0_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)); }
+static inline int Cbs0_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
+static inline int Cbs0_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
+
+#define Cbs0_QueForEachEntry( Que, pObj, i ) \
+ for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets default values of the parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs0_SetDefaultParams( Cbs0_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Cbs0_Par_t) );
+ pPars->nBTLimit = 1000; // limit on the number of conflicts
+ pPars->nJustLimit = 100; // limit on the size of justification queue
+ pPars->fUseHighest = 1; // use node with the highest ID
+ pPars->fUseLowest = 0; // use node with the highest ID
+ pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
+ pPars->fVerbose = 1; // print detailed statistics
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cbs0_Man_t * Cbs0_ManAlloc()
+{
+ Cbs0_Man_t * p;
+ p = ABC_CALLOC( Cbs0_Man_t, 1 );
+ p->pProp.nSize = p->pJust.nSize = 10000;
+ p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
+ p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
+ p->vModel = Vec_IntAlloc( 1000 );
+ Cbs0_SetDefaultParams( &p->Pars );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs0_ManStop( Cbs0_Man_t * p )
+{
+ Vec_IntFree( p->vModel );
+ ABC_FREE( p->pProp.pData );
+ ABC_FREE( p->pJust.pData );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns satisfying assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cbs0_ReadModel( Cbs0_Man_t * p )
+{
+ return p->vModel;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the solver is out of limits.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_ManCheckLimits( Cbs0_Man_t * p )
+{
+ return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saves the satisfying assignment as an array of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ Vec_IntClear( vCex );
+ p->pProp.iHead = 0;
+ Cbs0_QueForEachEntry( p->pProp, pVar, i )
+ if ( Gia_ObjIsCi(pVar) )
+// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
+ Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_QueIsEmpty( Cbs0_Que_t * p )
+{
+ return p->iHead == p->iTail;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_QuePush( Cbs0_Que_t * p, Gia_Obj_t * pObj )
+{
+ if ( p->iTail == p->nSize )
+ {
+ p->nSize *= 2;
+ p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
+ }
+ p->pData[p->iTail++] = pObj;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the object in the queue.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_QueHasNode( Cbs0_Que_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pTemp;
+ int i;
+ Cbs0_QueForEachEntry( *p, pTemp, i )
+ if ( pTemp == pObj )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_QueStore( Cbs0_Que_t * p, int * piHeadOld, int * piTailOld )
+{
+ int i;
+ *piHeadOld = p->iHead;
+ *piTailOld = p->iTail;
+ for ( i = *piHeadOld; i < *piTailOld; i++ )
+ Cbs0_QuePush( p, p->pData[i] );
+ p->iHead = *piTailOld;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_QueRestore( Cbs0_Que_t * p, int iHeadOld, int iTailOld )
+{
+ p->iHead = iHeadOld;
+ p->iTail = iTailOld;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Max number of fanins fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Count0, Count1;
+ assert( !Gia_IsComplement(pObj) );
+ assert( Gia_ObjIsAnd(pObj) );
+ Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
+ Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
+ return ABC_MAX( Count0, Count1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the highest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideHighest( Cbs0_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i;
+ Cbs0_QueForEachEntry( p->pJust, pObj, i )
+ if ( pObjMax == NULL || pObjMax < pObj )
+ pObjMax = pObj;
+ return pObjMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the lowest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideLowest( Cbs0_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMin = NULL;
+ int i;
+ Cbs0_QueForEachEntry( p->pJust, pObj, i )
+ if ( pObjMin == NULL || pObjMin > pObj )
+ pObjMin = pObj;
+ return pObjMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the maximum number of fanin fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideMaxFF( Cbs0_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i, iMaxFF = 0, iCurFF;
+ assert( p->pAig->pRefs != NULL );
+ Cbs0_QueForEachEntry( p->pJust, pObj, i )
+ {
+ iCurFF = Cbs0_VarFaninFanoutMax( p, pObj );
+ assert( iCurFF > 0 );
+ if ( iMaxFF < iCurFF )
+ {
+ iMaxFF = iCurFF;
+ pObjMax = pObj;
+ }
+ }
+ return pObjMax;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_ManCancelUntil( Cbs0_Man_t * p, int iBound )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ assert( iBound <= p->pProp.iTail );
+ p->pProp.iHead = iBound;
+ Cbs0_QueForEachEntry( p->pProp, pVar, i )
+ Cbs0_VarUnassign( pVar );
+ p->pProp.iTail = iBound;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns the variables a value.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs0_ManAssign( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pObjR = Gia_Regular(pObj);
+ assert( Gia_ObjIsCand(pObjR) );
+ assert( !Cbs0_VarIsAssigned(pObjR) );
+ Cbs0_VarAssign( pObjR );
+ Cbs0_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ Cbs0_QuePush( &p->pProp, pObjR );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates a variable.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_ManPropagateOne( Cbs0_Man_t * p, Gia_Obj_t * pVar )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( Cbs0_VarIsAssigned(pVar) );
+ if ( Gia_ObjIsCi(pVar) )
+ return 0;
+ assert( Gia_ObjIsAnd(pVar) );
+ Value0 = Cbs0_VarFanin0Value(pVar);
+ Value1 = Cbs0_VarFanin1Value(pVar);
+ if ( Cbs0_VarValue(pVar) )
+ { // value is 1
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 1;
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_ObjChild0(pVar) );
+ if ( Value1 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_ObjChild1(pVar) );
+ return 0;
+ }
+ // value is 0
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 0;
+ if ( Value0 == 1 && Value1 == 1 ) // both are 1
+ return 1;
+ if ( Value0 == 1 || Value1 == 1 ) // one is 1
+ {
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+ if ( Value1 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ return 0;
+ }
+ assert( Cbs0_VarIsJust(pVar) );
+ assert( !Cbs0_QueHasNode( &p->pJust, pVar ) );
+ Cbs0_QuePush( &p->pJust, pVar );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates a variable.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs0_ManPropagateTwo( Cbs0_Man_t * p, Gia_Obj_t * pVar )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( Gia_ObjIsAnd(pVar) );
+ assert( Cbs0_VarIsAssigned(pVar) );
+ assert( !Cbs0_VarValue(pVar) );
+ Value0 = Cbs0_VarFanin0Value(pVar);
+ Value1 = Cbs0_VarFanin1Value(pVar);
+ // value is 0
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 0;
+ if ( Value0 == 1 && Value1 == 1 ) // both are 1
+ return 1;
+ assert( Value0 == 1 || Value1 == 1 );
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+ if ( Value1 == 2 ) // first is unassigned
+ Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates all variables.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs0_ManPropagate( Cbs0_Man_t * p )
+{
+ Gia_Obj_t * pVar;
+ int i, k;
+ while ( 1 )
+ {
+ Cbs0_QueForEachEntry( p->pProp, pVar, i )
+ {
+ if ( Cbs0_ManPropagateOne( p, pVar ) )
+ return 1;
+ }
+ p->pProp.iHead = p->pProp.iTail;
+ k = p->pJust.iHead;
+ Cbs0_QueForEachEntry( p->pJust, pVar, i )
+ {
+ if ( Cbs0_VarIsJust( pVar ) )
+ p->pJust.pData[k++] = pVar;
+ else if ( Cbs0_ManPropagateTwo( p, pVar ) )
+ return 1;
+ }
+ if ( k == p->pJust.iTail )
+ break;
+ p->pJust.iTail = k;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solve the problem recursively.]
+
+ Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
+{
+ Gia_Obj_t * pVar, * pDecVar;
+ int iPropHead, iJustHead, iJustTail;
+ // propagate assignments
+ assert( !Cbs0_QueIsEmpty(&p->pProp) );
+ if ( Cbs0_ManPropagate( p ) )
+ return 1;
+ // check for satisfying assignment
+ assert( Cbs0_QueIsEmpty(&p->pProp) );
+ if ( Cbs0_QueIsEmpty(&p->pJust) )
+ return 0;
+ // quit using resource limits
+ p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+ if ( Cbs0_ManCheckLimits( p ) )
+ return 0;
+ // remember the state before branching
+ iPropHead = p->pProp.iHead;
+ Cbs0_QueStore( &p->pJust, &iJustHead, &iJustTail );
+ // find the decision variable
+ if ( p->Pars.fUseHighest )
+ pVar = Cbs0_ManDecideHighest( p );
+ else if ( p->Pars.fUseLowest )
+ pVar = Cbs0_ManDecideLowest( p );
+ else if ( p->Pars.fUseMaxFF )
+ pVar = Cbs0_ManDecideMaxFF( p );
+ else assert( 0 );
+ assert( Cbs0_VarIsJust( pVar ) );
+ // chose decision variable using fanout count
+ if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
+ else
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+ // decide on first fanin
+ Cbs0_ManAssign( p, pDecVar );
+ if ( !Cbs0_ManSolve_rec( p ) )
+ return 0;
+ Cbs0_ManCancelUntil( p, iPropHead );
+ Cbs0_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ Cbs0_ManAssign( p, Gia_Not(pDecVar) );
+ if ( !Cbs0_ManSolve_rec( p ) )
+ return 0;
+ p->Pars.nBTThis++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Looking for a satisfying assignment of the node.]
+
+ Description [Assumes that each node has flag pObj->fMark0 set to 0.
+ Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
+ The node may be complemented. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+ int RetValue;
+ assert( !p->pProp.iHead && !p->pProp.iTail );
+ assert( !p->pJust.iHead && !p->pJust.iTail );
+ p->Pars.nBTThis = p->Pars.nJustThis = 0;
+ Cbs0_ManAssign( p, pObj );
+ RetValue = Cbs0_ManSolve_rec( p );
+ if ( RetValue == 0 && !Cbs0_ManCheckLimits(p) )
+ Cbs0_ManSaveModel( p, p->vModel );
+ Cbs0_ManCancelUntil( p, 0 );
+ p->pJust.iHead = p->pJust.iTail = 0;
+ p->Pars.nBTTotal += p->Pars.nBTThis;
+ p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+ if ( Cbs0_ManCheckLimits( p ) )
+ RetValue = -1;
+// printf( "Outcome = %2d. Confs = %6d. Decision level max = %3d.\n",
+// RetValue, p->Pars.nBTThis, p->DecLevelMax );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints statistics of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
+{
+ printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
+ printf( "Conf = %5d ", p->Pars.nBTLimit );
+ printf( "JustMax = %5d ", p->Pars.nJustLimit );
+ printf( "\n" );
+ printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+ ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
+ printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+ ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
+ printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+ ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+ ABC_PRT( "Total time", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Procedure to test the new SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
+{
+ extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+ Cbs0_Man_t * p;
+ Vec_Int_t * vCex, * vVisit, * vCexStore;
+ Vec_Str_t * vStatus;
+ Gia_Obj_t * pRoot;
+ int i, status, clk, clkTotal = clock();
+ assert( Gia_ManRegNum(pAig) == 0 );
+ // prepare AIG
+ Gia_ManCreateRefs( pAig );
+ Gia_ManCleanMark0( pAig );
+ Gia_ManCleanMark1( pAig );
+ // create logic network
+ p = Cbs0_ManAlloc();
+ p->Pars.nBTLimit = nConfs;
+ p->pAig = pAig;
+ // create resulting data-structures
+ vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+ vCexStore = Vec_IntAlloc( 10000 );
+ vVisit = Vec_IntAlloc( 100 );
+ vCex = Cbs0_ReadModel( p );
+ // solve for each output
+ Gia_ManForEachCo( pAig, pRoot, i )
+ {
+ Vec_IntClear( vCex );
+ if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+ {
+ if ( Gia_ObjFaninC0(pRoot) )
+ {
+ printf( "Constant 1 output of SRM!!!\n" );
+ Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
+ Vec_StrPush( vStatus, 0 );
+ }
+ else
+ {
+// printf( "Constant 0 output of SRM!!!\n" );
+ Vec_StrPush( vStatus, 1 );
+ }
+ continue;
+ }
+ clk = clock();
+ p->Pars.fUseHighest = 1;
+ p->Pars.fUseLowest = 0;
+ status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
+/*
+ if ( status == -1 )
+ {
+ p->Pars.fUseHighest = 0;
+ p->Pars.fUseLowest = 1;
+ status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
+ }
+*/
+ Vec_StrPush( vStatus, (char)status );
+ if ( status == -1 )
+ {
+ p->nSatUndec++;
+ p->nConfUndec += p->Pars.nBTThis;
+ Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+ p->timeSatUndec += clock() - clk;
+ continue;
+ }
+ if ( status == 1 )
+ {
+ p->nSatUnsat++;
+ p->nConfUnsat += p->Pars.nBTThis;
+ p->timeSatUnsat += clock() - clk;
+ continue;
+ }
+ p->nSatSat++;
+ p->nConfSat += p->Pars.nBTThis;
+// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+ Cec_ManSatAddToStore( vCexStore, vCex, i );
+ p->timeSatSat += clock() - clk;
+ }
+ Vec_IntFree( vVisit );
+ p->nSatTotal = Gia_ManPoNum(pAig);
+ p->timeTotal = clock() - clkTotal;
+ if ( fVerbose )
+ Cbs0_ManSatPrintStats( p );
+ Cbs0_ManStop( p );
+ *pvStatus = vStatus;
+// printf( "Total number of cex literals = %d. (Ave = %d)\n",
+// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
+// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
+ return vCexStore;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 4f2c6e08..965b5981 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -243,6 +243,7 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe
// finally derive the new manager
pNew = Gia_ManRetimeDupForward( p, vCut );
Vec_PtrFree( vCut );
+ if ( vObjClasses )
Vec_IntFree( vObjClasses );
pNew->vFlopClasses = vFlopClasses;
return pNew;
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 7ee0ddc4..020683ad 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -405,7 +405,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
if ( pPars->fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
- printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
+ printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 055d7580..916414fc 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaCof.c \
+ src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
src/aig/gia/giaDfs.c \
src/aig/gia/giaDup.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-05 22:27:01 +0000