Version abc80518

abc.dsp

@@ -3245,6 +3245,26 @@ SOURCE=.\src\aig\mfx\mfxStrash.c
 SOURCE=.\src\aig\mfx\mfxWin.c
 # End Source File
 # End Group
+# Begin Group "bbr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrImage.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrReach.c
+# End Source File
+# End Group
 # Begin Group "saig"
 
 # PROP Default_Filter ""
@@ -3297,26 +3317,6 @@ SOURCE=.\src\aig\saig\saigScl.c
 SOURCE=.\src\aig\saig\saigTrans.c
 # End Source File
 # End Group
-# Begin Group "bbr"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbr.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrImage.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrNtbdd.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\bbr\bbrReach.c
-# End Source File
-# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"

src/aig/aig/aig.h

@@ -152,6 +152,7 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vOnehots;
     Aig_Man_t *      pManHaig;
     int              fCreatePios;
+    Vec_Int_t *      vEquPairs;      
     // timing statistics
     int              time1;
     int              time2;

src/aig/aig/aigDup.c

@@ -51,9 +51,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = p->nTruePos;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -90,6 +87,7 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // pass the HAIG manager
     if ( p->pManHaig != NULL )
     {
@@ -152,9 +150,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = p->nTruePos;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -184,6 +179,7 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // pass the HAIG manager
     if ( p->pManHaig != NULL )
     {
@@ -216,9 +212,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = p->nTruePos;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -256,6 +249,7 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     if ( (nNodes = Aig_ManCleanup( pNew )) )
         printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -292,7 +286,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
     pNew->fCatchExor = 1;
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -328,6 +321,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
         pObj->pData = pObjNew;
     }
     Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -394,7 +388,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -435,6 +428,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     assert( p->pEquivs != NULL || Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
         printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -541,7 +535,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -584,6 +577,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
 //    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
         printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -614,7 +608,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -658,6 +651,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
 //    if ( (nNodes = Aig_ManCleanup( pNew )) )
 //        printf( "Aig_ManDupLevelized(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -745,7 +739,6 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -766,6 +759,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
         else
             assert( 0 );
     }
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // check the new manager
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupRepres: Check has failed.\n" );
@@ -818,7 +812,6 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -839,6 +832,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
         else 
             assert( 0 );
     }
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // check the new manager
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupRepresDfs: Check has failed.\n" );

src/aig/aig/aigFrames.c

@@ -117,6 +117,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
             pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,fEnlarge?0:nFs-1) );
             Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
         }
+        Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
     }
     Aig_ManCleanup( pFrames );
     // return the new manager

src/aig/aig/aigObj.c

@@ -473,9 +473,10 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
 //        printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
 //            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
         assert( pObjNewR->pHaig != NULL );
-//        assert( pObjNewR->pHaig->pHaig == NULL );
         assert( !Aig_IsComplement(pObjNewR->pHaig) );
-        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+        assert( p->pManHaig->vEquPairs != NULL );
+        Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
+        Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
     }
     else
         pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;

src/aig/aig/aigRepr.c

@@ -270,7 +270,6 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -294,6 +293,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     // transfer the POs
     Aig_ManForEachPo( p, pObj, i )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Repr(p, pObj) );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // check the new manager
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupRepr: Check has failed.\n" );

src/aig/aig/aigRet.c

@@ -809,7 +809,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
 //        assert( Aig_Regular(pObjNew)->nRefs > 0 );
     }
     free( pLatches );
-    pNew->nRegs = nLatches;
+    Aig_ManSetRegNum( pNew, nLatches );
     // remove useless nodes
     Aig_ManCleanup( pNew );
     if ( !Aig_ManCheck( pNew ) )

src/aig/aig/aigScl.c

@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
     if ( p->vFlopNums )
@@ -101,6 +100,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     Aig_ManForEachPo( p, pObj, i )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManRemap(): The check has failed.\n" );

src/aig/dar/darBalance.c

@@ -359,9 +359,10 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
 //        printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
 //            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
         assert( pObjNewR->pHaig != NULL );
-//        assert( pObjNewR->pHaig->pHaig == NULL );
         assert( !Aig_IsComplement(pObjNewR->pHaig) );
-        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+        assert( pNew->pManHaig->vEquPairs != NULL );
+        Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
+        Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id );
     }
     else
         Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
@@ -390,7 +391,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -463,6 +463,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     Vec_VecFree( vStore );
     // remove dangling nodes
     Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // check the resulting AIG
     if ( !Aig_ManCheck(pNew) )
         printf( "Dar_ManBalance(): The check has failed.\n" );

src/aig/fra/fraSec.c

@@ -57,7 +57,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fVeryVerbose      =   0;  // enables very verbose reporting  
     p->TimeLimit         =   0;  // enables the timeout
     // internal parameters
-    p->fReportSolution   =   1;  // enables specialized format for reporting solution
+    p->fReportSolution   =   0;  // enables specialized format for reporting solution
 }
 
 /**Function*************************************************************

src/aig/ioa/ioaReadAig.c

@@ -104,7 +104,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     Vec_Int_t * vLits = NULL;
     Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
     Aig_Obj_t * pObj, * pNode0, * pNode1;
-    Aig_Man_t * pManNew;
+    Aig_Man_t * pNew;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
     char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
     unsigned uLit0, uLit1, uLit;
@@ -143,39 +143,39 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     }
 
     // allocate the empty AIG
-    pManNew = Aig_ManStart( nAnds );
+    pNew = Aig_ManStart( nAnds );
     pName = Ioa_FileNameGeneric( pFileName );
-    pManNew->pName = Aig_UtilStrsav( pName );
-//    pManNew->pSpec = Ioa_UtilStrsav( pFileName );
+    pNew->pName = Aig_UtilStrsav( pName );
+//    pNew->pSpec = Ioa_UtilStrsav( pFileName );
     free( pName );
 
     // prepare the array of nodes
     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
-    Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) );
+    Vec_PtrPush( vNodes, Aig_ManConst0(pNew) );
 
     // create the PIs
     for ( i = 0; i < nInputs + nLatches; i++ )
     {
-        pObj = Aig_ObjCreatePi(pManNew);    
+        pObj = Aig_ObjCreatePi(pNew);    
         Vec_PtrPush( vNodes, pObj );
     }
 /*
     // create the POs
     for ( i = 0; i < nOutputs + nLatches; i++ )
     {
-        pObj = Aig_ObjCreatePo(pManNew);   
+        pObj = Aig_ObjCreatePo(pNew);   
     }
 */
     // create the latches
-    pManNew->nRegs = nLatches;
+    pNew->nRegs = nLatches;
 /*
     nDigits = Ioa_Base10Log( nLatches );
     for ( i = 0; i < nLatches; i++ )
     {
-        pObj = Aig_ObjCreateLatch(pManNew);
+        pObj = Aig_ObjCreateLatch(pNew);
         Aig_LatchSetInit0( pObj );
-        pNode0 = Aig_ObjCreateBi(pManNew);
-        pNode1 = Aig_ObjCreateBo(pManNew);
+        pNode0 = Aig_ObjCreateBi(pNew);
+        pNode1 = Aig_ObjCreateBo(pNew);
         Aig_ObjAddFanin( pObj, pNode0 );
         Aig_ObjAddFanin( pNode1, pObj );
         Vec_PtrPush( vNodes, pNode1 );
@@ -211,7 +211,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
         pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
         pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
-        Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
+        Vec_PtrPush( vNodes, Aig_And(pNew, pNode0, pNode1) );
     }
 //    Bar_ProgressStop( pProgress );
 
@@ -259,9 +259,9 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
 
     // create the POs
     for ( i = 0; i < nOutputs; i++ )
-        Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
+        Aig_ObjCreatePo( pNew, Vec_PtrEntry(vDrivers, nLatches + i) );
     for ( i = 0; i < nLatches; i++ )
-        Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) );
+        Aig_ObjCreatePo( pNew, Vec_PtrEntry(vDrivers, i) );
     Vec_PtrFree( vDrivers );
 
 /*
@@ -275,11 +275,11 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
             // get the terminal type
             pType = pCur;
             if ( *pCur == 'i' )
-                vTerms = pManNew->vPis;
+                vTerms = pNew->vPis;
             else if ( *pCur == 'l' )
-                vTerms = pManNew->vBoxes;
+                vTerms = pNew->vBoxes;
             else if ( *pCur == 'o' )
-                vTerms = pManNew->vPos;
+                vTerms = pNew->vPos;
             else
             {
                 fprintf( stdout, "Wrong terminal type.\n" );
@@ -311,13 +311,13 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
         } 
 
         // assign the remaining names
-        Aig_ManForEachPi( pManNew, pObj, i )
+        Aig_ManForEachPi( pNew, pObj, i )
         {
             if ( pObj->pCopy ) continue;
             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
             Counter++;
         }
-        Aig_ManForEachLatchOutput( pManNew, pObj, i )
+        Aig_ManForEachLatchOutput( pNew, pObj, i )
         {
             if ( pObj->pCopy ) continue;
             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
@@ -325,7 +325,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
             Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
             Counter++;
         }
-        Aig_ManForEachPo( pManNew, pObj, i )
+        Aig_ManForEachPo( pNew, pObj, i )
         {
             if ( pObj->pCopy ) continue;
             Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
@@ -337,7 +337,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     else
     {
 //        printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
-        Aig_ManShortNames( pManNew );
+        Aig_ManShortNames( pNew );
     }
 */
 
@@ -346,16 +346,17 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     Vec_PtrFree( vNodes );
 
     // remove the extra nodes
-    Aig_ManCleanup( pManNew );
+    Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
 
     // check the result
-    if ( fCheck && !Aig_ManCheck( pManNew ) )
+    if ( fCheck && !Aig_ManCheck( pNew ) )
     {
         printf( "Ioa_ReadAiger: The network check has failed.\n" );
-        Aig_ManStop( pManNew );
+        Aig_ManStop( pNew );
         return NULL;
     }
-    return pManNew;
+    return pNew;
 }
 
 

src/aig/ntl/ntlExtract.c

@@ -715,7 +715,7 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
     pMiter = Aig_Miter(pAig, vPairs);
     Vec_PtrFree( vPairs );
     Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter  );
-    pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 );
+    Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) );
     Aig_ManCleanup( pAig );
     return pAig;    
 }

src/aig/ntl/ntlFraig.c

@@ -312,7 +312,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
-    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -346,7 +346,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
-    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
 
@@ -380,7 +380,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
-    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pTemp );
 
@@ -555,7 +555,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Aig_Man_t * pAigRed, * pAigCol;
     // collapse the AIG
     pAigCol = Ntl_ManCollapse( p, 1 );
-    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     // transform the collapsed AIG
     pAigRed = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pAigRed );

src/aig/saig/saig.h

@@ -80,7 +80,7 @@ extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigHaig.c ==========================================================*/
-extern void              Saig_ManHaigRecord( Aig_Man_t * p );
+extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
@@ -94,7 +94,7 @@ extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, in
 extern Aig_Man_t *       Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
 extern Aig_Man_t *       Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 /*=== saigRetStep.c ==========================================================*/
-extern void              Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
+extern int               Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs );
 /*=== saigScl.c ==========================================================*/
 extern void              Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
 /*=== saigTrans.c ==========================================================*/

src/aig/saig/saigHaig.c

@@ -43,17 +43,19 @@
 ***********************************************************************/
 void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
 {
-    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
+    Aig_Obj_t * pPo;
     // skip nodes without representative
     pObjRepr = pObj->pHaig;
     if ( pObjRepr == NULL )
         return;
-    assert( pObjRepr->Id < pObj->Id );
+//    assert( pObjRepr->Id < pObj->Id );
     // get the new node 
     pObjNew = pObj->pData;
     // get the new node of the representative
     pObjReprNew = pObjRepr->pData;
     // if this is the same node, no need to add constraints
+    assert( pObjNew != NULL && pObjReprNew != NULL );
     if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
         return;
     // these are different nodes - perform speculative reduction
@@ -61,10 +63,19 @@ void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
     // set the new node
     pObj->pData = pObjNew2;
     // add the constraint
-    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
-    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
-    assert( Aig_ObjPhaseReal(pMiter) == 1 );
-    Aig_ObjCreatePo( pFrames, pMiter );
+    if ( pObj->fMarkA )
+        return;
+//    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
+//    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+//    assert( Aig_ObjPhaseReal(pMiter) == 1 );
+//    Aig_ObjCreatePo( pFrames, pMiter );
+    if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
+        pObjReprNew = Aig_Not(pObjReprNew);
+    pPo = Aig_ObjCreatePo( pFrames, pObjNew );
+    Aig_ObjCreatePo( pFrames, pObjReprNew );
+
+    // remember the node corresponding to this PO
+    pPo->pData = pObj;
 }
 
 /**Function*************************************************************
@@ -98,27 +109,14 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
     Aig_ManSetPioNumbers( pHaig );
     for ( f = 0; f < nFrames; f++ )
     {
-        Aig_ManForEachObj( pHaig, pObj, i )
-        {
-            if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
-                continue;
-            if ( Saig_ObjIsPi(pHaig, pObj) )
-            {
-                pObj->pData = Aig_ObjCreatePi( pFrames );
-                continue;
-            }
-            if ( Saig_ObjIsLo(pHaig, pObj) )
-            {
-                Aig_ManHaigSpeculate( pFrames, pObj );
-                continue;
-            }
-            if ( Aig_ObjIsNode(pObj) )
-            {
-                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-                Aig_ManHaigSpeculate( pFrames, pObj );
-                continue;
-            }
-            assert( 0 );
+        // create primary inputs
+        Saig_ManForEachPi( pHaig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // create internal nodes
+        Aig_ManForEachNode( pHaig, pObj, i )
+        {        
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Aig_ManHaigSpeculate( pFrames, pObj );
         }
         if ( f == nFrames - 2 )
             nAssumptions = Aig_ManPoNum(pFrames);
@@ -148,76 +146,325 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
+{
+    Aig_Obj_t * pObj1, * pObj2;
+    int Id1, Id2, i, Counter = 0;
+    Aig_ManForEachObj( pHaig, pObj1, i )
+        pObj1->pHaig = NULL;
+    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
+    {
+        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+        pObj1 = Aig_ManObj( pHaig, Id1 );
+        pObj2 = Aig_ManObj( pHaig, Id2 );
+        assert( pObj1 != pObj2 );
+        assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
+        if ( Aig_ObjIsPi(pObj1) )
+        {
+            Counter += (int)(pObj2->pHaig != NULL);
+            pObj2->pHaig = pObj1;
+        }
+        else if ( Aig_ObjIsPi(pObj2) )
+        {
+            Counter += (int)(pObj1->pHaig != NULL);
+            pObj1->pHaig = pObj2;
+        }
+        else if ( pObj1->Id < pObj2->Id )
+        {
+            Counter += (int)(pObj2->pHaig != NULL);
+            pObj2->pHaig = pObj1;
+        }
+        else 
+        {
+            Counter += (int)(pObj1->pHaig != NULL);
+            pObj1->pHaig = pObj2;
+        }
+    }
+//    printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
+    return Counter;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManHaigVerifyComb( Aig_Man_t * pHaig )
 {
     int nBTLimit = 0;
+    Vec_Ptr_t * vResult;
     Aig_Man_t * pFrames;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
-    Aig_Obj_t * pObj;
-    int i, Lit, RetValue, Counter;
+    Aig_Obj_t * pObj1, * pObj2;
+    int i, RetValue, RetValue1, RetValue2, Counter, Lits[2];
     int clk = clock();
 
+    printf( "Filtering combinational cases:\n" );
+//    return;
+
     // create time frames with speculative reduction and convert them into CNF
 clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
-Aig_ManShow( pFrames, 0, NULL ); 
+    pFrames = Aig_ManHaigFrames( pHaig, 1 );
 
-    printf( "AIG:    " );
-    Aig_ManPrintStats( pAig );
-    printf( "HAIG:   " );
-    Aig_ManPrintStats( pHaig );
-    printf( "Frames: " );
+    // collect the HAIG nodes that were used to create spec miters
+    vResult = Vec_PtrAlloc( Aig_ManPoNum(pFrames)/2 );
+    Aig_ManForEachPo( pFrames, pObj1, i )
+    {
+        pObj2 = Aig_ManPo( pFrames, ++i );
+        Vec_PtrPush( vResult, pObj1->pData );
+    }
+
+    printf( "Frames:     " );
     Aig_ManPrintStats( pFrames );
-    printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n", 
-        Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
-    pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
-PRT( "Preparation", clock() - clk );
+
+//    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
+//    Aig_ManStop( pTemp );
+
+    printf( "Frames:     " );
+    Aig_ManPrintStats( pFrames );
+
+    printf( "Additional frames stats: Assumptions = %d. Asserts = %d. Pairs = %d.\n", 
+        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2 );
+//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
 
 //    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
-    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+//    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+//    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
     // create the SAT solver to be used for this problem
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     if ( pSat == NULL )
     {
         printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return -1;
+        return;
     }
-    
-    // solve each output
+PRT( "Preparation", clock() - clk );
+
+
+    // check in the second timeframe
 clk = clock();
-    if ( pFrames->nAsserts == 0 )
+    Counter = 0;
+    printf( "Started solving ...\r" );
+    Aig_ManForEachPo( pFrames, pObj1, i )
     {
-        RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-        if ( RetValue != l_False )
-            printf( "SAT solver is wrong\n" );
+        pObj2 = Aig_ManPo( pFrames, ++i );
+        assert( pObj1->fPhase == pObj2->fPhase );
+
+        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+
+        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue1 == l_False )
+        {
+            Lits[0] = lit_neg( Lits[0] );
+            Lits[1] = lit_neg( Lits[1] );
+            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+            assert( RetValue );
+        }
+
+        Lits[0]++;
+        Lits[1]--;
+
+        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue2 == l_False )
+        {
+            Lits[0] = lit_neg( Lits[0] );
+            Lits[1] = lit_neg( Lits[1] );
+            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+            assert( RetValue );
+        }
+
+        if ( RetValue1 != l_False || RetValue2 != l_False )
+        {
+            Counter++;
+        }
+        else
+        {
+            pObj1 = Vec_PtrEntry( vResult, i/2 );
+            assert( pObj1->pHaig != NULL );
+            pObj1->fMarkA = 1;
+        }
+        
+        if ( i % 50 == 1 )
+            printf( "Solving assertion %6d out of %6d.\r", 
+                (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2, 
+                pFrames->nAsserts/2 );
+//        if ( nClasses == 1000 )
+//            break;
     }
+    printf( "                                                          \r" );
+PRT( "Solving    ", clock() - clk );
+    if ( Counter )
+        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
     else
+        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
+
+    // clean up
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    Vec_PtrFree( vResult );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+    int nBTLimit = 0;
+    Aig_Man_t * pFrames, * pTemp;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj1, * pObj2;
+    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
+    int clk = clock();
+
+    nOvers = Aig_ManMapHaigNodes( pHaig );
+
+//    if ( nFrames == 2 )
+//        Aig_ManHaigVerifyComb( pHaig );
+
+    // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+    Aig_ManCleanMarkA( pHaig );
+
+    printf( "Frames:     " );
+    Aig_ManPrintStats( pFrames );
+
+    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
+    Aig_ManStop( pTemp );
+
+    printf( "Frames synt:" );
+    Aig_ManPrintStats( pFrames );
+
+    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
+        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
+//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
+
+//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+//    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+//    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
     {
-        Counter = 0;
-        Aig_ManForEachPo( pFrames, pObj, i )
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return 0;
+    }
+
+    if ( nFrames == 2 )
+    {
+        // add clauses for the first frame
+        Aig_ManForEachPo( pFrames, pObj1, i )
         {
-            if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
-                continue;
-            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
-            RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( RetValue != l_False )
-                Counter++;
+            if ( i >= Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+                break;
+
+            pObj2 = Aig_ManPo( pFrames, ++i );
+            assert( pObj1->fPhase == pObj2->fPhase );
+
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+            {
+                sat_solver_delete( pSat );
+                return 0;
+            }
+            Lits[0]++;
+            Lits[1]--;
+            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+            {
+                sat_solver_delete( pSat );
+                return 0;
+            }
         }
-PRT( "Solving    ", clock() - clk );
-        if ( Counter )
-            printf( "Verification failed for %d classes.\n", Counter );
-        else
-            printf( "Verification is successful.\n" );
+
+        if ( !sat_solver_simplify(pSat) )
+        {
+            sat_solver_delete( pSat );
+            return 0;
+        }
+    }
+PRT( "Preparation", clock() - clk );
+
+
+    // check in the second timeframe
+clk = clock();
+    Counter = 0;
+    printf( "Started solving ...\r" );
+    Aig_ManForEachPo( pFrames, pObj1, i )
+    {
+        if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+            continue;
+
+        pObj2 = Aig_ManPo( pFrames, ++i );
+        assert( pObj1->fPhase == pObj2->fPhase );
+
+        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
+
+        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue1 == l_False )
+        {
+            Lits[0] = lit_neg( Lits[0] );
+            Lits[1] = lit_neg( Lits[1] );
+//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+//            assert( RetValue );
+        }
+
+        Lits[0]++;
+        Lits[1]--;
+
+        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue2 == l_False )
+        {
+            Lits[0] = lit_neg( Lits[0] );
+            Lits[1] = lit_neg( Lits[1] );
+//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
+//            assert( RetValue );
+        }
+
+        if ( RetValue1 != l_False || RetValue2 != l_False )
+            Counter++;
+
+        if ( i % 50 == 1 )
+            printf( "Solving assertion %6d out of %6d.\r", 
+                (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2, 
+                pFrames->nAsserts/2 );
+//        if ( nClasses == 1000 )
+//            break;
     }
+    printf( "                                                          \r" );
+PRT( "Solving    ", clock() - clk );
+    if ( Counter )
+        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
+    else
+        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
 
     // clean up
     Aig_ManStop( pFrames );
     Cnf_DataFree( pCnf );
     sat_solver_delete( pSat );
-    return Counter;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -231,22 +478,28 @@ PRT( "Solving    ", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
 {
     int nBTLimit = 0;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
-    Aig_Obj_t * pObj, * pRepr;
-    int i, RetValue, Counter, Lits[2];
-    int nClasses = 0;
+    Aig_Obj_t * pObj1, * pObj2;
+    int i, RetValue1, RetValue2, Counter, Lits[2];
     int clk = clock();
+    int Delta;
+    int Id1, Id2;
 
     assert( nFrames == 1 || nFrames == 2 );
 
 clk = clock();
     pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
+//    Aig_ManForEachObj( pHaig, pObj, i )
+//        printf( "%d=%d  ", pObj->Id, pCnf->pVarNums[pObj->Id] );
+//    printf( "\n" );
+
     // create the SAT solver to be used for this problem
     pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
     if ( pSat == NULL )
     {
         printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
@@ -255,16 +508,15 @@ clk = clock();
 
     if ( nFrames == 2 )
     {
-        // add clauses for the first frame
-        Aig_ManForEachObj( pHaig, pObj, i )
+        Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
         {
-            pRepr = pObj->pHaig;
-            if ( pRepr == NULL )
-                continue;
-            if ( pRepr->fPhase ^ pObj->fPhase )
+            Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+            pObj1 = Aig_ManObj( pHaig, Id1 );
+            pObj2 = Aig_ManObj( pHaig, Id2 );
+            if ( pObj1->fPhase ^ pObj2->fPhase )
             {
-                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
                 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                 {
                     sat_solver_delete( pSat );
@@ -280,8 +532,8 @@ clk = clock();
             }
             else
             {
-                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
                 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                 {
                     sat_solver_delete( pSat );
@@ -297,12 +549,10 @@ clk = clock();
             }
         }
 
-        // add clauses for the next timeframe
-        { 
-            int nLitsAll = 2 * pCnf->nVars;
-            int * pLits = pCnf->pClauses[0];
-            for ( i = 0; i < pCnf->nLiterals; i++ )
-                pLits[i] += nLitsAll;
+        if ( !sat_solver_simplify(pSat) )
+        {
+            sat_solver_delete( pSat );
+            return 0;
         }
     }
 PRT( "Preparation", clock() - clk );
@@ -311,51 +561,53 @@ PRT( "Preparation", clock() - clk );
     // check in the second timeframe
 clk = clock();
     Counter = 0;
-    nClasses = 0;
-    Aig_ManForEachObj( pHaig, pObj, i )
+    Delta = (nFrames == 2)? pCnf->nVars : 0;
+    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
     {
-        pRepr = pObj->pHaig;
-        if ( pRepr == NULL )
-            continue;
-        nClasses++;
-        if ( pRepr->fPhase ^ pObj->fPhase )
+        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+        pObj1 = Aig_ManObj( pHaig, Id1 );
+        pObj2 = Aig_ManObj( pHaig, Id2 );
+        if ( pObj1->fPhase ^ pObj2->fPhase )
         {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
 
-            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( RetValue != l_False )
-                Counter++;
+            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
 
             Lits[0]++;
             Lits[1]++;
 
-            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( RetValue != l_False )
+            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+
+            if ( RetValue1 != l_False || RetValue2 != l_False )
                 Counter++;
         }
         else
         {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
 
-            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( RetValue != l_False )
-                Counter++;
+            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
 
             Lits[0]++;
             Lits[1]--;
 
-            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( RetValue != l_False )
+            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+
+            if ( RetValue1 != l_False || RetValue2 != l_False )
                 Counter++;
         }
+        if ( i % 50 == 1 )
+            printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
+
+//        if ( i / 2 > 1000 )
+//            break;
     }
 PRT( "Solving    ", clock() - clk );
     if ( Counter )
-        printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
+        printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
     else
-        printf( "Verification is successful for all %d classes.\n", nClasses );
+        printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
 
     Cnf_DataFree( pCnf );
     sat_solver_delete( pSat );
@@ -373,96 +625,174 @@ PRT( "Solving    ", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManHaigRecord( Aig_Man_t * p )
+Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
+{
+    Vec_Ptr_t * vTemp;
+    Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
+    int Id1, Id2, i;
+    // remove regular POs
+    Aig_ManSetPioNumbers( pHaig );
+    vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
+    Aig_ManForEachPo( pHaig, pObj, i )
+    {
+        if ( Saig_ObjIsPo(pHaig, pObj) )
+        {
+            Aig_ObjDisconnect( pHaig, pObj );
+            Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
+        }
+        else
+        {
+            Vec_PtrPush( vTemp, pObj );
+        }
+    }
+    Vec_PtrShrink( pHaig->vPos, 0 ); 
+    pHaig->nObjs[AIG_OBJ_PO] = Vec_PtrSize( vTemp );
+    // add new POs
+    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
+    {
+        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
+        pObj1 = Aig_ManObj( pHaig, Id1 );
+        pObj2 = Aig_ManObj( pHaig, Id2 );
+        assert( pObj1 != pObj2 );
+        assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
+        pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
+        pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
+        assert( Aig_ObjPhaseReal(pMiter) == 0 );
+        Aig_ObjCreatePo( pHaig, pMiter );
+    }
+    printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
+    // add the registers
+    Vec_PtrForEachEntry( vTemp, pObj, i )
+        Vec_PtrPush( pHaig->vPos, pObj );
+    Vec_PtrFree( vTemp );
+    assert( pHaig->nObjs[AIG_OBJ_PO] ==  Vec_PtrSize(pHaig->vPos) ); 
+    Aig_ManCleanup( pHaig );
+    Aig_ManSetRegNum( pHaig, pHaig->nRegs );
+//    return pHaig;
+
+    printf( "HAIG:       " );
+    Aig_ManPrintStats( pHaig );
+    printf( "HAIG is written into file \"haig.blif\".\n" );
+    Saig_ManDumpBlif( pHaig, "haig.blif" );
+
+    Vec_IntFree( pHaig->vEquPairs );
+    Aig_ManStop( pHaig );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
 {
-    extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
-    int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
+    int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Aig_Man_t * pNew, * pTemp;
     Aig_Obj_t * pObj;
-    int i;
+    int i, k, nStepsReal, clk = clock();
     Dar_ManDefaultRwrParams( pParsRwr );
+
+clk = clock();
     // duplicate this manager
     pNew = Aig_ManDupSimple( p );
-
     // create its history AIG
     pNew->pManHaig = Aig_ManDupSimple( pNew );
     Aig_ManForEachObj( pNew, pObj, i )
         pObj->pHaig = pObj->pData;
     // remove structural hashing table
     Aig_TableClear( pNew->pManHaig );
+    pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
+PRT( "HAIG setup time", clock() - clk );
 
-    // perform retiming
-    if ( fUseRetiming )
+clk = clock();
+    if ( fSeqHaig )
     {
-/*
-        // perform balancing
-        pNew = Dar_ManBalance( pTemp = pNew, 0 );
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-
-        // perform rewriting
-        Dar_ManRewrite( pNew, pParsRwr );
-        pNew = Aig_ManDupDfs( pTemp = pNew ); 
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-*/
-        // perform retiming
-        Saig_ManRetimeSteps( pNew, 1000, 1 ); 
-        pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-
-        // perform balancing
-        pNew = Dar_ManBalance( pTemp = pNew, 0 );
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-
-        // perform rewriting
-        Dar_ManRewrite( pNew, pParsRwr );
-        pNew = Aig_ManDupDfs( pTemp = pNew ); 
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
+        if ( fRetimingOnly )
+        {
+            // perform retiming
+            nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
+            pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
+            Aig_ManStop( pTemp );
+            printf( "Performed %d retiming moves.\n", nStepsReal );
+        }
+        else
+        {
+            for ( k = 0; k < nIters; k++ )
+            {
+                // perform balancing
+                pNew = Dar_ManBalance( pTemp = pNew, 0 );
+                Aig_ManStop( pTemp );
+
+                // perform rewriting
+                Dar_ManRewrite( pNew, pParsRwr );
+                pNew = Aig_ManDupDfs( pTemp = pNew ); 
+                Aig_ManStop( pTemp );
+
+                // perform retiming
+                nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
+                pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
+                Aig_ManStop( pTemp );
+                printf( "Performed %d retiming moves.\n", nStepsReal );
+            }
+        }
     }
     else
     {
-        // perform balancing
-        pNew = Dar_ManBalance( pTemp = pNew, 0 );
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-/*
-        // perform rewriting
-        Dar_ManRewrite( pNew, pParsRwr );
-        pNew = Aig_ManDupDfs( pTemp = pNew ); 
-        assert( pNew->pManHaig != NULL );
-        assert( pTemp->pManHaig == NULL );
-        Aig_ManStop( pTemp );
-*/
+        for ( k = 0; k < nIters; k++ )
+        {
+            // perform balancing
+            pNew = Dar_ManBalance( pTemp = pNew, 0 );
+            Aig_ManStop( pTemp );
+
+            // perform rewriting
+            Dar_ManRewrite( pNew, pParsRwr );
+            pNew = Aig_ManDupDfs( pTemp = pNew ); 
+            Aig_ManStop( pTemp );
+        }
     } 
+PRT( "Synthesis time ", clock() - clk );
 
     // use the haig for verification
-    Aig_ManAntiCleanup( pNew->pManHaig );
+//    Aig_ManAntiCleanup( pNew->pManHaig );
     Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
 //Aig_ManShow( pNew->pManHaig, 0, NULL ); 
 
-    printf( "AIG:    " );
+    printf( "AIG before: " );
+    Aig_ManPrintStats( p );
+    printf( "AIG after:  " );
     Aig_ManPrintStats( pNew );
-    printf( "HAIG:   " );
+    printf( "HAIG:       " );
     Aig_ManPrintStats( pNew->pManHaig );
 
-    if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
-        printf( "Constructing SAT solver has failed.\n" );         
+    if ( fUseCnf )
+    {
+        if ( !Aig_ManHaigVerify2( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+            printf( "Constructing SAT solver has failed.\n" );         
+    }
+    else
+    {
+        if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+            printf( "Constructing SAT solver has failed.\n" );         
+    }
 
+    Saig_ManHaigDump( pNew->pManHaig );
+    pNew->pManHaig = NULL;
+    return pNew;
+/*
     // cleanup
+    Vec_IntFree( pNew->pManHaig->vEquPairs );
     Aig_ManStop( pNew->pManHaig );
     pNew->pManHaig = NULL;
-    Aig_ManStop( pNew );
+    return pNew;
+*/
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/saig/saigRetStep.c

@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
+Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug )
 {
     Aig_Obj_t * pFanin0, * pFanin1;
     Aig_Obj_t * pInput0, * pInput1;
@@ -72,6 +72,12 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
     // get the condition when the register should be complemetned
     fCompl = Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj);
 
+    if ( fMakeBug )
+    {
+        printf( "Introducing bug during retiming.\n" );
+        pInput1 = Aig_Not( pInput1 );
+    }
+
     // create new node
     pObjNew = Aig_And( p, pInput0, pInput1 );
 
@@ -162,7 +168,7 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
+int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
 {
     Aig_Obj_t * pObj, * pObjNew;
     int RetValue, s, i;
@@ -175,12 +181,15 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
         {
             Aig_ManForEachNode( p, pObj, i )
             {
-                pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
+                pObjNew = Saig_ManRetimeNodeFwd( p, pObj, fAddBugs && (s == 10) );
+//                pObjNew = Saig_ManRetimeNodeFwd( p, pObj, 0 );
                 if ( pObjNew == NULL )
                     continue;
                 Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
+            if ( i == Vec_PtrSize(p->vObjs) )
+                break;
         }
     }
     else
@@ -195,6 +204,8 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
                 Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
+            if ( i == Vec_PtrSize(p->vObjs) )
+                break;
         }
     }
     p->fCreatePios = 0;
@@ -202,6 +213,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
     RetValue = Aig_ManCleanup( p );
     assert( RetValue == 0 );
     Aig_ManSetRegNum( p, p->nRegs ); 
+    return s;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -149,9 +149,9 @@ static int Abc_CommandFraigClean     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandFraigSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigDress     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-static int Abc_CommandHaigStart      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaigStop       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaigUse        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigStart      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigStop       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaigUse        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRecStart       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecStop        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -404,9 +404,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "dress",         Abc_CommandFraigDress,       1 );
 
-    Cmd_CommandAdd( pAbc, "Choicing",     "haig_start",    Abc_CommandHaigStart,        0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_start",    Abc_CommandHaigStart,        0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
 
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
@@ -7505,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
@@ -7519,13 +7519,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-//    printf( "This command is temporarily disabled.\n" );
-//    return 0;
+    printf( "This command is temporarily disabled.\n" );
+    return 0;
 
     // set defaults
     fVeryVerbose = 0;
     fVerbose = 1;
-    fBmc     = 1;
+    fBmc     = 0;
     nFrames  = 1;
     nLevels  = 200;
     Extra_UtilGetoptReset();
@@ -7685,7 +7685,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 
-//    Abc_NtkDarHaigRecord( pNtk );
 //    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
 /*
     if ( globalUtilOptind != 1 )
@@ -7699,11 +7698,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_NtkDarPartition( pNtk );
 //Abc_NtkDarTest( pNtk );
 
-
-Abc_NtkDarHaigRecord( pNtk );
-return 0;
-
-    pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
+//    pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
+    pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -7713,7 +7709,7 @@ return 0;
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 usage:
-    fprintf( pErr, "usage: test [-vwh]\n" );
+    fprintf( pErr, "usage: test [-bvwh]\n" );
     fprintf( pErr, "\t         testbench for new procedures\n" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -9398,19 +9394,29 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUseZeroCost, fVerbose, nIters;
-    extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
+    int c;
+    int nIters;
+    int nSteps;
+    int fRetimingOnly;
+    int fAddBugs;
+    int fUseCnf;
+    int fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nIters       = 2;
-    fUseZeroCost = 0;
-    fVerbose     = 1;
+    nIters        = 3;
+    nSteps        = 3000;
+    fRetimingOnly = 0;
+    fAddBugs      = 0;
+    fUseCnf       = 0;
+    fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ISrbcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9425,11 +9431,28 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nIters < 0 ) 
                 goto usage;
             break;
-        case 'z':
-            fUseZeroCost ^= 1;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nSteps = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSteps < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRetimingOnly ^= 1;
+            break;
+        case 'b':
+            fAddBugs ^= 1;
+            break;
+        case 'c':
+            fUseCnf ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            fUseCnf ^= 1;
             break;
         case 'h':
             goto usage;
@@ -9448,7 +9471,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
+    pNtkRes = Abc_NtkDarHaigRecord( pNtk, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -9459,10 +9482,17 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: haig [-Izvh]\n" );
-    fprintf( pErr, "\t         prints HAIG stats after sequential rewriting\n" );
-    fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
-    fprintf( pErr, "\t-z     : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
+    fprintf( pErr, "usage: haig [-IS num] [-rbcvh]\n" );
+    fprintf( pErr, "\t         run a few rounds of comb+seq synthesis to test HAIG recording\n" );
+    fprintf( pErr, "\t         the current network is set to be the result of synthesis performed\n" );
+    fprintf( pErr, "\t         (this network can be verified using command \"dsec\")\n" );
+    fprintf( pErr, "\t         HAIG is written out into the file \"haig.blif\"\n" );
+    fprintf( pErr, "\t         (this HAIG can be proved using \"r haig.blif; st; dprove -abc -F 16\")\n" );
+    fprintf( pErr, "\t-I num : the number of rounds of comb+seq synthesis [default = %d]\n", nIters );
+    fprintf( pErr, "\t-S num : the number of forward retiming moves performed [default = %d]\n", nSteps );
+    fprintf( pErr, "\t-r     : toggle the use of retiming only [default = %s]\n", fRetimingOnly? "yes": "no" );
+    fprintf( pErr, "\t-b     : toggle bug insertion [default = %s]\n", fAddBugs? "yes": "no" );
+    fprintf( pErr, "\t-c     : enable CNF-based proof (no speculative reduction) [default = %s]\n", fUseCnf? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;

src/base/abci/abcDar.c

@@ -1655,7 +1655,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
     pMan->vFlopNums = NULL;
 
     Aig_ManPrintStats(pMan);
-    Saig_ManRetimeSteps( pMan, 1000, 1 );
+    Saig_ManRetimeSteps( pMan, 1000, 1, 0 );
     Aig_ManPrintStats(pMan);
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -1674,18 +1674,23 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
 {
-    Aig_Man_t * pMan;
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
-        return;
+        return NULL;
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    Saig_ManHaigRecord( pMan );
+    pMan = Saig_ManHaigRecord( pTemp = pMan, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
+    Aig_ManStop( pTemp );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
+    return pNtkAig;
 }
 
 /**Function*************************************************************