initial commit of public abc

1 files changed, 465 insertions, 123 deletions

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dbe98631..31ef986c 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "main.h"
 #include "giaAig.h"
 #include "saig.h"
 #include "dar.h"
@@ -29,11 +30,14 @@
 #include "dch.h"
 #include "ssw.h"
 #include "cgt.h"
-//#include "fsim.h"
+#include "bbr.h"
 #include "gia.h"
 #include "cec.h"
+#include "csw.h"
 #include "giaAbs.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -100,6 +104,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->fCatchExor = fExors;
+    pMan->nConstrs = pNtk->nConstrs;
 
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     // transfer the pointers to the basic nodes
@@ -174,6 +179,7 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
+    pMan->nConstrs = pNtk->nConstrs;
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
@@ -184,13 +190,13 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
     // perform the conversion of the internal nodes (assumes DFS ordering)
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
     {
         pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
 //        printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
         if ( Abc_AigNodeIsChoice( pObj ) )
         {
-            for ( pPrev = pObj, pFanin = pObj->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+            for ( pPrev = pObj, pFanin = (Abc_Obj_t *)pObj->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
                 Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
 //            Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
         }
@@ -232,17 +238,18 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 //    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // transfer the pointers to the basic nodes
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         else
-            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
@@ -287,6 +294,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 //    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // consider the case of target enlargement
     if ( Abc_NtkCiNum(pNtkNew) < Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) )
     {
@@ -309,17 +317,17 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
         pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
         pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
-        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
-        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
     }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         else
-            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
@@ -412,6 +420,7 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
     assert( pMan->nAsserts == 0 );
     // perform strashing
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // duplicate the name and the spec
 //    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
 //    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -438,19 +447,19 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
         pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
         pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
-        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
-        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
-        Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjLi->pData), NULL );
-        Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjLo->pData), NULL );
+        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
+        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
     }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         else
-            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
@@ -490,6 +499,7 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
     assert( pMan->vCiNumsOrig != NULL );
     // perform strashing
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // duplicate the name and the spec
 //    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
 //    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -520,23 +530,23 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
         pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
         pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
-        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
-        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
+        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
         // find the name
         pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
-        Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjOld), NULL );
+        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName(pObjOld), NULL );
         // find the name
         pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
-        Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjOld), NULL );
+        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName(pObjOld), NULL );
     }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         else
-            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
@@ -546,7 +556,7 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
     }
     // check the resulting AIG
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkAfterTrim(): Network check has failed.\n" );
     return pNtkNew;
 }
 
@@ -571,6 +581,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     assert( Aig_ManBufNum(pMan) == 0 );
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // transfer the pointers to the basic nodes
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
@@ -578,15 +589,15 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
     // rebuild the AIG
     vNodes = Aig_ManDfsChoices( pMan );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
-        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+        pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
         if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
         {
             Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
-            pAbcRepr = pObj->pData;
-            pAbcObj  = pTemp->pData;
+            pAbcRepr = (Abc_Obj_t *)pObj->pData;
+            pAbcObj  = (Abc_Obj_t *)pTemp->pData;
             pAbcObj->pData  = pAbcRepr->pData;
             pAbcRepr->pData = pAbcObj;
         }
@@ -622,6 +633,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 //    assert( Aig_ManLatchNum(pMan) > 0 );
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew->nConstrs = pMan->nConstrs;
     // transfer the pointers to the basic nodes
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
@@ -640,7 +652,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Abc_NtkAddDummyBoxNames( pNtkNew );
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         // add the first fanin
         pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -650,9 +662,9 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
         // create the new node
         if ( Aig_ObjIsExor(pObj) )
-            pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+            pObj->pData = pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
         else
-            pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+            pObj->pData = pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
     }
     Vec_PtrFree( vNodes );
     // connect the PO nodes
@@ -665,7 +677,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Aig_ManForEachObj( pMan, pObj, i )
     {
         pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
-        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0((Abc_Obj_t *)pObj->pData)), pFaninNew );
     }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
@@ -860,7 +872,7 @@ Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
 {
-    extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+//    extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
@@ -1026,7 +1038,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
 {
-    extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
+    extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
     extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 
     Aig_Man_t * pMan, * pTemp;
@@ -1039,7 +1051,7 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
         return NULL;
 clk = clock();
     if ( pPars->fSynthesis )
-        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
+        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
     else
     {
         pGia = Gia_ManFromAig( pMan );
@@ -1121,23 +1133,23 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
         Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
     // process the nodes in topological order
     vCover = Vec_IntAlloc( 1 << 16 );
-    Vec_PtrForEachEntry( vMapped, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
     {
         // create new node
         pNodeNew = Abc_NtkCreateNode( pNtkNew );
         // add fanins according to the cut
-        pCut = pObj->pData;
+        pCut = (Cnf_Cut_t *)pObj->pData;
         Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
-            Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
+            Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)pLeaf->pData );
         // add logic function
         if ( pCut->nFanins < 5 )
         {
             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
             Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
-            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
+            pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
         }
         else
-            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+            pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
         // save the node
         pObj->pData = pNodeNew;
     }
@@ -1146,7 +1158,7 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         pObj = Aig_ManPo(p->pManAig, i);
-        pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        pNodeNew = Abc_ObjNotCond( (Abc_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
 
@@ -1240,7 +1252,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
     assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); 
-    pNtk->pModel = pMan->pData, pMan->pData = NULL;
+    pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1265,7 +1277,7 @@ int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConf
     assert( Abc_NtkLatchNum(pNtk) == 0 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose ); 
-    pNtk->pModel = pMan->pData, pMan->pData = NULL;
+    pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1362,7 +1374,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
     RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
     // transfer model if given
     if ( pNtk2 == NULL )
-        pNtk1->pModel = pMan->pData, pMan->pData = NULL;
+        pNtk1->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
 
 finish:
@@ -1458,10 +1470,10 @@ ABC_PRT( "Initial fraiging time", clock() - clk );
 ***********************************************************************/
 void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
 {
-    bool header_dumped = false;
+    int header_dumped = 0;
     int num_orig_latches = Abc_NtkLatchNum(pNtk);
     char **pNames = ABC_ALLOC( char *, num_orig_latches );
-    bool *p_irrelevant = ABC_ALLOC( bool, num_orig_latches );
+    int *p_irrelevant = ABC_ALLOC( int, num_orig_latches );
     char * pFlopName, * pReprName;
     Aig_Obj_t * pFlop, * pRepr;
     Abc_Obj_t * pNtkFlop; 
@@ -1560,7 +1572,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
     if ( pPars->fFlopVerbose )
         Abc_NtkPrintLatchEquivClasses(pNtk, pTemp);
 
-        Aig_ManStop( pTemp );
+    Aig_ManStop( pTemp );
     if ( pMan == NULL )
         return NULL;
 
@@ -1681,7 +1693,7 @@ static void sigfunc( int signo )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose, int * piFrames )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
@@ -1711,25 +1723,31 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
+        if ( piFrames )
+            *piFrames = iFrame;
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
-            printf( "No output was asserted in %d frames. ", iFrame );
+        {
+//            printf( "No output was asserted in %d frames. ", iFrame );
+            printf( "Incorrect return value.  " );
+        }
         else if ( RetValue == -1 )
             printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
         {
-//            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+//            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 
-            Fra_Cex_t * pCex = pNtk->pSeqModel;
+            Abc_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
 
 //            Aig_ManCounterExampleValueTest( pMan, pCex );
         }
+ABC_PRT( "Time", clock() - clk );
     }
     else
-    {
+    { 
 /*
         Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
         ABC_FREE( pNtk->pModel );
@@ -1737,7 +1755,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
-            Fra_Cex_t * pCex = pNtk->pSeqModel;
+            Abc_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
             RetValue = 0;
         }
@@ -1759,16 +1777,15 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
             printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
         {
-            Fra_Cex_t * pCex = pNtk->pSeqModel;
+            Abc_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
 */
-        Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0 );
+        RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     }
-ABC_PRT( "Time", clock() - clk );
     // verify counter-example
     if ( pNtk->pSeqModel ) 
     {
@@ -1782,6 +1799,73 @@ ABC_PRT( "Time", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
+{
+    Aig_Man_t * pMan;
+    int status, RetValue = -1, clk = clock();
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return RetValue;
+    }
+    assert( pMan->nRegs > 0 );
+    RetValue = Saig_ManBmcScalable( pMan, pPars );
+    ABC_FREE( pNtk->pModel );
+    ABC_FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    if ( RetValue == 1 )
+    {
+//        printf( "No output was asserted in %d frames. ", pPars->iFrame );
+        printf( "Incorrect return value.  " );
+    }
+    else if ( RetValue == -1 )
+    {
+        if ( pPars->nFailOuts == 0 )
+            printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", pPars->iFrame, pPars->nConfLimit );
+        else
+        {
+            printf( "The total of %d outputs was asserted in %d frames. Reached conflict limit (%d). ", pPars->nFailOuts, pPars->iFrame, pPars->nConfLimit );
+            if ( pNtk->pSeqModelVec )
+                Vec_PtrFreeFree( pNtk->pSeqModelVec );
+            pNtk->pSeqModelVec = pMan->pSeqModelVec;  pMan->pSeqModelVec = NULL;
+        }
+    }
+    else // if ( RetValue == 0 )
+    {
+        if ( !pPars->fSolveAll )
+        {
+            Abc_Cex_t * pCex = pNtk->pSeqModel;
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+        }
+        else
+        {
+            printf( "Incorrect return value.  " );
+//            printf( "At least one output was asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+        }
+    }
+    ABC_PRT( "Time", clock() - clk );
+    if ( pNtk->pSeqModel ) 
+    {
+        status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+        if ( status == 0 )
+            printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
+    }
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -1791,10 +1875,13 @@ ABC_PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
 {
     int RetValue, iFrame, clk = clock();
+    int nTotalProvedSat = 0;
     assert( pMan->nRegs > 0 );
+    if ( ppNtkRes )
+        *ppNtkRes = NULL;
     if ( pPars->fUseSeparate )
     {
         Aig_Man_t * pTemp, * pAux;
@@ -1804,17 +1891,39 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
         {
             if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
                 continue;
+            if ( pPars->fVerbose )
+                printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
             pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
             pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
             Aig_ManStop( pAux );
-            RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
+            if ( Aig_ManRegNum(pTemp) == 0 )
+            {
+                pTemp->pSeqModel = NULL;
+                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 ); 
+                if ( pTemp->pData )
+                    pTemp->pSeqModel = Gia_ManCreateFromComb( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), i, (int *)pTemp->pData );
+//                pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
+            }
+            else
+                RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
             if ( pTemp->pSeqModel )
             {
-                Ssw_Cex_t * pCex;
-                pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-                pCex->iPo = i;
-                Aig_ManStop( pTemp );
-                break;
+                if ( pPars->fDropSatOuts )
+                {
+                    printf( "Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
+                    Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
+                    Aig_ManStop( pTemp );
+                    nTotalProvedSat++;
+                    continue;
+                }
+                else
+                {
+                    Abc_Cex_t * pCex;
+                    pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                    pCex->iPo = i;
+                    Aig_ManStop( pTemp );
+                    break;
+                }
             }
             // if solved, remove the output
             if ( RetValue == 1 )
@@ -1838,17 +1947,19 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
             if ( Counter )
                 RetValue = -1;
         }
-/*
-        pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 );
-        Aig_ManStop( pTemp );
-        pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 );
-        Aig_ManStop( pTemp );
-*/
+        if ( ppNtkRes )
+        {
+            pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
+            *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0 );
+            Aig_ManStop( pTemp );
+        }
     }
     else
     {    
         RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     }
+    if ( nTotalProvedSat )
+        printf( "The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
@@ -1872,21 +1983,34 @@ ABC_PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t ** ppNtkRes )
 {
     Aig_Man_t * pMan;
+    int RetValue;
+    if ( ppNtkRes )
+        *ppNtkRes = NULL;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
         return -1;
     }
-    Abc_NtkDarBmcInter_int( pMan, pPars );
+    if ( pPars->fUseSeparate && ppNtkRes )
+    {
+        Aig_Man_t * pManNew;
+        RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, &pManNew );
+        *ppNtkRes = Abc_NtkFromAigPhase( pManNew );
+        Aig_ManStop( pManNew );
+    }
+    else
+    {
+        RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, NULL );
+    }
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
-    return 1;
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -1945,7 +2069,7 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
 {
     Aig_Man_t * pMan;
-    int RetValue, clkTotal = clock();
+    int RetValue = -1, clkTotal = clock();
     if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
     {
         Prove_Params_t Params, * pParams = &Params;
@@ -1990,7 +2114,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     }
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0, NULL );
         if ( RetValue == 0 )
         {
             printf( "Networks are not equivalent.\n" );
@@ -2023,7 +2147,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
-            Fra_Cex_t * pCex = pNtk->pSeqModel;
+            Abc_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
             if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
                 printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
@@ -2065,7 +2189,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
         ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
@@ -2272,7 +2396,7 @@ Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, in
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fVerbose )
 {
     extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
     Abc_Ntk_t * pNtkAig;
@@ -2280,17 +2404,23 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
-//    Aig_ManSeqCleanup( pMan );
-//    if ( fLatchConst && pMan->nRegs )
-//        pMan = Aig_ManConstReduce( pMan, fVerbose );
-//    if ( fLatchEqual && pMan->nRegs )
-//        pMan = Aig_ManReduceLaches( pMan, fVerbose );
-    if ( pMan->vFlopNums )
-        Vec_IntFree( pMan->vFlopNums );
-    pMan->vFlopNums = NULL;
+    if ( fSaveNames )
+    {
+        Aig_ManSeqCleanup( pMan );
+        if ( fLatchConst && pMan->nRegs )
+            pMan = Aig_ManConstReduce( pMan, fVerbose );
+        if ( fLatchEqual && pMan->nRegs )
+            pMan = Aig_ManReduceLaches( pMan, fVerbose );
+    }
+    else
+    {
+        if ( pMan->vFlopNums )
+            Vec_IntFree( pMan->vFlopNums );
+        pMan->vFlopNums = NULL;
+        pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
+        Aig_ManStop( pTemp );
+    }
 
-    pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
-    Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
 //Aig_ManPrintControlFanouts( pMan );
     Aig_ManStop( pMan );
@@ -2512,12 +2642,12 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
     extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
     extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
     Aig_Man_t * pMan;
-    Fra_Cex_t * pCex;
-    int status, RetValue, clk = clock();
+    Abc_Cex_t * pCex;
+    int status, RetValue = -1, clk = clock();
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
-        Abc_AigCleanup(pNtk->pManFunc);
+        Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
     }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
@@ -2530,7 +2660,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             {
             printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ", 
                 nFrames, nWords, pCex->iPo, pCex->iFrame );
-            status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+            status = Ssw_SmlRunCounterExample( pMan, pCex );
             if ( status == 0 )
                 printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
@@ -2557,7 +2687,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                status = Ssw_SmlRunCounterExample( pMan, pCex );
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
@@ -2587,7 +2717,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                status = Ssw_SmlRunCounterExample( pMan, pCex );
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
@@ -2614,22 +2744,21 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         pGia = Gia_ManFromAig( pMan );
         if ( Gia_ManSimSimulate( pGia, pPars ) )
         { 
-            if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
+            if ( pGia->pCexSeq )
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                    nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                    nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
+                status = Ssw_SmlRunCounterExample( pMan, pGia->pCexSeq );
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
             ABC_FREE( pNtk->pModel );
             ABC_FREE( pNtk->pSeqModel );
-            pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
-            RetValue = 1;
+            pNtk->pSeqModel = pGia->pCexSeq; pGia->pCexSeq = NULL;
+            RetValue = 0;
         }
         else
         {
-            RetValue = 0;
             printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
@@ -2646,18 +2775,17 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                status = Ssw_SmlRunCounterExample( pMan, pCex );
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
             ABC_FREE( pNtk->pModel );
             ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex;
-            RetValue = 1;
+            RetValue = 0;
         }
         else
         {
-            RetValue = 0;
             printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
@@ -2669,7 +2797,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                status = Ssw_SmlRunCounterExample( pMan, pCex );
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
@@ -2762,15 +2890,15 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
-{
+int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose )
+{ 
     Aig_Man_t * pMan, * pTemp;
     int clkTotal = clock();
     int RetValue;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
-        return;
-    RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+        return -1;
+    RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose );
     Aig_ManStop( pTemp );
     if ( RetValue == 1 )
     {
@@ -2787,6 +2915,7 @@ ABC_PRT( "Time", clock() - clkTotal );
         printf( "Networks are UNDECIDED.   " );
 ABC_PRT( "Time", clock() - clkTotal );
     }
+    return RetValue;
 }
 
 
@@ -2801,7 +2930,7 @@ ABC_PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
+Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
@@ -2810,8 +2939,29 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
     if ( pMan == NULL )
         return NULL;
 
-    Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, pPars );
+    if ( pPars->fConstr )
+    {
+        printf( "This option is currently not implemented.\n" );
+        Aig_ManStop( pMan );
+        return NULL;
+    }
+    if ( pPars->fConstr )
+    {
+        if ( Saig_ManDetectConstrTest(pMan) )
+        {
+            printf( "Performing abstraction while dynamically adding constraints...\n" );
+            pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+            Aig_ManStop( pTemp );
+            pMan = Saig_ManConCexAbstraction( pTemp = pMan, pPars );
+        }
+        else
+        {
+            printf( "Constraints are not available. Performing abstraction w/o constraints.\n" );
+            pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
+        }
+    }
+    else
+        pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
     if ( pTemp->pSeqModel )
     {
         ABC_FREE( pNtk->pModel );
@@ -3024,16 +3174,17 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
+int Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
 {
     extern void Saig_ManPrintCones( Aig_Man_t * pAig );
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
-        return;
+        return 0;
     assert( Aig_ManRegNum(pMan) > 0 );
     Saig_ManPrintCones( pMan );
     Aig_ManStop( pMan );
+    return 1;
 }
 
 /**Function*************************************************************
@@ -3114,6 +3265,33 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkPhaseFrameNum( Abc_Ntk_t * pNtk )
+{
+    extern int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits );
+    Vec_Int_t * vInits;
+    Aig_Man_t * pMan;
+    int nFrames;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return 1;
+    vInits = Abc_NtkGetLatchValues(pNtk);
+    nFrames = Saig_ManPhaseFrameNum( pMan, vInits );
+    Vec_IntFree( vInits );
+    Aig_ManStop( pMan );
+    return nFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
 {
     extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
@@ -3406,23 +3584,29 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose )
+int Abc_NtkDarReach( Abc_Ntk_t * pNtk, Saig_ParBbr_t * pPars )
 {
-    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
     Aig_Man_t * pMan;
+    int RetValue;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
-        return;
-    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
+        return -1;
+    RetValue = Aig_ManVerifyUsingBdds( pMan, pPars );
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
+    return RetValue;
 }
 
+ABC_NAMESPACE_IMPL_END
+
 #include "amap.h"
 #include "mio.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -3436,15 +3620,15 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
 ***********************************************************************/
 Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
 {
-    extern void * Abc_FrameReadLibGen();
-    Mio_Library_t * pLib = Abc_FrameReadLibGen();
+//    extern void * Abc_FrameReadLibGen();
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
     Amap_Out_t * pRes;
     Vec_Ptr_t * vNodesNew;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNodeNew, * pFaninNew;
     int i, k, iPis, iPos, nDupGates;
     // make sure gates exist in the current library
-    Vec_PtrForEachEntry( vMapping, pRes, i )
+    Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
         if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName ) == NULL )
         {
             printf( "Current library does not contain gate \"%s\".\n", pRes->pName );
@@ -3455,7 +3639,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
     pNtkNew->pManFunc = pLib;
     iPis = iPos = 0;
     vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
-    Vec_PtrForEachEntry( vMapping, pRes, i )
+    Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
     {
         if ( pRes->Type == -1 )
             pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
@@ -3468,7 +3652,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
         }
         for ( k = 0; k < pRes->nFans; k++ )
         {
-            pFaninNew = Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
+            pFaninNew = (Abc_Obj_t *)Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
             Abc_ObjAddFanin( pNodeNew, pFaninNew );
         }
         Vec_PtrPush( vNodesNew, pNodeNew );
@@ -3477,7 +3661,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
     assert( iPis == Abc_NtkCiNum(pNtkNew) );
     assert( iPos == Abc_NtkCoNum(pNtkNew) );
     // decouple the PO driver nodes to reduce the number of levels
-    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 //    if ( nDupGates && Map_ManReadVerbose(pMan) )
 //        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
@@ -3513,7 +3697,7 @@ Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
     Aig_ManStop( pMan );
     if ( vMapping == NULL )
         return NULL;
-    pMem = Vec_PtrPop( vMapping );
+    pMem = (Aig_MmFlex_t *)Vec_PtrPop( vMapping );
     pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
     Aig_MmFlexStop( pMem, 0 );
     Vec_PtrFree( vMapping );
@@ -3539,8 +3723,149 @@ Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
+{
+    Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return;
+    if ( fStruct )
+        Saig_ManDetectConstrTest( pMan );
+    else
+        Saig_ManDetectConstrFuncTest( pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
+    Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( fStruct )
+        pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+    else
+        pMan = Saig_ManDupUnfoldConstrsFunc( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    extern int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose );
+    extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+    Aig_Man_t * pMan;
+//    Vec_Int_t * vProbOne;
+//    Aig_Obj_t * pObj;
+//    int i, Entry;
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkConstrNum(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return;
+    // value in the init state
+//    Abc_AigSetNodePhases( pNtk );
+/*
+    // derive probabilities
+    vProbOne = Saig_ManComputeSwitchProbs( pMan, 48, 16, 1 );
+    // iterate over the constraint outputs
+    Saig_ManForEachPo( pMan, pObj, i )
+    {
+        Entry = Vec_IntEntry( vProbOne, Aig_ObjId(pObj) );
+        if ( i < Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan) )
+            printf( "Primary output :  ", i );
+        else
+            printf( "Constraint %3d :  ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
+        printf( "ProbOne = %f  ", Aig_Int2Float(Entry) );
+        printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
+        printf( "\n" );
+    }
+*/
+    // double-check
+    Ssw_ManProfileConstraints( pMan, 16, 64, 1 );
+    printf( "TwoFrameSatValue = %d.\n", Ssw_ManSetConstrPhases(pMan, 2, NULL) );
+    // clean up
+//    Vec_IntFree( vProbOne );
+    Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
 {
+//    extern void Saig_ManDetectConstr( Aig_Man_t * p );
+//    extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
+    extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
+
+
 //    extern void Fsim_ManTest( Aig_Man_t * pAig );
     extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
 //    Vec_Int_t * vPairs;
@@ -3571,8 +3896,24 @@ Aig_ManPrintStats( pMan );
     Aig_ManStop( pMan );
     Aig_ManStop( pMan2 );
 */
+//    Ioa_WriteAigerBufferTest( pMan, "test.aig", 0, 0 );
+//    Saig_ManFoldConstrTest( pMan );
+    {
+    extern void Saig_ManBmcSectionsTest( Aig_Man_t * p );
+    extern void Saig_ManBmcTerSimTest( Aig_Man_t * p );
+    extern void Saig_ManBmcSupergateTest( Aig_Man_t * p );
+    extern void Saig_ManBmcMappingTest( Aig_Man_t * p );
+//    Saig_ManBmcSectionsTest( pMan );
+//    Saig_ManBmcTerSimTest( pMan );
+//    Saig_ManBmcSupergateTest( pMan );
+//    Saig_ManBmcMappingTest( pMan );
+    }
+
+
 
 //    Saig_MvManSimulate( pMan, 1 );
+//    Saig_ManDetectConstr( pMan );
+//    Saig_ManDetectConstrFuncTest( pMan );
 
 //    Fsim_ManTest( pMan );
     Aig_ManStop( pMan );
@@ -3624,7 +3965,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
         return NULL;
 /*
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
+    pMan = Saig_ManCexAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
     Aig_ManStop( pTemp );
     if ( pMan == NULL )
         return NULL;
@@ -3642,7 +3983,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
     Aig_ManStop( pMan );
 */
 
-
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
 
@@ -3655,3 +3995,5 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+