diff options
Diffstat (limited to 'src/aig/gia/giaAig.c')
| -rw-r--r-- | src/aig/gia/giaAig.c | 247 |
1 files changed, 234 insertions, 13 deletions
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index fa9030c5..0e004f87 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -19,6 +19,12 @@ ***********************************************************************/ #include "giaAig.h" +#include "fra.h" +#include "dch.h" +#include "dar.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -84,6 +90,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; // create room to store equivalences if ( p->pEquivs ) pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) ); @@ -122,6 +129,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ) // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; // create the PIs Aig_ManCleanData( p ); Aig_ManForEachObj( p, pObj, i ) @@ -138,8 +146,6 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ) assert( 0 ); } Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); - if ( pNew->pNexts ) - Gia_ManDeriveReprs( pNew ); return pNew; } @@ -162,6 +168,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->iData = 1; @@ -178,7 +185,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) Aig_ManForEachPo( p, pObj, i ) Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) ); Aig_ManForEachPo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) ); + pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) ); Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); return pNew; } @@ -240,6 +247,7 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; // pNew->pSpec = Gia_UtilStrsav( p->pName ); // duplicate representation of choice nodes if ( fChoices ) @@ -249,6 +257,10 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) ppNodes[0] = Aig_ManConst0(pNew); Gia_ManForEachCi( p, pObj, i ) ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew ); + // transfer level + if ( p->vLevels ) + Gia_ManForEachCi( p, pObj, i ) + Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) ); // add logic for the POs Gia_ManForEachCo( p, pObj, i ) { @@ -282,6 +294,7 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; // pNew->pSpec = Gia_UtilStrsav( p->pName ); // create the PIs ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); @@ -312,6 +325,48 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) SeeAlso [] ***********************************************************************/ +Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t ** ppNodes; + Gia_Obj_t * pObj; + int i; + ppNodes = ABC_ALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); + // create the new manager + pNew = Aig_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->nConstrs = p->nConstrs; + // create the PIs + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); + else if ( Gia_ObjIsCi(pObj) ) + ppNodes[i] = Aig_ObjCreatePi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + ppNodes[i] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); + else if ( Gia_ObjIsConst0(pObj) ) + ppNodes[i] = Aig_ManConst0(pNew); + else + assert( 0 ); + pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) ); + } + Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + ABC_FREE( ppNodes ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) { Aig_Man_t * pMan; @@ -329,41 +384,69 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) Synopsis [Transfers representatives from pGia to pAig.] - Description [] + Description [Assumes that pGia was created from pAig.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ) +void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) { Aig_Obj_t * pObj; Gia_Obj_t * pGiaObj, * pGiaRepr; int i; - assert( p->pReprs == NULL ); + assert( pAig->pReprs == NULL ); assert( pGia->pReprs != NULL ); // move pointers from AIG to GIA - Aig_ManForEachObj( p, pObj, i ) + Aig_ManForEachObj( pAig, pObj, i ) { assert( i == 0 || !Gia_LitIsCompl(pObj->iData) ); pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) ); pGiaObj->Value = i; } // set the pointers to the nodes in AIG - Aig_ManReprStart( p, Aig_ManObjNumMax(p) ); + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + Gia_ManForEachObj( pGia, pGiaObj, i ) + { + pGiaRepr = Gia_ObjReprObj( pGia, i ); + if ( pGiaRepr == NULL ) + continue; + Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) ); + } +} + +/**Function************************************************************* + + Synopsis [Transfers representatives from pGia to pAig.] + + Description [Assumes that pAig was created from pGia.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ) +{ + Gia_Obj_t * pGiaObj, * pGiaRepr; + int i; + assert( pAig->pReprs == NULL ); + assert( pGia->pReprs != NULL ); + // set the pointers to the nodes in AIG + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); Gia_ManForEachObj( pGia, pGiaObj, i ) { pGiaRepr = Gia_ObjReprObj( pGia, i ); if ( pGiaRepr == NULL ) continue; - Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) ); + Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Gia_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Gia_Lit2Var(pGiaObj->Value)) ); } } /**Function************************************************************* - Synopsis [Applied DC2 to the GIA manager.] + Synopsis [Transfers representatives from pAig to pGia.] Description [] @@ -372,21 +455,159 @@ void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p ) +void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) { - extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose ); + Gia_Obj_t * pObjGia; + Aig_Obj_t * pObjAig, * pReprAig; + int i; + assert( pAig->pReprs != NULL ); + assert( pGia->pReprs == NULL ); + assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManPoNum(pAig) ); + pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) ); + for ( i = 0; i < Gia_ManObjNum(pGia); i++ ) + Gia_ObjSetRepr( pGia, i, GIA_VOID ); + Gia_ManForEachObj( pGia, pObjGia, i ) + { +// Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 ); + if ( Gia_ObjIsCo(pObjGia) ) + continue; + assert( i == 0 || !Gia_LitIsCompl(Gia_ObjValue(pObjGia)) ); + pObjAig = Aig_ManObj( pAig, Gia_Lit2Var(Gia_ObjValue(pObjGia)) ); + pObjAig->iData = i; + } + Aig_ManForEachObj( pAig, pObjAig, i ) + { + if ( Aig_ObjIsPo(pObjAig) ) + continue; + if ( pAig->pReprs[i] == NULL ) + continue; + pReprAig = pAig->pReprs[i]; + Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData ); + } + pGia->pNexts = Gia_ManDeriveNexts( pGia ); +} + +/**Function************************************************************* + + Synopsis [Applies DC2 to the GIA manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ) +{ +// extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose ); Gia_Man_t * pGia; Aig_Man_t * pNew, * pTemp; pNew = Gia_ManToAig( p, 0 ); - pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 ); + pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose ); Aig_ManStop( pTemp ); pGia = Gia_ManFromAig( pNew ); Aig_ManStop( pNew ); return pGia; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ) +{ + Gia_Man_t * pGia; + Aig_Man_t * pNew; + pNew = Gia_ManToAig( p, 0 ); + pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars ); + pGia = Gia_ManFromAig( pNew ); + Aig_ManStop( pNew ); + return pGia; +} + +/**Function************************************************************* + + Synopsis [Computes equivalences after structural sequential cleanup.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ) +{ + Aig_Man_t * pNew, * pTemp; + pNew = Gia_ManToAigSimple( p ); + pTemp = Aig_ManScl( pNew, fConst, fEquiv, fVerbose ); + Gia_ManReprFromAigRepr( pNew, p ); + Aig_ManStop( pTemp ); + Aig_ManStop( pNew ); +} + +/**Function************************************************************* + + Synopsis [Solves SAT problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSolveSat( Gia_Man_t * p ) +{ +// extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); + Aig_Man_t * pNew; + int RetValue, clk = clock(); + pNew = Gia_ManToAig( p, 0 ); + RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0 ); + if ( RetValue == 0 ) + { + Gia_Obj_t * pObj; + int i, * pInit = (int *)pNew->pData; + Gia_ManConst0(p)->fMark0 = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->fMark0 = pInit[i]; + Gia_ManForEachAnd( p, pObj, i ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachPo( p, pObj, i ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + Gia_ManForEachPo( p, pObj, i ) + if ( pObj->fMark0 != 1 ) + break; + if ( i != Gia_ManPoNum(p) ) + Abc_Print( 1, "Counter-example verification has failed. " ); +// else +// Abc_Print( 1, "Counter-example verification succeeded. " ); + } +/* + else if ( RetValue == 1 ) + Abc_Print( 1, "The SAT problem is unsatisfiable. " ); + else if ( RetValue == -1 ) + Abc_Print( 1, "The SAT problem is undecided. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); +*/ + Aig_ManStop( pNew ); + return RetValue; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |