summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h42
-rw-r--r--src/aig/aig/aigMan.c1
-rw-r--r--src/aig/aig/aigPartReg.c62
-rw-r--r--src/aig/bdc/bdcInt.h8
-rw-r--r--src/aig/dar/darCore.c3
-rw-r--r--src/aig/fra/fra.h1
-rw-r--r--src/aig/fra/fraHot.c43
-rw-r--r--src/aig/fra/fraInd.c10
-rw-r--r--src/aig/hop/hop.h8
-rw-r--r--src/aig/ivy/ivy.h8
-rw-r--r--src/aig/rwt/rwt.h8
11 files changed, 157 insertions, 37 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 744a044e..bd77c0a4 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -143,6 +143,7 @@ struct Aig_Man_t_
void * pSeqModel;
Aig_Man_t * pManHaig;
Aig_Man_t * pManExdc;
+ Vec_Ptr_t * vOnehots;
// timing statistics
int time1;
int time2;
@@ -241,28 +242,28 @@ static inline int Aig_WordFindFirstBit( unsigned uWord )
return -1;
}
-static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
-static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); }
-static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); }
-static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
-
-static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; }
-static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; }
-static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
-static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
-static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
-static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
+static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
+static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
+static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
+static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
+
+static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; }
+static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; }
+static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
+static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
+static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
+static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
-static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
-static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
-static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
-
-static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
-static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
-static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
-static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
-static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
+static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
+static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
+static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
+
+static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
+static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
+static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
+static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
+static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Aig_Obj_t * Aig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
@@ -529,6 +530,7 @@ extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSiz
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
+extern Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 57032703..12f2e702 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -329,6 +329,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
+ if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pObjCopies );
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 88ae66ee..3a008d12 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -230,6 +230,67 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
/**Function*************************************************************
+ Synopsis [Creates projection of 1-hot registers onto the given partition.]
+
+ Description [Assumes that the relevant register outputs are labeled with
+ the current traversal ID.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose )
+{
+ Vec_Ptr_t * vOnehotsPart = NULL;
+ Vec_Int_t * vGroup, * vGroupNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int nOffset, iReg, i, k;
+ // set the PI numbers
+ Aig_ManForEachPi( pPart, pObj, i )
+ pObj->iData = i;
+ // go through each group and check if registers are involved in this one
+ nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+ Vec_PtrForEachEntry( vOnehots, vGroup, i )
+ {
+ vGroupNew = NULL;
+ Vec_IntForEachEntry( vGroup, iReg, k )
+ {
+ pObj = Aig_ManPi( pAig, nOffset+iReg );
+ if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ continue;
+ if ( vGroupNew == NULL )
+ vGroupNew = Vec_IntAlloc( Vec_IntSize(vGroup) );
+ pObjNew = pObj->pData;
+ Vec_IntPush( vGroupNew, pObjNew->iData );
+ }
+ if ( vGroupNew == NULL )
+ continue;
+ if ( Vec_IntSize(vGroupNew) > 1 )
+ {
+ if ( vOnehotsPart == NULL )
+ vOnehotsPart = Vec_PtrAlloc( 100 );
+ Vec_PtrPush( vOnehotsPart, vGroupNew );
+ }
+ else
+ Vec_IntFree( vGroupNew );
+ }
+ // clear the PI numbers
+ Aig_ManForEachPi( pPart, pObj, i )
+ pObj->iData = 0;
+ // print out
+ if ( vOnehotsPart && fVerbose )
+ {
+ printf( "Partition contains %d groups of 1-hot registers: { ", Vec_PtrSize(vOnehotsPart) );
+ Vec_PtrForEachEntry( vOnehotsPart, vGroup, k )
+ printf( "%d ", Vec_IntSize(vGroup) );
+ printf( "}\n" );
+ }
+ return vOnehotsPart;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes partitioning of registers.]
Description []
@@ -292,6 +353,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
pObj = Aig_ManPi(pAig, nOffset+iOut);
pObj->pData = Aig_ObjCreatePi(pNew);
Aig_ObjCreatePo( pNew, pObj->pData );
+ Aig_ObjSetTravIdCurrent( pAig, pObj ); // added
}
// create the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index 9649f870..5f7b1186 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -110,10 +110,10 @@ struct Bdc_Man_t_
};
// working with complemented attributes of objects
-static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
-static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
+static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); }
static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 141d9b79..b13c7313 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -95,11 +95,11 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
// Aig_ManForEachNodeInOrder( pAig, pObj )
{
// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
-
// Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )
continue;
if ( i > nNodesOld )
+// if ( p->pPars->fUseZeros && i > nNodesOld )
break;
// consider freeing the cuts
@@ -109,6 +109,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
// compute cuts for the node
p->nNodesTried++;
clk = clock();
+ Dar_ObjSetCuts( pObj, NULL );
Dar_ObjComputeCuts_rec( p, pObj );
p->timeCuts += clock() - clk;
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index cc64b024..48588eb2 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -297,6 +297,7 @@ extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t *
extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
+extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 4a3f9b03..222f5bcc 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -420,6 +420,49 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
return pNew;
}
+
+/**Function*************************************************************
+
+ Synopsis [Assumes one-hot implications in the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+**********************************************************************/
+void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
+{
+ Vec_Int_t * vGroup;
+ Aig_Obj_t * pObj1, * pObj2;
+ int k, i, j, Out1, Out2, pLits[2];
+ //
+ // these constrants should be added to different timeframes!
+ // (also note that PIs follow first - then registers)
+ //
+ Vec_PtrForEachEntry( vOnehots, vGroup, k )
+ {
+ Vec_IntForEachEntry( vGroup, Out1, i )
+ Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
+ {
+ pObj1 = Aig_ManPi( p->pManFraig, Out1 );
+ pObj2 = Aig_ManPi( p->pManFraig, Out2 );
+ pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
+ pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
+ // add contraint to solver
+ if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
+ {
+ printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
+ sat_solver_delete( p->pSat );
+ p->pSat = NULL;
+ return;
+ }
+ }
+ }
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 0715524e..7e0d080c 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -253,6 +253,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
+ int clk = clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@@ -281,6 +282,9 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_PtrForEachEntry( vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+ // create the projection of 1-hot registers
+ if ( pAig->vOnehots )
+ pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
// run SSW
pNew = Fra_FraigInduction( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
@@ -299,6 +303,10 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
+ if ( fVerbose )
+ {
+ PRT( "Total time", clock() - clk );
+ }
return pNew;
}
@@ -485,6 +493,8 @@ p->timeTrav += clock() - clk2;
// add one-hotness clauses
if ( p->pPars->fUse1Hot )
Fra_OneHotAssume( p, p->vOneHots );
+// if ( p->pManAig->vOnehots )
+// Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
// report the intermediate results
if ( pPars->fVerbose )
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index af1d9cd3..6390ff70 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -124,10 +124,10 @@ static inline void Hop_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^=
static inline int Hop_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Hop_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
-static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) & ~01); }
-static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) ^ 01); }
-static inline Hop_Obj_t * Hop_NotCond( Hop_Obj_t * p, int c ) { return (Hop_Obj_t *)((unsigned long)(p) ^ (c)); }
-static inline int Hop_IsComplement( Hop_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
+static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
+static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
+static inline Hop_Obj_t * Hop_NotCond( Hop_Obj_t * p, int c ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
+static inline int Hop_IsComplement( Hop_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_Not(p->pConst1); }
static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; }
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index c7435a63..9832e061 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -186,10 +186,10 @@ static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i
static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
-static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) & ~01); }
-static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ 01); }
-static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c)); }
-static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
+static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
+static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
+static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
+static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); }
static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; }
diff --git a/src/aig/rwt/rwt.h b/src/aig/rwt/rwt.h
index 9199ff2a..56f66f34 100644
--- a/src/aig/rwt/rwt.h
+++ b/src/aig/rwt/rwt.h
@@ -112,10 +112,10 @@ struct Rwt_Node_t_ // 24 bytes
};
// manipulation of complemented attributes
-static inline int Rwt_IsComplement( Rwt_Node_t * p ) { return (int)(((unsigned long)p) & 01); }
-static inline Rwt_Node_t * Rwt_Regular( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) & ~01); }
-static inline Rwt_Node_t * Rwt_Not( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) ^ 01); }
-static inline Rwt_Node_t * Rwt_NotCond( Rwt_Node_t * p, int c ) { return (Rwt_Node_t *)((unsigned long)(p) ^ (c)); }
+static inline int Rwt_IsComplement( Rwt_Node_t * p ) { return (int)(((PORT_PTRUINT_T)p) & 01); }
+static inline Rwt_Node_t * Rwt_Regular( Rwt_Node_t * p ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) & ~01); }
+static inline Rwt_Node_t * Rwt_Not( Rwt_Node_t * p ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) ^ 01); }
+static inline Rwt_Node_t * Rwt_NotCond( Rwt_Node_t * p, int c ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:14:38 +0000