diff options
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 4 | ||||
| -rw-r--r-- | src/misc/vec/vecInt.h | 83 | ||||
| -rw-r--r-- | src/proof/fra/fraClau.c | 18 |
4 files changed, 86 insertions, 20 deletions
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 11ec55f2..aec38f40 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -23,6 +23,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaGlitch.c \ src/aig/gia/giaHash.c \ src/aig/gia/giaIf.c \ + src/aig/gia/giaIso.c \ src/aig/gia/giaMan.c \ src/aig/gia/giaMem.c \ src/aig/gia/giaPat.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 70c51d7a..adaf76b7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27798,6 +27798,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); // extern int Gia_ManSuppSizeTest( Gia_Man_t * p ); // extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); + extern void Gia_IsoTest( Gia_Man_t * p ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -27834,8 +27835,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // pAbc->pGia = Gia_VtaTest( pTemp = pAbc->pGia ); // Gia_ManStopP( &pTemp ); // Gia_ManSuppSizeTest( pAbc->pGia ); - // Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); + + Gia_IsoTest( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 39ab2623..72aa1ab6 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -359,6 +359,22 @@ static inline int Vec_IntSize( Vec_Int_t * p ) SeeAlso [] ***********************************************************************/ +static inline int Vec_IntCap( Vec_Int_t * p ) +{ + return p->nCap; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline int Vec_IntEntry( Vec_Int_t * p, int i ) { assert( i >= 0 && i < p->nSize ); @@ -455,6 +471,27 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) /**Function************************************************************* + Synopsis [Resizes the vector to the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntGrowResize( Vec_Int_t * p, int nCapMin ) +{ + p->nSize = nCapMin; + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); + assert( p->pArray ); + p->nCap = nCapMin; +} + +/**Function************************************************************* + Synopsis [Fills the vector with given number of entries.] Description [] @@ -1215,7 +1252,7 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2 /**Function************************************************************* - Synopsis [Performs fast mapping for one node.] + Synopsis [] Description [] @@ -1250,6 +1287,32 @@ static inline void Vec_IntSelectSort( int * pArray, int nSize ) SeeAlso [] ***********************************************************************/ +static inline void Vec_IntSelectSortCost( int * pArray, int nSize, Vec_Int_t * vCosts ) +{ + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( Vec_IntEntry(vCosts, pArray[j]) < Vec_IntEntry(vCosts, pArray[best_i]) ) + best_i = j; + temp = pArray[i]; + pArray[i] = pArray[best_i]; + pArray[best_i] = temp; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Vec_IntPrint( Vec_Int_t * vVec ) { int i, Entry; @@ -1279,6 +1342,24 @@ static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 ) return memcmp( Vec_IntArray(p1), Vec_IntArray(p2), sizeof(int)*Vec_IntSize(p1) ); } +/**Function************************************************************* + + Synopsis [Appends the contents of the second vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) +{ + int Entry, i; + Vec_IntForEachEntry( vVec2, Entry, i ) + Vec_IntPush( vVec1, Entry ); +} + ABC_NAMESPACE_HEADER_END diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c index fb87550d..48640d1d 100644 --- a/src/proof/fra/fraClau.c +++ b/src/proof/fra/fraClau.c @@ -315,24 +315,6 @@ static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec ) /**Function************************************************************* - Synopsis [Appends the contents of the second vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) -{ - int Entry, i; - Vec_IntForEachEntry( vVec2, Entry, i ) - Vec_IntPush( vVec1, Entry ); -} - -/**Function************************************************************* - Synopsis [Complements all literals in the clause.] Description [] |