Changes to arithmetic logic detection.

6 files changed, 724 insertions, 59 deletions

diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
new file mode 100644
index 00000000..32be3b30
--- /dev/null
+++ b/src/proof/acec/acecCl.c
@@ -0,0 +1,55 @@
+/**CFile****************************************************************
+
+  FileName    [acecCl.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecCl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index 1b73c36f..39f092b2 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -90,38 +90,30 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts )
+Vec_Wec_t * Gia_PolynComputeMap( Vec_Int_t * vAdds, int nObjs )
 {
-    Vec_Int_t * vOrder  = Vec_IntAlloc( 1000 );
-    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
-    Vec_Int_t * vRoots  = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) );
-    Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
-    Vec_Wec_t * vMap    = Vec_WecStart( Gia_ManObjNum(pGia) );
-    int i, k, Index, Driver, Entry1, Entry2 = -1;
     // map nodes driven by adders into adder indexes
-    for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
+    Vec_Wec_t * vMap = Vec_WecStart( nObjs );  int i;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
-        Entry1 = Vec_IntEntry( vAdds, 5*i + 3 );
-        Entry2 = Vec_IntEntry( vAdds, 5*i + 4 );
+        int Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
+        int Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
         Vec_WecPush( vMap, Entry1, i );
         Vec_WecPush( vMap, Entry1, Entry2 );
         Vec_WecPush( vMap, Entry2, i );
         Vec_WecPush( vMap, Entry2, Entry1 );
     }
-    // collect roots
-    Gia_ManForEachCoDriverId( pGia, Driver, i )
-    {
-        Vec_IntPush( vRoots, Driver );
-        Vec_BitWriteEntry( vIsRoot, Driver, 1 );
-    }
-    // collect additional outputs
-    Vec_IntForEachEntry( vAddCos, Driver, i )
-    {
-        Vec_IntPush( vRoots, Driver );
+    return vMap;
+}
+Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Int_t * vRoots, Vec_Int_t ** pvIns )
+{
+    Vec_Int_t * vOrder  = Vec_IntAlloc( 1000 );
+    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
+    int i, k, Index, Driver, Entry1, Entry2 = -1;
+    // mark roots
+    Vec_IntForEachEntry( vRoots, Driver, i )
         Vec_BitWriteEntry( vIsRoot, Driver, 1 );
-    }
-    // detect full adder tree
-    *pvOuts = Vec_IntDup( vRoots );
+    // collect boxes
     while ( 1 )
     {
         // iterate through boxes driving this one
@@ -143,9 +135,9 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
             Vec_IntRemove( vRoots, Entry1 );
             Vec_IntRemove( vRoots, Entry2 );
             // set new marks
-            Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
-            Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
-            Driver = Vec_IntEntry( vAdds, 5*Index + 2 );
+            Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
+            Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
+            Driver = Vec_IntEntry( vAdds, 6*Index + 2 );
             Vec_BitWriteEntry( vIsRoot, Entry1, 1 );
             Vec_BitWriteEntry( vIsRoot, Entry2, 1 );
             Vec_BitWriteEntry( vIsRoot, Driver, 1 );
@@ -158,19 +150,99 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
             break;
     }
     // collect remaining leaves
-    Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
-        if ( Driver )
-            Vec_IntPush( vLeaves, i );
-    *pvIns = vLeaves;
-    // cleanup
+    if ( pvIns )
+    {
+        *pvIns = Vec_IntAlloc( Vec_BitSize(vIsRoot) );
+        Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
+            if ( Driver )
+                Vec_IntPush( *pvIns, i );
+    }
     Vec_BitFree( vIsRoot );
+    return vOrder;
+}
+Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts )
+{
+    Vec_Int_t * vOrder;
+    Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
+    Vec_Int_t * vRoots = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    int i, Driver;
+    // collect roots
+    Gia_ManForEachCoDriverId( pGia, Driver, i )
+        Vec_IntPush( vRoots, Driver );
+    // collect additional outputs
+    if ( vAddCos )
+        Vec_IntForEachEntry( vAddCos, Driver, i )
+            Vec_IntPush( vRoots, Driver );
+    // remember roots
+    if ( pvOuts )
+        *pvOuts = Vec_IntDup( vRoots );
+    // create order
+    vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, pvIns );
     Vec_IntFree( vRoots );
     Vec_WecFree( vMap );
+    printf( "Collected %d boxes.\n", Vec_IntSize(vOrder) );
     return vOrder;
 }
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_PolyCollectRoots_rec( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
+{
+    int k;
+    for ( k = 0; k < 3; k++ )
+    {
+        int i, Index, Sum, Carry = Vec_IntEntry( vAdds, 6*iBox+k );
+        Vec_Int_t * vLevel = Vec_WecEntry( vMap, Carry );
+        if ( Carry == 0 )
+            continue;
+        Vec_IntForEachEntryDouble( vLevel, Index, Sum, i )
+            if ( Vec_IntEntry(vAdds, 6*Index+4) == Carry && !Vec_BitEntry(vMarks, Sum) )
+            {
+                Vec_IntPush( vRoots, Sum );
+                Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, Index, vRoots );
+            }
+    }
+}
+void Gia_PolyCollectRoots( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
+{
+    Vec_IntClear( vRoots );
+    Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+3) );
+    Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+4) );
+    Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, iBox, vRoots );
+}
+Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes )
+{
+    extern Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds );
+    Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( pGia, vAdds );
+    Vec_Wec_t * vMap   = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
+    Vec_Wec_t * vRes   = Vec_WecStart( Vec_IntSize(vRootBoxes) );
+    Vec_Int_t * vRoots = Vec_IntAlloc( 64 );
+    Vec_Int_t * vOrder;
+    int i, iBox;
+    Vec_IntForEachEntry( vRootBoxes, iBox, i )
+    {
+        Gia_PolyCollectRoots( vAdds, vMap, vMarks, iBox, vRoots );
+        vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, NULL );
+        Vec_IntAppend( Vec_WecEntry(vRes, i), vOrder );
+        Vec_IntFree( vOrder );
+    }
+    Vec_BitFree( vMarks );
+    Vec_IntFree( vRoots );
+    Vec_WecFree( vMap );
+    return vRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collect internal node order.]
 
   Description []
@@ -197,15 +269,15 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t
     Vec_IntForEachEntryReverse( vOrder, Index, i )
     {
         // mark inputs
-        Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
-        Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
-        Entry3 = Vec_IntEntry( vAdds, 5*Index + 2 );
+        Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
+        Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
+        Entry3 = Vec_IntEntry( vAdds, 6*Index + 2 );
         Vec_BitWriteEntry( vVisited, Entry1, 1 );
         Vec_BitWriteEntry( vVisited, Entry2, 1 );
         Vec_BitWriteEntry( vVisited, Entry3, 1 );
         // traverse from outputs
-        Entry1 = Vec_IntEntry( vAdds, 5*Index + 3 );
-        Entry2 = Vec_IntEntry( vAdds, 5*Index + 4 );
+        Entry1 = Vec_IntEntry( vAdds, 6*Index + 3 );
+        Entry2 = Vec_IntEntry( vAdds, 6*Index + 4 );
         Gia_PolynCoreCollect_rec( pGia, Entry1, vNodes, vVisited );
         Gia_PolynCoreCollect_rec( pGia, Entry2, vNodes, vVisited );
     }
@@ -325,7 +397,7 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos,
     //Gia_ManShow( pGia, vNodes, 0 );
     
     printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ", 
-        Vec_IntSize(vAdds)/5, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
+        Vec_IntSize(vAdds)/6, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose );
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
new file mode 100644
index 00000000..11d68d37
--- /dev/null
+++ b/src/proof/acec/acecPa.c
@@ -0,0 +1,282 @@
+/**CFile****************************************************************
+
+  FileName    [acecPa.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecPa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pas_ManVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Truth0, Truth1;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->Value;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjIsXor(pObj) );
+    Truth0 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
+    Truth1 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
+    Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
+    Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
+    return (pObj->Value = Truth0 & Truth1);
+}
+void Pas_ManVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
+{
+    Gia_Obj_t * pObj;
+    unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
+    int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
+
+    if ( !fFadd )
+        return;
+
+    Gia_ManIncrementTravId( p );
+    for ( k = 0; k < 3; k++ )
+    {
+        iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+        if ( iObj == 0 )
+            continue;
+        pObj = Gia_ManObj( p, iObj );
+        pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    }
+
+    iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
+    TruthXor = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+    TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
+
+    iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
+    TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+    TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
+
+    if ( fFadd ) // FADD
+    {
+        if ( TruthXor != 0x96 )
+            printf( "Fadd %d sum is wrong.\n", iBox );
+        if ( TruthMaj != 0xE8 )
+            printf( "Fadd %d carry is wrong.\n", iBox );
+    }
+    else
+    {
+        if ( TruthXor != 0x66 )
+            printf( "Hadd %d sum is wrong.\n", iBox );
+        if ( TruthMaj != 0x88 )
+            printf( "Hadd %d carry is wrong.\n", iBox );
+    }
+}
+void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase )
+{
+    int k, iBox;
+    Vec_IntForEachEntry( vOrder, iBox, k )
+        Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase )
+{
+    int k, iBox, iXor, Sign, fXorPhase;
+    assert( pObj != Gia_ManConst0(p) );
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( fPhase )
+        Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase );
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) );
+    if ( iBox == -1 )
+        return;
+    iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
+    Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
+    fXorPhase = ((Sign >> 3) & 1);
+    // remember complemented HADD
+    if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase )
+        Vec_BitWriteEntry( vConstPhase, iBox, 1 );
+    for ( k = 0; k < 3; k++ )
+    {
+        int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+        int fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
+        fXorPhase ^= fPhaseThis;
+        if ( iObj == 0 )
+            continue;
+        Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase );
+    }
+    Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
+}
+Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase )
+{
+    Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) );
+    Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+    int i, iRoot;
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vRoots, iRoot, i )
+        Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase );
+    *pvConstPhase = vConstPhase;
+    return vPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts )
+{
+    Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
+    Vec_Bit_t * vPhase, * vConstPhase;
+    int i, k, Entry, nTrees;
+
+    // map carries into adder indexes and mark driven nodes
+    Vec_IntForEachEntry( vOrder, i, k )
+    {
+        int Carry = Vec_IntEntry(vAdds, 6*i+4);
+        if ( Vec_BitEntry(vUnique, Carry) )
+            printf( "Carry %d participates more than once.\n", Carry );
+        Vec_BitWriteEntry( vUnique, Carry, 1 );
+        Vec_IntWriteEntry( vMap, Carry, i );
+        // mark driven 
+        Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 );
+        Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 );
+        Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 );
+    }
+    // collect carries that do not drive other adders
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) )
+            Vec_IntPush( vRoots, i );
+    nTrees = Vec_IntSize( vRoots );
+
+    Vec_IntPrint( vRoots );
+
+    // compute phases
+    if ( Vec_IntSize(vRoots) > 0 )
+    {
+        int nCompls = 0;
+
+        vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase );
+        Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase );
+
+        printf( "Outputs: " );
+        Vec_IntForEachEntry( vOuts, Entry, i )
+            printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+        printf( "\n" );
+
+        printf( "Inputs: " );
+        Vec_IntForEachEntry( vIns, Entry, i )
+        {
+            printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+            nCompls += Vec_BitEntry(vPhase, Entry);
+        }
+        printf( "   Compl = %d\n", nCompls );
+
+        Vec_BitFreeP( &vPhase );
+        Vec_BitFreeP( &vConstPhase );
+    }
+
+    Vec_IntFree( vRoots );
+    Vec_IntFree( vMap );
+    Vec_BitFree( vUnique );
+    Vec_BitFree( vUsed );
+    return nTrees;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pas_ManComputeCutsTest( Gia_Man_t * p )
+{
+    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
+    extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts );
+
+    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
+    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+    Vec_Int_t * vIns, * vOuts;
+    Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts );
+    int nTrees, nFadds = Ree_ManCountFadds( vAdds );
+    //Ree_ManPrintAdders( vAdds, 1 );
+    printf( "Detected %d FAs and %d HAs.  Collected %d adders.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    // detect trees
+    clk = Abc_Clock();
+    nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts );
+    Vec_IntFree( vAdds );
+    Vec_IntFree( vOrder );
+    Vec_IntFree( vIns );
+    Vec_IntFree( vOuts );
+
+    printf( "Detected %d adder trees. ", nTrees );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c
new file mode 100644
index 00000000..294066fa
--- /dev/null
+++ b/src/proof/acec/acecPool.c
@@ -0,0 +1,132 @@
+/**CFile****************************************************************
+
+  FileName    [acecPool.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecPool.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+    Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(p) );
+    int i, k;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+        for ( k = 0; k < 3; k++ )
+            Vec_BitWriteEntry( vMarks, Vec_IntEntry(vAdds, 6*i+k), 1 );
+    return vMarks;
+}
+
+Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+    int i, k, iTop, fVerbose = 0;
+    Vec_Int_t * vTops = Vec_IntAlloc( 1000 );
+    Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( p, vAdds );
+
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+        if ( !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+3)) && 
+             !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+4)) )
+            Vec_IntPush( vTops, i );
+
+    if ( fVerbose )
+    Vec_IntForEachEntry( vTops, iTop, i )
+    {
+        printf( "%4d : ", iTop );
+        for ( k = 0; k < 3; k++ )
+            printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+        printf( " -> " );
+        for ( k = 3; k < 5; k++ )
+            printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+        printf( "\n" );
+    }
+
+    Vec_BitFree( vMarks );
+    return vTops;
+}
+void Acec_ManPool( Gia_Man_t * p )
+{
+    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
+    extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
+
+    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
+    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
+    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
+    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
+    Vec_Int_t * vTops, * vTree;
+    Vec_Wec_t * vTrees;
+
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+    int i, nFadds = Ree_ManCountFadds( vAdds );
+    printf( "Detected %d FAs and %d HAs.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+    clk = Abc_Clock();
+    Ree_ManRemoveTrivial( p, vAdds );
+    Ree_ManRemoveContained( p, vAdds );
+    nFadds = Ree_ManCountFadds( vAdds );
+    printf( "Detected %d FAs and %d HAs.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+    //Ree_ManPrintAdders( vAdds, 1 );
+
+    // detect topmost nodes
+    vTops = Acec_ManPoolTopMost( p, vAdds );
+    printf( "Detected %d topmost adder%s.\n", Vec_IntSize(vTops), Vec_IntSize(vTops) > 1 ? "s":"" );
+
+    // collect adder trees
+    vTrees = Gia_PolynCoreOrderArray( p, vAdds, vTops );
+    Vec_WecForEachLevel( vTrees, vTree, i )
+        printf( "Adder %5d : Tree with %5d nodes.\n", Vec_IntEntry(vTops, i), Vec_IntSize(vTree) );
+
+    Vec_WecFree( vTrees );
+    Vec_IntFree( vAdds );
+    Vec_IntFree( vTops );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 1f10d249..e2340dba 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -69,6 +69,18 @@ void Ree_TruthPrecompute()
     }
     printf( "\n" );
 }
+void Ree_TruthPrecompute2()
+{
+    int i, b;
+    for ( i = 0; i < 8; i++ )
+    {
+        word Truth = 0xE8;
+        for ( b = 0; b < 3; b++ )
+            if ( (i >> b) & 1 )
+                Truth = Abc_Tt6Flip( Truth, b );
+        printf( "%d = %X\n", i, 0xFF & (int)Truth );
+    }
+}
 
 /**Function*************************************************************
 
@@ -239,7 +251,7 @@ void Ree_ManCutPrint( int * pCut, int Count, word Truth )
 void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData )
 {
     int fVerbose = 0;
-    int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[5], Count = 0;
+    int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[6], Count = 0;
     if ( fVerbose )
         printf( "Object %d\n", iObj );
     Vec_IntFill( vCuts, 2, 1 );
@@ -290,7 +302,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
 ***********************************************************************/
 Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
 {
-    int i, j, k, iObj, iObj2, Value, Truth, CountX, CountM, Index = 0;
+    int i, j, k, iObj, iObj2, Value, Truth, Truth2, CountX, CountM, Index = 0;
     int nEntries = Hash_IntManEntryNum(p);
     Vec_Int_t * vAdds = Vec_IntAlloc( 1000 );
     Vec_Int_t * vXors = Vec_IntStart( nEntries + 1 );
@@ -325,9 +337,9 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
         if ( Index == -1 )
             continue;
         if ( Truth == 0x66 || Truth == 0x99 || Truth == 0x69 || Truth == 0x96 )
-            Vec_WecPush( vXorMap, Index, iObj );
+            Vec_IntPushTwo( Vec_WecEntry(vXorMap, Index), iObj, Truth );
         else
-            Vec_WecPush( vMajMap, Index, iObj );
+            Vec_IntPushTwo( Vec_WecEntry(vMajMap, Index), iObj, Truth );
     }
     Vec_IntFree( vIndex );
     // create pairs
@@ -336,11 +348,22 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
         Vec_Int_t * vXorOne = Vec_WecEntry( vXorMap, i );
         Vec_Int_t * vMajOne = Vec_WecEntry( vMajMap, i );
         Hash_IntObj_t * pObj = Hash_IntObj( p, Value );
-        Vec_IntForEachEntry( vXorOne, iObj, j )
-        Vec_IntForEachEntry( vMajOne, iObj2, k )
+        Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
+        Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
         {
+            int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
+            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++ )
+                if ( Truth2 == SignMaj[n] )
+                    break;
+            if ( n == 8 ) 
+                for ( n = 0; n < 8; n++ )
+                    if ( Truth2 == SignAnd[n] )
+                        break;
+            assert( n < 8 );
             Vec_IntPushThree( vAdds, pObj->iData0, pObj->iData1, pObj->iData2 ); 
-            Vec_IntPushTwo( vAdds, iObj, iObj2 );
+            Vec_IntPushThree( vAdds, iObj, iObj2, SignXor | n );
         }
     }
     Vec_IntFree( vIndexRev );
@@ -384,7 +407,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
     vAdds = Ree_ManDeriveAdds( pHash, vData );
     if ( fVerbose )
         printf( "Adds = %d.  Total = %d.  Hashed = %d.  Hashed/Adds = %.2f.\n", 
-            Vec_IntSize(vAdds)/5, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 5.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
+            Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
     Vec_IntFree( vData );
     Hash_IntManStop( pHash );
     return vAdds;
@@ -392,6 +415,52 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Highlight nodes inside FAs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ree_CollectInsiders_rec( Gia_Man_t * pGia, int iObj, Vec_Bit_t * vVisited, Vec_Bit_t * vInsiders )
+{
+    if ( Vec_BitEntry(vVisited, iObj) )
+        return;
+    Vec_BitSetEntry( vVisited, iObj, 1 );
+    Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId0p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+    Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId1p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+    Vec_BitSetEntry( vInsiders, iObj, 1 );
+}
+Vec_Bit_t * Ree_CollectInsiders( Gia_Man_t * pGia, Vec_Int_t * vAdds )
+{
+    Vec_Bit_t * vVisited = Vec_BitStart( Gia_ManObjNum(pGia) );
+    Vec_Bit_t * vInsiders = Vec_BitStart( Gia_ManObjNum(pGia) );
+    int i, Entry1, Entry2, Entry3;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+    {
+        if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+            continue;
+        // mark inputs
+        Entry1 = Vec_IntEntry( vAdds, 6*i + 0 );
+        Entry2 = Vec_IntEntry( vAdds, 6*i + 1 );
+        Entry3 = Vec_IntEntry( vAdds, 6*i + 2 );
+        Vec_BitWriteEntry( vVisited, Entry1, 1 );
+        Vec_BitWriteEntry( vVisited, Entry2, 1 );
+        Vec_BitWriteEntry( vVisited, Entry3, 1 );
+        // traverse from outputs
+        Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
+        Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
+        Ree_CollectInsiders_rec( pGia, Entry1, vVisited, vInsiders );
+        Ree_CollectInsiders_rec( pGia, Entry2, vVisited, vInsiders );
+    }
+    Vec_BitFree( vVisited );
+    return vInsiders;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -401,28 +470,80 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Ree_ManComputeCutsTest( Gia_Man_t * p )
+// removes HAs whose AND2 is part of XOR2 without additional fanout
+void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+    Gia_Obj_t * pObjX, * pObjM;
+    int i, k = 0;
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+    {
+        if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+        {
+            pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
+            pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+            if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
+                continue;
+        }
+        memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+    }
+    assert( k <= i );
+    Vec_IntShrink( vAdds, 6*k );
+}
+// removes HAs fully contained inside FAs
+void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+    Vec_Bit_t * vInsiders = Ree_CollectInsiders( p, vAdds );
+    int i, k = 0;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+    {
+        if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+            if ( Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+4)) )
+                continue;
+        memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+    }
+    assert( k <= i );
+    Vec_IntShrink( vAdds, 6*k );
+    Vec_BitFree( vInsiders );
+}
+
+int Ree_ManCountFadds( Vec_Int_t * vAdds )
 {
-    abctime clk = Abc_Clock();
-    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
     int i, Count = 0;
-    for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+        if ( Vec_IntEntry(vAdds, 6*i+2) != 0 )
+            Count++;
+    return Count;
+}
+void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose )
+{
+    int i;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
-        if ( Vec_IntEntry(vAdds, 5*i+2) == 0 )
+        //if ( Vec_IntEntry(vAdds, 6*i+2) == 0 )
+        //    continue;
+        if ( !fVerbose )
             continue;
-        Count++;
-        continue;
         printf( "%6d : ", i );
-        printf( "%6d ", Vec_IntEntry(vAdds, 5*i+0) );
-        printf( "%6d ", Vec_IntEntry(vAdds, 5*i+1) );
-        printf( "%6d ", Vec_IntEntry(vAdds, 5*i+2) );
+        printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) );
+        printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) );
+        printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) );
         printf( "   ->  " );
-        printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) );
-        printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) );
+        printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) );
+        printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) );
+        printf( "  (%d)", Vec_IntEntry(vAdds, 6*i+5) );
         printf( "\n" );
     }
+}
+void Ree_ManComputeCutsTest( Gia_Man_t * p )
+{
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+    int nFadds = Ree_ManCountFadds( vAdds );
+    Ree_ManPrintAdders( vAdds, 1 );
+    printf( "Detected %d FAs and %d HAs.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
     Vec_IntFree( vAdds );
-    printf( "Detected %d FAs and %d HAs.  ", Count, Vec_IntSize(vAdds)/5-Count );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index e66bf6e8..df6db695 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,7 +1,10 @@
-SRC +=    src/proof/acec/acecCore.c \
+SRC +=    src/proof/acec/acecCl.c \
+    src/proof/acec/acecCore.c \
     src/proof/acec/acecCo.c \
     src/proof/acec/acecRe.c \
+    src/proof/acec/acecPa.c \
     src/proof/acec/acecPo.c \
+    src/proof/acec/acecPool.c \
     src/proof/acec/acecCover.c \
     src/proof/acec/acecFadds.c \
     src/proof/acec/acecOrder.c \