Updates to arithmetic verification.

src/proof/acec/acecCore.c

@@ -70,12 +70,14 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
 ***********************************************************************/
 void Acec_BoxFree( Acec_Box_t * pBox )
 {
+    Vec_WecFreeP( &pBox->vAdds );
     Vec_WecFreeP( &pBox->vLeafs );
     Vec_WecFreeP( &pBox->vRoots );
     Vec_WecFreeP( &pBox->vLeafLits );
     Vec_WecFreeP( &pBox->vRootLits );
     Vec_WecFreeP( &pBox->vUnique );
     Vec_WecFreeP( &pBox->vShared );
+    Vec_BitFreeP( &pBox->vInvHadds );
     ABC_FREE( pBox );
 }
 void Acec_BoxFreeP( Acec_Box_t ** ppBox )

src/proof/acec/acecInt.h

@@ -41,12 +41,14 @@ typedef struct Acec_Box_t_ Acec_Box_t;
 struct Acec_Box_t_
 {
     Gia_Man_t *    pGia;      // AIG manager
+    Vec_Wec_t *    vAdds;     // adders by rank
     Vec_Wec_t *    vLeafs;    // leaf literals by rank
     Vec_Wec_t *    vRoots;    // root literals by rank
     Vec_Wec_t *    vLeafLits; // leaf literals by rank
     Vec_Wec_t *    vRootLits; // root literals by rank
     Vec_Wec_t *    vShared;   // shared leaves
     Vec_Wec_t *    vUnique;   // unique leaves
+    Vec_Bit_t *    vInvHadds; // complemented half adders
 };
 
 ////////////////////////////////////////////////////////////////////////

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) );