diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-27 18:37:39 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-27 18:37:39 -0700 |
commit | 613e8b2ad6b24369467179b15c2ab2638f9b8672 (patch) | |
tree | 4dc851dd295a5f7703cb018af20847e001712d67 /src/aig/gia | |
parent | 324d73c29a22766063df46f9e35a3cbe719a83c2 (diff) | |
download | abc-613e8b2ad6b24369467179b15c2ab2638f9b8672.tar.gz abc-613e8b2ad6b24369467179b15c2ab2638f9b8672.tar.bz2 abc-613e8b2ad6b24369467179b15c2ab2638f9b8672.zip |
SAT sweeping under constraints.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAiger.c | 3 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 41 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 30 |
4 files changed, 75 insertions, 2 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 6dad5eb5..41093a30 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -874,6 +874,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); @@ -1071,8 +1072,10 @@ extern void Gia_ManCleanTruth( Gia_Man_t * p ); extern void Gia_ManFillValue( Gia_Man_t * p ); extern void Gia_ObjSetPhase( Gia_Obj_t * pObj ); extern void Gia_ManSetPhase( Gia_Man_t * p ); +extern void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues ); extern void Gia_ManSetPhase1( Gia_Man_t * p ); extern void Gia_ManCleanPhase( Gia_Man_t * p ); +extern int Gia_ManCheckCoPhase( Gia_Man_t * p ); extern int Gia_ManLevelNum( Gia_Man_t * p ); extern void Gia_ManCreateValueRefs( Gia_Man_t * p ); extern void Gia_ManCreateRefs( Gia_Man_t * p ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 19ea1447..e30d88de 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -1044,6 +1044,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int p->vNamesOut = pInit->vNamesOut; pInit->vNamesOut = NULL; p->pAigExtra = pInit->pAigExtra; pInit->pAigExtra = NULL; p->nAnd2Delay = pInit->nAnd2Delay; pInit->nAnd2Delay = 0; + p->nConstrs = pInit->nConstrs; pInit->nConstrs = 0; } else p = pInit; @@ -1137,7 +1138,6 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Vec_StrFree( vStrExt ); if ( fVerbose ) printf( "Finished writing extension \"a\".\n" ); } -/* // write constraints if ( p->nConstrs ) { @@ -1145,7 +1145,6 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_FileWriteBufferSize( pFile, 4 ); Gia_FileWriteBufferSize( pFile, p->nConstrs ); } -*/ // write timing information if ( p->nAnd2Delay ) { diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 78aac33c..f3f60267 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2243,6 +2243,47 @@ Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG with nodes ordered by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, nLevels = Gia_ManLevelNum( p ); + int * pCounts = ABC_CALLOC( int, nLevels + 1 ); + int * pNodes = ABC_ALLOC( int, Gia_ManAndNum(p) ); + Gia_ManForEachAnd( p, pObj, i ) + pCounts[Gia_ObjLevel(p, pObj)]++; + for ( i = 1; i <= nLevels; i++ ) + pCounts[i] += pCounts[i-1]; + Gia_ManForEachAnd( p, pObj, i ) + pNodes[pCounts[Gia_ObjLevel(p, pObj)-1]++] = i; + // duplicate + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( i = 0; i < Gia_ManAndNum(p) && (pObj = Gia_ManObj(p, pNodes[i])); i++ ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + ABC_FREE( pCounts ); + ABC_FREE( pNodes ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 6f4389a8..1d122112 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -366,6 +366,16 @@ void Gia_ManSetPhase( Gia_Man_t * p ) Gia_ManForEachObj( p, pObj, i ) Gia_ObjSetPhase( pObj ); } +void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjIsCi(pObj) ) + pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) ); + else + Gia_ObjSetPhase( pObj ); +} /**Function************************************************************* @@ -410,6 +420,26 @@ void Gia_ManCleanPhase( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Returns the number of COs whose value is 1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCheckCoPhase( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachCo( p, pObj, i ) + Counter += pObj->fPhase; + return Counter; +} + +/**Function************************************************************* + Synopsis [Prepares copies for the model.] Description [] |