Version abc90313

1 files changed, 189 insertions, 50 deletions

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index acdd3c13..b87c77e5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -30,6 +30,57 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if AIG is not in the required topo order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr;
+    if ( pObj->Value == 0 )
+        return 1;
+    pObj->Value = 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) )
+        return 0;
+    if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
+        return 0;
+    pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+    return pRepr == NULL || pRepr->Value == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if AIG is not in the required topo order.]
+
+  Description [AIG should be in such an order that the representative
+  is always traversed before the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckTopoOrder( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, RetValue = 1;
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Given representatives, derives pointers to the next objects.]
 
   Description []
@@ -192,18 +243,21 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
+static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     if ( fUseAll )
     {
         if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
             return NULL;
-    }
+    } 
     else
     {
         if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
             return NULL;
     }
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
+        return NULL;
     return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
 }
 
@@ -218,20 +272,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
+void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
+    if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
     {
-        Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll );
+        Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
         pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
 
@@ -246,12 +300,24 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pRepr;
     int i;
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     Gia_ManSetPhase( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
@@ -259,12 +325,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
     Gia_ManForEachCi( p, pObj, i )
     {
         pObj->Value = Gia_ManAppendCi(pNew);
-        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
+        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
             pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     }
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
+        Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
@@ -386,6 +452,52 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
 
 /**Function*************************************************************
 
+  Synopsis    [Removes pointers to the unmarked nodes..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr, iPrev;
+    pNew = Gia_ManDupDfs( p );
+    // start representatives
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
+    for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = iPrev = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+        {
+            Gia_ObjSetRepr( pNew, iNode, iRepr );
+            assert( iPrev < iNode );
+            iPrev = iNode;
+        }
+    }
+    Vec_IntFree( vClass );
+    pNew->pNexts = Gia_ManDeriveNexts( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reduces AIG while remapping equivalence classes.]
 
   Description [Drops the pairs of outputs if they are proved equivalent.]
@@ -398,7 +510,9 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
 {
     Gia_Man_t * pNew, * pFinal;
-    pNew = Gia_ManEquivReduce( p, 0 );
+    pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
+    if ( pNew == NULL )
+        return NULL;
     if ( fMiterPairs )
         Gia_ManEquivFixOutputPairs( pNew );
     if ( fSeq )
@@ -409,6 +523,8 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
     pFinal = Gia_ManDupMarked( pNew );
     Gia_ManEquivDeriveReprs( p, pNew, pFinal );
     Gia_ManStop( pNew );
+    pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
+    Gia_ManStop( pNew );
     return pFinal;
 }
 
@@ -448,25 +564,24 @@ int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
 int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
 {
     Gia_Obj_t * pObj;
-    int i, nNodes[2] = {0,0}, nDiffs[2];
+    int i, nNodes[2], nDiffs[2];
     assert( (Gia_ManPoNum(p) & 1) == 0 );
     Gia_ObjSetColors( p, 0 );
     Gia_ManForEachPi( p, pObj, i )
         Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
+    nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
     Gia_ManForEachPo( p, pObj, i )
         nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
 //    Gia_ManForEachObj( p, pObj, i )
 //        if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
 //            assert( Gia_ObjColors(p, i) );
-    nDiffs[0] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]);
-    nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]);
+    nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
+    nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
     if ( fVerbose )
     {
         printf( "CI+AND = %7d  A = %7d  B = %7d  Ad = %7d  Bd = %7d  AB = %7d.\n", 
-            Gia_ManCiNum(p) + Gia_ManAndNum(p), 
-            Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1], 
-            nDiffs[0], nDiffs[1], 
-            Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] );
+            Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1], 
+            Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
     }
     return (nDiffs[0] + nDiffs[1]) / 2;
 }
@@ -482,13 +597,16 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     unsigned iLitNew;
     pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
     if ( pRepr == NULL )
         return;
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+        return;
     iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
         Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
@@ -506,15 +624,15 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
 }
 
 /**Function*************************************************************
@@ -528,7 +646,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -539,9 +657,21 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
         printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
         return NULL;
     }
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -549,9 +679,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+        Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
+        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
     Vec_IntForEachEntry( vXorLits, iLitNew, i )
         Gia_ManAppendCo( pNew, iLitNew );
     if ( Vec_IntSize(vXorLits) == 0 )
@@ -570,12 +700,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
 }
 
 
-static inline int  Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
-static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
-
-static inline int  Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
-static inline int  Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
-
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG in the DFS order.]
@@ -587,17 +711,20 @@ static inline int  Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     int iLitNew;
     pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
     if ( pRepr == NULL )
         return;
-    iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-    if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
-        Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) );
-    Gia_ObjSetSpec( p, f, pObj, iLitNew );
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+        return;
+    iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+    if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+        Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
+    Gia_ObjSetCopyF( p, f, pObj, iLitNew );
 }
 
 /**Function*************************************************************
@@ -611,15 +738,15 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
 {
-    if ( ~Gia_ObjSpec(p, f, pObj) )
+    if ( ~Gia_ObjCopyF(p, f, pObj) )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
-    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f );
-    Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) );
-    Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
+    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
+    Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
+    Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
 }
 
 /**Function*************************************************************
@@ -654,31 +781,43 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
         return NULL;
     }
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, 0 );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
+        Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
     for ( f = 0; f < nFrames; f++ )
     {
-        Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 );
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
         Gia_ManForEachPi( p, pObj, i )
-            Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) );
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
         Gia_ManForEachRo( p, pObj, i )
-            Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+            Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
         Gia_ManForEachCo( p, pObj, i )
         {
-            Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
-            Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) );
+            Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
         }
         if ( f == nFrames - 1 )
             break;
         Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
-            Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) );
+            Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
     }
     Vec_IntForEachEntry( vXorLits, iLitNew, i )
         Gia_ManAppendCo( pNew, iLitNew );