From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/aig/dch/dch.h | 20 +++++++++----- src/aig/dch/dchAig.c | 15 +++++++---- src/aig/dch/dchChoice.c | 71 ++++++++++++++++++++++++++++++++++++++++++++++--- src/aig/dch/dchClass.c | 35 +++++++++++++----------- src/aig/dch/dchCnf.c | 15 +++++++---- src/aig/dch/dchCore.c | 23 +++++++++++++++- src/aig/dch/dchInt.h | 19 +++++++------ src/aig/dch/dchMan.c | 39 +++++++++++++++------------ src/aig/dch/dchSat.c | 5 ++++ src/aig/dch/dchSim.c | 13 ++++++--- src/aig/dch/dchSimSat.c | 17 +++++++----- src/aig/dch/dchSweep.c | 5 ++++ 12 files changed, 207 insertions(+), 70 deletions(-) (limited to 'src/aig/dch') diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index 7271d256..69f340e5 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -21,6 +21,7 @@ #ifndef __DCH_H__ #define __DCH_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -29,9 +30,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -65,14 +67,20 @@ struct Dch_Pars_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== dchAig.c ==========================================================*/ +extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); /*=== dchCore.c ==========================================================*/ extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); +extern int Dch_ManReadVerbose( Dch_Pars_t * p ); extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ); +/*=== dchScript.c ==========================================================*/ +extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ); + + +ABC_NAMESPACE_HEADER_END + -#ifdef __cplusplus -} -#endif #endif diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c index d38a1304..91a00c63 100644 --- a/src/aig/dch/dchAig.c +++ b/src/aig/dch/dchAig.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -67,8 +70,8 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) assert( Vec_PtrSize(vAigs) > 0 ); // make sure they have the same number of PIs/POs nNodes = 0; - pAig = Vec_PtrEntry( vAigs, 0 ); - Vec_PtrForEachEntry( vAigs, pAig2, i ) + pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 ); + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i ) { assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) ); assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) ); @@ -77,19 +80,19 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) } // map constant nodes pAigTotal = Aig_ManStart( nNodes ); - Vec_PtrForEachEntry( vAigs, pAig2, k ) + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal); // map primary inputs Aig_ManForEachPi( pAig, pObj, i ) { pObjPi = Aig_ObjCreatePi( pAigTotal ); - Vec_PtrForEachEntry( vAigs, pAig2, k ) + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) Aig_ManPi( pAig2, i )->pData = pObjPi; } // construct the AIG in the order of POs Aig_ManForEachPo( pAig, pObj, i ) { - Vec_PtrForEachEntry( vAigs, pAig2, k ) + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) { pObjPo = Aig_ManPo( pAig2, i ); Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) ); @@ -112,3 +115,5 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c index 019f4ec4..c20d2974 100644 --- a/src/aig/dch/dchChoice.c +++ b/src/aig/dch/dchChoice.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -204,8 +207,8 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_ if ( pRepr == NULL ) return; // get the corresponding new nodes - pObjNew = Aig_Regular(pObj->pData); - pReprNew = Aig_Regular(pRepr->pData); + pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData); + pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData); if ( pObjNew == pReprNew ) return; // skip the earlier nodes @@ -240,7 +243,7 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_ SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig ) { Aig_Man_t * pChoices, * pTemp; Aig_Obj_t * pObj; @@ -268,8 +271,70 @@ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) return pChoices; } + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig ) +{ + Aig_Man_t * pChoices; + Aig_Obj_t * pObj; + int i; + // start recording equivalences + pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + pChoices->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + // map constants and PIs + Aig_ManCleanData( pAig ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pChoices ); + // construct choices for the internal nodes + assert( pAig->pReprs != NULL ); + Aig_ManForEachNode( pAig, pObj, i ) + Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); + Aig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); + Dch_DeriveChoiceCountEquivs( pChoices ); + return pChoices; +} + +/**Function************************************************************* + + Synopsis [Derives the AIG with choices from representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +{ + Aig_Man_t * pChoices, * pTemp; + pChoices = Dch_DeriveChoiceAigInt( pAig ); +// pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices ); +// Aig_ManStop( pTemp ); + // there is no need for cleanup + ABC_FREE( pChoices->pReprs ); + pChoices = Aig_ManDupDfs( pTemp = pChoices ); + Aig_ManStop( pTemp ); + return pChoices; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c index 9f4bd68c..83a3bc2e 100644 --- a/src/aig/dch/dchClass.c +++ b/src/aig/dch/dchClass.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + /* The candidate equivalence classes are stored as a vector of pointers to the array of pointers to the nodes in each class. @@ -280,10 +283,10 @@ void Dch_ClassesPrintOne( Dch_Cla_t * p, Aig_Obj_t * pRepr ) { Aig_Obj_t * pObj; int i; - printf( "{ " ); + Abc_Print( 1, "{ " ); Dch_ClassForEachNode( p, pRepr, pObj, i ) - printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); - printf( "}\n" ); + Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + Abc_Print( 1, "}\n" ); } /**Function************************************************************* @@ -302,21 +305,21 @@ void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose ) Aig_Obj_t ** ppClass; Aig_Obj_t * pObj; int i; - printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", + Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", p->nCands1, p->nClasses, p->nLits ); if ( !fVeryVerbose ) return; - printf( "Constants { " ); + Abc_Print( 1, "Constants { " ); Aig_ManForEachObj( p->pAig, pObj, i ) if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) ) - printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); - printf( "}\n" ); + Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); + Abc_Print( 1, "}\n" ); Dch_ManForEachClass( p, ppClass, i ) { - printf( "%3d (%3d) : ", i, p->pClassSizes[i] ); + Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] ); Dch_ClassesPrintOne( p, ppClass[0] ); } - printf( "\n" ); + Abc_Print( 1, "\n" ); } /**Function************************************************************* @@ -456,20 +459,20 @@ int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi return 0; // get the new representative - pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); assert( Vec_PtrSize(p->vClassOld) > 0 ); assert( Vec_PtrSize(p->vClassNew) > 0 ); // create old class pClassOld = Dch_ObjRemoveClass( p, pReprOld ); - Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) { pClassOld[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL ); } // create new class pClassNew = pClassOld + i; - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { pClassNew[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); @@ -572,21 +575,21 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs return 0; // collect the nodes to be refined Vec_PtrClear( p->vClassNew ); - Vec_PtrForEachEntry( vRoots, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) Vec_PtrPush( p->vClassNew, pObj ); // check if there is a new class if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; p->nCands1 -= Vec_PtrSize(p->vClassNew); - pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 ); Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); if ( Vec_PtrSize(p->vClassNew) == 1 ) return 1; // create a new class composed of these nodes ppClassNew = p->pMemClassesFree; p->pMemClassesFree += Vec_PtrSize(p->vClassNew); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { ppClassNew[i] = pObj; Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); @@ -604,3 +607,5 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchCnf.c b/src/aig/dch/dchCnf.c index 81fc2f2c..4175a123 100644 --- a/src/aig/dch/dchCnf.c +++ b/src/aig/dch/dchCnf.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -169,7 +172,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1); @@ -182,7 +185,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) assert( RetValue ); } // add A & B => C or !A + !B + C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); if ( p->pPars->fPolarFlip ) @@ -293,7 +296,7 @@ void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ) vFrontier = Vec_PtrAlloc( 100 ); Dch_ObjAddToFrontier( p, pObj, vFrontier ); // explore nodes in the frontier - Vec_PtrForEachEntry( vFrontier, pNode, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i ) { // create the supergate assert( Dch_ObjSatNum(p,pNode) ); @@ -304,14 +307,14 @@ void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k ) Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Dch_AddClausesMux( p, pNode ); } else { Dch_CollectSuper( pNode, fUseMuxes, p->vFanins ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k ) Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Dch_AddClausesSuper( p, pNode, p->vFanins ); } @@ -327,3 +330,5 @@ void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index d38d5668..bc78682b 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -55,6 +58,22 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) p->nCallsRecycle = 100; // calls to perform before recycling SAT solver } +/**Function************************************************************* + + Synopsis [Returns verbose parameter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ManReadVerbose( Dch_Pars_t * p ) +{ + return p->fVerbose; +} + /**Function************************************************************* Synopsis [Performs computation of AIGs with choices.] @@ -91,7 +110,7 @@ p->timeTotal = clock() - clkTotal; pResult = Dch_DeriveChoiceAig( pAig ); // count the number of representatives if ( pPars->fVerbose ) - printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", + Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", Dch_DeriveChoiceCountReprs( pAig ), Dch_DeriveChoiceCountEquivs( pResult ), Aig_ManChoiceNum( pResult ) ); @@ -135,3 +154,5 @@ p->timeTotal = clock() - clkTotal; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h index a419335d..6072d97b 100644 --- a/src/aig/dch/dchInt.h +++ b/src/aig/dch/dchInt.h @@ -21,6 +21,7 @@ #ifndef __DCH_INT_H__ #define __DCH_INT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,9 +34,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -100,7 +102,7 @@ struct Dch_Man_t_ static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } -static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; } +static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return (Aig_Obj_t *)pObj->pData; } static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) @@ -118,7 +120,6 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) //////////////////////////////////////////////////////////////////////// /*=== dchAig.c ===================================================*/ -extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); /*=== dchChoice.c ===================================================*/ extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ); extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ); @@ -155,9 +156,11 @@ extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig /*=== dchSweep.c ===================================================*/ extern void Dch_ManSweep( Dch_Man_t * p ); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index c8bd8533..dc856309 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -74,34 +77,34 @@ Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ) void Dch_ManPrintStats( Dch_Man_t * p ) { int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3; - printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", + Abc_Print( 1, "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); - printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", + Abc_Print( 1, "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", Aig_ManNodeNum(p->pAigTotal), Aig_ManNodeNum(p->pAigTotal)-nNodeNum, nNodeNum, 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) ); - printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", + Abc_Print( 1, "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", p->nSatVars, p->nConeMax, p->nRecycles ); - printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + Abc_Print( 1, "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, p->nSatCallsSat, p->nSatFailsReal ); - printf( "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", + Abc_Print( 1, "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", p->nLits, p->nReprs, p->nEquivs, p->nChoices ); - printf( "Choicing runtime statistics:\n" ); + Abc_Print( 1, "Choicing runtime statistics:\n" ); p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice; - ABC_PRTP( "Sim init ", p->timeSimInit, p->timeTotal ); - ABC_PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); - ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal ); - ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal ); - ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); - ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal ); - ABC_PRTP( "Choice ", p->timeChoice, p->timeTotal ); - ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); - ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + Abc_PrintTimeP( 1, "Sim init ", p->timeSimInit, p->timeTotal ); + Abc_PrintTimeP( 1, "Sim SAT ", p->timeSimSat, p->timeTotal ); + Abc_PrintTimeP( 1, "SAT solving", p->timeSat, p->timeTotal ); + Abc_PrintTimeP( 1, " sat ", p->timeSatSat, p->timeTotal ); + Abc_PrintTimeP( 1, " unsat ", p->timeSatUnsat, p->timeTotal ); + Abc_PrintTimeP( 1, " undecided", p->timeSatUndec, p->timeTotal ); + Abc_PrintTimeP( 1, "Choice ", p->timeChoice, p->timeTotal ); + Abc_PrintTimeP( 1, "Other ", p->timeOther, p->timeTotal ); + Abc_PrintTimeP( 1, "TOTAL ", p->timeTotal, p->timeTotal ); if ( p->pPars->timeSynth ) { - ABC_PRT( "Synthesis ", p->pPars->timeSynth ); + Abc_PrintTime( 1, "Synthesis ", p->pPars->timeSynth ); } } @@ -154,7 +157,7 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) { Aig_Obj_t * pObj; int i; - Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i ) Dch_ObjSetSatNum( p, pObj, 0 ); Vec_PtrClear( p->vUsedNodes ); // memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); @@ -184,3 +187,5 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index 6966e635..f5e346ef 100644 --- a/src/aig/dch/dchSat.c +++ b/src/aig/dch/dchSat.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -159,3 +162,5 @@ p->timeSatUndec += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c index 44a96970..b2d24761 100644 --- a/src/aig/dch/dchSim.c +++ b/src/aig/dch/dchSim.c @@ -20,13 +20,16 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj ) { - return Vec_PtrEntry( vSims, pObj->Id ); + return (unsigned *)Vec_PtrEntry( vSims, pObj->Id ); } static inline unsigned Dch_ObjRandomSim() { @@ -82,7 +85,7 @@ int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) ***********************************************************************/ unsigned Dch_NodeHash( void * p, Aig_Obj_t * pObj ) { - Vec_Ptr_t * vSims = p; + Vec_Ptr_t * vSims = (Vec_Ptr_t *)p; static int s_FPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, @@ -130,7 +133,7 @@ unsigned Dch_NodeHash( void * p, Aig_Obj_t * pObj ) ***********************************************************************/ int Dch_NodeIsConst( void * p, Aig_Obj_t * pObj ) { - Vec_Ptr_t * vSims = p; + Vec_Ptr_t * vSims = (Vec_Ptr_t *)p; unsigned * pSim; int k, nWords; nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); @@ -163,7 +166,7 @@ int Dch_NodeIsConst( void * p, Aig_Obj_t * pObj ) ***********************************************************************/ int Dch_NodesAreEqual( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { - Vec_Ptr_t * vSims = p; + Vec_Ptr_t * vSims = (Vec_Ptr_t *)p; unsigned * pSim0, * pSim1; int k, nWords; nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0); @@ -290,3 +293,5 @@ Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbo //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 4f31b928..325543d1 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -20,6 +20,9 @@ #include "dchInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -88,9 +91,9 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); Dch_ManCollectTfoCands_rec( p, pObj1 ); Dch_ManCollectTfoCands_rec( p, pObj2 ); - Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); - Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); - Vec_PtrForEachEntry( p->vSimClasses, pObj, i ) + Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease ); + Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i ) pObj->fMarkA = 0; } @@ -185,13 +188,13 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) Dch_ManResimulateSolved_rec( p, pRepr ); p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis ); // resimulate the cone of influence of the other nodes - Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i ) Dch_ManResimulateOther_rec( p, pRoot ); // refine these nodes RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 ); // resimulate the cone of influence of the cand classes RetValue2 = 0; - Vec_PtrForEachEntry( p->vSimClasses, pRoot, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i ) { ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize ); for ( k = 0; k < nSize; k++ ) @@ -235,7 +238,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) Dch_ManResimulateSolved_rec( p, pRepr ); p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis ); // resimulate the cone of influence of the other nodes - Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i ) Dch_ManResimulateOther_rec( p, pRoot ); // refine this class if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) ) @@ -251,3 +254,5 @@ p->timeSimSat += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c index afaf7426..4b054be2 100644 --- a/src/aig/dch/dchSweep.c +++ b/src/aig/dch/dchSweep.c @@ -21,6 +21,9 @@ #include "dchInt.h" #include "bar.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -139,3 +142,5 @@ void Dch_ManSweep( Dch_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3