summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAig.c26
-rw-r--r--src/aig/gia/giaCSatP.c1209
-rw-r--r--src/aig/gia/giaCSatP.h117
-rw-r--r--src/aig/gia/giaCex.c2
-rw-r--r--src/aig/gia/giaDup.c321
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/aig/gia/giaMini.c48
-rw-r--r--src/aig/gia/giaMuxes.c67
-rw-r--r--src/aig/gia/giaPat2.c97
-rw-r--r--src/aig/gia/giaResub6.c451
-rw-r--r--src/aig/gia/giaSif.c257
-rw-r--r--src/aig/gia/giaSimBase.c81
-rw-r--r--src/aig/gia/giaSupps.c142
-rw-r--r--src/aig/gia/giaSwitch.c8
-rw-r--r--src/aig/gia/giaUtil.c50
-rw-r--r--src/aig/gia/module.make3
17 files changed, 2843 insertions, 41 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5548def6..488f12cf 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1312,6 +1312,8 @@ extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupNoBuf( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap );
extern Gia_Man_t * Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis );
@@ -1351,6 +1353,7 @@ extern Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int n
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
+extern Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 91a9c600..c764a099 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -611,6 +611,27 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
SeeAlso []
***********************************************************************/
+int Gia_ManTestChoices( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj; int i;
+ Vec_Int_t * vPointed = Vec_IntStart( Gia_ManObjNum(p) );
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( Gia_ObjSibl(p, i) )
+ Vec_IntWriteEntry( vPointed, Gia_ObjSibl(p, i), 1 );
+ Gia_ManCreateRefs( p );
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( Vec_IntEntry(vPointed, i) && Gia_ObjRefNumId(p, i) > 0 )
+ {
+ printf( "Gia_ManCheckChoices: Member %d", i );
+ printf( " of a choice node has %d fanouts.\n", Gia_ObjRefNumId(p, i) );
+ ABC_FREE( p->pRefs );
+ Vec_IntFree( vPointed );
+ return 0;
+ }
+ ABC_FREE( p->pRefs );
+ Vec_IntFree( vPointed );
+ return 1;
+}
Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
{
int fUseMapping = 0;
@@ -628,6 +649,11 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
// pGia = Gia_ManFromAig( pNew );
pGia = Gia_ManFromAigChoices( pNew );
Aig_ManStop( pNew );
+ if ( !p->pManTime && !Gia_ManTestChoices(pGia) )
+ {
+ Gia_ManStop( pGia );
+ pGia = Gia_ManDup( p );
+ }
Gia_ManTransferTiming( pGia, p );
return pGia;
}
diff --git a/src/aig/gia/giaCSatP.c b/src/aig/gia/giaCSatP.c
new file mode 100644
index 00000000..00ab880b
--- /dev/null
+++ b/src/aig/gia/giaCSatP.c
@@ -0,0 +1,1209 @@
+/**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"
+#include "giaCSatP.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+//#define gia_assert(exp) ((void)0)
+//#define gia_assert(exp) (assert(exp))
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+static inline int CbsP_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
+static inline void CbsP_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
+static inline void CbsP_VarUnassign( CbsP_Man_t * pMan, Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pMan->vValue->pArray[Gia_ObjId(pMan->pAig,pVar)] = ~0; }
+static inline int CbsP_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
+static inline void CbsP_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
+static inline int CbsP_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !CbsP_VarIsAssigned(Gia_ObjFanin0(pVar)) && !CbsP_VarIsAssigned(Gia_ObjFanin1(pVar)); }
+static inline int CbsP_VarFanin0Value( Gia_Obj_t * pVar ) { return !CbsP_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (CbsP_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
+static inline int CbsP_VarFanin1Value( Gia_Obj_t * pVar ) { return !CbsP_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (CbsP_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
+
+static inline int CbsP_VarDecLevel( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*Value); }
+static inline Gia_Obj_t * CbsP_VarReason0( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*Value+1); }
+static inline Gia_Obj_t * CbsP_VarReason1( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*Value+2); }
+static inline int CbsP_ClauseDecLevel( CbsP_Man_t * p, int hClause ) { return CbsP_VarDecLevel( p, p->pClauses.pData[hClause] ); }
+
+#define CbsP_QueForEachEntry( Que, pObj, i ) \
+ for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+
+#define CbsP_ClauseForEachVar( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
+#define CbsP_ClauseForEachVar1( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets default values of the parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CbsP_SetDefaultParams( CbsP_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(CbsP_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
+
+ pPars->fUseProved = 1;
+
+
+ pPars->nJscanThis = 0;
+ pPars->nRscanThis = 0;
+ pPars->maxJscanUndec = 0;
+ pPars->maxRscanUndec = 0;
+ pPars->maxJscanSolved = 0;
+ pPars->maxRscanSolved = 0;
+
+
+ pPars->accJscanSat = 0;
+ pPars->accJscanUnsat = 0;
+ pPars->accJscanUndec = 0;
+ pPars->accRscanSat = 0;
+ pPars->accRscanUnsat = 0;
+ pPars->accRscanUndec = 0;
+ pPars->nSat = 0;
+ pPars->nUnsat = 0;
+ pPars->nUndec = 0;
+
+ pPars->nJscanLimit = 100;
+ pPars->nRscanLimit = 100;
+ pPars->nPropLimit = 500;
+}
+void CbsP_ManSetConflictNum( CbsP_Man_t * p, int Num )
+{
+ p->Pars.nBTLimit = Num;
+}
+
+static inline void CbsP_UpdateRecord( CbsP_Par_t * pPars, int res ){
+ if( CBS_UNDEC == res ){
+ pPars->nUndec ++ ;
+ if( pPars-> maxJscanUndec < pPars->nJscanThis )
+ pPars-> maxJscanUndec = pPars->nJscanThis;
+ if( pPars-> maxRscanUndec < pPars->nRscanThis )
+ pPars-> maxRscanUndec = pPars->nRscanThis;
+ if( pPars-> maxPropUndec < pPars->nPropThis )
+ pPars-> maxPropUndec = pPars->nPropThis;
+
+ pPars->accJscanUndec += pPars->nJscanThis;
+ pPars->accRscanUndec += pPars->nRscanThis;
+ pPars-> accPropUndec += pPars->nPropThis;
+ } else {
+ if( pPars->maxJscanSolved < pPars->nJscanThis )
+ pPars->maxJscanSolved = pPars->nJscanThis;
+ if( pPars->maxRscanSolved < pPars->nRscanThis )
+ pPars->maxRscanSolved = pPars->nRscanThis;
+ if( pPars-> maxPropSolved < pPars->nPropThis )
+ pPars-> maxPropSolved = pPars->nPropThis;
+ if( CBS_SAT == res ){
+ pPars->nSat ++ ;
+ pPars->accJscanSat += pPars->nJscanThis;
+ pPars->accRscanSat += pPars->nRscanThis;
+ pPars-> accPropSat += pPars->nPropThis;
+ } else
+ if( CBS_UNSAT == res ){
+ pPars->nUnsat ++ ;
+ pPars->accJscanUnsat += pPars->nJscanThis;
+ pPars->accRscanUnsat += pPars->nRscanThis;
+ pPars-> accPropUnsat += pPars->nPropThis;
+ }
+ }
+
+}
+
+void CbsP_PrintRecord( CbsP_Par_t * pPars ){
+ printf("max of solved: jscan# %13d rscan %13d prop %13d\n" , pPars->maxJscanSolved, pPars->maxRscanSolved , pPars->maxPropSolved );
+ printf("max of undec: jscan# %13d rscan %13d prop %13d\n" , pPars->maxJscanUndec , pPars->maxRscanUndec , pPars->maxPropUndec );
+ printf("acc of sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat , pPars->accRscanSat , pPars->accPropSat );
+ printf("acc of unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat , pPars->accRscanUnsat , pPars->accPropUnsat );
+ printf("acc of undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec , pPars->accRscanUndec , pPars->accPropUndec );
+ if( pPars->nSat )
+ printf("avg of sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat / pPars->nSat , pPars->accRscanSat / pPars->nSat , pPars->accPropSat / pPars->nSat );
+ if( pPars->nUnsat )
+ printf("avg of unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat / pPars->nUnsat , pPars->accRscanUnsat / pPars->nUnsat , pPars->accPropUnsat / pPars->nUnsat );
+ if( pPars->nUndec )
+ printf("avg of undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec / pPars->nUndec , pPars->accRscanUndec / pPars->nUndec , pPars->accPropUndec / pPars->nUndec );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia )
+{
+ CbsP_Man_t * p;
+ p = ABC_CALLOC( CbsP_Man_t, 1 );
+ 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->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 );
+ p->pAig = pGia;
+ p->vValue = Vec_IntAlloc( Gia_ManObjNum(pGia) );
+ Vec_IntFill( p->vValue, Gia_ManObjNum(pGia), ~0 );
+ //memset( p->vValue->pArray, (unsigned) ~0, sizeof(int) * Gia_ManObjNum(pGia) );
+ CbsP_SetDefaultParams( &p->Pars );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CbsP_ManStop( CbsP_Man_t * p )
+{
+ Vec_IntFree( p->vLevReas );
+ Vec_IntFree( p->vModel );
+ Vec_PtrFree( p->vTemp );
+ Vec_IntFree( p->vValue );
+ ABC_FREE( p->pClauses.pData );
+ ABC_FREE( p->pProp.pData );
+ ABC_FREE( p->pJust.pData );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns satisfying assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * CbsP_ReadModel( CbsP_Man_t * p )
+{
+ return p->vModel;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the solver is out of limits.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+static inline int CbsP_ManCheckPropLimits( CbsP_Man_t * p )
+{
+ return p->Pars.nPropThis > p->Pars.nPropLimit;
+}
+static inline int CbsP_ManCheckLimits( CbsP_Man_t * p )
+{
+ return CbsP_ManCheckPropLimits(p) || p->Pars.nJscanThis > p->Pars.nJscanLimit || p->Pars.nRscanThis > p->Pars.nRscanLimit || 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 CbsP_ManSaveModel( CbsP_Man_t * p, Vec_Int_t * vCex )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ Vec_IntClear( vCex );
+ p->pProp.iHead = 0;
+ CbsP_QueForEachEntry( p->pProp, pVar, i )
+ if ( Gia_ObjIsCi(pVar) )
+ Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !CbsP_VarValue(pVar)) );
+// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !CbsP_VarValue(pVar)) );
+}
+static inline void CbsP_ManSaveModelAll( CbsP_Man_t * p, Vec_Int_t * vCex )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ Vec_IntClear( vCex );
+ p->pProp.iHead = 0;
+ CbsP_QueForEachEntry( p->pProp, pVar, i )
+ Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !CbsP_VarValue(pVar)) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_QueIsEmpty( CbsP_Que_t * p )
+{
+ return p->iHead == p->iTail;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_QuePush( CbsP_Que_t * p, Gia_Obj_t * pObj )
+{
+ assert( !Gia_IsComplement(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 CbsP_QueHasNode( CbsP_Que_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pTemp;
+ int i;
+ CbsP_QueForEachEntry( *p, pTemp, i )
+ if ( pTemp == pObj )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_QueStore( CbsP_Que_t * p, int * piHeadOld, int * piTailOld )
+{
+ int i;
+ *piHeadOld = p->iHead;
+ *piTailOld = p->iTail;
+ for ( i = *piHeadOld; i < *piTailOld; i++ )
+ CbsP_QuePush( p, p->pData[i] );
+ p->iHead = *piTailOld;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_QueRestore( CbsP_Que_t * p, int iHeadOld, int iTailOld )
+{
+ p->iHead = iHeadOld;
+ p->iTail = iTailOld;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finalized the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_QueFinish( CbsP_Que_t * p )
+{
+ int iHeadOld = p->iHead;
+ assert( p->iHead < p->iTail );
+ CbsP_QuePush( p, NULL );
+ p->iHead = p->iTail;
+ return iHeadOld;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Max number of fanins fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_VarFaninFanoutMax( CbsP_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Count0, Count1;
+ assert( !Gia_IsComplement(pObj) );
+ assert( Gia_ObjIsAnd(pObj) );
+ Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
+ Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
+ return Abc_MaxInt( Count0, Count1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the highest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * CbsP_ManDecideHighest( CbsP_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i;
+ CbsP_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 * CbsP_ManDecideLowest( CbsP_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMin = NULL;
+ int i;
+ CbsP_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 * CbsP_ManDecideMaxFF( CbsP_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i, iMaxFF = 0, iCurFF;
+ assert( p->pAig->pRefs != NULL );
+ CbsP_QueForEachEntry( p->pJust, pObj, i )
+ {
+ iCurFF = CbsP_VarFaninFanoutMax( p, pObj );
+ assert( iCurFF > 0 );
+ if ( iMaxFF < iCurFF )
+ {
+ iMaxFF = iCurFF;
+ pObjMax = pObj;
+ }
+ }
+ return pObjMax;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_ManCancelUntil( CbsP_Man_t * p, int iBound )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ assert( iBound <= p->pProp.iTail );
+ p->pProp.iHead = iBound;
+ CbsP_QueForEachEntry( p->pProp, pVar, i )
+ CbsP_VarUnassign( p, pVar );
+ p->pProp.iTail = iBound;
+ Vec_IntShrink( p->vLevReas, 3*iBound );
+}
+
+//int s_Counter = 0;
+
+/**Function*************************************************************
+
+ Synopsis [Assigns the variables a value.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_ManAssign( CbsP_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( !CbsP_VarIsAssigned(pObjR) );
+ CbsP_VarAssign( pObjR );
+ CbsP_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ assert( p->vValue->pArray[Gia_ObjId(p->pAig,pObjR)] == ~0 );
+ p->vValue->pArray[Gia_ObjId(p->pAig,pObjR)] = p->pProp.iTail;
+ CbsP_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 );
+ if( pRes0 )
+ p->Pars.nPropThis ++ ;
+// s_Counter++;
+// s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns clause size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_ManClauseSize( CbsP_Man_t * p, int hClause )
+{
+ CbsP_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 CbsP_ManPrintClause( CbsP_Man_t * p, int Level, int hClause )
+{
+ CbsP_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( CbsP_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), CbsP_VarValue(pObj), CbsP_VarDecLevel(p, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_ManPrintClauseNew( CbsP_Man_t * p, int Level, int hClause )
+{
+ CbsP_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( CbsP_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%c%d ", CbsP_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void CbsP_ManDeriveReason( CbsP_Man_t * p, int Level )
+{
+ CbsP_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 = CbsP_VarDecLevel( p, pObj );
+ if ( iLitLevel < Level )
+ {
+ pQue->pData[k++] = pObj;
+ continue;
+ }
+ assert( iLitLevel == Level );
+ pReason = CbsP_VarReason0( p, pObj );
+ if ( pReason == pObj ) // no reason
+ {
+ //assert( pQue->pData[pQue->iHead] == NULL );
+ pQue->pData[pQue->iHead] = pObj;
+ continue;
+ }
+ CbsP_QuePush( pQue, pReason );
+ pReason = CbsP_VarReason1( p, pObj );
+ if ( pReason != pObj ) // second reason
+ CbsP_QuePush( pQue, pReason );
+ }
+ assert( pQue->pData[pQue->iHead] != NULL );
+ pQue->iTail = k;
+ // clear the marks
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vTemp, pObj, i )
+ pObj->fMark0 = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_ManAnalyze( CbsP_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
+{
+ CbsP_Que_t * pQue = &(p->pClauses);
+ assert( CbsP_VarIsAssigned(pVar) );
+ assert( CbsP_VarIsAssigned(pFan0) );
+ assert( pFan1 == NULL || CbsP_VarIsAssigned(pFan1) );
+ assert( CbsP_QueIsEmpty( pQue ) );
+ CbsP_QuePush( pQue, NULL );
+ CbsP_QuePush( pQue, pVar );
+ CbsP_QuePush( pQue, pFan0 );
+ if ( pFan1 )
+ CbsP_QuePush( pQue, pFan1 );
+ CbsP_ManDeriveReason( p, Level );
+ return CbsP_QueFinish( pQue );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs resolution of two clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_ManResolve( CbsP_Man_t * p, int Level, int hClause0, int hClause1 )
+{
+ CbsP_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( CbsP_QueIsEmpty( pQue ) );
+ CbsP_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;
+ CbsP_QuePush( pQue, pObj );
+ p->Pars.nRscanThis ++ ;
+ LevelCur = CbsP_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;
+ CbsP_QuePush( pQue, pObj );
+ p->Pars.nRscanThis ++ ;
+ LevelCur = CbsP_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ pQue->pData[i]->fMark0 = 1;
+ CbsP_ManDeriveReason( p, LevelMax );
+ return CbsP_QueFinish( pQue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates a variable.]
+
+ Description [Returns clause handle if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int CbsP_ManPropagateOne( CbsP_Man_t * p, Gia_Obj_t * pVar, int Level )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( CbsP_VarIsAssigned(pVar) );
+ if ( Gia_ObjIsCi(pVar) )
+ return 0;
+ assert( Gia_ObjIsAnd(pVar) );
+ Value0 = CbsP_VarFanin0Value(pVar);
+ Value1 = CbsP_VarFanin1Value(pVar);
+ if ( CbsP_VarValue(pVar) )
+ { // value is 1
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ {
+ if ( Value0 == 0 && Value1 != 0 )
+ return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
+ if ( Value0 != 0 && Value1 == 0 )
+ return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
+ assert( Value0 == 0 && Value1 == 0 );
+ return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ }
+ if ( Value0 == 2 ) // first is unassigned
+ CbsP_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
+ if ( Value1 == 2 ) // first is unassigned
+ CbsP_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 CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ if ( Value0 == 1 || Value1 == 1 ) // one is 1
+ {
+ if ( Value0 == 2 ) // first is unassigned
+ CbsP_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // second is unassigned
+ CbsP_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
+ return 0;
+ }
+ assert( CbsP_VarIsJust(pVar) );
+ assert( !CbsP_QueHasNode( &p->pJust, pVar ) );
+ CbsP_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 CbsP_ManPropagateTwo( CbsP_Man_t * p, Gia_Obj_t * pVar, int Level )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( Gia_ObjIsAnd(pVar) );
+ assert( CbsP_VarIsAssigned(pVar) );
+ assert( !CbsP_VarValue(pVar) );
+ Value0 = CbsP_VarFanin0Value(pVar);
+ Value1 = CbsP_VarFanin1Value(pVar);
+ // value is 0
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 0;
+ if ( Value0 == 1 && Value1 == 1 ) // both are 1
+ return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ assert( Value0 == 1 || Value1 == 1 );
+ if ( Value0 == 2 ) // first is unassigned
+ CbsP_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // first is unassigned
+ CbsP_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates all variables.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int CbsP_ManPropagate( CbsP_Man_t * p, int Level )
+{
+ int hClause;
+ Gia_Obj_t * pVar;
+ int i, k;
+ while ( 1 )
+ {
+ CbsP_QueForEachEntry( p->pProp, pVar, i )
+ {
+ if ( (hClause = CbsP_ManPropagateOne( p, pVar, Level )) )
+ return hClause;
+ if( CbsP_ManCheckPropLimits(p) )
+ return 0;
+ }
+ p->pProp.iHead = p->pProp.iTail;
+ k = p->pJust.iHead;
+ CbsP_QueForEachEntry( p->pJust, pVar, i )
+ {
+ if ( CbsP_VarIsJust( pVar ) )
+ p->pJust.pData[k++] = pVar;
+ else if ( (hClause = CbsP_ManPropagateTwo( p, pVar, Level )) )
+ return hClause;
+ if( CbsP_ManCheckPropLimits(p) )
+ return 0;
+ }
+ if ( k == p->pJust.iTail )
+ break;
+ p->pJust.iTail = k;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solve the problem recursively.]
+
+ Description [Returns learnt clause if unsat, NULL if sat or undecided.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int CbsP_ManSolve_rec( CbsP_Man_t * p, int Level )
+{
+ CbsP_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pVar = NULL, * pDecVar;
+ int hClause, hLearn0, hLearn1;
+ int iPropHead, iJustHead, iJustTail;
+ // propagate assignments
+ assert( !CbsP_QueIsEmpty(&p->pProp) );
+ if ( (hClause = CbsP_ManPropagate( p, Level )) )
+ return hClause;
+
+ // quit using resource limits
+ if ( CbsP_ManCheckLimits( p ) )
+ return 0;
+ // check for satisfying assignment
+ assert( CbsP_QueIsEmpty(&p->pProp) );
+ if ( CbsP_QueIsEmpty(&p->pJust) )
+ return 0;
+ p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+ // remember the state before branching
+ iPropHead = p->pProp.iHead;
+ CbsP_QueStore( &p->pJust, &iJustHead, &iJustTail );
+ p->Pars.nJscanThis += iJustTail - iJustHead;
+ if ( CbsP_ManCheckLimits( p ) )
+ return 0;
+ // find the decision variable
+ if ( p->Pars.fUseHighest )
+ pVar = CbsP_ManDecideHighest( p );
+ else if ( p->Pars.fUseLowest )
+ pVar = CbsP_ManDecideLowest( p );
+ else if ( p->Pars.fUseMaxFF )
+ pVar = CbsP_ManDecideMaxFF( p );
+ else assert( 0 );
+ assert( CbsP_VarIsJust( pVar ) );
+ // chose decision variable using fanout count
+
+ if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
+ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
+ else
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+
+// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
+// pDecVar = Gia_Not(pDecVar);
+ // decide on first fanin
+ CbsP_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+ if ( !(hLearn0 = CbsP_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( CbsP_ManCheckLimits( p ) )
+ return 0;
+ if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+ return hLearn0;
+ CbsP_ManCancelUntil( p, iPropHead );
+ CbsP_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ CbsP_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+ if ( !(hLearn1 = CbsP_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( CbsP_ManCheckLimits( p ) )
+ return 0;
+ if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+ return hLearn1;
+ hClause = CbsP_ManResolve( p, Level, hLearn0, hLearn1 );
+// CbsP_ManPrintClauseNew( p, Level, hClause );
+// if ( Level > CbsP_ClauseDecLevel(p, hClause) )
+// p->Pars.nBTThisNc++;
+ p->Pars.nBTThis++;
+ return hClause;
+}
+
+/**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 [The two procedures differ in the CEX format.]
+
+ SeeAlso []
+
+***********************************************************************/
+int CbsP_ManSolve( CbsP_Man_t * p, Gia_Obj_t * pObj )
+{
+ int RetValue = 0;
+// s_Counter = 0;
+ assert( !p->pProp.iHead && !p->pProp.iTail );
+ assert( !p->pJust.iHead && !p->pJust.iTail );
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ CbsP_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( !CbsP_ManSolve_rec(p, 0) && !CbsP_ManCheckLimits(p) )
+ CbsP_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
+ CbsP_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_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
+ if ( CbsP_ManCheckLimits( p ) )
+ RetValue = -1;
+// printf( "%d ", s_Counter );
+ return RetValue;
+}
+int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
+{
+ abctime clk = Abc_Clock();
+ int RetValue = 0;
+// s_Counter = 0;
+ assert( !p->pProp.iHead && !p->pProp.iTail );
+ assert( !p->pJust.iHead && !p->pJust.iTail );
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ p->Pars.nJscanThis = p->Pars.nRscanThis = p->Pars.nPropThis = 0;
+ CbsP_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( pObj2 )
+ CbsP_ManAssign( p, pObj2, 0, NULL, NULL );
+ if ( !CbsP_ManSolve_rec(p, 0) && !CbsP_ManCheckLimits(p) )
+ CbsP_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
+ CbsP_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_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
+ if ( CbsP_ManCheckLimits( p ) )
+ RetValue = -1;
+
+ if( CBS_SAT == RetValue ){
+ p->nSatSat ++;
+ p->timeSatSat += Abc_Clock() - clk;
+ p->nConfSat += p->Pars.nBTThis;
+ } else
+ if( CBS_UNSAT == RetValue ){
+ p->nSatUnsat ++;
+ p->timeSatUnsat += Abc_Clock() - clk;
+ p->nConfUnsat += p->Pars.nBTThis;
+ } else {
+ p->nSatUndec ++;
+ p->timeSatUndec += Abc_Clock() - clk;
+ p->nConfUndec += p->Pars.nBTThis;
+ }
+// printf( "%d ", s_Counter );
+ CbsP_UpdateRecord(&p->Pars,RetValue);
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints statistics of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CbsP_ManSatPrintStats( CbsP_Man_t * p )
+{
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
+ printf( "JustMax = %5d ", p->Pars.nJustLimit );
+ printf( "\n" );
+ printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, 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, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, 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, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, 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 * CbsP_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
+{
+ extern void Gia_ManCollectTest( Gia_Man_t * pAig );
+ extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+ CbsP_Man_t * p;
+ Vec_Int_t * vCex, * vVisit, * vCexStore;
+ Vec_Str_t * vStatus;
+ Gia_Obj_t * pRoot;
+ int i, status;
+ abctime clk, clkTotal = Abc_Clock();
+ assert( Gia_ManRegNum(pAig) == 0 );
+// Gia_ManCollectTest( pAig );
+ // prepare AIG
+ Gia_ManCreateRefs( pAig );
+ Gia_ManCleanMark0( pAig );
+ Gia_ManCleanMark1( pAig );
+ Gia_ManFillValue( pAig ); // maps nodes into trail ids
+ Gia_ManSetPhase( pAig ); // maps nodes into trail ids
+ // create logic network
+ p = CbsP_ManAlloc( pAig );
+ p->Pars.nBTLimit = nConfs;
+ // create resulting data-structures
+ vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+ vCexStore = Vec_IntAlloc( 10000 );
+ vVisit = Vec_IntAlloc( 100 );
+ vCex = CbsP_ReadModel( p );
+ // solve for each output
+ Gia_ManForEachCo( pAig, pRoot, i )
+ {
+// printf( "\n" );
+
+ 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 = Abc_Clock();
+ p->Pars.fUseHighest = 1;
+ p->Pars.fUseLowest = 0;
+ status = CbsP_ManSolve( p, Gia_ObjChild0(pRoot) );
+// printf( "\n" );
+/*
+ if ( status == -1 )
+ {
+ p->Pars.fUseHighest = 0;
+ p->Pars.fUseLowest = 1;
+ status = CbsP_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 += Abc_Clock() - clk;
+ continue;
+ }
+ if ( status == 1 )
+ {
+ if ( f0Proved )
+ Gia_ManPatchCoDriver( pAig, i, 0 );
+ p->nSatUnsat++;
+ p->nConfUnsat += p->Pars.nBTThis;
+ p->timeSatUnsat += Abc_Clock() - clk;
+ continue;
+ }
+ p->nSatSat++;
+ p->nConfSat += p->Pars.nBTThis;
+// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+ Cec_ManSatAddToStore( vCexStore, vCex, i );
+ p->timeSatSat += Abc_Clock() - clk;
+ }
+ Vec_IntFree( vVisit );
+ p->nSatTotal = Gia_ManPoNum(pAig);
+ p->timeTotal = Abc_Clock() - clkTotal;
+ if ( fVerbose )
+ CbsP_ManSatPrintStats( p );
+// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
+ CbsP_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 ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaCSatP.h b/src/aig/gia/giaCSatP.h
new file mode 100644
index 00000000..4182cd14
--- /dev/null
+++ b/src/aig/gia/giaCSatP.h
@@ -0,0 +1,117 @@
+#ifndef ABC__aig__gia__giaCSatP_h
+#define ABC__aig__gia__giaCSatP_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+typedef struct CbsP_Par_t_ CbsP_Par_t;
+struct CbsP_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 nBTThisNc; // 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;
+ int fUseProved;
+
+ // statistics
+ int nJscanThis;
+ int nRscanThis;
+ int nPropThis;
+ int maxJscanUndec;
+ int maxRscanUndec;
+ int maxPropUndec;
+ int maxJscanSolved;
+ int maxRscanSolved;
+ int maxPropSolved;
+ int nSat, nUnsat, nUndec;
+ long accJscanSat;
+ long accJscanUnsat;
+ long accJscanUndec;
+ long accRscanSat;
+ long accRscanUnsat;
+ long accRscanUndec;
+ long accPropSat;
+ long accPropUnsat;
+ long accPropUndec;
+
+ // other limits
+ int nJscanLimit;
+ int nRscanLimit;
+ int nPropLimit;
+};
+
+typedef struct CbsP_Que_t_ CbsP_Que_t;
+struct CbsP_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 CbsP_Man_t_ CbsP_Man_t;
+struct CbsP_Man_t_
+{
+ CbsP_Par_t Pars; // parameters
+ Gia_Man_t * pAig; // AIG manager
+ CbsP_Que_t pProp; // propagation queue
+ CbsP_Que_t pJust; // justification queue
+ CbsP_Que_t pClauses; // clause queue
+ Gia_Obj_t ** pIter; // iterator through clause vars
+ Vec_Int_t * vLevReas; // levels and decisions
+ Vec_Int_t * vValue;
+ 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
+ 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
+ abctime timeSatUnsat; // unsat
+ abctime timeSatSat; // sat
+ abctime timeSatUndec; // undecided
+ abctime timeTotal; // total runtime
+};
+
+CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia );
+void CbsP_ManStop( CbsP_Man_t * p );
+void CbsP_ManSatPrintStats( CbsP_Man_t * p );
+void CbsP_PrintRecord( CbsP_Par_t * pPars );
+int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+
+#define CBS_UNSAT 1
+#define CBS_SAT 0
+#define CBS_UNDEC -1
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c
index b0e72284..d1241873 100644
--- a/src/aig/gia/giaCex.c
+++ b/src/aig/gia/giaCex.c
@@ -195,7 +195,7 @@ void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex )
pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) );
// the register values in the counter-example should be zero
Gia_ManForEachRo( pGia, pObj, k )
- assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
+ assert( Abc_InfoHasBit(pCex->pData, iBit) == 0 ), iBit++;
// iterate through the timeframes
nObjs = Gia_ManObjNum(pGia);
for ( i = 0; i <= pCex->iFrame; i++ )
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b3fcd295..cc501562 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -811,6 +811,55 @@ Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
+Gia_Man_t * Gia_ManDupNoBuf( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
+Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Vec_IntEntry(vMap, i) >= 0 )
+ pObj->Value = Gia_ManObj( p, Vec_IntEntry(vMap, i) )->Value;
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
@@ -865,7 +914,9 @@ Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
// Vec_IntFree( vPiPermInv );
Gia_ManForEachObj1( p, pObj, i )
{
- if ( Gia_ObjIsAnd(pObj) )
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
{
@@ -1086,6 +1137,23 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(pOne) + Gia_ManRegNum(pTwo) );
return pNew;
}
+void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs )
+{
+ Gia_Obj_t * pObj; int i;
+ assert( Vec_IntSize(vLits) == Gia_ManCiNum(p) );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Vec_IntEntry(vLits, i);
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( fBufs && Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Vec_IntClear( vLits );
+ Gia_ManForEachCo( p, pObj, i )
+ Vec_IntPush( vLits, Gia_ObjFanin0Copy(pObj) );
+ assert( Vec_IntSize(vLits) == Gia_ManCoNum(p) );
+}
/**Function*************************************************************
@@ -2934,6 +3002,92 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
/**Function*************************************************************
+ Synopsis [Creates miter of two designs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOut, int fVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, iLit;
+ int nInputs1 = Gia_ManCiNum(pTop) - Gia_ManCoNum(pBot);
+ int nInputs2 = Gia_ManCiNum(pBot) - Gia_ManCoNum(pTop);
+ if ( nInputs1 == nInputs2 )
+ printf( "Assuming that the circuits have %d shared inputs, ordered first.\n", nInputs1 );
+ else
+ {
+ printf( "The number of inputs and outputs does not match.\n" );
+ return NULL;
+ }
+ pNew = Gia_ManStart( Gia_ManObjNum(pBot) + Gia_ManObjNum(pTop) );
+ pNew->pName = Abc_UtilStrsav( "miter" );
+ Gia_ManFillValue( pBot );
+ Gia_ManFillValue( pTop );
+ Gia_ManConst0(pBot)->Value = 0;
+ Gia_ManConst0(pTop)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachCi( pBot, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+// Gia_ManForEachCo( pBot, pObj, i )
+// Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachAnd( pBot, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ Gia_ManForEachCo( pBot, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ManForEachCi( pTop, pObj, i )
+ if ( i < nInputs1 )
+ pObj->Value = Gia_ManCi(pBot, i)->Value;
+ else
+ pObj->Value = Gia_ManCo(pBot, i-nInputs1)->Value;
+// Gia_ManForEachCo( pTop, pObj, i )
+// Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachAnd( pTop, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ Gia_ManForEachCo( pTop, pObj, i )
+ {
+ if ( fDualOut )
+ {
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ManCi(pBot, i+nInputs1)->Value );
+ }
+ else
+ {
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ManCi(pBot, i+nInputs1)->Value );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ }
+ Gia_ManHashStop( pNew );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ assert( (pBot->vBarBufs == NULL) == (pTop->vBarBufs == NULL) );
+ if ( pBot->vBarBufs )
+ {
+ pNew->vBarBufs = Vec_IntAlloc( 1000 );
+ Vec_IntAppend( pNew->vBarBufs, pBot->vBarBufs );
+ Vec_IntAppend( pNew->vBarBufs, pTop->vBarBufs );
+ //printf( "Miter has %d buffers (%d groups).\n", pNew->nBufs, Vec_IntSize(pNew->vBarBufs) );
+ }
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the AND of all POs.]
Description []
@@ -5067,6 +5221,171 @@ Gia_Man_t * Gia_ManDupAddPis( Gia_Man_t * p, int nMulti )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManDupUifBoxTypes( Vec_Int_t * vBarBufs )
+{
+ Vec_Int_t * vTypes = Vec_IntAlloc( 10 );
+ int i, Entry;
+ Vec_IntForEachEntry( vBarBufs, Entry, i )
+ if ( Vec_IntFind(vTypes, Entry & 0xFFFE) < 0 )
+ Vec_IntPush( vTypes, Entry & 0xFFFE );
+ return vTypes;
+}
+Vec_Wec_t ** Gia_ManDupUifBuildMap( Gia_Man_t * p )
+{
+ Vec_Int_t * vTypes = Gia_ManDupUifBoxTypes( p->vBarBufs );
+ Vec_Wec_t ** pvMap = ABC_ALLOC( Vec_Wec_t *, 2*Vec_IntSize(vTypes) );
+ Vec_Int_t * vBufs = Vec_IntAlloc( p->nBufs );
+ Gia_Obj_t * pObj; int i, Item, j, k = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ if ( Gia_ObjIsBuf(pObj) )
+ Vec_IntPush( vBufs, i );
+ assert( p->nBufs == Vec_IntSize(vBufs) );
+ for ( i = 0; i < 2*Vec_IntSize(vTypes); i++ )
+ pvMap[i] = Vec_WecAlloc( 10 );
+ Vec_IntForEachEntry( p->vBarBufs, Item, i )
+ {
+ int Type = Vec_IntFind( vTypes, Item & 0xFFFE );
+ Vec_Int_t * vVec = Vec_WecPushLevel(pvMap[2*Type + (Item&1)]);
+ for ( j = 0; j < (Item >> 16); j++ )
+ Vec_IntPush( vVec, Vec_IntEntry(vBufs, k++) );
+ }
+ assert( p->nBufs == k );
+ for ( i = 0; i < Vec_IntSize(vTypes); i++ )
+ assert( Vec_WecSize(pvMap[2*i+0]) == Vec_WecSize(pvMap[2*i+1]) );
+ Vec_IntFree( vTypes );
+ Vec_IntFree( vBufs );
+ return pvMap;
+}
+int Gia_ManDupUifConstrOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vVec0, Vec_Int_t * vVec1 )
+{
+ Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vVec0) );
+ int i, o0, o1, iRes;
+ Vec_IntForEachEntryTwo( vVec0, vVec1, o0, o1, i )
+ Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Gia_ManObj(p, o0)->Value, Abc_LitNot(Gia_ManObj(p, o1)->Value)) );
+ iRes = Gia_ManHashAndMulti( pNew, vTemp );
+ Vec_IntFree( vTemp );
+ return iRes;
+}
+int Gia_ManDupUifConstr( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t ** pvMap, int nTypes )
+{
+ int t, i, k, iUif = 1;
+ for ( t = 0; t < nTypes; t++ )
+ {
+ assert( Vec_WecSize(pvMap[2*t+0]) == Vec_WecSize(pvMap[2*t+1]) );
+ for ( i = 0; i < Vec_WecSize(pvMap[2*t+0]); i++ )
+ for ( k = i + 1; k < Vec_WecSize(pvMap[2*t+0]); k++ )
+ {
+ int iCond1 = Gia_ManDupUifConstrOne( pNew, p, Vec_WecEntry(pvMap[2*t+0], i), Vec_WecEntry(pvMap[2*t+0], k) );
+ int iCond2 = Gia_ManDupUifConstrOne( pNew, p, Vec_WecEntry(pvMap[2*t+1], i), Vec_WecEntry(pvMap[2*t+1], k) );
+ int iRes = Gia_ManHashOr( pNew, Abc_LitNot(iCond1), iCond2 );
+ iUif = Gia_ManHashAnd( pNew, iUif, iRes );
+ }
+ }
+ return iUif;
+}
+Gia_Man_t * Gia_ManDupUif( Gia_Man_t * p )
+{
+ Vec_Int_t * vTypes = Gia_ManDupUifBoxTypes( p->vBarBufs );
+ Vec_Wec_t ** pvMap = Gia_ManDupUifBuildMap( p );
+ Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj;
+ int i, iUif = 0;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ }
+ iUif = Gia_ManDupUifConstr( pNew, p, pvMap, Vec_IntSize(vTypes) );
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, pObj->Value, iUif) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ for ( i = 0; i < 2*Vec_IntSize(vTypes); i++ )
+ Vec_WecFree( pvMap[i] );
+ ABC_FREE( pvMap );
+ if ( p->vBarBufs )
+ pNew->vBarBufs = Vec_IntDup( p->vBarBufs );
+ printf( "Added UIF constraints for %d type%s of boxes.\n", Vec_IntSize(vTypes), Vec_IntSize(vTypes) > 1 ? "s" :"" );
+ Vec_IntFree( vTypes );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManDupBlackBoxBuildMap( Gia_Man_t * p )
+{
+ Vec_Int_t * vMap = Vec_IntAlloc( p->nBufs ); int i, Item;
+ Vec_IntForEachEntry( p->vBarBufs, Item, i )
+ Vec_IntFillExtra( vMap, Vec_IntSize(vMap) + (Item >> 16), Item & 1 );
+ assert( p->nBufs == Vec_IntSize(vMap) );
+ return vMap;
+}
+Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p )
+{
+ Vec_Int_t * vMap = Gia_ManDupBlackBoxBuildMap( p );
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, k = 0, iCi = 0, nCis = Gia_ManCiNum(p) + Vec_IntSum(vMap);
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ for ( i = 0; i < nCis; i++ )
+ Gia_ManAppendCi( pNew );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ {
+ if ( Vec_IntEntry(vMap, k++) ) // out
+ pObj->Value = Gia_ManCiLit(pNew, iCi++);
+ else
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ }
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManCiLit(pNew, iCi++);
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ assert( k == p->nBufs && iCi == nCis );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ Vec_IntFree( vMap );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index a40673a7..ec733b85 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -539,7 +539,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
Abc_Print( 1, " %s =%8d", p->pMuxes? "nod" : "and", Gia_ManAndNum(p) );
SetConsoleTextAttribute( hConsole, 13 ); // magenta
Abc_Print( 1, " lev =%5d", Gia_ManLevelNum(p) );
- Abc_Print( 1, " (%.2f)", Gia_ManLevelAve(p) );
+ Abc_Print( 1, " (%7.2f)", Gia_ManLevelAve(p) );
SetConsoleTextAttribute( hConsole, 7 ); // normal
}
#else
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index 6cc528f2..f0558cc4 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -182,13 +182,56 @@ void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc )
SeeAlso []
***********************************************************************/
+void Gia_ManReadMiniAigNames( char * pFileName, Gia_Man_t * pGia )
+{
+ char * filename3 = Abc_UtilStrsavTwo( pFileName, ".ilo" );
+ FILE * pFile = fopen( filename3, "rb" );
+ if ( pFile )
+ {
+ char Buffer[5000], * pName; int i, iLines = 0;
+ Vec_Ptr_t * vTemp = Vec_PtrAlloc( Gia_ManRegNum(pGia) );
+ assert( pGia->vNamesIn == NULL );
+ pGia->vNamesIn = Vec_PtrAlloc( Gia_ManCiNum(pGia) );
+ assert( pGia->vNamesOut == NULL );
+ pGia->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pGia) );
+ while ( fgets(Buffer, 5000, pFile) )
+ {
+ if ( Buffer[strlen(Buffer)-1] == '\n' )
+ Buffer[strlen(Buffer)-1] = 0;
+ if ( iLines < Gia_ManPiNum(pGia) )
+ Vec_PtrPush( pGia->vNamesIn, Abc_UtilStrsav(Buffer) );
+ else if ( iLines < Gia_ManCiNum(pGia) )
+ Vec_PtrPush( vTemp, Abc_UtilStrsav(Buffer) );
+ else
+ Vec_PtrPush( pGia->vNamesOut, Abc_UtilStrsav(Buffer) );
+ iLines++;
+ }
+ Vec_PtrForEachEntry( char *, vTemp, pName, i )
+ {
+ Vec_PtrPush( pGia->vNamesIn, Abc_UtilStrsav(pName) );
+ Vec_PtrPush( pGia->vNamesOut, Abc_UtilStrsavTwo(pName, "_in") );
+ }
+ Vec_PtrFreeFree( vTemp );
+ fclose( pFile );
+ printf( "Read ILO names into file \"%s\".\n", filename3 );
+ }
+ ABC_FREE( filename3 );
+}
Gia_Man_t * Gia_ManReadMiniAig( char * pFileName, int fGiaSimple )
{
Mini_Aig_t * p = Mini_AigLoad( pFileName );
- Gia_Man_t * pGia = Gia_ManFromMiniAig( p, NULL, fGiaSimple );
+ Gia_Man_t * pTemp, * pGia = Gia_ManFromMiniAig( p, NULL, fGiaSimple );
ABC_FREE( pGia->pName );
pGia->pName = Extra_FileNameGeneric( pFileName );
Mini_AigStop( p );
+ Gia_ManReadMiniAigNames( pFileName, pGia );
+ if ( !Gia_ManIsNormalized(pGia) )
+ {
+ pGia = Gia_ManDupNormalize( pTemp = pGia, 0 );
+ ABC_SWAP( Vec_Ptr_t *, pTemp->vNamesIn, pGia->vNamesIn );
+ ABC_SWAP( Vec_Ptr_t *, pTemp->vNamesOut, pGia->vNamesOut );
+ Gia_ManStop( pTemp );
+ }
return pGia;
}
void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
@@ -764,7 +807,10 @@ int * Abc_FrameReadMiniAigEquivClasses( Abc_Frame_t * pAbc )
if ( pAbc->pGia2 == NULL )
printf( "Internal GIA with equivalence classes is not available.\n" );
if ( pAbc->pGia2->pReprs == NULL )
+ {
printf( "Equivalence classes of internal GIA are not available.\n" );
+ return NULL;
+ }
if ( Gia_ManObjNum(pAbc->pGia2) != Gia_ManObjNum(pAbc->pGiaMiniAig) )
printf( "Internal GIA with equivalence classes is not directly derived from MiniAig.\n" );
// derive the set of equivalent node pairs
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index 7b3aa54c..ff542c30 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -149,6 +149,73 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
/**Function*************************************************************
+ Synopsis [Creates AIG with XORs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCreateXors( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew; Gia_Obj_t * pObj, * pFan0, * pFan1;
+ Vec_Int_t * vRefs = Vec_IntStart( Gia_ManObjNum(p) );
+ int i, iLit0, iLit1, nXors = 0, nObjs = 0;
+ Gia_ManForEachObj( p, pObj, i )
+ pObj->fMark0 = 0;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ {
+ Vec_IntAddToEntry( vRefs, Gia_ObjId(p, Gia_Regular(pFan0)), 1 );
+ Vec_IntAddToEntry( vRefs, Gia_ObjId(p, Gia_Regular(pFan1)), 1 );
+ pObj->fMark0 = 1;
+ nXors++;
+ }
+ else
+ {
+ Vec_IntAddToEntry( vRefs, Gia_ObjFaninId0(pObj, i), 1 );
+ Vec_IntAddToEntry( vRefs, Gia_ObjFaninId1(pObj, i), 1 );
+ }
+ }
+ Gia_ManForEachCo( p, pObj, i )
+ Vec_IntAddToEntry( vRefs, Gia_ObjFaninId0p(p, pObj), 1 );
+ Gia_ManForEachAnd( p, pObj, i )
+ nObjs += Vec_IntEntry(vRefs, i) > 0;
+ pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Gia_ManCoNum(p) + nObjs );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( pObj->fMark0 )
+ {
+ Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1);
+ iLit0 = Abc_LitNotCond( Gia_Regular(pFan0)->Value, Gia_IsComplement(pFan0) );
+ iLit1 = Abc_LitNotCond( Gia_Regular(pFan1)->Value, Gia_IsComplement(pFan1) );
+ pObj->Value = Gia_ManAppendXorReal( pNew, iLit0, iLit1 );
+ }
+ else if ( Vec_IntEntry(vRefs, i) > 0 )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ assert( pNew->nObjs == pNew->nObjsAlloc );
+ pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjs );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ Vec_IntFree( vRefs );
+ //printf( "Created %d XORs.\n", nXors );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Derives GIA without MUXes.]
Description []
diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
index f14ce34a..dff2c59d 100644
--- a/src/aig/gia/giaPat2.c
+++ b/src/aig/gia/giaPat2.c
@@ -346,7 +346,7 @@ void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
else if ( Val0 == 4 && Val1 != 4 )
Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
- else if ( Val1 == 4 && Val1 != 4 )
+ else if ( Val1 == 4 && Val0 != 4 )
Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
else if ( Abc_Random(0) & 1 )
Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
@@ -890,6 +890,8 @@ int Min_ManCountSize( Vec_Wec_t * vCexes, int iFirst, int iLimit )
}
Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTries, int nMinCexes, Vec_Int_t * vStats[3], int fUseSim, int fUseSat, int fVerbose )
{
+ int fUseSynthesis = 1;
+ abctime clkSim = Abc_Clock(), clkSat = Abc_Clock();
Vec_Int_t * vOuts = vOuts0 ? vOuts0 : Vec_IntStartNatural( Gia_ManCoNum(p) );
Min_Man_t * pNew = Min_ManFromGia( p, vOuts );
Vec_Wec_t * vCexes = Vec_WecStart( Vec_IntSize(vOuts) * nMinCexes );
@@ -945,6 +947,7 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[0]) );
assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[1]) );
assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[2]) );
+ clkSim = Abc_Clock() - clkSim;
if ( fUseSat )
Gia_ManForEachCoVec( vOuts, p, pObj, i )
@@ -952,11 +955,13 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
continue;
{
+ abctime clk = Abc_Clock();
int iObj = Min_ManCo(pNew, i);
int Index = Gia_ObjCioId(pObj);
Vec_Int_t * vMap = Vec_IntAlloc( 100 );
Gia_Man_t * pCon = Gia_ManDupCones2( p, &Index, 1, vMap );
- Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCon, 8, 0, 0, 0, 0 );
+ Gia_Man_t * pCon1= fUseSynthesis ? Gia_ManAigSyn2( pCon, 0, 1, 0, 100, 0, 0, 0 ) : NULL;
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( fUseSynthesis ? pCon1 : pCon, 8, 0, 0, 0, 0 );
sat_solver* pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
int Lit = Abc_Var2Lit( 1, 0 );
int status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
@@ -972,8 +977,11 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
while ( nAllCalls++ < 100 )
{
int v, iVar = pCnf->nVars - Gia_ManPiNum(pCon), nVars = Gia_ManPiNum(pCon);
- sat_solver_randomize( pSat, iVar, nVars );
+ if ( nAllCalls > 1 )
+ sat_solver_randomize( pSat, iVar, nVars );
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ if ( status != l_True )
+ break;
assert( status == l_True );
Vec_IntClear( vLits );
for ( v = 0; v < nVars; v++ )
@@ -1004,11 +1012,22 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pCon );
+ Gia_ManStopP( &pCon1 );
Vec_IntFree( vMap );
+ if ( fVerbose )
+ {
+ printf( "SAT solving for output %3d (cexes = %5d) : ", i, nCurrCexes );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
}
}
+ clkSat = Abc_Clock() - clkSat - clkSim;
if ( fVerbose )
printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts );
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Simulation time ", clkSim );
+ if ( fVerbose )
+ Abc_PrintTime( 1, "SAT solving time ", clkSat );
//Vec_WecPrint( vCexes, 0 );
if ( vOuts != vOuts0 )
Vec_IntFreeP( &vOuts );
@@ -1076,7 +1095,7 @@ Vec_Ptr_t * Min_ReloadCexes( Vec_Wec_t * vCexes, int nMinCexes )
Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, int nWords0, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose )
{
abctime clk = Abc_Clock();
- int fVeryVerbose = 0;
+ //int fVeryVerbose = 0;
Vec_Wrd_t * vSimsPi = NULL;
Vec_Int_t * vLevel;
int w, nBits, nTotal = 0, fFailed = ABC_INFINITY;
@@ -1259,39 +1278,51 @@ Vec_Wrd_t * Gia_ManCollectSims( Gia_Man_t * pSwp, int nWords, Vec_Int_t * vOuts,
Vec_Int_t * vMap = Vec_IntAlloc( 100 );
Gia_Man_t * pSwp2 = Gia_ManDupCones2( pSwp, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vMap );
Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
- Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose );
- Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 );
- Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) );
- if ( fVerbose )
- Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) );
- if ( fVeryVerbose )
+ if ( Vec_IntSum(vStats[2]) == 0 )
{
- printf( "Unsolved = %4d ", Vec_IntSize(vOuts) );
- Gia_ManPrintStats( pSwp2, NULL );
- Vec_IntForEachEntry( vOuts, iObj, i )
+ for ( i = 0; i < 3; i++ )
+ Vec_IntFree( vStats[i] );
+ Vec_IntFree( vMap );
+ Gia_ManStop( pSwp2 );
+ Vec_WecFree( vCexes );
+ return NULL;
+ }
+ else
+ {
+ Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose );
+ Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 );
+ Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) );
+ if ( fVerbose )
+ Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) );
+ if ( fVeryVerbose )
{
- printf( "%4d : ", i );
- printf( "Out = %5d ", Vec_IntEntry(vMap, i) );
- printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) );
- printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) );
- printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) );
- printf( "Count = %5d ", Vec_IntEntry(vCounts, i) );
- printf( "\n" );
- if ( i == 20 )
- break;
+ printf( "Unsolved = %4d ", Vec_IntSize(vOuts) );
+ Gia_ManPrintStats( pSwp2, NULL );
+ Vec_IntForEachEntry( vOuts, iObj, i )
+ {
+ printf( "%4d : ", i );
+ printf( "Out = %5d ", Vec_IntEntry(vMap, i) );
+ printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) );
+ printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) );
+ printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) );
+ printf( "Count = %5d ", Vec_IntEntry(vCounts, i) );
+ printf( "\n" );
+ if ( i == 20 )
+ break;
+ }
}
+ for ( i = 0; i < 3; i++ )
+ Vec_IntFree( vStats[i] );
+ Vec_IntFree( vCounts );
+ Vec_WrdFree( vSimsPo );
+ Vec_WecFree( vCexes );
+ Gia_ManStop( pSwp2 );
+ //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) );
+ vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi );
+ Vec_WrdFree( vSimsPo );
+ Vec_IntFree( vMap );
+ return vSimsPi;
}
- for ( i = 0; i < 3; i++ )
- Vec_IntFree( vStats[i] );
- Vec_IntFree( vCounts );
- Vec_WrdFree( vSimsPo );
- Vec_WecFree( vCexes );
- Gia_ManStop( pSwp2 );
- //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) );
- vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi );
- Vec_WrdFree( vSimsPo );
- Vec_IntFree( vMap );
- return vSimsPi;
}
Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose )
{
diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c
new file mode 100644
index 00000000..3203a699
--- /dev/null
+++ b/src/aig/gia/giaResub6.c
@@ -0,0 +1,451 @@
+/**CFile****************************************************************
+
+ FileName [giaResub6.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Resubstitution.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaResub6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_NODE 100
+
+typedef struct Res6_Man_t_ Res6_Man_t;
+struct Res6_Man_t_
+{
+ int nIns; // inputs
+ int nDivs; // divisors
+ int nDivsA; // divisors alloc
+ int nOuts; // outputs
+ int nPats; // patterns
+ int nWords; // words
+ Vec_Wrd_t vIns; // input sim data
+ Vec_Wrd_t vOuts; // input sim data
+ word ** ppLits; // literal sim info
+ word ** ppSets; // set sim info
+ Vec_Int_t vSol; // current solution
+ Vec_Int_t vSolBest; // best solution
+ Vec_Int_t vTempBest;// current best solution
+};
+
+extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Res6_Man_t * Res6_ManStart( int nIns, int nNodes, int nOuts, int nPats )
+{
+ Res6_Man_t * p; int i;
+ p = ABC_CALLOC( Res6_Man_t, 1 );
+ p->nIns = nIns;
+ p->nDivs = 1 + nIns + nNodes;
+ p->nDivsA = p->nDivs + MAX_NODE;
+ p->nOuts = nOuts;
+ p->nPats = nPats;
+ p->nWords =(nPats + 63)/64;
+ Vec_WrdFill( &p->vIns, 2*p->nDivsA*p->nWords, 0 );
+ Vec_WrdFill( &p->vOuts, (1 << nOuts)*p->nWords, 0 );
+ p->ppLits = ABC_CALLOC( word *, 2*p->nDivsA );
+ p->ppSets = ABC_CALLOC( word *, 1 << nOuts );
+ for ( i = 0; i < 2*p->nDivsA; i++ )
+ p->ppLits[i] = Vec_WrdEntryP( &p->vIns, i*p->nWords );
+ for ( i = 0; i < (1 << nOuts); i++ )
+ p->ppSets[i] = Vec_WrdEntryP( &p->vOuts, i*p->nWords );
+ Abc_TtFill( p->ppLits[1], p->nWords );
+ Vec_IntGrow( &p->vSol, 2*MAX_NODE+nOuts );
+ Vec_IntGrow( &p->vSolBest, 2*MAX_NODE+nOuts );
+ Vec_IntGrow( &p->vTempBest, 2*MAX_NODE+nOuts );
+ return p;
+}
+static inline void Res6_ManStop( Res6_Man_t * p )
+{
+ Vec_WrdErase( &p->vIns );
+ Vec_WrdErase( &p->vOuts );
+ Vec_IntErase( &p->vSol );
+ Vec_IntErase( &p->vSolBest );
+ Vec_IntErase( &p->vTempBest );
+ ABC_FREE( p->ppLits );
+ ABC_FREE( p->ppSets );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Res6_Man_t * Res6_ManRead( char * pFileName )
+{
+ Res6_Man_t * p = NULL;
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ else
+ {
+ int i, k, nIns, nNodes, nOuts, nPats;
+ char Temp[100], Buffer[100];
+ char * pLine = fgets( Buffer, 100, pFile );
+ if ( pLine == NULL )
+ {
+ printf( "Cannot read the header line of input file \"%s\".\n", pFileName );
+ return NULL;
+ }
+ if ( 5 != sscanf(pLine, "%s %d %d %d %d", Temp, &nIns, &nNodes, &nOuts, &nPats) )
+ {
+ printf( "Cannot read the parameters from the header of input file \"%s\".\n", pFileName );
+ return NULL;
+ }
+ p = Res6_ManStart( nIns, nNodes, nOuts, nPats );
+ pLine = ABC_ALLOC( char, nPats + 100 );
+ for ( i = 1; i < p->nDivs; i++ )
+ {
+ char * pNext = fgets( pLine, nPats + 100, pFile );
+ if ( pNext == NULL )
+ {
+ printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
+ Res6_ManStop( p );
+ ABC_FREE( pLine );
+ fclose( pFile );
+ return NULL;
+ }
+ for ( k = 0; k < p->nPats; k++ )
+ if ( pNext[k] == '0' )
+ Abc_TtSetBit( p->ppLits[2*i+1], k );
+ else if ( pNext[k] == '1' )
+ Abc_TtSetBit( p->ppLits[2*i], k );
+ }
+ for ( i = 0; i < (1 << p->nOuts); i++ )
+ {
+ char * pNext = fgets( pLine, nPats + 100, pFile );
+ if ( pNext == NULL )
+ {
+ printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
+ Res6_ManStop( p );
+ ABC_FREE( pLine );
+ fclose( pFile );
+ return NULL;
+ }
+ for ( k = 0; k < p->nPats; k++ )
+ if ( pNext[k] == '1' )
+ Abc_TtSetBit( p->ppSets[i], k );
+ }
+ ABC_FREE( pLine );
+ fclose( pFile );
+ }
+ return p;
+}
+void Res6_ManWrite( char * pFileName, Res6_Man_t * p )
+{
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName );
+ else
+ {
+ int i, k;
+ fprintf( pFile, "resyn %d %d %d %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
+ for ( i = 1; i < p->nDivs; i++, fputc('\n', pFile) )
+ for ( k = 0; k < p->nPats; k++ )
+ if ( Abc_TtGetBit(p->ppLits[2*i+1], k) )
+ fputc( '0', pFile );
+ else if ( Abc_TtGetBit(p->ppLits[2*i], k) )
+ fputc( '1', pFile );
+ else
+ fputc( '-', pFile );
+ for ( i = 0; i < (1 << p->nOuts); i++, fputc('\n', pFile) )
+ for ( k = 0; k < p->nPats; k++ )
+ fputc( '0' + Abc_TtGetBit(p->ppSets[i], k), pFile );
+ fclose( pFile );
+ }
+}
+void Res6_ManPrintProblem( Res6_Man_t * p, int fVerbose )
+{
+ int i, nInputs = (p->nIns && p->nIns < 6) ? p->nIns : 6;
+ printf( "Problem: In = %d Div = %d Out = %d Pattern = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
+ if ( !fVerbose )
+ return;
+ printf( "%02d : %s\n", 0, "const0" );
+ printf( "%02d : %s\n", 1, "const1" );
+ for ( i = 1; i < p->nDivs; i++ )
+ {
+ if ( nInputs < 6 )
+ {
+ *p->ppLits[2*i+0] = Abc_Tt6Stretch( *p->ppLits[2*i+0], nInputs );
+ *p->ppLits[2*i+1] = Abc_Tt6Stretch( *p->ppLits[2*i+1], nInputs );
+ }
+ printf("%02d : ", 2*i+0), Dau_DsdPrintFromTruth2(p->ppLits[2*i+0], nInputs), printf( "\n" );
+ printf("%02d : ", 2*i+1), Dau_DsdPrintFromTruth2(p->ppLits[2*i+1], nInputs), printf( "\n" );
+ }
+ for ( i = 0; i < (1 << p->nOuts); i++ )
+ {
+ if ( nInputs < 6 )
+ *p->ppSets[i] = Abc_Tt6Stretch( *p->ppSets[i], nInputs );
+ printf("%02d : ", i), Dau_DsdPrintFromTruth2(p->ppSets[i], nInputs), printf( "\n" );
+ }
+}
+static inline Vec_Int_t * Res6_ManReadSol( char * pFileName )
+{
+ Vec_Int_t * vRes = NULL; int Num;
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ else
+ {
+ while ( fgetc(pFile) != '\n' );
+ vRes = Vec_IntAlloc( 10 );
+ while ( fscanf(pFile, "%d", &Num) == 1 )
+ Vec_IntPush( vRes, Num );
+ fclose ( pFile );
+ }
+ return vRes;
+}
+static inline void Res6_ManWriteSol( char * pFileName, Vec_Int_t * p )
+{
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName );
+ else
+ {
+ int i, iLit;
+ Vec_IntForEachEntry( p, iLit, i )
+ fprintf( pFile, "%d ", iLit );
+ fclose ( pFile );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Res6_LitSign( int iLit )
+{
+ return Abc_LitIsCompl(iLit) ? '~' : ' ';
+}
+static inline int Res6_LitChar( int iLit, int nDivs )
+{
+ return Abc_Lit2Var(iLit) < nDivs ? (nDivs < 28 ? 'a'+Abc_Lit2Var(iLit)-1 : 'd') : 'x';
+}
+static inline void Res6_LitPrint( int iLit, int nDivs )
+{
+ if ( iLit < 2 )
+ printf( "%d", iLit );
+ else
+ {
+ printf( "%c%c", Res6_LitSign(iLit), Res6_LitChar(iLit, nDivs) );
+ if ( Abc_Lit2Var(iLit) >= nDivs || nDivs >= 28 )
+ printf( "%d", Abc_Lit2Var(iLit) );
+ }
+}
+Vec_Int_t * Res6_FindSupport( Vec_Int_t * vSol, int nDivs )
+{
+ int i, iLit;
+ Vec_Int_t * vSupp = Vec_IntAlloc( 10 );
+ Vec_IntForEachEntry( vSol, iLit, i )
+ if ( iLit >= 2 && iLit < 2*nDivs )
+ Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
+ return vSupp;
+}
+void Res6_PrintSuppSims( Vec_Int_t * vSol, word ** ppLits, int nWords, int nDivs )
+{
+ Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
+ int i, k, iObj;
+ Vec_IntForEachEntry( vSupp, iObj, i )
+ {
+ for ( k = 0; k < 64*nWords; k++ )
+ if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
+ printf( "0" );
+ else if ( Abc_TtGetBit(ppLits[2*iObj], k) )
+ printf( "1" );
+ else
+ printf( "-" );
+ printf( "\n" );
+ }
+ for ( k = 0; k < 64*nWords; k++ )
+ {
+ Vec_IntForEachEntry( vSupp, iObj, i )
+ if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
+ printf( "0" );
+ else if ( Abc_TtGetBit(ppLits[2*iObj+0], k) )
+ printf( "1" );
+ else
+ printf( "-" );
+ printf( "\n" );
+ if ( k == 9 )
+ break;
+ }
+ Vec_IntFree( vSupp );
+}
+int Res6_FindSupportSize( Vec_Int_t * vSol, int nDivs )
+{
+ Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
+ int Res = Vec_IntSize(vSupp);
+ Vec_IntFree( vSupp );
+ return Res;
+}
+void Res6_PrintSolution( Vec_Int_t * vSol, int nDivs )
+{
+ int iNode, nNodes = Vec_IntSize(vSol)/2-1;
+ assert( Vec_IntSize(vSol) % 2 == 0 );
+ printf( "Solution: In = %d Div = %d Node = %d Out = %d\n", Res6_FindSupportSize(vSol, nDivs), nDivs-1, nNodes, 1 );
+ for ( iNode = 0; iNode <= nNodes; iNode++ )
+ {
+ int * pLits = Vec_IntEntryP( vSol, 2*iNode );
+ printf( "x%-2d = ", nDivs + iNode );
+ Res6_LitPrint( pLits[0], nDivs );
+ if ( pLits[0] != pLits[1] )
+ {
+ printf( " %c ", pLits[0] < pLits[1] ? '&' : '^' );
+ Res6_LitPrint( pLits[1], nDivs );
+ }
+ printf( "\n" );
+ }
+}
+int Res6_FindGetCost( Res6_Man_t * p, int iDiv )
+{
+ int w, Cost = 0;
+ //printf( "DivLit = %d\n", iDiv );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[iDiv], p->nIns ); printf( "\n" );
+ //printf( "Set0\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppSets[0], p->nIns ); printf( "\n" );
+ //printf( "Set1\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppSets[1], p->nIns ); printf( "\n" );
+ for ( w = 0; w < p->nWords; w++ )
+ Cost += Abc_TtCountOnes( (p->ppLits[iDiv][w] & p->ppSets[0][w]) | (p->ppLits[iDiv^1][w] & p->ppSets[1][w]) );
+ return Cost;
+}
+int Res6_FindBestDiv( Res6_Man_t * p, int * pCost )
+{
+ int d, dBest = -1, CostBest = ABC_INFINITY;
+ for ( d = 0; d < 2*p->nDivs; d++ )
+ {
+ int Cost = Res6_FindGetCost( p, d );
+ printf( "Div = %d Cost = %d\n", d, Cost );
+ if ( CostBest >= Cost )
+ CostBest = Cost, dBest = d;
+ }
+ if ( pCost )
+ *pCost = CostBest;
+ return dBest;
+}
+int Res6_FindBestEval( Res6_Man_t * p, Vec_Int_t * vSol, int Start )
+{
+ int i, iLit0, iLit1;
+ assert( Vec_IntSize(vSol) % 2 == 0 );
+ Vec_IntForEachEntryDoubleStart( vSol, iLit0, iLit1, i, 2*Start )
+ {
+ if ( iLit0 > iLit1 )
+ {
+ Abc_TtXor( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 );
+ Abc_TtXor( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 1 );
+ }
+ else
+ {
+ Abc_TtAnd( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 );
+ Abc_TtOr ( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0^1], p->ppLits[iLit1^1], p->nWords );
+ }
+
+ //printf( "Node %d\n", i/2 );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+0], 6 ); printf( "\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+1], 6 ); printf( "\n" );
+ }
+ return Res6_FindGetCost( p, Vec_IntEntryLast(vSol) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res6_ManResubVerify( Res6_Man_t * p, Vec_Int_t * vSol )
+{
+ int Cost = Res6_FindBestEval( p, vSol, 0 );
+ if ( Cost == 0 )
+ printf( "Verification successful.\n" );
+ else
+ printf( "Verification FAILED with %d errors on %d patterns.\n", Cost, p->nPats );
+}
+void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose )
+{
+ char FileNameSol[1000];
+ if ( pFileNameSol )
+ strcpy( FileNameSol, pFileNameSol );
+ else
+ {
+ strcpy( FileNameSol, pFileNameRes );
+ strcpy( FileNameSol + strlen(FileNameSol) - strlen(".resub"), ".sol" );
+ }
+ {
+ Res6_Man_t * p = Res6_ManRead( pFileNameRes );
+ Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol );
+ if ( p == NULL || vSol == NULL )
+ return;
+ if ( fVerbose )
+ Res6_ManPrintProblem( p, 0 );
+ if ( fVerbose )
+ Res6_PrintSolution( vSol, p->nDivs );
+ //if ( fVerbose )
+ // Res6_PrintSuppSims( vSol, p->ppLits, p->nWords, p->nDivs );
+ Res6_ManResubVerify( p, vSol );
+ Vec_IntFree( vSol );
+ Res6_ManStop( p );
+ }
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaSif.c b/src/aig/gia/giaSif.c
new file mode 100644
index 00000000..d25ae5db
--- /dev/null
+++ b/src/aig/gia/giaSif.c
@@ -0,0 +1,257 @@
+/**CFile****************************************************************
+
+ FileName [giaSif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaSif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_ManCutMerge( int * pCut, int * pCut1, int * pCut2, int nSize )
+{
+ int * pBeg = pCut+1;
+ int * pBeg1 = pCut1+1;
+ int * pBeg2 = pCut2+1;
+ int * pEnd1 = pBeg1 + pCut1[0];
+ int * pEnd2 = pBeg2 + pCut2[0];
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( pBeg == pCut+nSize )
+ {
+ pCut[0] = -1;
+ return;
+ }
+ if ( *pBeg1 == *pBeg2 )
+ *pBeg++ = *pBeg1++, pBeg2++;
+ else if ( *pBeg1 < *pBeg2 )
+ *pBeg++ = *pBeg1++;
+ else
+ *pBeg++ = *pBeg2++;
+ }
+ while ( pBeg1 < pEnd1 )
+ {
+ if ( pBeg == pCut+nSize )
+ {
+ pCut[0] = -1;
+ return;
+ }
+ *pBeg++ = *pBeg1++;
+ }
+ while ( pBeg2 < pEnd2 )
+ {
+ if ( pBeg == pCut+nSize )
+ {
+ pCut[0] = -1;
+ return;
+ }
+ *pBeg++ = *pBeg2++;
+ }
+ pCut[0] = pBeg-(pCut+1);
+ assert( pCut[0] < nSize );
+}
+static inline int Gia_ManCutChoice( Gia_Man_t * p, int Level, int iObj, int iSibl, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
+{
+ int * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
+ int * pCut2 = Vec_IntEntryP( vCuts, iSibl*nSize );
+ int Level2 = Vec_IntEntry( vTimes, iSibl ); int i;
+ assert( iObj > iSibl );
+ if ( Level < Level2 || (Level == Level2 && pCut[0] <= pCut2[0]) )
+ return Level;
+ for ( i = 0; i <= pCut2[0]; i++ )
+ pCut[i] = pCut2[i];
+ return Level2;
+}
+static inline int Gia_ManCutOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
+{
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ int iFan0 = Gia_ObjFaninId0(pObj, iObj);
+ int iFan1 = Gia_ObjFaninId1(pObj, iObj);
+ int Cut0[2] = { 1, iFan0 };
+ int Cut1[2] = { 1, iFan1 };
+ int * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
+ int * pCut0 = Vec_IntEntryP( vCuts, iFan0*nSize );
+ int * pCut1 = Vec_IntEntryP( vCuts, iFan1*nSize );
+ int Level_ = Vec_IntEntry( vTimes, iObj );
+ int Level0 = Vec_IntEntry( vTimes, iFan0 );
+ int Level1 = Vec_IntEntry( vTimes, iFan1 );
+ int Level = Abc_MaxInt( Level0, Level1 );
+ if ( Level == 0 )
+ Level = 1;
+ if ( Level0 == Level1 )
+ Gia_ManCutMerge( pCut, pCut0, pCut1, nSize );
+ else if ( Level0 > Level1 )
+ Gia_ManCutMerge( pCut, pCut0, Cut1, nSize );
+ else //if ( Level0 < Level1 )
+ Gia_ManCutMerge( pCut, pCut1, Cut0, nSize );
+ if ( pCut[0] == -1 )
+ {
+ pCut[0] = 2;
+ pCut[1] = iFan0;
+ pCut[2] = iFan1;
+ Level++;
+ }
+ if ( Gia_ObjSibl(p, iObj) )
+ Level = Gia_ManCutChoice( p, Level, iObj, Gia_ObjSibl(p, iObj), vCuts, vTimes, nSize );
+ assert( pCut[0] > 0 && pCut[0] < nSize );
+ Vec_IntUpdateEntry( vTimes, iObj, Level );
+ return Level > Level_;
+}
+int Gia_ManCheckIter( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period )
+{
+ int i, fChange = 0, nSize = nLutSize+1;
+ Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+ Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObjRo), Vec_IntEntry(vTimes, Gia_ObjId(p, pObjRi)) - Period );
+ Gia_ManForEachAnd( p, pObj, i )
+ fChange |= Gia_ManCutOne( p, i, vCuts, vTimes, nSize );
+ Gia_ManForEachRi( p, pObj, i )
+ Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) );
+ return fChange;
+}
+int Gia_ManCheckPeriod( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int * pIters )
+{
+ Gia_Obj_t * pObj; int i;
+ assert( Gia_ManRegNum(p) > 0 );
+ Vec_IntFill( vTimes, Gia_ManObjNum(p), -ABC_INFINITY );
+ Vec_IntWriteEntry( vTimes, 0, 0 );
+ Gia_ManForEachPi( p, pObj, i )
+ Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), 0 );
+ for ( *pIters = 0; *pIters < 100; (*pIters)++ )
+ {
+ if ( !Gia_ManCheckIter(p, vCuts, vTimes, nLutSize, Period) )
+ return 1;
+ Gia_ManForEachPo( p, pObj, i )
+ if ( Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) > Period )
+ return 0;
+ }
+ return 0;
+}
+static inline void Gia_ManPrintCutOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
+{
+ int i, * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
+ printf( "Obj %4d : Depth %d CutSize %d Cut {", iObj, Vec_IntEntry(vTimes, iObj), pCut[0] );
+ for ( i = 1; i <= pCut[0]; i++ )
+ printf( " %d", pCut[i] );
+ printf( " }\n" );
+}
+int Gia_ManTestMapComb( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize )
+{
+ Gia_Obj_t * pObj; int i, Id, Res = 0, nSize = nLutSize+1;
+ Vec_IntFill( vTimes, Gia_ManObjNum(p), 0 );
+ Gia_ManForEachCiId( p, Id, i )
+ Vec_IntWriteEntry( vCuts, Id*nSize, 1 );
+ Gia_ManForEachCiId( p, Id, i )
+ Vec_IntWriteEntry( vCuts, Id*nSize+1, Id );
+ Gia_ManForEachAnd( p, pObj, i )
+ Gia_ManCutOne( p, i, vCuts, vTimes, nSize );
+ Gia_ManForEachCo( p, pObj, i )
+ Res = Abc_MaxInt( Res, Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) );
+ //Gia_ManForEachAnd( p, pObj, i )
+ // Gia_ManPrintCutOne( p, i, vCuts, vTimes, nSize );
+ return Res;
+}
+void Gia_ManPrintTimes( Gia_Man_t * p, Vec_Int_t * vTimes, int Period )
+{
+ int Pos[16] = {0};
+ int Neg[16] = {0};
+ Gia_Obj_t * pObj; int i;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ int Time = Vec_IntEntry(vTimes, i)-Period;
+ Time = Abc_MinInt( Time, 10*Period );
+ Time = Abc_MaxInt( Time, -10*Period );
+ if ( Time >= 0 )
+ Pos[(Time + Period-1)/Period]++;
+ else
+ Neg[(-Time + Period-1)/Period]++;
+ }
+ printf( "Statistics: " );
+ for ( i = 15; i > 0; i-- )
+ if ( Neg[i] )
+ printf( " -%d=%d", i, Neg[i] );
+ for ( i = 0; i < 16; i++ )
+ if ( Pos[i] )
+ printf( " %d=%d", i, Pos[i] );
+ printf( "\n" );
+}
+Gia_Man_t * Gia_ManTestSif( Gia_Man_t * p, int nLutSize, int fVerbose )
+{
+ int nIters, nSize = nLutSize+1; // (2+1+nSize)*4=40 bytes/node
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vCuts = Vec_IntStart( Gia_ManObjNum(p) * nSize );
+ Vec_Int_t * vTimes = Vec_IntAlloc( Gia_ManObjNum(p) );
+ int Lower = 0;
+ int Upper = Gia_ManTestMapComb( p, vCuts, vTimes, nLutSize );
+ if ( fVerbose && Gia_ManRegNum(p) )
+ printf( "Clock period %2d is %s\n", Lower, 0 ? "Yes" : "No " );
+ if ( fVerbose && Gia_ManRegNum(p) )
+ printf( "Clock period %2d is %s\n", Upper, 1 ? "Yes" : "No " );
+ while ( Gia_ManRegNum(p) > 0 && Upper - Lower > 1 )
+ {
+ int Middle = (Upper + Lower) / 2;
+ int Status = Gia_ManCheckPeriod( p, vCuts, vTimes, nLutSize, Middle, &nIters );
+ if ( Status )
+ Upper = Middle;
+ else
+ Lower = Middle;
+ if ( fVerbose )
+ printf( "Clock period %2d is %s after %d iterations\n", Middle, Status ? "Yes" : "No ", nIters );
+ }
+ if ( fVerbose )
+ printf( "Clock period = %2d ", Upper );
+ if ( fVerbose )
+ printf( "LUT size = %d ", nLutSize );
+ if ( fVerbose )
+ printf( "Memory usage = %.2f MB ", 4.0*(2+1+nSize)*Gia_ManObjNum(p)/(1 << 20) );
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ //Gia_ManCheckPeriod( p, vCuts, vTimes, nLutSize, Upper, &nIters );
+ //Gia_ManPrintTimes( p, vTimes, Upper );
+ Vec_IntFree( vCuts );
+ Vec_IntFree( vTimes );
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index c31064fe..002f6bc2 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -750,7 +750,7 @@ void Gia_ManSimProfile( Gia_Man_t * pGia )
Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
- printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n",
+ printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n",
64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
Vec_WrdFree( vSims );
}
@@ -2485,15 +2485,21 @@ void Gia_ManSimGen( Gia_Man_t * pGia )
SeeAlso []
***********************************************************************/
-int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int fVerbose )
+int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int TimeLimit, int fVerbose )
{
Vec_Wrd_t * vSim0, * vSim1, * vSim2;
abctime clk = Abc_Clock();
int n, i, RetValue = 1;
+ int TimeStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0; // in CPU ticks
printf( "Simulating %d round with %d machine words.\n", nRounds, nWords );
Abc_RandomW(0);
for ( n = 0; RetValue && n < nRounds; n++ )
{
+ if ( TimeStop && Abc_Clock() > TimeStop )
+ {
+ printf( "Computation timed out after %d seconds and %d rounds.\n", TimeLimit, n );
+ break;
+ }
vSim0 = Vec_WrdStartRandom( Gia_ManCiNum(p0) * nWords );
p0->vSimsPi = vSim0;
p1->vSimsPi = vSim0;
@@ -2700,6 +2706,77 @@ Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose )
return p;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ Vec_Wrd_t * vSims = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords );
+ Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat );
+ Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie );
+ Gia_Obj_t * pObj; int * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
+ Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
+ pFlat->vSimsPi = NULL;
+ pHie->vSimsPi = NULL;
+ Vec_WrdFree( vSims );
+
+ printf( "Comparing two AIGs using %d simulation words.\n", nWords );
+ printf( "Hierarchical: " ); Gia_ManPrintStats( pHie, NULL );
+ printf( "Flat: " ); Gia_ManPrintStats( pFlat, NULL );
+
+ Vec_MemHashAlloc( vStore, 1 << 12 );
+ Gia_ManForEachCand( pFlat, pObj, i )
+ {
+ word * pSim = Vec_WrdEntryP(vSims0, i*nWords);
+ nC0s += Abc_TtIsConst0(pSim, nWords);
+ nC1s += Abc_TtIsConst1(pSim, nWords);
+ Vec_MemHashInsert( vStore, pSim );
+ }
+ nUnique = Vec_MemEntryNum( vStore );
+ printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n",
+ 64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pFlat), Gia_ManCandNum(pFlat), nC0s, nC1s );
+
+ assert( Gia_ManCiNum(pFlat) == Gia_ManCiNum(pHie) );
+ Gia_ManForEachCand( pHie, pObj, i )
+ {
+ word * pSim = Vec_WrdEntryP(vSims1, i*nWords);
+ pSpot = Vec_MemHashLookup( vStore, pSim );
+ Abc_TtNot( pSim, nWords );
+ pSpot2 = Vec_MemHashLookup( vStore, pSim );
+ Abc_TtNot( pSim, nWords );
+ nBoundary += Gia_ObjIsBuf(pObj);
+ if ( *pSpot != -1 || *pSpot2 != -1 )
+ {
+ nMatched++;
+ continue;
+ }
+ //Extra_PrintBinary( stdout, (unsigned *)pSim, 64*nWords ); printf("\n");
+ nFound[1] += Gia_ObjIsBuf(pObj);
+ nFound[2]++;
+ //if ( Gia_ObjIsBuf(pObj) )
+ // printf( "%d(%d) ", i, nBoundary-1 );
+ }
+ Vec_MemHashFree( vStore );
+ Vec_MemFree( vStore );
+ Vec_WrdFree( vSims0 );
+ Vec_WrdFree( vSims1 );
+
+ printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary. ",
+ nMatched, 100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)),
+ nFound[2], 100.0*nFound[2]/Abc_MaxInt(1, Gia_ManCandNum(pHie)),
+ nFound[1], 100.0*nFound[1]/Abc_MaxInt(1, nBoundary) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c
index f95d815d..96721d66 100644
--- a/src/aig/gia/giaSupps.c
+++ b/src/aig/gia/giaSupps.c
@@ -46,6 +46,7 @@ struct Supp_Man_t_
Gia_Man_t * pGia; // used for object names
// computed data
Vec_Wrd_t * vDivs[2]; // simulation values
+ Vec_Wrd_t * vDivsC[2]; // simulation values
Vec_Wrd_t * vPats[2]; // simulation values
Vec_Ptr_t * vMatrix; // simulation values
Vec_Wrd_t * vMask; // simulation values
@@ -138,13 +139,15 @@ int Supp_DeriveLines( Supp_Man_t * p )
{
int n, i, iObj, nWords = p->nWords;
int nDivWords = Abc_Bit6WordNum( Vec_IntSize(p->vCands) );
+ //Vec_IntPrint( p->vCands );
for ( n = 0; n < 2; n++ )
{
p->vDivs[n] = Vec_WrdStart( 64*nWords*nDivWords );
p->vPats[n] = Vec_WrdStart( 64*nWords*nDivWords );
+ //p->vDivsC[n] = Vec_WrdStart( 64*nWords*nDivWords );
if ( p->vSimsC )
Vec_IntForEachEntry( p->vCands, iObj, i )
- Abc_TtAndSharp( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSimsC, iObj*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n );
+ Abc_TtAndSharp( Vec_WrdEntryP(p->vDivsC[n], i*nWords), Vec_WrdEntryP(p->vSimsC, iObj*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n );
else
Vec_IntForEachEntry( p->vCands, iObj, i )
Abc_TtCopy( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n );
@@ -194,6 +197,8 @@ void Supp_ManDelete( Supp_Man_t * p )
Supp_ManCleanMatrix( p );
Vec_WrdFreeP( &p->vDivs[0] );
Vec_WrdFreeP( &p->vDivs[1] );
+ Vec_WrdFreeP( &p->vDivsC[0] );
+ Vec_WrdFreeP( &p->vDivsC[1] );
Vec_WrdFreeP( &p->vPats[0] );
Vec_WrdFreeP( &p->vPats[1] );
Vec_PtrFreeP( &p->vMatrix );
@@ -656,6 +661,110 @@ int Supp_ManReconstruct( Supp_Man_t * p, int fVerbose )
return Supp_ManRandomSolution( p, iSet, fVerbose );
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int s_Counter = 0;
+
+void Supp_DeriveDumpSims( FILE * pFile, Vec_Wrd_t * vDivs, int nWords )
+{
+ int i, k, nDivs = Vec_WrdSize(vDivs)/nWords;
+ for ( i = 0; i < nDivs; i++ )
+ {
+ word * pSim = Vec_WrdEntryP(vDivs, i*nWords);
+ for ( k = 0; k < 64*nWords; k++ )
+ fprintf( pFile, "%c", '0'+Abc_TtGetBit(pSim, k) );
+ fprintf( pFile, "\n" );
+ }
+}
+void Supp_DeriveDumpSimsC( FILE * pFile, Vec_Wrd_t * vDivs[2], int nWords )
+{
+ int i, k, nDivs = Vec_WrdSize(vDivs[0])/nWords;
+ for ( i = 0; i < nDivs; i++ )
+ {
+ word * pSim0 = Vec_WrdEntryP(vDivs[0], i*nWords);
+ word * pSim1 = Vec_WrdEntryP(vDivs[1], i*nWords);
+ for ( k = 0; k < 64*nWords; k++ )
+ if ( Abc_TtGetBit(pSim0, k) )
+ fprintf( pFile, "0" );
+ else if ( Abc_TtGetBit(pSim1, k) )
+ fprintf( pFile, "1" );
+ else
+ fprintf( pFile, "-" );
+ fprintf( pFile, "\n" );
+ }
+}
+void Supp_DeriveDumpProb( Vec_Wrd_t * vIsfs, Vec_Wrd_t * vDivs, int nWords )
+{
+ char Buffer[100]; int nDivs = Vec_WrdSize(vDivs)/nWords;
+ int RetValue = sprintf( Buffer, "%02d.resub", s_Counter );
+ FILE * pFile = fopen( Buffer, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file.\n" );
+ fprintf( pFile, "resyn %d %d %d %d\n", 0, nDivs, 1, 64*nWords );
+ //fprintf( pFile, "%d %d %d %d\n", 0, nDivs, 1, 64*nWords );
+ Supp_DeriveDumpSims( pFile, vDivs, nWords );
+ Supp_DeriveDumpSims( pFile, vIsfs, nWords );
+ fclose ( pFile );
+ RetValue = 0;
+}
+void Supp_DeriveDumpProbC( Vec_Wrd_t * vIsfs, Vec_Wrd_t * vDivs[2], int nWords )
+{
+ char Buffer[100]; int nDivs = Vec_WrdSize(vDivs[0])/nWords;
+ int RetValue = sprintf( Buffer, "%02d.resub", s_Counter );
+ FILE * pFile = fopen( Buffer, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file.\n" );
+ fprintf( pFile, "resyn %d %d %d %d\n", 0, nDivs, 1, 64*nWords );
+ //fprintf( pFile, "%d %d %d %d\n", 0, nDivs, 1, 64*nWords );
+ Supp_DeriveDumpSimsC( pFile, vDivs, nWords );
+ Supp_DeriveDumpSims( pFile, vIsfs, nWords );
+ fclose ( pFile );
+ RetValue = 0;
+}
+void Supp_DeriveDumpSol( Vec_Int_t * vSet, Vec_Int_t * vRes, int nDivs )
+{
+ char Buffer[100];
+ int RetValue = sprintf( Buffer, "%02d.sol", s_Counter );
+ int i, iLit, iLitRes = -1, nSupp = Vec_IntSize(vSet);
+ FILE * pFile = fopen( Buffer, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file.\n" );
+ fprintf( pFile, "sol name aig %d\n", Vec_IntSize(vRes)/2 );
+ //Vec_IntPrint( vSet );
+ //Vec_IntPrint( vRes );
+ Vec_IntForEachEntry( vRes, iLit, i )
+ {
+ assert( iLit != 2 && iLit != 3 );
+ if ( iLit < 2 )
+ iLitRes = iLit;
+ else if ( iLit-4 < 2*nSupp )
+ {
+ int iDiv = Vec_IntEntry(vSet, Abc_Lit2Var(iLit-4));
+ assert( iDiv >= 0 && iDiv < nDivs );
+ iLitRes = Abc_Var2Lit(1+iDiv, Abc_LitIsCompl(iLit));
+ }
+ else
+ iLitRes = iLit + 2*((nDivs+1)-(nSupp+2));
+ fprintf( pFile, "%d ", iLitRes );
+ }
+ if ( Vec_IntSize(vRes) & 1 )
+ fprintf( pFile, "%d ", iLitRes );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+ RetValue = 0;
+ printf( "Dumped solution info file \"%s\".\n", Buffer );
+}
+
/**Function*************************************************************
Synopsis []
@@ -705,6 +814,10 @@ Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVe
Vec_IntForEachEntry( vSet, iObj, i )
Vec_IntPush( *pvDivs, Vec_IntEntry(p->vCands, iObj) );
}
+ //Supp_DeriveDumpProbC( p->vIsfs, p->vDivsC, p->nWords );
+ //Supp_DeriveDumpProb( p->vIsfs, p->vDivs[1], p->nWords );
+ //Supp_DeriveDumpSol( vSet, vRes, Vec_WrdSize(p->vDivs[1])/p->nWords );
+ //s_Counter++;
}
return vRes;
}
@@ -802,11 +915,38 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t *
Supp_PrintOne( p, iBest );
}
vRes = Supp_ManFindBestSolution( p, p->vSolutions, fVerbose, pvDivs );
+ //Vec_IntPrint( vRes );
Supp_ManDelete( p );
// if ( vRes && Vec_IntSize(vRes) == 0 )
// Vec_IntFreeP( &vRes );
return vRes;
}
+void Supp_ManComputeTest( Gia_Man_t * p )
+{
+ Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+ Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
+ int i, iPoId, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
+ Vec_Wrd_t * vIsfs = Vec_WrdStart( 2*nWords );
+ Vec_Int_t * vCands = Vec_IntAlloc( 4 );
+ Vec_Int_t * vRes;
+
+// for ( i = 0; i < Gia_ManCiNum(p)+5; i++ )
+ for ( i = 0; i < Gia_ManCiNum(p); i++ )
+ Vec_IntPush( vCands, 1+i );
+
+ iPoId = Gia_ObjId(p, Gia_ManPo(p, 0));
+ Abc_TtCopy( Vec_WrdEntryP(vIsfs, 0*nWords), Vec_WrdEntryP(vSims, iPoId*nWords), nWords, 1 );
+ Abc_TtCopy( Vec_WrdEntryP(vIsfs, 1*nWords), Vec_WrdEntryP(vSims, iPoId*nWords), nWords, 0 );
+
+ vRes = Supp_ManCompute( vIsfs, vCands, NULL, vSims, NULL, nWords, p, NULL, 1, 1, 0 );
+ Vec_IntPrint( vRes );
+
+ Vec_WrdFree( vSimsPi );
+ Vec_WrdFree( vSims );
+ Vec_WrdFree( vIsfs );
+ Vec_IntFree( vCands );
+ Vec_IntFree( vRes );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index b1c5eb82..4722ef0f 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -795,6 +795,14 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
Gia_ManForEachAnd( p, pObj, i )
SwiTotal += pSwi[Gia_ObjFaninId0(pObj, i)] + pSwi[Gia_ObjFaninId1(pObj, i)];
}
+ if ( 0 )
+ {
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ printf( "Switch %6.2f ", pSwi[i] );
+ Gia_ObjPrint( p, pObj );
+ }
+ }
Vec_IntFree( vSwitching );
return SwiTotal;
}
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 431be5b7..d8130550 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -3080,7 +3080,55 @@ Gia_Man_t * Gia_ManTransformCond( Gia_Man_t * p )
Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
return NULL;
}
-
+void Gia_ManWriteSol( Gia_Man_t * p, char * pFileName )
+{
+ char * pBasicName = Extra_FileNameGeneric( pFileName );
+ char * pFileName2 = Abc_UtilStrsavTwo( pBasicName, ".sol" );
+ FILE * pFile = fopen( pFileName2, "wb" );
+ ABC_FREE( pBasicName );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName2 );
+ else
+ {
+ Gia_Obj_t * pObj; int i;
+ Gia_ManForEachAnd( p, pObj, i )
+ fprintf( pFile, "%d %d ", Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
+ Gia_ManForEachCo( p, pObj, i )
+ fprintf( pFile, "%d %d ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) );
+ fclose( pFile );
+ printf( "Finished writing solution file \"%s\".\n", pFileName2 );
+ }
+ ABC_FREE( pFileName2 );
+}
+void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName )
+{
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName );
+ else
+ {
+ Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+ Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+ int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
+ word * pTemp = ABC_ALLOC( word, nWords );
+ fprintf( pFile, "%d %d %d %d\n", Gia_ManCiNum(p), 0, Gia_ManCoNum(p), 1 << Gia_ManCiNum(p) );
+ for ( i = 0; i < Gia_ManCiNum(p); i++ )
+ Abc_TtPrintBinary1( pFile, Vec_WrdEntryP(vSimsPi, i*nWords), Gia_ManCiNum(p) ), fprintf(pFile, "\n");
+ for ( i = 0; i < (1 << Gia_ManCoNum(p)); i++ )
+ {
+ Abc_TtFill( pTemp, nWords );
+ for ( k = 0; k < Gia_ManCoNum(p); k++ )
+ Abc_TtAndCompl( pTemp, pTemp, 0, Vec_WrdEntryP(vSimsPo, k*nWords), !((i>>k)&1), nWords );
+ Abc_TtPrintBinary1( pFile, pTemp, Gia_ManCiNum(p) ), fprintf(pFile, "\n");
+ }
+ ABC_FREE( pTemp );
+ fclose( pFile );
+ Vec_WrdFree( vSimsPi );
+ Vec_WrdFree( vSimsPo );
+ printf( "Finished writing resub file \"%s\".\n", pFileName );
+ Gia_ManWriteSol( p, pFileName );
+ }
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index d801a243..171d8be3 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -15,6 +15,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaCSat.c \
src/aig/gia/giaCSat2.c \
src/aig/gia/giaCSat3.c \
+ src/aig/gia/giaCSatP.c \
src/aig/gia/giaCTas.c \
src/aig/gia/giaCut.c \
src/aig/gia/giaDecs.c \
@@ -68,6 +69,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaResub.c \
src/aig/gia/giaResub2.c \
src/aig/gia/giaResub3.c \
+ src/aig/gia/giaResub6.c \
src/aig/gia/giaRetime.c \
src/aig/gia/giaRex.c \
src/aig/gia/giaSatEdge.c \
@@ -82,6 +84,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaShrink.c \
src/aig/gia/giaShrink6.c \
src/aig/gia/giaShrink7.c \
+ src/aig/gia/giaSif.c \
src/aig/gia/giaSim.c \
src/aig/gia/giaSim2.c \
src/aig/gia/giaSimBase.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 02:16:27 +0000