summaryrefslogtreecommitdiffstats
path: root/src/aig/dch
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dch')
-rw-r--r--src/aig/dch/dch.h20
-rw-r--r--src/aig/dch/dchAig.c15
-rw-r--r--src/aig/dch/dchChoice.c71
-rw-r--r--src/aig/dch/dchClass.c35
-rw-r--r--src/aig/dch/dchCnf.c15
-rw-r--r--src/aig/dch/dchCore.c23
-rw-r--r--src/aig/dch/dchInt.h19
-rw-r--r--src/aig/dch/dchMan.c39
-rw-r--r--src/aig/dch/dchSat.c5
-rw-r--r--src/aig/dch/dchSim.c13
-rw-r--r--src/aig/dch/dchSimSat.c17
-rw-r--r--src/aig/dch/dchSweep.c5
12 files changed, 207 insertions, 70 deletions
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 ///
////////////////////////////////////////////////////////////////////////
@@ -57,6 +60,22 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
/**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.]
Description [Takes several AIGs and performs choicing.]
@@ -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
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:20:50 +0000