summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h11
-rw-r--r--src/aig/aig/aigJust.c2
-rw-r--r--src/aig/dar/darCore.c6
-rw-r--r--src/aig/llb/llb1Group.c8
-rw-r--r--src/aig/llb/llb2Driver.c2
-rw-r--r--src/aig/llb/llb2Image.c2
-rw-r--r--src/aig/llb/llb4Nonlin.c2
-rw-r--r--src/aig/saig/saigAbsCba.c6
-rw-r--r--src/aig/saig/saigAbsPba.c6
-rw-r--r--src/aig/saig/saigCexMin.c30
-rw-r--r--src/aig/saig/saigDup.c2
-rw-r--r--src/aig/saig/saigRefSat.c6
12 files changed, 57 insertions, 26 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 655c0c99..a0216f37 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -419,20 +419,15 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over all objects, including those currently not used
#define Aig_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterator over the objects whose IDs are stored in an array
+#define Aig_ManForEachObjVec( vIds, p, pObj, i ) \
+ for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
// iterator over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
// iterator over all nodes
#define Aig_ManForEachExor( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
-// iterator over the nodes whose IDs are stored in the array
-#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \
- for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
-// iterator over the nodes in the topological order
-#define Aig_ManForEachNodeInOrder( p, pObj ) \
- for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
- p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
- p->iNext = p->pOrderData[2*p->iPrev+1] )
// these two procedures are only here for the use inside the iterator
static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; }
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index 87ea8f69..eca17d40 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -259,7 +259,7 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
pPack = Aig_ManPackStart( pAig );
vNodes = Aig_ManPackConstNodes( pPack );
// Aig_ManForEachPo( pAig, pObj, i )
- Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+ Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
{
if ( pObj->fPhase ) // const 1
{
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index a80277d5..6ca3082d 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -27,6 +27,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+// iterator over the nodes in the topological order
+#define Aig_ManForEachNodeInOrder( p, pObj ) \
+ for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
+ p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
+ p->iNext = p->pOrderData[2*p->iPrev+1] )
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb1Group.c b/src/aig/llb/llb1Group.c
index 4ebfc3a3..d865c239 100644
--- a/src/aig/llb/llb1Group.c
+++ b/src/aig/llb/llb1Group.c
@@ -318,19 +318,19 @@ Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec
// mark Cut1
Aig_ManIncrementTravId( pMan->pAig );
- Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+ Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
// collect unmarked Cut2
- Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+ Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
Vec_PtrPush( p->vOuts, pObj );
// mark nodes reachable from Cut2
Aig_ManIncrementTravId( pMan->pAig );
- Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+ Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
// collect marked Cut1
- Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+ Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
Vec_PtrPush( p->vIns, pObj );
diff --git a/src/aig/llb/llb2Driver.c b/src/aig/llb/llb2Driver.c
index 3b4f23fc..041a39d5 100644
--- a/src/aig/llb/llb2Driver.c
+++ b/src/aig/llb/llb2Driver.c
@@ -172,7 +172,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int Tim
bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes );
// mark the duplicated flop inputs
- Aig_ManForEachNodeVec( p, vVarsNs, pObj, i )
+ Aig_ManForEachObjVec( vVarsNs, p, pObj, i )
{
if ( !Saig_ObjIsLi(p, pObj) )
continue;
diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c
index caf8f9f7..5baa5c57 100644
--- a/src/aig/llb/llb2Image.c
+++ b/src/aig/llb/llb2Image.c
@@ -262,7 +262,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
int i, TimeStop;
TimeStop = dd->TimeStop; dd->TimeStop = 0;
bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd );
- Aig_ManForEachNodeVec( pAig, vNodeIds, pObj, i )
+ Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i )
{
bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 25ef8c96..69d741a5 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -340,7 +340,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
// mark internal nodes to be used
Aig_ManCleanMarkA( pAig );
vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
- Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+ Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
pObj->fMarkA = 1;
printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
*/
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 9d470164..66cf5586 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -337,7 +337,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
vRoots = Vec_VecEntryInt( vFrameCos, f );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManCbaUnrollCollect_rec( pAig, pObj,
Vec_VecEntryInt(vFrameObjs, f),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -355,7 +355,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
- Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+ Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -382,7 +382,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
break;
// transfer
vRoots = Vec_VecEntryInt( vFrameCos, f );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
{
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
if ( *pvReg2Frame )
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index f2a595f7..a22871b7 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -91,7 +91,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
Vec_IntPush( vRoots, Aig_ObjId(pObj) );
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManUnrollForPba_rec( pAig, pObj,
Vec_VecEntryInt( vFrameObjs, f ),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
- Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+ Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -132,7 +132,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
if ( f == nFrames - 1 )
break;
vRoots = Vec_VecEntryInt( vFrameCos, f );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
{
if ( Saig_ObjIsLi(pAig, pObj) )
{
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index ac397297..5dfcda01 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -321,6 +321,36 @@ Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
return pCexMin;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, int f, Vec_Int_t * vTemp )
+{
+ Vec_Int_t * vFrameCisOne;
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_IntClear( vTemp );
+ if ( f == Vec_VecSize(vFrameCis) - 1 )
+ {
+ pObj = Aig_ManPo( pAig, pCex->iPo );
+ Vec_IntPush( vTemp, Aig_ObjId(pObj) );
+ return;
+ }
+ vFrameCisOne = Vec_VecEntryInt( vFrameCis, f+1 );
+ Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+ if ( Saig_ObjIsLo(pAig, pObj) )
+ Vec_IntPush( vTemp, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 103cdf7b..fce6cf42 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs
assert( Vec_IntSize(vPairs) % 2 == 0 );
- Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
+ Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
{
pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index d117c643..b2ea80a6 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -287,7 +287,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
vRoots = Vec_VecEntryInt( vFrameCos, f );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManUnrollCollect_rec( pAig, pObj,
Vec_VecEntryInt(vFrameObjs, f),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -305,7 +305,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
- Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+ Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -332,7 +332,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
break;
// transfer
vRoots = Vec_VecEntryInt( vFrameCos, f );
- Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
}
// create output
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-24 12:47:36 +0000