Updates to arithmetic verification.

12 files changed, 501 insertions, 27 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index dc6c679a..3bc97e6b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1242,6 +1242,8 @@ extern Gia_Man_t *         Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
 extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
 extern Gia_Man_t *         Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
 extern Gia_Man_t *         Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis );
+extern Gia_Man_t *         Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
+extern Gia_Man_t *         Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
 extern Gia_Man_t *         Gia_ManDupOneHot( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupLevelized( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index cdb6a208..b0ba3472 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3046,6 +3046,71 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim
     return pNew;
 
 }
+void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+    if ( ~pObj->Value )
+        return;
+    if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level )
+    {
+        pObj->Value = Gia_ManAppendCi( pNew );
+        //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+        return;
+    }
+    Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level );
+    Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+}
+Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
+{
+    Gia_Man_t * pNew;
+    int i;
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManLevelNum( p );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level );
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
+    return pNew;
+}
+
+void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+    if ( ~pObj->Value )
+        return;
+    if ( !Gia_ObjIsAnd(pObj) || Level <= 0 )
+    {
+        pObj->Value = Gia_ManAppendCi( pNew );
+        //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+        return;
+    }
+    Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 );
+    Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+}
+Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
+{
+    Gia_Man_t * pNew;
+    int i;
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level );
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
+    return pNew;
+
+}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 4dd85aab..4deebd7a 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -1014,16 +1014,23 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds )
+Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold )
 {
-    Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
+    Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry;
+    if ( vBold )
+        Vec_IntForEachEntry( vBold, Entry, i )
+            Vec_BitWriteEntry( vIsBold, Entry, 1 );
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
         if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 )
             continue;
+        if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) )
+            continue;
         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i );
         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i );
     }
+    Vec_BitFree( vIsBold );
     return vMapAdds;
 }
 Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors )
@@ -1105,7 +1112,7 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
 ***********************************************************************/
 void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
 {
-    Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
+    Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold );
     Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
     Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
     Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9db3d7d6..58a14e81 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -482,6 +482,7 @@ static int Abc_CommandAbc9ATree              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Polyn              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Acec               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Anorm              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Decla              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1126,6 +1127,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&polyn",        Abc_CommandAbc9Polyn,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&acec",         Abc_CommandAbc9Acec,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&anorm",        Abc_CommandAbc9Anorm,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&decla",        Abc_CommandAbc9Decla,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
@@ -40799,6 +40801,57 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Decla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fBooth = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBooth ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Decla(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Acec_ManDecla( pAbc->pGia, fBooth, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &decla [-bvh]\n" );
+    Abc_Print( -2, "\t         removes carry look ahead adders\n" );
+    Abc_Print( -2, "\t-b     : toggles working with Booth multipliers [default = %s]\n",  fBooth? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
@@ -42690,7 +42743,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Jf_ManTestCnf( pAbc->pGia );
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
-    Acec_MultFindPPsTest( pAbc->pGia );
 
 //    printf( "\nThis command is currently disabled.\n\n" );
     return 0;
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index 8180e984..c8c89701 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -561,6 +561,18 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
         printf( " }\n" );
     }
 }
+static inline void Vec_WecPrintLits( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i, k, iLit;
+    Vec_WecForEachLevel( p, vVec, i )
+    {
+        printf( " %4d : %2d  {", i, Vec_IntSize(vVec) );
+        Vec_IntForEachEntry( vVec, iLit, k )
+            printf( " %c%d", Abc_LitIsCompl(iLit) ? '-' : '+', Abc_Lit2Var(iLit) );
+        printf( " }\n" );
+    }
+}
 
 /**Function*************************************************************
 
diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index 5a24bec7..fcbd32df 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -66,6 +66,8 @@ struct Acec_ParCec_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== acecCl.c ========================================================*/
+extern Gia_Man_t *   Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose );
 /*=== acecCore.c ========================================================*/
 extern void          Acec_ManCecSetDefaultParams( Acec_ParCec_t * p );
 extern int           Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars );
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index 145f2e0b..6a5f4040 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -335,6 +335,94 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 In[3] = {0}, Out[2];
+        assert( Vec_IntSize(vLevel) > 0 );
+        assert( Vec_IntSize(vLevel) <= 3 );
+        if ( Vec_IntSize(vLevel) == 1 )
+        {
+            Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) );
+            continue;
+        }
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            In[k] = iLit;
+        Acec_InsertFadd( p, In, Out );
+        Vec_IntPush( vRes, Out[0] );
+        if ( i+1 < Vec_WecSize(pBox->vRootLits) )
+            Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
+        else
+            Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
+    }
+    assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
+    Vec_IntShrink( vRes, Gia_ManCoNum(p) );
+    return vRes;
+}
+Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;  int i;
+    assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) );
+    // create new manager
+    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 )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    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 );
+    }
+    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 );
+    Vec_Int_t * vResult;
+    Vec_BitFreeP( &vIgnore );
+    if ( pBox == NULL ) // cannot match
+    {
+        printf( "Cannot find arithmetic boxes.\n" );
+        return Gia_ManDup( pGia );
+    }
+    vResult = Acec_RewriteTop( pGia, pBox );
+    pNew = Acec_RewriteReplace( pGia, vResult );
+    Vec_IntFree( vResult );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 6b631a1b..4fddcfab 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define TRUTH_UNUSED 0x1234567812345678
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -70,6 +72,79 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs )
+{
+    Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0;
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        {
+            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+            if ( Vec_IntSize(vSupp) > 6  )
+            {
+                nOvers++;
+                Vec_WrdPush( vTruths, TRUTH_UNUSED );
+                continue;
+            }
+            vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+            if ( Vec_IntSize(vSupp) > 5  )
+            {
+                nOvers++;
+                Vec_WrdPush( vTruths, TRUTH_UNUSED );
+                continue;
+            }
+            Vec_WrdPush( vTruths, Truth );
+        }
+        Vec_PtrPush( vFunc, vTruths );
+    }
+    if ( nOvers )
+        printf( "Detected %d oversize support nodes.\n", nOvers );
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    // verify the classes
+    Vec_WecForEachLevel( vReprs, vLevel, i )
+    {
+        Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 )
+        {
+            word Truth = Vec_WrdEntry( vTruths, k );
+            word Truth2 = Vec_WrdEntry( vTruths, j );
+            if ( Entry == Entry2 )
+            {
+                nErrors++;
+                if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
+            }
+            if ( Entry == Abc_LitNot(Entry2) )
+            {
+                nErrors++;
+                if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
+            }
+        }
+    }
+    if ( nErrors )
+        printf( "Total errors in equivalence classes = %d.\n", nErrors );
+    Vec_VecFree( (Vec_Vec_t *)vFunc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
 {
     Gia_Obj_t * pObj;
@@ -148,13 +223,15 @@ void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
 }
 void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
 {
-    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
-    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vSupp;
+    Vec_Wrd_t * vTemp;
     Vec_Int_t * vLevel;
     int i, k, Entry;
     printf( "Leaf literals and their classes:\n" );
     Vec_WecForEachLevel( vLits, vLevel, i )
     {
+        if ( Vec_IntSize(vLevel) == 0 )
+            continue;
         printf( "Rank %2d : %2d  ", i, Vec_IntSize(vLevel) );
         Vec_IntForEachEntry( vLevel, Entry, k )
             printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
@@ -162,13 +239,25 @@ void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits
     }
     if ( !fVerbose )
         return;
+    vSupp = Vec_IntAlloc( 100 );
+    vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
     Vec_WecForEachLevel( vLits, vLevel, i )
     {
-        if ( i != 20 )
+        //if ( i != 20 )
+        //    continue;
+        if ( Vec_IntSize(vLevel) == 0 )
             continue;
         Vec_IntForEachEntry( vLevel, Entry, k )
         {
             word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+/*
+            {
+                int iObj = Abc_Lit2Var(Entry);
+                Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
+                Gia_ManShow( pGia0, NULL, 0, 0, 0 );
+                Gia_ManStop( pGia0 );
+            }
+*/
             printf( "Rank = %4d : ", i );
             printf( "Obj = %4d  ", Abc_Lit2Var(Entry) );
             if ( Vec_IntSize(vSupp) > 6  )
@@ -218,7 +307,7 @@ int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
     Vec_IntFree( vRes );
     return nCommon;
 }
-void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
+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 );
     Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
@@ -229,14 +318,24 @@ void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * v
     {
         Vec_WecInsertLevel( vLits0, 0 );
         Vec_WecInsertLevel( vRoots0, 0 );
+        printf( "Shifted one level up.\n" );
     }
     else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
     {
         Vec_WecInsertLevel( vLits1, 0 );
         Vec_WecInsertLevel( vRoots1, 0 );
+        printf( "Shifted one level down.\n" );
     }
-    Vec_WecPrint( vRes0, 0 );
-    Vec_WecPrint( vRes1, 0 );
+    //printf( "Input literals:\n" );
+    //Vec_WecPrintLits( vLits0 );
+    printf( "Equiv classes:\n" );
+    Vec_WecPrintLits( vRes0 );
+    //printf( "Input literals:\n" );
+    //Vec_WecPrintLits( vLits1 );
+    printf( "Equiv classes:\n" );
+    Vec_WecPrintLits( vRes1 );
+    //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
+    //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
     Vec_WecFree( vRes0 );
     Vec_WecFree( vRes1 );
 }
@@ -250,10 +349,14 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
     Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
         Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
-    Acec_MatchCheckShift( pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
+    Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
     
     //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 );
 
     // reorder nodes to have the same order
     assert( pBox0->vShared == NULL );
@@ -350,8 +453,11 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
         printf( "Matching of adder trees in LHS and RHS succeeded.  " );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         // remove the last output
-        //Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
-        //Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
+        Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
+        Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
+
+        Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
+        Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
     }
     // solve regular CEC problem 
     Cec_ManCecSetDefaultParams( pCecPars );
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index cc5786bb..c49945db 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -71,8 +71,10 @@ extern Vec_Wec_t *   Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd
 extern Vec_Int_t *   Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
 extern Vec_Bit_t *   Acec_BoothFindPPG( Gia_Man_t * p );
 /*=== acecNorm.c ========================================================*/
+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 void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 /*=== acecUtil.c ========================================================*/
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 7f87df85..5e5ca688 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -450,6 +450,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose
     Hash_IntManStop( pHash );
     Ree_ManRemoveTrivial( p, vAdds );
     Ree_ManRemoveContained( p, vAdds );
+    //Ree_ManPrintAdders( vAdds, 1 );
     return vAdds;
 }
 
@@ -523,6 +524,10 @@ void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
         {
             pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
             pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+            // rule out if MAJ is a fanout of XOR
+            //if ( pObjX == Gia_ObjFanin0(pObjM) || pObjX == Gia_ObjFanin1(pObjM) )
+            //    continue;
+            // rule out if MAJ is a fanin of XOR and has no other fanouts
             if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
                 continue;
         }
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 295fd738..2b356574 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -66,6 +66,30 @@ void Acec_BoxFreeP( Acec_Box_t ** ppBox )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_VerifyBoxLeaves( Acec_Box_t * pBox, Vec_Bit_t * vIgnore )
+{
+    Vec_Int_t * vLevel;
+    int i, k, iLit, Count = 0;
+    if ( vIgnore == NULL )
+        return;
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( Gia_ObjIsAnd(Gia_ManObj(pBox->pGia, Abc_Lit2Var(iLit))) && !Vec_BitEntry(vIgnore, Abc_Lit2Var(iLit)) )
+                printf( "Internal node %d of rank %d is not part of PPG.\n", Abc_Lit2Var(iLit), i ), Count++;
+    printf( "Detected %d suspicious leaves.\n", Count );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Filters trees by removing TFO of roots.]
 
   Description []
@@ -103,6 +127,18 @@ 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 )
     {
+/*
+        if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
+        {
+            printf( "**** removing special one \n" );
+            continue;
+        }
+        if ( Vec_IntEntry(vAdds, 6*Box+3) == 48 && Vec_IntEntry(vAdds, 6*Box+4) == 49 )
+        {
+            printf( "**** removing special one \n" );
+            continue;
+        }
+*/
         if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
         {
             printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); 
@@ -125,6 +161,73 @@ void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees
 
 /**Function*************************************************************
 
+  Synopsis    [Filters trees by removing TFO of roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_TreeMarkTFI_rec( Gia_Man_t * p, int Id, Vec_Bit_t * vMarked )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, Id);
+    if ( Vec_BitEntry(vMarked, Id) )
+        return;
+    Vec_BitWriteEntry( vMarked, Id, 1 );
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId0(pObj, Id), vMarked );
+    Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId1(pObj, Id), vMarked );
+}
+void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+    Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+    Gia_Obj_t * pObj;
+    int i, k = 0, Box, Rank;
+    // mark leaves
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        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 );
+    }
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+3), 0 );
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4), 0 );
+    }
+    // mark TFI of leaves
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Vec_BitEntry(vIsLeaf, i) )
+            Acec_TreeMarkTFI_rec( p, i, vMarked );
+    // remove those that overlap with the marked TFI
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+        {
+            printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); 
+            continue;
+        }
+        Vec_IntWriteEntry( vTree, k++, Box );
+        Vec_IntWriteEntry( vTree, k++, Rank );
+    }
+    Vec_IntShrink( vTree, k );
+    Vec_BitFree( vIsLeaf );
+    Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+    Vec_Int_t * vLevel;
+    int i;
+    Vec_WecForEachLevel( vTrees, vLevel, i )
+        Acec_TreeFilterOne2( p, vAdds, vLevel );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -392,7 +495,7 @@ 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 );
+    Acec_TreeFilterTrees( p, vAdds, vTrees );
     // sort by size
     Vec_WecSort( vTrees, 1 );
     return vTrees;
@@ -437,20 +540,11 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
     {
         printf( " %4d : %2d  {", i, Vec_IntSize(vLevel) );
         Vec_IntForEachEntry( vLevel, iBox, k )
+        {
             printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox, 
                                      Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
-        printf( " }\n" );
-    }
-}
-void Vec_WecPrintLits( Vec_Wec_t * p )
-{
-    Vec_Int_t * vVec;
-    int i, k, Entry;
-    Vec_WecForEachLevel( p, vVec, i )
-    {
-        printf( " %4d : %2d  {", i, Vec_IntSize(vVec) );
-        Vec_IntForEachEntry( vVec, Entry, k )
-            printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
+            //printf( "(%d,%d,%d)", Vec_IntEntry(vAdds, 6*iBox+0), Vec_IntEntry(vAdds, 6*iBox+1), Vec_IntEntry(vAdds, 6*iBox+2) );
+        }
         printf( " }\n" );
     }
 }
@@ -505,7 +599,10 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
     Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
         Vec_IntForEachEntry( vLevel, Box, k )
             if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
+            {
+                //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box );
                 Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0, vVisit );
+            }
     Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
     Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds );
     Vec_BitFree( vVisit );
@@ -521,7 +618,14 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
                     Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
             for ( k = 3; k < 5; k++ )
                 if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
+                {
+                    //if ( Vec_IntEntry(vAdds, 6*Box+k) == 10942 )
+                    //{
+                    //    printf( "++++++++++++ Skipping special\n" );
+                    //    continue;
+                    //}
                     Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
+                }
             if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) )
                 Vec_WecPush( pBox->vLeafLits, i, 1 );
         }
@@ -531,8 +635,9 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
     Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
         Vec_IntSort( vLevel, 0 );
     Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
-        Vec_IntSort( vLevel, 0 );
+        Vec_IntSort( vLevel, 1 );
     //return pBox;
+/*
     // push literals forward
     //Vec_WecPrint( pBox->vLeafLits, 0 );
     Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
@@ -555,6 +660,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
         }
     }
     printf( "Pushed forward %d input literals.\n", Count );
+*/
     //Vec_WecPrint( pBox->vLeafLits, 0 );
     return pBox;
 }
@@ -607,13 +713,17 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
     Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
     Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
     if ( vTrees && Vec_WecSize(vTrees) > 0 )
+    {
         pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
+        Acec_VerifyBoxLeaves( pBox, vIgnore );
+    }
     if ( pBox )//&& fVerbose )
         printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
             0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
     if ( pBox && fVerbose )
         Acec_PrintBox( pBox, vAdds );
+    //Acec_PrintAdders( pBox0->vAdds, vAdds );
     //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
     Vec_WecFreeP( &vTrees );
     Vec_IntFree( vAdds );
diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c
index 191856cf..be12afef 100644
--- a/src/proof/acec/acecUtil.c
+++ b/src/proof/acec/acecUtil.c
@@ -90,6 +90,29 @@ void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
     Vec_IntFree( vXors );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupTopMostRange( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vTops = Vec_IntAlloc( 10 );
+    int i;
+    for ( i = 45; i < 52; i++ )
+        Vec_IntPush( vTops, Gia_ObjId( p, Gia_ObjFanin0(Gia_ManCo(p, i)) ) );
+    pNew = Gia_ManDupAndConesLimit( p, Vec_IntArray(vTops), Vec_IntSize(vTops), 100 );
+    Vec_IntFree( vTops );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////