Updates to arithmetic verification.

5 files changed, 55 insertions, 30 deletions

diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index 6a5f4040..6185677b 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -350,9 +350,15 @@ Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
 {
     Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 );
     Vec_Int_t * vLevel;
-    int i, k, iLit;
-    Vec_WecPrintLits( pBox->vRootLits );
-    Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+    int i, k, iStart, iLit, Driver, Count = 0;
+    // determine how much to shift
+    Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
+        if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
+            break;
+    assert( iStart < Gia_ManCoNum(p) );
+    //Vec_WecPrintLits( pBox->vRootLits );
+    Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
     {
         int In[3] = {0}, Out[2];
         assert( Vec_IntSize(vLevel) > 0 );
@@ -370,9 +376,11 @@ Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
             Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
         else
             Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
+        Count++;
     }
     assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
     Vec_IntShrink( vRes, Gia_ManCoNum(p) );
+    printf( "Added %d adders for replace CLAs.  ", Count );
     return vRes;
 }
 Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
@@ -384,7 +392,6 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -394,22 +401,26 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
     Gia_ManForEachCo( p, pObj, i )
     {
         int iLit = Vec_IntEntry( vRes, i );
-        int Phase1 = Gia_ObjPhase(pObj);
-        int Phase2 = Abc_LitIsCompl(iLit) ^ Gia_ObjPhase(Gia_ManObj(p, Abc_Lit2Var(iLit)));
-        int iLitNew = Abc_Var2Lit( Abc_Lit2Var(iLit), Phase1 ^ Phase2 );
-        pObj->Value = Gia_ManAppendCo( pNew, iLitNew );
+        Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+        pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
     }
+    // set correct phase
+    Gia_ManSetPhase( p );
+    Gia_ManSetPhase( pNew );
+    Gia_ManForEachCo( pNew, pObj, i )
+        if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
+            Gia_ObjFlipFaninC0( pObj );
+    // remove dangling nodes
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     return pNew;
 }
 Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
 {
-    int status = -1;
     abctime clk = Abc_Clock();
     Gia_Man_t * pNew = NULL;
     Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL;
-    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
     Vec_Int_t * vResult;
     Vec_BitFreeP( &vIgnore );
     if ( pBox == NULL ) // cannot match
@@ -418,8 +429,10 @@ Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
         return Gia_ManDup( pGia );
     }
     vResult = Acec_RewriteTop( pGia, pBox );
+    Acec_BoxFreeP( &pBox );
     pNew = Acec_RewriteReplace( pGia, vResult );
     Vec_IntFree( vResult );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return pNew;
 }
 
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 4fddcfab..06385f3c 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -328,12 +328,12 @@ void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLi
     }
     //printf( "Input literals:\n" );
     //Vec_WecPrintLits( vLits0 );
-    printf( "Equiv classes:\n" );
-    Vec_WecPrintLits( vRes0 );
+    //printf( "Equiv classes:\n" );
+    //Vec_WecPrintLits( vRes0 );
     //printf( "Input literals:\n" );
     //Vec_WecPrintLits( vLits1 );
-    printf( "Equiv classes:\n" );
-    Vec_WecPrintLits( vRes1 );
+    //printf( "Equiv classes:\n" );
+    //Vec_WecPrintLits( vRes1 );
     //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
     //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
     Vec_WecFree( vRes0 );
@@ -353,10 +353,10 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
     
     //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
     //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
-    printf( "Outputs:\n" );
-    Vec_WecPrintLits( pBox0->vRootLits );
-    printf( "Outputs:\n" );
-    Vec_WecPrintLits( pBox1->vRootLits );
+    //printf( "Outputs:\n" );
+    //Vec_WecPrintLits( pBox0->vRootLits );
+    //printf( "Outputs:\n" );
+    //Vec_WecPrintLits( pBox1->vRootLits );
 
     // reorder nodes to have the same order
     assert( pBox0->vShared == NULL );
@@ -438,8 +438,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     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, pPars->fVerbose );
-    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, pPars->fVerbose );
+    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 );
     if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index c49945db..b8ec2455 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -75,7 +75,7 @@ extern void          Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
 extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
 /*=== acecTree.c ========================================================*/
 extern void          Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds );
-extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose );
+extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
 extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 /*=== acecUtil.c ========================================================*/
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 0d209524..6b36589c 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -201,7 +201,7 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
 Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
 {
     Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
-    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
     Gia_Man_t * pNew  = Acec_InsertBox( pBox, 1 );
     Acec_BoxFreeP( &pBox );
     Vec_BitFreeP( &vIgnore );
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 2b356574..fe5ca01b 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -127,6 +127,10 @@ void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
     // remove those that overlap with roots
     Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
     {
+        // special case of the first bit
+//        if ( i == 0 )
+//            continue;
+
 /*
         if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
         {
@@ -415,7 +419,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 );
@@ -468,7 +472,7 @@ void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int
     Acec_TreeFindTrees2_rec( vAdds, vMap, In,  Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
     Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
 }
-Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
+Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut )
 {
     Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
     Vec_Int_t * vMap   = Acec_TreeFindPoints( p, vAdds, vIgnore );
@@ -495,7 +499,10 @@ Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vI
     Vec_BitFree( vFound );
     Vec_IntFree( vMap );
     // filter trees
-    Acec_TreeFilterTrees( p, vAdds, vTrees );
+    if ( fFilterIn )
+        Acec_TreeFilterTrees2( p, vAdds, vTrees );
+    else if ( fFilterOut )
+        Acec_TreeFilterTrees( p, vAdds, vTrees );
     // sort by size
     Vec_WecSort( vTrees, 1 );
     return vTrees;
@@ -511,7 +518,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
     printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Vec_WecPrint( vTrees, 0 );
@@ -572,7 +579,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
     Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
     Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
     Vec_Int_t * vLevel, * vMap;
-    int i, j, k, Box, Rank, Count = 0;
+    int i, j, k, Box, Rank;//, Count = 0;
 
     Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
     pBox->pGia        = p;
@@ -583,6 +590,11 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
     // collect boxes; mark inputs/outputs
     Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
     {
+//        if ( 37 == Box && 6 == Rank )
+//        {
+//            printf( "Skipping one adder...\n" );
+//            continue;
+//        }
         Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
         Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
         Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
@@ -677,7 +689,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
     printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     //Vec_WecPrint( vTrees, 0 );
@@ -707,11 +719,11 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose )
 {
     Acec_Box_t * pBox = NULL;
     Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
-    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
+    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore, fFilterIn, fFilterOut );
     if ( vTrees && Vec_WecSize(vTrees) > 0 )
     {
         pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );