diff options
| -rw-r--r-- | abcexe.dsp | 4 | ||||
| -rw-r--r-- | abclib.dsp | 54 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 30 | ||||
| -rw-r--r-- | src/misc/vec/vecVec.h | 138 | ||||
| -rw-r--r-- | src/opt/res/resWin.c | 4 | ||||
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 4 | ||||
| -rw-r--r-- | src/sat/pdr/pdrInv.c | 2 |
7 files changed, 195 insertions, 41 deletions
@@ -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 @@ -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 diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 123bed95..2b0b0684 100644 --- a/src/base/abci/abc.c +++ b/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(); diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index 18f6d75c..e888e4cf 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -56,12 +56,28 @@ struct Vec_Vec_t_ for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \ for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelStop( vGlob, vVec, i, LevelStop ) \ + for ( i = 0; (i < LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ - for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) + for ( i = LevelStart; (i < LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \ - for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) + for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) #define Vec_VecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ - for ( i = LevelStart; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) + for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) + +// iterators through levels +#define Vec_VecForEachLevelInt( vGlob, vVec, i ) \ + for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelIntStart( vGlob, vVec, i, LevelStart ) \ + for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelIntStop( vGlob, vVec, i, LevelStop ) \ + for ( i = 0; (i < LevelStop) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelIntStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ + for ( i = LevelStart; (i < LevelStop) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) +#define Vec_VecForEachLevelIntReverse( vGlob, vVec, i ) \ + for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) +#define Vec_VecForEachLevelIntReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ + for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) // iteratores through entries #define Vec_VecForEachEntry( Type, vGlob, pEntry, i, k ) \ @@ -73,7 +89,7 @@ struct Vec_Vec_t_ for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ ) \ Vec_PtrForEachEntry( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) #define Vec_VecForEachEntryStartStop( Type, vGlob, pEntry, i, k, LevelStart, LevelStop ) \ - for ( i = LevelStart; i <= LevelStop; i++ ) \ + for ( i = LevelStart; i < LevelStop; i++ ) \ Vec_PtrForEachEntry( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) #define Vec_VecForEachEntryReverse( Type, vGlob, pEntry, i, k ) \ for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ @@ -82,9 +98,31 @@ struct Vec_Vec_t_ for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \ Vec_PtrForEachEntryReverse( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) #define Vec_VecForEachEntryReverseStart( Type, vGlob, pEntry, i, k, LevelStart ) \ - for ( i = LevelStart; i >= 0; i-- ) \ + for ( i = LevelStart-1; i >= 0; i-- ) \ Vec_PtrForEachEntry( Type, (Vec_Ptr_t *)Vec_VecEntry(vGlob, i), pEntry, k ) +// iteratores through entries +#define Vec_VecForEachEntryInt( Type, vGlob, Entry, i, k ) \ + for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ + Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntLevel( Type, vGlob, Entry, i, Level ) \ + Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, Level), Entry, i ) +#define Vec_VecForEachEntryIntStart( Type, vGlob, Entry, i, k, LevelStart ) \ + for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ ) \ + Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntStartStop( Type, vGlob, Entry, i, k, LevelStart, LevelStop ) \ + for ( i = LevelStart; i < LevelStop; i++ ) \ + Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverse( Type, vGlob, Entry, i, k ) \ + for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ + Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverseReverse( Type, vGlob, Entry, i, k ) \ + for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \ + Vec_IntForEachEntryReverse( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) +#define Vec_VecForEachEntryIntReverseStart( Type, vGlob, Entry, i, k, LevelStart ) \ + for ( i = LevelStart-1; i >= 0; i-- ) \ + Vec_IntForEachEntry( Type, (Vec_Int_t *)Vec_VecEntry(vGlob, i), Entry, k ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -158,6 +196,28 @@ static inline void Vec_VecExpand( Vec_Vec_t * p, int Level ) /**Function************************************************************* + Synopsis [Allocates a vector with the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecExpandInt( Vec_Vec_t * p, int Level ) +{ + int i; + if ( p->nSize >= Level + 1 ) + return; + Vec_IntGrow( (Vec_Int_t *)p, Level + 1 ); + for ( i = p->nSize; i <= Level; i++ ) + p->pArray[i] = Vec_PtrAlloc( 0 ); + p->nSize = Level + 1; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -183,6 +243,22 @@ static inline int Vec_VecSize( Vec_Vec_t * p ) SeeAlso [] ***********************************************************************/ +static inline int Vec_VecLevelSize( Vec_Vec_t * p, int i ) +{ + return Vec_PtrSize( (Vec_Ptr_t *)p->pArray[i] ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void * Vec_VecEntry( Vec_Vec_t * p, int i ) { assert( i >= 0 && i < p->nSize ); @@ -239,7 +315,7 @@ static inline void Vec_VecFreeP( Vec_Vec_t ** p ) SeeAlso [] ***********************************************************************/ -static inline Vec_Vec_t * Vec_VecDupPtr( Vec_Vec_t * p ) +static inline Vec_Vec_t * Vec_VecDup( Vec_Vec_t * p ) { Vec_Ptr_t * vNew, * vVec; int i; @@ -262,11 +338,12 @@ static inline Vec_Vec_t * Vec_VecDupPtr( Vec_Vec_t * p ) ***********************************************************************/ static inline Vec_Vec_t * Vec_VecDupInt( Vec_Vec_t * p ) { - Vec_Ptr_t * vNew, * vVec; + Vec_Ptr_t * vNew; + Vec_Int_t * vVec; int i; vNew = Vec_PtrAlloc( Vec_VecSize(p) ); - Vec_VecForEachLevel( p, vVec, i ) - Vec_PtrPush( vNew, Vec_IntDup((Vec_Int_t *)vVec) ); + Vec_VecForEachLevelInt( p, vVec, i ) + Vec_PtrPush( vNew, Vec_IntDup(vVec) ); return (Vec_Vec_t *)vNew; } @@ -344,6 +421,30 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry ) SeeAlso [] ***********************************************************************/ +static inline void Vec_VecPushInt( Vec_Vec_t * p, int Level, int Entry ) +{ + if ( p->nSize < Level + 1 ) + { + int i; + Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 ); + for ( i = p->nSize; i < Level + 1; i++ ) + p->pArray[i] = Vec_PtrAlloc( 0 ); + p->nSize = Level + 1; + } + Vec_IntPush( (Vec_Int_t*)p->pArray[Level], Entry ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry ) { if ( p->nSize < Level + 1 ) @@ -354,6 +455,25 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_VecPushUniqueInt( Vec_Vec_t * p, int Level, int Entry ) +{ + if ( p->nSize < Level + 1 ) + Vec_VecPushInt( p, Level, Entry ); + else + Vec_IntPushUnique( (Vec_Int_t*)p->pArray[Level], Entry ); +} + +/**Function************************************************************* + Synopsis [Comparison procedure for two arrays.] Description [] diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c index a26e7831..e6eeac6a 100644 --- a/src/opt/res/resWin.c +++ b/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 ); diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index 8b58bde1..742ce381 100644 --- a/src/sat/pdr/pdrCore.c +++ b/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; diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c index 5eb32790..daf542e9 100644 --- a/src/sat/pdr/pdrInv.c +++ b/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; |