summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaDup.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaDup.c')
-rw-r--r--src/aig/gia/giaDup.c57
1 files changed, 49 insertions, 8 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 86d8039f..269c2215 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1192,7 +1192,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
/**Function*************************************************************
- Synopsis [Duplicates the AIG in the DFS order while rehashing.]
+ Synopsis [Cofactors w.r.t. a primary input variable.]
Description []
@@ -1201,16 +1201,16 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-void Gia_ManDupCofactor_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManDupCofactorVar_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
- Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
- Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
-Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
+Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@@ -1227,7 +1227,7 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
Gia_ManPi( p, iVar )->Value = Value; // modification!
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
@@ -1239,6 +1239,47 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
/**Function*************************************************************
+ Synopsis [Cofactors w.r.t. an internal node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, iObjValue = -1;
+ assert( Gia_ManRegNum(p) == 0 );
+ assert( iObj > 0 && iObj < Gia_ManObjNum(p) );
+ assert( Gia_ObjIsCand(Gia_ManObj(p, iObj)) );
+ assert( Value == 0 || Value == 1 );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), iObjValue) );
+ if ( i == iObj )
+ iObjValue = Abc_LitNotCond(pObj->Value, !Value), pObj->Value = Value;
+ }
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Existentially quantified given variable.]
Description []
@@ -1312,7 +1353,7 @@ Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
// first part
Gia_ManPi( p, iVar )->Value = 0; // modification!
Gia_ManForEachCo( p, pObj, i )
- Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
// second part
@@ -1320,7 +1361,7 @@ Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = ~0;
Gia_ManForEachCo( p, pObj, i )
- Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
// combination
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );