Updates to arithmetic verification.

src/base/wlc/wlcReadVer.c

@@ -429,6 +429,7 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
     Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
     Vec_IntForEachEntry( p->vInits, Value, i )
     {
+        char * pname = Wlc_ObjName( p, Value );
         if ( Value < 0 )
         {
             for ( k = 0; k < -Value; k++ )

src/proof/acec/acecCore.c

@@ -319,7 +319,7 @@ void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int C
 void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
 {
     Vec_Int_t * vLevel1, * vLevel2; 
-    int i, k, Prev, This, Entry;
+    int i, k, Prev, This, Entry, Counter = 0;
     Vec_WecForEachLevel( vLits, vLevel1, i )
     {
         if ( i == Vec_WecSize(vLits) - 1 )
@@ -347,8 +347,10 @@ void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
 
             assert( Vec_IntSize(vLevel1)                  == Vec_IntSize(vLevel2) );
             assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
+            Counter++;
         }
     }
+    printf( "Moved %d pairs of PPs to normalize the matrix.\n", Counter );
 }
 
 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 )
@@ -490,12 +492,14 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     Gia_Man_t * pMiter;
     Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
     Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
-    Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
-    Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
-    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
-    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
-    Vec_BitFreeP( &vIgnore0 );
-    Vec_BitFreeP( &vIgnore1 );
+//    Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
+//    Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
+//    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
+//    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
+//    Vec_BitFreeP( &vIgnore0 );
+//    Vec_BitFreeP( &vIgnore1 );
+    Acec_Box_t * pBox0 = Acec_ProduceBox( pGia0, pPars->fVerbose );
+    Acec_Box_t * pBox1 = Acec_ProduceBox( pGia1, pPars->fVerbose );
     if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
         printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
     else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching

src/proof/acec/acecInt.h

@@ -88,7 +88,7 @@ extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
 extern Vec_Int_t *   Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );
 /*=== acecUtil.c ========================================================*/
-extern Acec_Box_t *  Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose );
+extern Acec_Box_t *  Acec_ProduceBox( Gia_Man_t * p, int fVerbose );
 
 
 

src/proof/acec/acecTree.c

@@ -333,6 +333,37 @@ void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxe
     Vec_BitFree( vPhase );
     Vec_BitFree( vRoots );
 }
+void Acec_TreeVerifyConnections( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+    Vec_Int_t * vCounts = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, k, n, Box;
+    // mark outputs
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+        {
+            Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+3 ), 0 );
+            Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+4 ), 0 );
+        }
+    // count fanouts
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            for ( n = 0; n < 3; n++ )
+                if ( Vec_IntEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n) ) != -1 )
+                    Vec_IntAddToEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n), 1 );
+    // print out
+    printf( "The adder tree has %d internal cut points. ", Vec_IntCountLarger(vCounts, -1) );
+    if ( Vec_IntCountLarger(vCounts, 1) == 0 )
+        printf( "There is no internal fanouts.\n" );
+    else
+    {
+        printf( "These %d points have more than one fanout:\n", Vec_IntCountLarger(vCounts, 1) );
+        Vec_IntForEachEntry( vCounts, Box, i )
+            if ( Box > 1 )
+                printf( "Node %d(lev %d) has fanout %d.\n", i, Gia_ObjLevelId(p, i), Box );
+    }
+    Vec_IntFree( vCounts );
+}
 
 /**Function*************************************************************
 
@@ -534,7 +565,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
   SideEffects []
 
   SeeAlso     []
-
+`
 ***********************************************************************/
 void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
 {
@@ -560,6 +591,10 @@ void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
     Vec_WecPrintLits( pBox->vLeafLits );
     printf( "Outputs:\n" );
     Vec_WecPrintLits( pBox->vRootLits );
+//    printf( "Node %d has level %d.\n", 3715, Gia_ObjLevelId(pBox->pGia, 3715) );
+//    printf( "Node %d has level %d.\n", 167, Gia_ObjLevelId(pBox->pGia, 167) );
+//    printf( "Node %d has level %d.\n", 278, Gia_ObjLevelId(pBox->pGia, 278) );
+//    printf( "Node %d has level %d.\n", 597, Gia_ObjLevelId(pBox->pGia, 597) );
 }
 
 int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )