Version abc90311

4 files changed, 295 insertions, 90 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 91507947..c5d55565 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -80,6 +80,7 @@ struct Gia_Cex_t_
     unsigned       pData[0];      // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
 };
 
+// new AIG manager
 typedef struct Gia_Man_t_ Gia_Man_t;
 struct Gia_Man_t_
 {
@@ -109,6 +110,7 @@ struct Gia_Man_t_
     int            nFansAlloc;    // the size of fanout representation
     int *          pMapping;      // mapping for each node
     Gia_Cex_t *    pCexComb;      // combinational counter-example
+    int *          pCopies;       // intermediate copies
 };
 
 
@@ -446,7 +448,7 @@ extern Gia_Man_t *         Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nL
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fXorOuts, int fComb, int fVerbose );
+extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset );
@@ -454,9 +456,11 @@ extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
+extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll );
 extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut );
+extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
 /*=== giaFanout.c =========================================================*/
 extern void                Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -526,7 +530,10 @@ extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );
 extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
-extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts );
+extern Gia_Cex_t *         Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
+extern void                Gia_ManPrintCounterExample( Gia_Cex_t * p );
+
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4821dba9..1d940b78 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -756,25 +756,12 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fComb, int fVerbose )
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i, iLit;
-    if ( fComb )
-    {
-        if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
-        {
-            printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
-            return NULL;
-        }
-        if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
-        {
-            printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
-            return NULL;
-        }
-    }
-    else
+    if ( fSeq )
     {
         if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) )
         {
@@ -792,6 +779,19 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
             return NULL;
         }
     }
+    else
+    {
+        if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
+        {
+            printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
+            return NULL;
+        }
+        if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
+        {
+            printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
+            return NULL;
+        }
+    }
     // start the manager
     pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
     pNew->pName = Aig_UtilStrsav( "miter" );
@@ -802,31 +802,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
     Gia_ManConst0(p1)->Value = 0;
     // map internal nodes and outputs
     Gia_ManHashAlloc( pNew );
-    if ( fComb )
-    {
-        // create combinational inputs
-        Gia_ManForEachCi( p0, pObj, i )
-            pObj->Value = Gia_ManAppendCi( pNew );
-        Gia_ManForEachCi( p1, pObj, i )
-            pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
-        // create combinational outputs
-        Gia_ManForEachCo( p0, pObj, i )
-        {
-            Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
-            Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
-            if ( fXorOuts )
-            {
-                iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
-                Gia_ManAppendCo( pNew, iLit );
-            }
-            else
-            {
-                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
-            }
-        }
-    }
-    else
+    if ( fSeq )
     {
         // create primary inputs
         Gia_ManForEachPi( p0, pObj, i )
@@ -843,15 +819,15 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
         {
             Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
             Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) );
-            if ( fXorOuts )
+            if ( fDualOut )
             {
-                iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
-                Gia_ManAppendCo( pNew, iLit );
+                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
             }
             else
             {
-                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+                iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+                Gia_ManAppendCo( pNew, iLit );
             }
         }
         // create register inputs
@@ -867,6 +843,30 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
         }
         Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) );
     }
+    else
+    {
+        // create combinational inputs
+        Gia_ManForEachCi( p0, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachCi( p1, pObj, i )
+            pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
+        // create combinational outputs
+        Gia_ManForEachCo( p0, pObj, i )
+        {
+            Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
+            Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
+            if ( fDualOut )
+            {
+                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+                Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+            }
+            else
+            {
+                iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+                Gia_ManAppendCo( pNew, iLit );
+            }
+        }
+    }
     Gia_ManHashStop( pNew );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 9e190da3..acdd3c13 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -156,13 +156,13 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
 ***********************************************************************/
 void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
 {
-    int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits;
+    int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
     for ( i = 1; i < Gia_ManObjNum(p); i++ )
     {
         if ( Gia_ObjIsHead(p, i) )
             Counter++;
         else if ( Gia_ObjIsConst(p, i) )
-            Counter1++;
+            Counter0++;
         else if ( Gia_ObjIsNone(p, i) )
             CounterX++;
         if ( Gia_ObjProved(p, i) )
@@ -170,8 +170,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     }
     CounterX -= Gia_ManCoNum(p);
     nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
-    printf( "cls =%7d  cst =%8d  lit =%8d  unused =%8d  proof =%6d  mem =%5.2f Mb\n", 
-        Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
+    printf( "cst =%8d  cls =%7d  lit =%8d  unused =%8d  proof =%6d  mem =%5.2f Mb\n", 
+        Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
@@ -192,10 +192,18 @@ 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 )
+static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
 {
-    if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
-        return NULL;
+    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;
+    }
     return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
 }
 
@@ -210,20 +218,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
 {
     Gia_Obj_t * pRepr;
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+    if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
     {
-        Gia_ManEquivReduce_rec( pNew, p, pRepr );
+        Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll );
         pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
 
@@ -238,7 +246,7 @@ 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 )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pRepr;
@@ -251,12 +259,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p )
     Gia_ManForEachCi( p, pObj, i )
     {
         pObj->Value = Gia_ManAppendCi(pNew);
-        if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
             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) );
+        Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
@@ -390,7 +398,7 @@ 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 );
+    pNew = Gia_ManEquivReduce( p, 0 );
     if ( fMiterPairs )
         Gia_ManEquivFixOutputPairs( pNew );
     if ( fSeq )
@@ -474,27 +482,43 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduce_rec( 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 )
 {
     Gia_Obj_t * pRepr;
-    int iLitNew;
-    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 );
-    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    unsigned iLitNew;
     pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
     if ( pRepr == NULL )
         return;
     iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-    if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+    if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
         Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
     pObj->Value = iLitNew;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+{
+    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 );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reduces AIG using equivalence classes.]
 
   Description []
@@ -504,33 +528,28 @@ 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 )
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
 {
     Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pRepr;
+    Gia_Obj_t * pObj;
     Vec_Int_t * vXorLits;
     int i, iLitNew;
     if ( !p->pReprs )
+    {
+        printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
         return NULL;
+    }
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
+    Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
-    Gia_ManFillValue( p );
+    Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
-    Gia_ManHashAlloc( pNew );
-    Gia_ManForEachCi( p, pObj, i )
-    {
-        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
-        if ( pRepr == NULL )
-            continue;
-        iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-        if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
-            Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
-        pObj->Value = iLitNew;
-    }
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
     Vec_IntForEachEntry( vXorLits, iLitNew, i )
@@ -542,14 +561,140 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p )
     }
     Gia_ManForEachRi( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Vec_IntFree( vXorLits );
     Gia_ManHashStop( pNew );
+    Vec_IntFree( vXorLits );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     return pNew;
 }
 
+
+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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+{
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+{
+    if ( ~Gia_ObjSpec(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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initialized SRM with the given number of frames.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    Vec_Int_t * vXorLits;
+    int f, i, iLitNew;
+    if ( !p->pReprs )
+    {
+        printf( "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
+        return NULL;
+    }
+    if ( Gia_ManRegNum(p) == 0 )
+    {
+        printf( "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
+        return NULL;
+    }
+    if ( Gia_ManRegNum(p) != pInit->nRegs )
+    {
+        printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\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 );
+    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) );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) );
+        Gia_ManForEachRo( p, pObj, i )
+            Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+        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) );
+        }
+        if ( f == nFrames - 1 )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) );
+    }
+    Vec_IntForEachEntry( vXorLits, iLitNew, i )
+        Gia_ManAppendCo( pNew, iLitNew );
+    if ( Vec_IntSize(vXorLits) == 0 )
+    {
+        printf( "Speculatively reduced model has no primary outputs.\n" );
+        Gia_ManAppendCo( pNew, 0 );
+    }
+    ABC_FREE( p->pCopies );
+    Vec_IntFree( vXorLits );
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Transforms equiv classes by removing the AB nodes.]
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index cc1a3861..822f1e64 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -580,6 +580,29 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
 
 /**Function*************************************************************
 
+  Synopsis    [Allocates a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+{
+    Gia_Cex_t * pCex;
+    int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+    pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
+    memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
+    pCex->nRegs  = nRegs;
+    pCex->nPis   = nRealPis;
+    pCex->nBits  = nRegs + nRealPis * nFrames;
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resimulates the counter-example.]
 
   Description []
@@ -589,7 +612,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts )
+int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut )
 {
     Gia_Obj_t * pObj, * pObjRi, * pObjRo;
     int RetValue, i, k, iBit = 0;
@@ -608,7 +631,7 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut
             pObjRo->fMark0 = pObjRi->fMark0;
     }
     assert( iBit == p->nBits );
-    if ( fDoubleOuts )
+    if ( fDualOut )
         RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
     else
         RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
@@ -616,6 +639,36 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints out the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintCounterExample( Gia_Cex_t * p )
+{
+    int i, f, k;
+    printf( "Counter-example: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d\n", 
+        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
+    printf( "State    : " );
+    for ( k = 0; k < p->nRegs; k++ )
+        printf( "%d", Aig_InfoHasBit(p->pData, k) );
+    printf( "\n" );
+    for ( f = 0; f <= p->iFrame; f++ )
+    {
+        printf( "Frame %2d : ", f );
+        for ( i = 0; i < p->nPis; i++ )
+            printf( "%d", Aig_InfoHasBit(p->pData, k++) );
+        printf( "\n" );
+    }
+    assert( k == p->nBits );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////