Improvements in Vec_Vec_t.

abcexe.dsp

@@ -87,10 +87,6 @@ LINK32=link.exe
 # PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
 # Begin Source File
 
-SOURCE=.\src\aig\au\auCut.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\main\main.c
 # End Source File
 # End Group

abclib.dsp

@@ -4155,7 +4155,7 @@ SOURCE=.\src\aig\au\auBridge.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auCone.c
+SOURCE=.\src\aig\au\auCec.c
 # End Source File
 # Begin Source File
 
@@ -4163,27 +4163,27 @@ SOURCE=.\src\aig\au\auCore.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auCut.c
+SOURCE=.\src\aig\au\auCut.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auCut.h
+SOURCE=.\src\aig\au\auCutDiv.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auData.c
+SOURCE=.\src\aig\au\auCutEnum.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auDec.c
+SOURCE=.\src\aig\au\auCutExp.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auDecomp.c
+SOURCE=.\src\aig\au\auData.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auDiv.c
+SOURCE=.\src\aig\au\auDec6.c
 # End Source File
 # Begin Source File
 
@@ -4199,11 +4199,23 @@ SOURCE=.\src\aig\au\auFour.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auHash.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auInt.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auNpn.c
+SOURCE=.\src\aig\au\auMffc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auNpn6.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auNpnTab.c
 # End Source File
 # Begin Source File
 
@@ -4215,15 +4227,35 @@ SOURCE=.\src\aig\au\auNtk.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auResub.c
+SOURCE=.\src\aig\au\auResCore.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auSweep.c
+SOURCE=.\src\aig\au\auResDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auResDiv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auSat.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auSatData.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auTable.c
+SOURCE=.\src\aig\au\auSatSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auSupp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auSweep.c
 # End Source File
 # Begin Source File
 

src/base/abci/abc.c

@@ -8686,12 +8686,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 
-/*
-{
-//    extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
-    extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig );
-//    pNtkRes = Au_ManTransformTest( pNtk );
-    pNtkRes = Au_ManResubTest( pNtk );
+
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
+        pNtkRes = Au_ManTransformTest( pNtk );
+    }
+    else
+    {
+        extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig );
+        pNtkRes = Au_ManResubTest( pNtk );
+    }
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8699,15 +8704,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-}
-*/
 
-/*
+
+
 {
-    extern void Au_DsdVecTest( int nVars );
-    Au_DsdVecTest( 6 );
+//    extern void Au_Sat3DeriveImpls();
+//    Au_Sat3DeriveImpls();
+//    extern void Au_Sat3DeriveJusts();
+//    Au_Sat3DeriveJusts();
 }
-*/
+
 {
 //    extern void Au_NtkReadFour( Abc_Ntk_t * pNtk );
 //    extern void Au_Data4VerifyFour();

src/opt/res/resWin.c

@@ -114,7 +114,7 @@ int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
 
     // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
     Vec_PtrClear( p->vLeaves );
-    Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax )
+    Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax+1 )
     {
         Vec_PtrForEachEntry( Abc_Obj_t *, vFront, pObj, k )
         {
@@ -135,7 +135,7 @@ int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
 
     // collect the nodes in the reverse order
     Vec_PtrClear( p->vNodes );
-    Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 )
+    Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax+1, 0 )
     {
         Vec_PtrForEachEntry( Abc_Obj_t *, vFront, pObj, k )
             Vec_PtrPush( p->vNodes, pObj );

src/sat/pdr/pdrCore.c

@@ -130,7 +130,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
     int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1;
     int Counter = 0;
     int clk = clock();
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax-1 )
+    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
     {
         Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
         vArrayK1 = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, k+1 );
@@ -229,7 +229,7 @@ int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
     Pdr_Set_t * pThis;
     Vec_Ptr_t * vArrayK;
     int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax )
+    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
             if ( Pdr_SetContains( pSet, pThis ) )
                 return 1;

src/sat/pdr/pdrInv.c

@@ -130,7 +130,7 @@ int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
 {
     Vec_Ptr_t * vArrayK;
     int k, kMax = Vec_PtrSize(p->vSolvers)-1;
-    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
+    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
         if ( Vec_PtrSize(vArrayK) == 0 )
             return k;
     return -1;