diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-11 13:36:54 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-11 13:36:54 +0700 |
| commit | 89d08cfd06ecb1653ef0613049447c91bc114f46 (patch) | |
| tree | f2ce4af11434ea14401e505eba7a0ca6270cfaa8 /src/proof/acec/acecRe.c | |
| parent | 4bfb97d3e1b313f4b72ee0fa7adfa8949236db85 (diff) | |
| download | abc-89d08cfd06ecb1653ef0613049447c91bc114f46.tar.gz abc-89d08cfd06ecb1653ef0613049447c91bc114f46.tar.bz2 abc-89d08cfd06ecb1653ef0613049447c91bc114f46.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecRe.c')
| -rw-r--r-- | src/proof/acec/acecRe.c | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 60b894c8..161b6fbb 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -370,7 +370,7 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j ) Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k ) { - int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77}; + int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0x77, 0xBB, 0xDD, 0xEE}; int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17}; int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3; for ( n = 0; n < 8; n++ ) @@ -390,6 +390,14 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos Vec_WecFree( vMajMap ); return vAdds; } +int Ree_ManCompare( int * pCut0, int * pCut1 ) +{ + if ( pCut0[3] < pCut1[3] ) return -1; + if ( pCut0[3] > pCut1[3] ) return 1; + if ( pCut0[4] < pCut1[4] ) return -1; + if ( pCut0[4] > pCut1[4] ) return 1; + return 0; +} Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose ) { extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ); @@ -427,6 +435,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose Vec_IntFree( vTemp ); Vec_IntFree( vCuts ); vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose ); + qsort( Vec_IntArray(vAdds), Vec_IntSize(vAdds)/6, 24, (int (*)(const void *, const void *))Ree_ManCompare ); if ( fVerbose ) printf( "Adders = %d. Total cuts = %d. Hashed cuts = %d. Hashed/Adders = %.2f.\n", Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) ); |