Updates to arithmetic verification.

3 files changed, 90 insertions, 24 deletions

diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 06385f3c..a2341704 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -307,6 +307,50 @@ int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
     Vec_IntFree( vRes );
     return nCommon;
 }
+void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int Class )
+{
+    int i;
+    for ( i = Vec_IntSize(vClasses)-1; i >= 0; i-- )
+        if ( Vec_IntEntry(vClasses,i) >= Class )
+            break;
+    Vec_IntInsert( vLits, i+1, Lit );
+    Vec_IntInsert( vClasses, i+1, Class );
+}
+void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
+{
+    Vec_Int_t * vLevel1, * vLevel2; 
+    int i, k, Prev, This, Entry;
+    Vec_WecForEachLevel( vLits, vLevel1, i )
+    {
+        if ( i == Vec_WecSize(vLits) - 1 )
+            break;
+        vLevel2 = Vec_WecEntry(vClasses, i);
+        assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
+        Prev = -1;
+        Vec_IntForEachEntry( vLevel2, This, k )
+        {
+            if ( Prev != This )
+            {
+                Prev = This;
+                continue;
+            }
+            Prev = -1;
+            Entry = Vec_IntEntry( vLevel1, k );
+
+            Vec_IntDrop( vLevel1, k );
+            Vec_IntDrop( vLevel2, k-- );
+
+            Vec_IntDrop( vLevel1, k );
+            Vec_IntDrop( vLevel2, k-- );
+
+            Vec_IntInsertOrder( Vec_WecEntry(vLits, i+1), Vec_WecEntry(vClasses, i+1), Entry, This );
+
+            assert( Vec_IntSize(vLevel1)                  == Vec_IntSize(vLevel2) );
+            assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
+        }
+    }
+}
+
 void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
 {
     Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
@@ -318,14 +362,20 @@ void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLi
     {
         Vec_WecInsertLevel( vLits0, 0 );
         Vec_WecInsertLevel( vRoots0, 0 );
+        Vec_WecInsertLevel( vRes0, 0 );
         printf( "Shifted one level up.\n" );
     }
     else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
     {
         Vec_WecInsertLevel( vLits1, 0 );
         Vec_WecInsertLevel( vRoots1, 0 );
+        Vec_WecInsertLevel( vRes1, 0 );
         printf( "Shifted one level down.\n" );
     }
+    Acec_MoveDuplicates( vLits0, vRes0 );
+    Acec_MoveDuplicates( vLits1, vRes1 );
+
+    //Vec_WecPrintLits( vLits1 );
     //printf( "Input literals:\n" );
     //Vec_WecPrintLits( vLits0 );
     //printf( "Equiv classes:\n" );
@@ -410,6 +460,10 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
     printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
     printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
 
+    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vShared, Vec_IntArray(vMap0), 0 );
+    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vShared, Vec_IntArray(vMap1), 0 );
+    //printf( "\n" );
+
     //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
     //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );
 
@@ -448,8 +502,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
         printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
     else 
     {
-        pGia0n = Acec_InsertBox( pBox0, 1 );
-        pGia1n = Acec_InsertBox( pBox1, 1 );
+        pGia0n = Acec_InsertBox( pBox0, 0 );
+        pGia1n = Acec_InsertBox( pBox1, 0 );
         printf( "Matching of adder trees in LHS and RHS succeeded.  " );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         // remove the last output
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 6b36589c..f2acb37b 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -76,9 +76,19 @@ Vec_Int_t * Acec_InsertTree( Gia_Man_t * pNew, Vec_Wec_t * vLeafMap )
         {
             if ( Vec_IntSize(vLevel) == 2 )
                 Vec_IntPush( vLevel, 0 );
-            In[2] = Vec_IntPop( vLevel );
-            In[1] = Vec_IntPop( vLevel );
-            In[0] = Vec_IntPop( vLevel );
+            //In[2] = Vec_IntPop( vLevel );
+            //In[1] = Vec_IntPop( vLevel );
+            //In[0] = Vec_IntPop( vLevel );
+
+            In[0] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
+            In[1] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
+            In[2] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
             Acec_InsertFadd( pNew, In, Out );
             Vec_IntPush( vLevel, Out[0] );
             if ( i+1 < Vec_WecSize(vLeafMap) )
@@ -114,11 +124,22 @@ int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
     return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
 }
-Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits )
+Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Int_t * vRootLits )
 {
     Vec_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
     Vec_Int_t * vLevel, * vRootRanks;  
     int i, k, iLit, iLitNew;
+    // add roo literals
+    if ( vRootLits )
+        Vec_IntForEachEntry( vRootLits, iLit, i )
+        {
+            if ( i < Vec_WecSize(vLeafMap) )
+                vLevel = Vec_WecEntry(vLeafMap, i);
+            else
+                vLevel = Vec_WecPushLevel(vLeafMap);
+            Vec_IntPush( vLevel, iLit );
+        }
+    // add other literals
     Vec_WecForEachLevel( vLeafLits, vLevel, i )
         Vec_IntForEachEntry( vLevel, iLit, k )
         {
@@ -137,7 +158,7 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
     Gia_Man_t * p = pBox->pGia;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
-    Vec_Int_t * vRootRanks, * vLevel;
+    Vec_Int_t * vRootRanks, * vLevel, * vTemp;
     int i, k, iLit, iLitNew;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -148,26 +169,14 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
         pObj->Value = Gia_ManAppendCi( pNew );
     // implement tree
     if ( fAll )
-        vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits );
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits, NULL );
     else
     {
-        Vec_Wec_t * vLeafLits;
         assert( pBox->vShared != NULL );
         assert( pBox->vUnique != NULL );
-        vRootRanks = Acec_BuildTree( p, p, pBox->vShared );
-        // add these roots to the unique ones
-        vLeafLits = Vec_WecDup( pBox->vUnique );
-        Vec_IntForEachEntry( vRootRanks, iLit, i )
-        {
-            if ( i < Vec_WecSize(vLeafLits) )
-                vLevel = Vec_WecEntry(vLeafLits, i);
-            else
-                vLevel = Vec_WecPushLevel(vLeafLits);
-            Vec_IntPush( vLevel, iLit );
-        }
-        Vec_IntFree( vRootRanks );
-        vRootRanks = Acec_BuildTree( pNew, p, vLeafLits );
-        Vec_WecFree( vLeafLits );
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vShared, NULL );
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vUnique, vTemp = vRootRanks );
+        Vec_IntFree( vTemp );
     }
     // update polarity of literals
     Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index fe5ca01b..2461c89b 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -207,6 +207,9 @@ void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
     Gia_ManForEachAnd( p, pObj, i )
         if ( Vec_BitEntry(vIsLeaf, i) )
             Acec_TreeMarkTFI_rec( p, i, vMarked );
+    // additional one
+//if ( 10942 < Gia_ManObjNum(p) )
+//    Acec_TreeMarkTFI_rec( p, 10942, vMarked );
     // remove those that overlap with the marked TFI
     Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
     {
@@ -419,7 +422,7 @@ Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * v
     int i;
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
-        if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
+        if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
             continue;
         Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
         Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );