Experiments with don't-cares.

7 files changed, 1387 insertions, 9 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 0068855a..1853ce2e 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -787,10 +787,6 @@ SOURCE=.\src\base\wlc\wlcAbs.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\base\wlc\wlcPth.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\wlc\wlcAbs2.c
 # End Source File
 # Begin Source File
@@ -815,6 +811,10 @@ SOURCE=.\src\base\wlc\wlcNtk.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wlc\wlcPth.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wlc\wlcReadSmt.c
 # End Source File
 # Begin Source File
@@ -1073,6 +1073,14 @@ SOURCE=.\src\base\acb\acbCom.c
 
 SOURCE=.\src\base\acb\acbFunc.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\base\acb\acbMfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\acb\acbUtil.c
+# End Source File
 # End Group
 # End Group
 # Begin Group "bdd"
@@ -5687,6 +5695,10 @@ SOURCE=.\src\proof\acec\acec.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\acec\acec2Booth.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\acec\acecBo.c
 # End Source File
 # Begin Source File
diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
index c9d2128d..0eaf7a47 100644
--- a/src/base/acb/acb.h
+++ b/src/base/acb/acb.h
@@ -64,6 +64,8 @@ struct Acb_Ntk_t_
     int             nRegs;      // flop count
     int             nFaninMax;  // default fanin count
     int             nObjTravs;  // trav ID
+    int             LevelMax;   // max level
+    int             nPaths;     // the number of paths
     // stucture
     Vec_Str_t       vObjType;   // type     
     Vec_Int_t       vObjFans;   // fanin offsets
@@ -82,6 +84,10 @@ struct Acb_Ntk_t_
     Vec_Int_t       vAttrSto;   // attribute storage
     Vec_Int_t       vNtkObjs;   // instances
     Vec_Int_t       vTargets;   // targets
+    Vec_Int_t       vLevelD;    // level
+    Vec_Int_t       vLevelR;    // level
+    Vec_Int_t       vPathD;     // path
+    Vec_Int_t       vPathR;     // path
     // other
     Vec_Int_t       vArray0;
     Vec_Int_t       vArray1;
@@ -166,11 +172,12 @@ static inline void           Acb_NtkSetRegNum( Acb_Ntk_t * p, int nRegs )    { p
 static inline int            Acb_NtkPiNum( Acb_Ntk_t * p )                   { return Acb_NtkCiNum(p) - Acb_NtkRegNum(p);                                                  }
 static inline int            Acb_NtkPoNum( Acb_Ntk_t * p )                   { return Acb_NtkCoNum(p) - Acb_NtkRegNum(p);                                                  }
 static inline int            Acb_NtkCioOrderNum( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vOrder);                                                             }
-static inline int            Acb_NtkObjNum( Acb_Ntk_t * p )                  { return Vec_StrSize(&p->vObjType)-1;                                                         }
 static inline int            Acb_NtkObjNumAlloc( Acb_Ntk_t * p )             { return Vec_StrCap(&p->vObjType)-1;                                                          }
+static inline int            Acb_NtkObjNum( Acb_Ntk_t * p )                  { return Vec_StrSize(&p->vObjType)-1;                                                         }
+static inline int            Acb_NtkObjNumMax( Acb_Ntk_t * p )               { return Vec_StrSize(&p->vObjType);                                                           }
 static inline int            Acb_NtkTypeNum( Acb_Ntk_t * p, int Type )       { return Vec_StrCountEntry(&p->vObjType, (char)Type);                                         }
-static inline int            Acb_NtkBoxNum( Acb_Ntk_t * p )                  { return Acb_NtkTypeNum(p, ABC_OPER_BOX);                                                      }
-static inline int            Acb_NtkNodeNum( Acb_Ntk_t * p )                 { return Vec_StrCountLarger(&p->vObjType, (char)ABC_OPER_BOX);                                 }
+static inline int            Acb_NtkBoxNum( Acb_Ntk_t * p )                  { return Acb_NtkTypeNum(p, ABC_OPER_BOX);                                                     }
+static inline int            Acb_NtkNodeNum( Acb_Ntk_t * p )                 { return Vec_StrCountLarger(&p->vObjType, (char)ABC_OPER_BOX);                                }
 static inline int            Acb_NtkSeqNum( Acb_Ntk_t * p )                  { return Vec_IntSize(&p->vSeq);                                                               }
 
 static inline void           Acb_NtkCleanObjCopies( Acb_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy,  Vec_StrCap(&p->vObjType), -1);                                   }
@@ -181,6 +188,10 @@ static inline void           Acb_NtkCleanObjNames( Acb_Ntk_t * p )           { V
 static inline void           Acb_NtkCleanObjRanges( Acb_Ntk_t * p )          { Vec_IntFill(&p->vObjRange, Vec_StrCap(&p->vObjType),  0);                                   }
 static inline void           Acb_NtkCleanObjTravs( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjTrav,  Vec_StrCap(&p->vObjType),  0);                                   }
 static inline void           Acb_NtkCleanObjAttrs( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjAttr,  Vec_StrCap(&p->vObjType),  0); Vec_IntFill(&p->vAttrSto, 1, -1); }
+static inline void           Acb_NtkCleanObjLevelD( Acb_Ntk_t * p )          { Vec_IntFill(&p->vLevelD,   Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjLevelR( Acb_Ntk_t * p )          { Vec_IntFill(&p->vLevelR,   Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjPathD( Acb_Ntk_t * p )           { Vec_IntFill(&p->vPathD,    Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjPathR( Acb_Ntk_t * p )           { Vec_IntFill(&p->vPathR,    Vec_StrCap(&p->vObjType),  0);                                   }
 
 static inline int            Acb_NtkHasObjCopies( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vObjCopy)  > 0; }
 static inline int            Acb_NtkHasObjFuncs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjFunc)  > 0; }
@@ -190,6 +201,10 @@ static inline int            Acb_NtkHasObjNames( Acb_Ntk_t * p )             { r
 static inline int            Acb_NtkHasObjRanges( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vObjRange) > 0; }
 static inline int            Acb_NtkHasObjTravs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjTrav)  > 0; }
 static inline int            Acb_NtkHasObjAttrs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjAttr)  > 0; }
+static inline int            Acb_NtkHasObjLevelD( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vLevelD)   > 0; }
+static inline int            Acb_NtkHasObjLevelR( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vLevelR)   > 0; }
+static inline int            Acb_NtkHasObjPathD( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vPathD)    > 0; }
+static inline int            Acb_NtkHasObjPathR( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vPathR)    > 0; }
 
 static inline void           Acb_NtkFreeObjCopies( Acb_Ntk_t * p )           { Vec_IntErase(&p->vObjCopy);            }
 static inline void           Acb_NtkFreeObjFuncs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjFunc);            }
@@ -199,6 +214,10 @@ static inline void           Acb_NtkFreeObjNames( Acb_Ntk_t * p )            { V
 static inline void           Acb_NtkFreeObjRanges( Acb_Ntk_t * p )           { Vec_IntErase(&p->vObjRange);           }
 static inline void           Acb_NtkFreeObjTravs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjTrav);            }
 static inline void           Acb_NtkFreeObjAttrs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjAttr);            }
+static inline void           Acb_NtkFreeObjLevelD( Acb_Ntk_t * p )           { Vec_IntErase(&p->vLevelD);             }
+static inline void           Acb_NtkFreeObjLevelR( Acb_Ntk_t * p )           { Vec_IntErase(&p->vLevelR);             }
+static inline void           Acb_NtkFreeObjPathD( Acb_Ntk_t * p )            { Vec_IntErase(&p->vPathD);              }
+static inline void           Acb_NtkFreeObjPathR( Acb_Ntk_t * p )            { Vec_IntErase(&p->vPathR);              }
 
 static inline Acb_ObjType_t  Acb_ObjType( Acb_Ntk_t * p, int i )             { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i);        }
 static inline void           Acb_ObjCleanType( Acb_Ntk_t * p, int i )        { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE );                      }
@@ -233,6 +252,10 @@ static inline int            Acb_ObjAttr( Acb_Ntk_t * p, int i )             { a
 static inline int            Acb_ObjAttrSize( Acb_Ntk_t * p, int i )         { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0;  }
 static inline int *          Acb_ObjAttrArray( Acb_Ntk_t * p, int i )        { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; }
 static inline int            Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2)  if (a[k] == x) return a[k+1]; return 0; }
+static inline int            Acb_ObjLevelD( Acb_Ntk_t * p, int i )           { assert(i>0); return Vec_IntEntry(&p->vLevelD, i);                                            }
+static inline int            Acb_ObjLevelR( Acb_Ntk_t * p, int i )           { assert(i>0); return Vec_IntEntry(&p->vLevelR, i);                                            }
+static inline int            Acb_ObjPathD( Acb_Ntk_t * p, int i )            { assert(i>0); return Vec_IntEntry(&p->vPathD, i);                                             }
+static inline int            Acb_ObjPathR( Acb_Ntk_t * p, int i )            { assert(i>0); return Vec_IntEntry(&p->vPathR, i);                                             }
 
 static inline void           Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x );                      }
 static inline void           Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjFunc(p, i) ==  0); Vec_IntSetEntry( &p->vObjFunc, i, x );                      }
@@ -240,6 +263,14 @@ static inline void           Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { a
 static inline void           Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) ==  0);Vec_WrdSetEntry( &p->vObjTruth, i, x );                     }
 static inline void           Acb_ObjSetName( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjName(p, i) ==  0); Vec_IntSetEntry( &p->vObjName, i, x );                      }
 static inline void           Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s )  { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s);  }
+static inline int            Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelD, i, x );  return x;                                             }
+static inline int            Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelR, i, x );  return x;                                             }
+static inline int            Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x )  { Vec_IntSetEntry( &p->vPathD, i, x );   return x;                                             }
+static inline int            Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x )  { Vec_IntSetEntry( &p->vPathR, i, x );   return x;                                             }
+static inline int            Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x );  return x;                                       }
+static inline int            Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x );  return x;                                       }
+static inline int            Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x )  { Vec_IntAddToEntry( &p->vPathD, i, x );   return x;                                         }
+static inline int            Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x )  { Vec_IntAddToEntry( &p->vPathR, i, x );   return x;                                         }
 
 static inline int            Acb_ObjNtkId( Acb_Ntk_t * p, int i )            { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0;      }
 static inline Acb_Ntk_t *    Acb_ObjNtk( Acb_Ntk_t * p, int i )              { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i));                                       }
@@ -282,6 +313,8 @@ static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )               { i
     for ( i = 0; (i < Acb_NtkCoNum(p))  && (((iObj) = Acb_NtkCo(p, i)), 1); i++ ) 
 #define Acb_NtkForEachCoDriver( p, iObj, i )                              \
     for ( i = 0; (i < Acb_NtkCoNum(p))  && (((iObj) = Acb_ObjFanin(p, Acb_NtkCo(p, i), 0)), 1); i++ ) 
+#define Acb_NtkForEachCoAndDriver( p, iObj, iDriver, i )                  \
+    for ( i = 0; (i < Acb_NtkCoNum(p))  && (((iObj) = Acb_NtkCo(p, i)), 1)  && (((iDriver) = Acb_ObjFanin(p, iObj, 0)), 1); i++ ) 
 
 #define Acb_NtkForEachCiVec( vVec, p, iObj, i )                           \
     for ( i = 0; (i < Vec_IntSize(vVec))  && (((iObj) = Acb_NtkCi(p, Vec_IntEntry(vVec,i))), 1); i++ ) 
@@ -298,8 +331,12 @@ static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )               { i
 
 #define Acb_NtkForEachObj( p, i )                                         \
     for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) ) {} else   
-#define Acb_NtkForEachNode( p, i )                                         \
+#define Acb_NtkForEachObjReverse( p, i )                                  \
+    for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) ) {} else   
+#define Acb_NtkForEachNode( p, i )                                        \
     for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else   
+#define Acb_NtkForEachNodeReverse( p, i )                                 \
+    for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else   
 #define Acb_NtkForEachObjType( p, Type, i )                               \
     for ( i = 1; i < Vec_StrSize(&p->vObjType) && (((Type) = Acb_ObjType(p, i)), 1); i++ ) if ( !Type ) {} else
 #define Acb_NtkForEachBox( p, i )                                         \
@@ -310,6 +347,9 @@ static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )               { i
 #define Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )            \
     for ( k = 0, pFanins = Acb_ObjFanins(p, iObj); k < pFanins[0] && ((iFanin = pFanins[k+1]), 1); k++ )
 
+#define Acb_ObjForEachFanout( p, iObj, iFanout, k )                       \
+    Vec_IntForEachEntry( Vec_WecEntry(&p->vFanouts, iObj), iFanout, k ) if ( !Acb_ObjType(p, iFanout) ) {} else 
+
 #define Acb_ObjForEachFon( p, iObj, iFon )                                \
     for ( assert(Acb_ObjIsBox(p, iObj)), iFon = iObj + 1; iFon < Acb_NtkObjNum(p) && Acb_ObjIsFon(p, iFon); iFon++ ) 
 
@@ -446,6 +486,10 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
     Vec_IntErase( &p->vAttrSto );    
     Vec_IntErase( &p->vNtkObjs );    
     Vec_IntErase( &p->vTargets );    
+    Vec_IntErase( &p->vLevelD );    
+    Vec_IntErase( &p->vLevelR );    
+    Vec_IntErase( &p->vPathD );    
+    Vec_IntErase( &p->vPathR );    
     // other
     Vec_IntErase( &p->vArray0 );    
     Vec_IntErase( &p->vArray1 );    
diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c
new file mode 100644
index 00000000..9d44ae3f
--- /dev/null
+++ b/src/base/acb/acbMfs.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [acb.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acb.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
new file mode 100644
index 00000000..4dcae435
--- /dev/null
+++ b/src/base/acb/acbUtil.c
@@ -0,0 +1,340 @@
+/**CFile****************************************************************
+
+  FileName    [acbUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acbUtil.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkCreateFanout( Acb_Ntk_t * p )
+{
+    int k, iObj, iFanin, * pFanins; 
+    Vec_WecInit( &p->vFanouts, Acb_NtkObjNumMax(p) );
+    Acb_NtkForEachObj( p, iObj )
+        Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+            Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm )
+{
+    int * pFanin, iFanin, i;
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( !fTerm && Acb_ObjIsCi(p, iObj) )
+        return;
+    Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
+        Acb_ObjCollectTfi_rec( p, iFanin, fTerm );
+    Vec_IntPush( &p->vArray0, iObj );
+}
+Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm )
+{
+    Vec_IntClear( &p->vArray0 );
+    Acb_NtkIncTravId( p );
+    Acb_ObjCollectTfi_rec( p, iObj, fTerm );
+    return &p->vArray0;
+}
+
+void Acb_ObjCollectTfo_rec( Acb_Ntk_t * p, int iObj, int fTerm )
+{
+    int iFanout, i;
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( !fTerm && Acb_ObjIsCo(p, iObj) )
+        return;
+    Acb_ObjForEachFanout( p, iObj, iFanout, i )
+        Acb_ObjCollectTfo_rec( p, iFanout, fTerm );
+    Vec_IntPush( &p->vArray1, iObj );
+}
+Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm )
+{
+    Vec_IntClear( &p->vArray1 );
+    Acb_NtkIncTravId( p );
+    Acb_ObjCollectTfo_rec( p, iObj, fTerm );
+    return &p->vArray1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj )
+{
+    int * pFanins, iFanin, k, Level = 0;
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+        Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iFanin) );
+    return Acb_ObjSetLevelD( p, iObj, Level + !Acb_ObjIsCio(p, iObj) );
+}
+int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
+{
+    int i, iObj, Level = 0;
+    if ( vTfo == NULL )
+    {
+        Acb_NtkCleanObjLevelD( p );
+        Acb_NtkForEachObj( p, iObj )
+            Acb_ObjComputeLevelD( p, iObj );
+    }
+    else
+    {
+        // it is assumed that vTfo contains CO nodes and level of new nodes was already updated
+        Vec_IntForEachEntry( vTfo, iObj, i )
+            Acb_ObjComputeLevelD( p, iObj );
+    }
+    Acb_NtkForEachCo( p, iObj, i )
+        Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iObj) );
+    p->LevelMax = Level;
+    return Level;
+}
+
+int Acb_ObjComputeLevelR( Acb_Ntk_t * p, int iObj )
+{
+    int iFanout, k, Level = 0;
+    Acb_ObjForEachFanout( p, iObj, iFanout, k )
+        Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iFanout) );
+    return Acb_ObjSetLevelR( p, iObj, Level + !Acb_ObjIsCio(p, iObj) );
+}
+int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
+{
+    int i, iObj, Level = 0;
+    if ( vTfi == NULL )
+    {
+        Acb_NtkCleanObjLevelR( p );
+        Acb_NtkForEachObjReverse( p, iObj )
+            Acb_ObjComputeLevelR( p, iObj );
+    }
+    else
+    {
+        // it is assumed that vTfi contains CI nodes
+        Vec_IntForEachEntryReverse( vTfi, iObj, i )
+            Acb_ObjComputeLevelR( p, iObj );
+    }
+    Acb_NtkForEachCi( p, iObj, i )
+        Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) );
+    assert( p->LevelMax == Level );
+    return Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_ObjSlack( Acb_Ntk_t * p, int iObj )
+{
+    assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj) );
+    return !Acb_ObjIsCio(p, iObj) + p->LevelMax - Acb_ObjLevelD(p, iObj) - Acb_ObjLevelR(p, iObj);
+}
+int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
+{
+    int * pFanins, iFanin, k, Path = 0;
+    assert( !Acb_ObjIsCi(p, iObj) );
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+        if ( !Acb_ObjSlack(p, iFanin) )
+            Path += Acb_ObjPathD(p, iFanin);
+    return Acb_ObjSetPathD( p, iObj, Path );
+}
+int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
+{
+    int i, iObj, Path = 0;
+    if ( vTfo == NULL )
+    {
+        Acb_NtkCleanObjPathD( p );
+        Acb_NtkForEachCi( p, iObj, i )
+            if ( Acb_ObjLevelR(p, iObj) == p->LevelMax )
+                Acb_ObjSetPathD( p, iObj, 1 );
+        Acb_NtkForEachObj( p, iObj )
+            if ( !Acb_ObjIsCi(p, iObj) && !Acb_ObjSlack(p, iObj) )
+                Acb_ObjComputePathD( p, iObj );
+    }
+    else
+    {
+        // it is assumed that vTfo contains CO nodes
+        assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) );
+        Vec_IntForEachEntry( vTfo, iObj, i )
+            if ( !Acb_ObjSlack(p, iObj) )
+                Acb_ObjComputePathD( p, iObj );
+            else
+                Acb_ObjSetPathD( p, iObj, 0 );
+    }
+    Acb_NtkForEachCo( p, iObj, i )
+        Path += Acb_ObjPathD(p, iObj);
+    p->nPaths = Path;
+    return Path;
+}
+
+int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj )
+{
+    int iFanout, k, Path = 0;
+    assert( !Acb_ObjIsCo(p, iObj) );
+    Acb_ObjForEachFanout( p, iObj, iFanout, k )
+        if ( !Acb_ObjSlack(p, iFanout) )
+            Path += Acb_ObjPathR(p, iFanout);
+    return Acb_ObjSetPathR( p, iObj, Path );
+}
+int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
+{
+    int i, iObj, Level = p->LevelMax, Path = 0;
+    if ( vTfi == NULL )
+    {
+        Acb_NtkCleanObjPathR( p );
+        Acb_NtkForEachCo( p, iObj, i )
+            if ( Acb_ObjLevelD(p, iObj) == p->LevelMax )
+                Acb_ObjSetPathR( p, iObj, 1 );
+        Acb_NtkForEachObjReverse( p, iObj )
+            if ( !Acb_ObjIsCo(p, iObj) && !Acb_ObjSlack(p, iObj) )
+                Acb_ObjComputePathR( p, iObj );
+    }
+    else
+    {
+        // it is assumed that vTfi contains CI nodes
+        assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) );
+        Vec_IntForEachEntryReverse( vTfi, iObj, i )
+            if ( !Acb_ObjSlack(p, iObj) )
+                Acb_ObjComputePathR( p, iObj );
+            else
+                Acb_ObjSetPathR( p, iObj, 0 );
+    }
+    Acb_NtkForEachCi( p, iObj, i )
+        Path += Acb_ObjPathR(p, iObj);
+    assert( p->nPaths == Path );
+    return Path;
+}
+
+
+int Acb_NtkComputePaths( Acb_Ntk_t * p )
+{
+    int LevelD = Acb_NtkComputeLevelD( p, NULL );
+    int LevelR = Acb_NtkComputeLevelR( p, NULL );
+    int PathD  = Acb_NtkComputePathsD( p, NULL );
+    int PathR  = Acb_NtkComputePathsR( p, NULL );
+    assert( PathD  == PathR );
+    return PathR;
+}
+
+void Abc_NtkComputePaths( Abc_Ntk_t * p )
+{
+    extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p );
+    Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p );
+
+    Acb_NtkCreateFanout( pNtk );
+    printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) );
+
+    Acb_ManFree( pNtk->pDesign );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_ObjPath( Acb_Ntk_t * p, int iObj )
+{
+    return Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
+}
+void Acb_ObjUpdateTiming( Acb_Ntk_t * p, int iObj )
+{
+}
+void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
+{
+    int i, Entry;
+    if ( iObj > 0 )
+    {
+        // assuming that level of the new nodes is up to date
+        Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
+        Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
+        int nLevelD = Acb_NtkComputeLevelD( p, vTfo );
+        int nLevelR = Acb_NtkComputeLevelR( p, vTfi );
+        int nPathD = Acb_NtkComputePathsD( p, vTfo );
+        int nPathR = Acb_NtkComputePathsR( p, vTfi );
+        Vec_IntForEachEntry( vTfi, Entry, i )
+            Acb_ObjUpdateTiming( p, Entry );
+        Vec_IntForEachEntry( vTfo, Entry, i )
+            Acb_ObjUpdateTiming( p, Entry );
+    }
+    else
+    {
+        int LevelD = Acb_NtkComputeLevelD( p, NULL );
+        int LevelR = Acb_NtkComputeLevelR( p, NULL );
+        int PathD  = Acb_NtkComputePathsD( p, NULL );
+        int PathR  = Acb_NtkComputePathsR( p, NULL );
+        Acb_NtkForEachNode( p, Entry )
+            Acb_ObjUpdateTiming( p, Entry );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/module.make b/src/base/acb/module.make
index 09c7ffd6..ce5dcaeb 100644
--- a/src/base/acb/module.make
+++ b/src/base/acb/module.make
@@ -1,4 +1,6 @@
 SRC +=    src/base/acb/acbAbc.c \
     src/base/acb/acbAig.c \
     src/base/acb/acbCom.c \
-    src/base/acb/acbFunc.c 
+    src/base/acb/acbFunc.c \
+    src/base/acb/acbMfs.c \
+    src/base/acb/acbUtil.c 
diff --git a/src/proof/acec/acec2Mult.c b/src/proof/acec/acec2Mult.c
new file mode 100644
index 00000000..62fd1279
--- /dev/null
+++ b/src/proof/acec/acec2Mult.c
@@ -0,0 +1,927 @@
+/**CFile****************************************************************
+
+  FileName    [acec2Mult.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: acec2Mult.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecMem.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+static unsigned s_FuncTruths[1920] = {
+0xF335ACC0, 0xF553CAA0, 0xCF1DB8C0, 0xDD47E288, 0xBB27E488, 0xAF1BD8A0, 0xC1FDBC80, 0xD4D7E828,
+0xB2B7E848, 0xA1FBDA80, 0x89EFE680, 0x8E9FE860, 0xF3AC35C0, 0xF5CA53A0, 0xCFB81DC0, 0xDDE24788,
+0xBBE42788, 0xAFD81BA0, 0xC1BCFD80, 0xD4E8D728, 0xB2E8B748, 0xA1DAFB80, 0x89E6EF80, 0x8EE89F60,
+0xFA3C3C50, 0xFC5A5A30, 0xCB1CF8D0, 0xDE48D278, 0xBE28B478, 0xAD1AF8B0, 0xCBF81CD0, 0xDED24878,
+0xBEB42878, 0xADF81AB0, 0x8EE896F0, 0x8E96E8F0, 0xE334ECC4, 0xF660C66C, 0xEE3C3C44, 0xFC66660C,
+0xB926EC8C, 0xBE289C6C, 0xE3EC34C4, 0xF6C6606C, 0xB296E8CC, 0xB2E896CC, 0xB9EC268C, 0xBE9C286C,
+0xF660A66A, 0xE552EAA2, 0xDE489A6A, 0xD946EA8A, 0xFA66660A, 0xEE5A5A22, 0xD4E896AA, 0xD496E8AA,
+0xF6A6606A, 0xE5EA52A2, 0xD9EA468A, 0xDE9A486A, 0x0CCA533F, 0x0AAC355F, 0x30E2473F, 0x22B81D77,
+0x44D81B77, 0x50E4275F, 0x3E02437F, 0x2B2817D7, 0x4D4817B7, 0x5E04257F, 0x7610197F, 0x7160179F,
+0x0C53CA3F, 0x0A35AC5F, 0x3047E23F, 0x221DB877, 0x441BD877, 0x5027E45F, 0x3E43027F, 0x2B1728D7,
+0x4D1748B7, 0x5E25047F, 0x7619107F, 0x7117609F, 0x05C3C3AF, 0x03A5A5CF, 0x34E3072F, 0x21B72D87,
+0x41D74B87, 0x52E5074F, 0x3407E32F, 0x212DB787, 0x414BD787, 0x5207E54F, 0x7117690F, 0x7169170F,
+0x1CCB133B, 0x099F3993, 0x11C3C3BB, 0x039999F3, 0x46D91373, 0x41D76393, 0x1C13CB3B, 0x09399F93,
+0x4D691733, 0x4D176933, 0x4613D973, 0x4163D793, 0x099F5995, 0x1AAD155D, 0x21B76595, 0x26B91575,
+0x059999F5, 0x11A5A5DD, 0x2B176955, 0x2B691755, 0x09599F95, 0x1A15AD5D, 0x2615B975, 0x2165B795,
+0xF33A5CC0, 0xF55C3AA0, 0xCF2E74C0, 0xDD742E88, 0xBB724E88, 0xAF4E72A0, 0xC2FE7C40, 0xD7D428E8,
+0xB7B248E8, 0xA4FE7A20, 0x98FE6E08, 0x9F8E60E8, 0xF35C3AC0, 0xF53A5CA0, 0xCF742EC0, 0xDD2E7488,
+0xBB4E7288, 0xAF724EA0, 0xC27CFE40, 0xD728D4E8, 0xB748B2E8, 0xA47AFE20, 0x986EFE08, 0x9F608EE8,
+0xF53C3CA0, 0xF35A5AC0, 0xC72CF4E0, 0xD278DE48, 0xB478BE28, 0xA74AF2E0, 0xC7F42CE0, 0xD2DE7848,
+0xB4BE7828, 0xA7F24AE0, 0x96F08EE8, 0x968EF0E8, 0xD338DCC8, 0xC66CF660, 0xDD3C3C88, 0xCF6666C0,
+0x9B62CEC8, 0x9C6CBE28, 0xD3DC38C8, 0xC6F66C60, 0x96B2CCE8, 0x96CCB2E8, 0x9BCE62C8, 0x9CBE6C28,
+0xA66AF660, 0xB558BAA8, 0x9A6ADE48, 0x9D64AEA8, 0xAF6666A0, 0xBB5A5A88, 0x96AAD4E8, 0x96D4AAE8,
+0xA6F66A60, 0xB5BA58A8, 0x9DAE64A8, 0x9ADE6A48, 0x0CC5A33F, 0x0AA3C55F, 0x30D18B3F, 0x228BD177,
+0x448DB177, 0x50B18D5F, 0x3D0183BF, 0x282BD717, 0x484DB717, 0x5B0185DF, 0x670191F7, 0x60719F17,
+0x0CA3C53F, 0x0AC5A35F, 0x308BD13F, 0x22D18B77, 0x44B18D77, 0x508DB15F, 0x3D8301BF, 0x28D72B17,
+0x48B74D17, 0x5B8501DF, 0x679101F7, 0x609F7117, 0x0AC3C35F, 0x0CA5A53F, 0x38D30B1F, 0x2D8721B7,
+0x4B8741D7, 0x58B50D1F, 0x380BD31F, 0x2D2187B7, 0x4B4187D7, 0x580DB51F, 0x690F7117, 0x69710F17,
+0x2CC72337, 0x3993099F, 0x22C3C377, 0x3099993F, 0x649D3137, 0x639341D7, 0x2C23C737, 0x3909939F,
+0x694D3317, 0x69334D17, 0x64319D37, 0x634193D7, 0x5995099F, 0x4AA74557, 0x659521B7, 0x629B5157,
+0x5099995F, 0x44A5A577, 0x69552B17, 0x692B5517, 0x5909959F, 0x4A45A757, 0x62519B57, 0x652195B7,
+0xFCC5A330, 0xFAA3C550, 0xFCD18B0C, 0xEE8BD144, 0xEE8DB122, 0xFAB18D0A, 0xFDC180BC, 0xE8EBD414,
+0xE8EDB212, 0xFBA180DA, 0xEF8980E6, 0xE8F98E06, 0xFCA3C530, 0xFAC5A350, 0xFC8BD10C, 0xEED18B44,
+0xEEB18D22, 0xFA8DB10A, 0xFD80C1BC, 0xE8D4EB14, 0xE8B2ED12, 0xFB80A1DA, 0xEF8089E6, 0xE88EF906,
+0xFAC3C350, 0xFCA5A530, 0xF8D0CB1C, 0xED84E1B4, 0xEB82E1D2, 0xF8B0AD1A, 0xF8CBD01C, 0xEDE184B4,
+0xEBE182D2, 0xF8ADB01A, 0xE88EF096, 0xE8F08E96, 0xECC4E334, 0xF990C99C, 0xEEC3C344, 0xFC99990C,
+0xEC8CB926, 0xEB82C9C6, 0xECE3C434, 0xF9C9909C, 0xE8CCB296, 0xE8B2CC96, 0xECB98C26, 0xEBC982C6,
+0xF990A99A, 0xEAA2E552, 0xED84A9A6, 0xEA8AD946, 0xFA99990A, 0xEEA5A522, 0xE8D4AA96, 0xE8AAD496,
+0xF9A9909A, 0xEAE5A252, 0xEAD98A46, 0xEDA984A6, 0x033A5CCF, 0x055C3AAF, 0x032E74F3, 0x11742EBB,
+0x11724EDD, 0x054E72F5, 0x023E7F43, 0x17142BEB, 0x17124DED, 0x045E7F25, 0x10767F19, 0x170671F9,
+0x035C3ACF, 0x053A5CAF, 0x03742EF3, 0x112E74BB, 0x114E72DD, 0x05724EF5, 0x027F3E43, 0x172B14EB,
+0x174D12ED, 0x047F5E25, 0x107F7619, 0x177106F9, 0x053C3CAF, 0x035A5ACF, 0x072F34E3, 0x127B1E4B,
+0x147D1E2D, 0x074F52E5, 0x07342FE3, 0x121E7B4B, 0x141E7D2D, 0x07524FE5, 0x17710F69, 0x170F7169,
+0x133B1CCB, 0x066F3663, 0x113C3CBB, 0x036666F3, 0x137346D9, 0x147D3639, 0x131C3BCB, 0x06366F63,
+0x17334D69, 0x174D3369, 0x134673D9, 0x14367D39, 0x066F5665, 0x155D1AAD, 0x127B5659, 0x157526B9,
+0x056666F5, 0x115A5ADD, 0x172B5569, 0x17552B69, 0x06566F65, 0x151A5DAD, 0x152675B9, 0x12567B59,
+0xFCCA5330, 0xFAAC3550, 0xFCE2470C, 0xEEB81D44, 0xEED81B22, 0xFAE4270A, 0xFEC2407C, 0xEBE814D4,
+0xEDE812B2, 0xFEA4207A, 0xFE98086E, 0xF9E8068E, 0xFC53CA30, 0xFA35AC50, 0xFC47E20C, 0xEE1DB844,
+0xEE1BD822, 0xFA27E40A, 0xFE40C27C, 0xEB14E8D4, 0xED12E8B2, 0xFE20A47A, 0xFE08986E, 0xF906E88E,
+0xF5C3C3A0, 0xF3A5A5C0, 0xF4E0C72C, 0xE1B4ED84, 0xE1D2EB82, 0xF2E0A74A, 0xF4C7E02C, 0xE1EDB484,
+0xE1EBD282, 0xF2A7E04A, 0xF096E88E, 0xF0E8968E, 0xDCC8D338, 0xC99CF990, 0xDDC3C388, 0xCF9999C0,
+0xCEC89B62, 0xC9C6EB82, 0xDCD3C838, 0xC9F99C90, 0xCCE896B2, 0xCC96E8B2, 0xCE9BC862, 0xC9EBC682,
+0xA99AF990, 0xBAA8B558, 0xA9A6ED84, 0xAEA89D64, 0xAF9999A0, 0xBBA5A588, 0xAA96E8D4, 0xAAE896D4,
+0xA9F99A90, 0xBAB5A858, 0xAE9DA864, 0xA9EDA684, 0x0335ACCF, 0x0553CAAF, 0x031DB8F3, 0x1147E2BB,
+0x1127E4DD, 0x051BD8F5, 0x013DBF83, 0x1417EB2B, 0x1217ED4D, 0x015BDF85, 0x0167F791, 0x0617F971,
+0x03AC35CF, 0x05CA53AF, 0x03B81DF3, 0x11E247BB, 0x11E427DD, 0x05D81BF5, 0x01BF3D83, 0x14EB172B,
+0x12ED174D, 0x01DF5B85, 0x01F76791, 0x06F91771, 0x0A3C3C5F, 0x0C5A5A3F, 0x0B1F38D3, 0x1E4B127B,
+0x1E2D147D, 0x0D1F58B5, 0x0B381FD3, 0x1E124B7B, 0x1E142D7D, 0x0D581FB5, 0x0F691771, 0x0F176971,
+0x23372CC7, 0x3663066F, 0x223C3C77, 0x3066663F, 0x3137649D, 0x3639147D, 0x232C37C7, 0x3606636F,
+0x3317694D, 0x3369174D, 0x3164379D, 0x3614397D, 0x5665066F, 0x45574AA7, 0x5659127B, 0x5157629B,
+0x5066665F, 0x445A5A77, 0x5569172B, 0x5517692B, 0x5606656F, 0x454A57A7, 0x5162579B, 0x5612597B,
+0x3F53CA0C, 0x5F35AC0A, 0x3F47E230, 0x771DB822, 0x771BD844, 0x5F27E450, 0x35F3C0AC, 0x53F5A0CA,
+0x34F7E320, 0x717DB282, 0x717BD484, 0x52F7E540, 0x1CDFCB08, 0x4D7D8E82, 0x1DCFC0B8, 0x47DD88E2,
+0x46DFD940, 0x4D6FD490, 0x2B7B8E84, 0x1ABFAD08, 0x2B6FB290, 0x26BFB920, 0x27BB88E4, 0x1BAFA0D8,
+0x3FCA530C, 0x5FAC350A, 0x3FE24730, 0x77B81D22, 0x77D81B44, 0x5FE42750, 0x35C0F3AC, 0x53A0F5CA,
+0x34E3F720, 0x71B27D82, 0x71D47B84, 0x52E5F740, 0x1CCBDF08, 0x4D8E7D82, 0x1DC0CFB8, 0x4788DDE2,
+0x46D9DF40, 0x4DD46F90, 0x2B8E7B84, 0x1AADBF08, 0x2BB26F90, 0x26B9BF20, 0x2788BBE4, 0x1BA0AFD8,
+0x3C50FA3C, 0x5A30FC5A, 0x3E43F270, 0x7B1278D2, 0x7D1478B4, 0x5E25F470, 0x3CFA503C, 0x5AFC305A,
+0x3EF24370, 0x7B7812D2, 0x7D7814B4, 0x5EF42570, 0x1CD0CBF8, 0x4878DED2, 0x1CCBD0F8, 0x48DE78D2,
+0x4DD469F0, 0x4D69D4F0, 0x2878BEB4, 0x1AB0ADF8, 0x2B69B2F0, 0x2BB269F0, 0x28BE78B4, 0x1AADB0F8,
+0x3E43CE4C, 0x6F066CC6, 0x3C44EE3C, 0x660CFC66, 0x7619DC4C, 0x7D146C9C, 0x34E3C4EC, 0x60F66CC6,
+0x34C4E3EC, 0x606CF6C6, 0x7169D4CC, 0x71D469CC, 0x3ECE434C, 0x6F6C06C6, 0x3CEE443C, 0x66FC0C66,
+0x76DC194C, 0x7D6C149C, 0x2B698ECC, 0x2B8E69CC, 0x286CBE9C, 0x268CB9EC, 0x26B98CEC, 0x28BE6C9C,
+0x6F066AA6, 0x5E25AE2A, 0x7B126A9A, 0x7619BA2A, 0x660AFA66, 0x5A22EE5A, 0x60F66AA6, 0x52E5A2EA,
+0x71B269AA, 0x7169B2AA, 0x606AF6A6, 0x52A2E5EA, 0x4D8E69AA, 0x4D698EAA, 0x48DE6A9A, 0x46D98AEA,
+0x468AD9EA, 0x486ADE9A, 0x6F6A06A6, 0x5EAE252A, 0x7B6A129A, 0x76BA192A, 0x66FA0A66, 0x5AEE225A,
+0xC0AC35F3, 0xA0CA53F5, 0xC0B81DCF, 0x88E247DD, 0x88E427BB, 0xA0D81BAF, 0xCA0C3F53, 0xAC0A5F35,
+0xCB081CDF, 0x8E824D7D, 0x8E842B7B, 0xAD081ABF, 0xE32034F7, 0xB282717D, 0xE2303F47, 0xB822771D,
+0xB92026BF, 0xB2902B6F, 0xD484717B, 0xE54052F7, 0xD4904D6F, 0xD94046DF, 0xD844771B, 0xE4505F27,
+0xC035ACF3, 0xA053CAF5, 0xC01DB8CF, 0x8847E2DD, 0x8827E4BB, 0xA01BD8AF, 0xCA3F0C53, 0xAC5F0A35,
+0xCB1C08DF, 0x8E4D827D, 0x8E2B847B, 0xAD1A08BF, 0xE33420F7, 0xB271827D, 0xE23F3047, 0xB877221D,
+0xB92620BF, 0xB22B906F, 0xD471847B, 0xE55240F7, 0xD44D906F, 0xD94640DF, 0xD877441B, 0xE45F5027,
+0xC3AF05C3, 0xA5CF03A5, 0xC1BC0D8F, 0x84ED872D, 0x82EB874B, 0xA1DA0B8F, 0xC305AFC3, 0xA503CFA5,
+0xC10DBC8F, 0x8487ED2D, 0x8287EB4B, 0xA10BDA8F, 0xE32F3407, 0xB787212D, 0xE3342F07, 0xB721872D,
+0xB22B960F, 0xB2962B0F, 0xD787414B, 0xE54F5207, 0xD4964D0F, 0xD44D960F, 0xD741874B, 0xE5524F07,
+0xC1BC31B3, 0x90F99339, 0xC3BB11C3, 0x99F30399, 0x89E623B3, 0x82EB9363, 0xCB1C3B13, 0x9F099339,
+0xCB3B1C13, 0x9F930939, 0x8E962B33, 0x8E2B9633, 0xC131BCB3, 0x9093F939, 0xC311BBC3, 0x9903F399,
+0x8923E6B3, 0x8293EB63, 0xD4967133, 0xD4719633, 0xD7934163, 0xD9734613, 0xD9467313, 0xD7419363,
+0x90F99559, 0xA1DA51D5, 0x84ED9565, 0x89E645D5, 0x99F50599, 0xA5DD11A5, 0x9F099559, 0xAD1A5D15,
+0x8E4D9655, 0x8E964D55, 0x9F950959, 0xAD5D1A15, 0xB2719655, 0xB2967155, 0xB7219565, 0xB9267515,
+0xB9752615, 0xB7952165, 0x9095F959, 0xA151DAD5, 0x8495ED65, 0x8945E6D5, 0x9905F599, 0xA511DDA5,
+0x3FA3C50C, 0x5FC5A30A, 0x3F8BD130, 0x77D18B22, 0x77B18D44, 0x5F8DB150, 0x3AF3C05C, 0x5CF5A03A,
+0x38FBD310, 0x7D7182B2, 0x7B7184D4, 0x58FDB510, 0x2CEFC704, 0x7D4D828E, 0x2ECFC074, 0x74DD882E,
+0x64FD9D04, 0x6F4D90D4, 0x7B2B848E, 0x4AEFA702, 0x6F2B90B2, 0x62FB9B02, 0x72BB884E, 0x4EAFA072,
+0x3FC5A30C, 0x5FA3C50A, 0x3FD18B30, 0x778BD122, 0x778DB144, 0x5FB18D50, 0x3AC0F35C, 0x5CA0F53A,
+0x38D3FB10, 0x7D8271B2, 0x7B8471D4, 0x58B5FD10, 0x2CC7EF04, 0x7D824D8E, 0x2EC0CF74, 0x7488DD2E,
+0x649DFD04, 0x6F904DD4, 0x7B842B8E, 0x4AA7EF02, 0x6F902BB2, 0x629BFB02, 0x7288BB4E, 0x4EA0AF72,
+0x3CA0F53C, 0x5AC0F35A, 0x3D83F1B0, 0x78D27B12, 0x78B47D14, 0x5B85F1D0, 0x3CF5A03C, 0x5AF3C05A,
+0x3DF183B0, 0x787BD212, 0x787DB414, 0x5BF185D0, 0x2CE0C7F4, 0x7848D2DE, 0x2CC7E0F4, 0x78D248DE,
+0x69F04DD4, 0x694DF0D4, 0x7828B4BE, 0x4AE0A7F2, 0x692BF0B2, 0x69F02BB2, 0x78B428BE, 0x4AA7E0F2,
+0x3D83CD8C, 0x6CC66F06, 0x3C88DD3C, 0x66C0CF66, 0x6791CDC4, 0x6C9C7D14, 0x38D3C8DC, 0x6CC660F6,
+0x38C8D3DC, 0x6C60C6F6, 0x6971CCD4, 0x69CC71D4, 0x3DCD838C, 0x6C6FC606, 0x3CDD883C, 0x66CFC066,
+0x67CD91C4, 0x6C7D9C14, 0x692BCC8E, 0x69CC2B8E, 0x6C289CBE, 0x62C89BCE, 0x629BC8CE, 0x6C9C28BE,
+0x6AA66F06, 0x5B85AB8A, 0x6A9A7B12, 0x6791ABA2, 0x66A0AF66, 0x5A88BB5A, 0x6AA660F6, 0x58B5A8BA,
+0x69AA71B2, 0x6971AAB2, 0x6A60A6F6, 0x58A8B5BA, 0x69AA4D8E, 0x694DAA8E, 0x6A9A48DE, 0x649DA8AE,
+0x64A89DAE, 0x6A489ADE, 0x6A6FA606, 0x5BAB858A, 0x6A7B9A12, 0x67AB91A2, 0x66AFA066, 0x5ABB885A,
+0xC05C3AF3, 0xA03A5CF5, 0xC0742ECF, 0x882E74DD, 0x884E72BB, 0xA0724EAF, 0xC50C3FA3, 0xA30A5FC5,
+0xC7042CEF, 0x828E7D4D, 0x848E7B2B, 0xA7024AEF, 0xD31038FB, 0x82B27D71, 0xD1303F8B, 0x8B2277D1,
+0x9B0262FB, 0x90B26F2B, 0x84D47B71, 0xB51058FD, 0x90D46F4D, 0x9D0464FD, 0x8D4477B1, 0xB1505F8D,
+0xC03A5CF3, 0xA05C3AF5, 0xC02E74CF, 0x88742EDD, 0x88724EBB, 0xA04E72AF, 0xC53F0CA3, 0xA35F0AC5,
+0xC72C04EF, 0x827D8E4D, 0x847B8E2B, 0xA74A02EF, 0xD33810FB, 0x827DB271, 0xD13F308B, 0x8B7722D1,
+0x9B6202FB, 0x906FB22B, 0x847BD471, 0xB55810FD, 0x906FD44D, 0x9D6404FD, 0x8D7744B1, 0xB15F508D,
+0xC35F0AC3, 0xA53F0CA5, 0xC27C0E4F, 0x872D84ED, 0x874B82EB, 0xA47A0E2F, 0xC30A5FC3, 0xA50C3FA5,
+0xC20E7C4F, 0x87842DED, 0x87824BEB, 0xA40E7A2F, 0xD31F380B, 0x87B72D21, 0xD3381F0B, 0x872DB721,
+0x960FB22B, 0x96B20F2B, 0x87D74B41, 0xB51F580D, 0x96D40F4D, 0x960FD44D, 0x874BD741, 0xB5581F0D,
+0xC27C3273, 0x933990F9, 0xC37722C3, 0x993F3099, 0x986E323B, 0x936382EB, 0xC72C3723, 0x93399F09,
+0xC7372C23, 0x939F3909, 0x968E332B, 0x96338E2B, 0xC2327C73, 0x939039F9, 0xC32277C3, 0x99303F99,
+0x98326E3B, 0x938263EB, 0x96D43371, 0x9633D471, 0x93D76341, 0x9D376431, 0x9D643731, 0x9363D741,
+0x955990F9, 0xA47A5475, 0x956584ED, 0x986E545D, 0x995F5099, 0xA57744A5, 0x95599F09, 0xA74A5745,
+0x96558E4D, 0x968E554D, 0x959F5909, 0xA7574A45, 0x9655B271, 0x96B25571, 0x9565B721, 0x9B625751,
+0x9B576251, 0x95B76521, 0x959059F9, 0xA4547A75, 0x958465ED, 0x98546E5D, 0x99505F99, 0xA54477A5,
+0xCF5C3A03, 0xAF3A5C05, 0xF3742E03, 0xBB2E7411, 0xDD4E7211, 0xF5724E05, 0xC5FC30A3, 0xA3FA50C5,
+0xF73420E3, 0xB2BE7141, 0xD4DE7121, 0xF75240E5, 0xDF1C08CB, 0x8EBE4D41, 0xD1FC0C8B, 0x8BEE44D1,
+0xDF4640D9, 0xD4F64D09, 0x8EDE2B21, 0xBF1A08AD, 0xB2F62B09, 0xBF2620B9, 0x8DEE22B1, 0xB1FA0A8D,
+0xCF3A5C03, 0xAF5C3A05, 0xF32E7403, 0xBB742E11, 0xDD724E11, 0xF54E7205, 0xC530FCA3, 0xA350FAC5,
+0xF72034E3, 0xB271BE41, 0xD471DE21, 0xF74052E5, 0xDF081CCB, 0x8E4DBE41, 0xD10CFC8B, 0x8B44EED1,
+0xDF4046D9, 0xD44DF609, 0x8E2BDE21, 0xBF081AAD, 0xB22BF609, 0xBF2026B9, 0x8D22EEB1, 0xB10AFA8D,
+0xC350FAC3, 0xA530FCA5, 0xF2703E43, 0xB721B4E1, 0xD741D2E1, 0xF4705E25, 0xC3FA50C3, 0xA5FC30A5,
+0xF23E7043, 0xB7B421E1, 0xD7D241E1, 0xF45E7025, 0xD01CF8CB, 0x84B4EDE1, 0xD0F81CCB, 0x84EDB4E1,
+0xD44DF069, 0xD4F04D69, 0x82D2EBE1, 0xB01AF8AD, 0xB2F02B69, 0xB22BF069, 0x82EBD2E1, 0xB0F81AAD,
+0xCE4C3E43, 0x9F099CC9, 0xC344EEC3, 0x990CFC99, 0xDC4C7619, 0xD741C6C9, 0xC4EC34E3, 0x90F99CC9,
+0xC434ECE3, 0x909CF9C9, 0xD4CC7169, 0xD471CC69, 0xCE3E4C43, 0x9F9C09C9, 0xC3EE44C3, 0x99FC0C99,
+0xDC764C19, 0xD7C641C9, 0x8ECC2B69, 0x8E2BCC69, 0x82C6EBC9, 0x8C26ECB9, 0x8CEC26B9, 0x82EBC6C9,
+0x9F099AA9, 0xAE2A5E25, 0xB721A6A9, 0xBA2A7619, 0x990AFA99, 0xA522EEA5, 0x90F99AA9, 0xA2EA52E5,
+0xB271AA69, 0xB2AA7169, 0x909AF9A9, 0xA252EAE5, 0x8E4DAA69, 0x8EAA4D69, 0x84EDA6A9, 0x8AEA46D9,
+0x8A46EAD9, 0x84A6EDA9, 0x9F9A09A9, 0xAE5E2A25, 0xB7A621A9, 0xBA762A19, 0x99FA0A99, 0xA5EE22A5,
+0x30A3C5FC, 0x50C5A3FA, 0x0C8BD1FC, 0x44D18BEE, 0x22B18DEE, 0x0A8DB1FA, 0x3A03CF5C, 0x5C05AF3A,
+0x08CBDF1C, 0x4D418EBE, 0x2B218EDE, 0x08ADBF1A, 0x20E3F734, 0x7141B2BE, 0x2E03F374, 0x7411BB2E,
+0x20B9BF26, 0x2B09B2F6, 0x7121D4DE, 0x40E5F752, 0x4D09D4F6, 0x40D9DF46, 0x7211DD4E, 0x4E05F572,
+0x30C5A3FC, 0x50A3C5FA, 0x0CD18BFC, 0x448BD1EE, 0x228DB1EE, 0x0AB18DFA, 0x3ACF035C, 0x5CAF053A,
+0x08DFCB1C, 0x4D8E41BE, 0x2B8E21DE, 0x08BFAD1A, 0x20F7E334, 0x71B241BE, 0x2EF30374, 0x74BB112E,
+0x20BFB926, 0x2BB209F6, 0x71D421DE, 0x40F7E552, 0x4DD409F6, 0x40DFD946, 0x72DD114E, 0x4EF50572,
+0x3CAF053C, 0x5ACF035A, 0x0D8FC1BC, 0x48DE4B1E, 0x28BE2D1E, 0x0B8FA1DA, 0x3C05AF3C, 0x5A03CF5A,
+0x0DC18FBC, 0x484BDE1E, 0x282DBE1E, 0x0BA18FDA, 0x2FE30734, 0x7B4B121E, 0x2F07E334, 0x7B124B1E,
+0x2BB20F96, 0x2B0FB296, 0x7D2D141E, 0x4FE50752, 0x4D0FD496, 0x4DD40F96, 0x7D142D1E, 0x4F07E552,
+0x31B3C1BC, 0x60F66336, 0x3CBB113C, 0x66F30366, 0x23B389E6, 0x28BE3936, 0x3B13CB1C, 0x6F066336,
+0x3BCB131C, 0x6F630636, 0x2B338E96, 0x2B8E3396, 0x31C1B3BC, 0x6063F636, 0x3C11BB3C, 0x6603F366,
+0x2389B3E6, 0x2839BE36, 0x7133D496, 0x71D43396, 0x7D391436, 0x73D91346, 0x7313D946, 0x7D143936,
+0x60F66556, 0x51D5A1DA, 0x48DE5956, 0x45D589E6, 0x66F50566, 0x5ADD115A, 0x6F066556, 0x5D15AD1A,
+0x4D8E5596, 0x4D558E96, 0x6F650656, 0x5DAD151A, 0x71B25596, 0x7155B296, 0x7B125956, 0x7515B926,
+0x75B91526, 0x7B591256, 0x6065F656, 0x51A1D5DA, 0x4859DE56, 0x4589D5E6, 0x6605F566, 0x5A11DD5A,
+0xCFAC3503, 0xAFCA5305, 0xF3B81D03, 0xBBE24711, 0xDDE42711, 0xF5D81B05, 0xCAFC3053, 0xACFA5035,
+0xFB3810D3, 0xBEB24171, 0xDED42171, 0xFD5810B5, 0xEF2C04C7, 0xBE8E414D, 0xE2FC0C47, 0xB8EE441D,
+0xFD64049D, 0xF6D4094D, 0xDE8E212B, 0xEF4A02A7, 0xF6B2092B, 0xFB62029B, 0xD8EE221B, 0xE4FA0A27,
+0xCF35AC03, 0xAF53CA05, 0xF31DB803, 0xBB47E211, 0xDD27E411, 0xF51BD805, 0xCA30FC53, 0xAC50FA35,
+0xFB1038D3, 0xBE41B271, 0xDE21D471, 0xFD1058B5, 0xEF042CC7, 0xBE418E4D, 0xE20CFC47, 0xB844EE1D,
+0xFD04649D, 0xF609D44D, 0xDE218E2B, 0xEF024AA7, 0xF609B22B, 0xFB02629B, 0xD822EE1B, 0xE40AFA27,
+0xC3A0F5C3, 0xA5C0F3A5, 0xF1B03D83, 0xB4E1B721, 0xD2E1D741, 0xF1D05B85, 0xC3F5A0C3, 0xA5F3C0A5,
+0xF13DB083, 0xB4B7E121, 0xD2D7E141, 0xF15BD085, 0xE02CF4C7, 0xB484E1ED, 0xE0F42CC7, 0xB4E184ED,
+0xF069D44D, 0xF0D4694D, 0xD282E1EB, 0xE04AF2A7, 0xF0B2692B, 0xF069B22B, 0xD2E182EB, 0xE0F24AA7,
+0xCD8C3D83, 0x9CC99F09, 0xC388DDC3, 0x99C0CF99, 0xCDC46791, 0xC6C9D741, 0xC8DC38D3, 0x9CC990F9,
+0xC838DCD3, 0x9C90C9F9, 0xCCD46971, 0xCC69D471, 0xCD3D8C83, 0x9C9FC909, 0xC3DD88C3, 0x99CFC099,
+0xCD67C491, 0xC6D7C941, 0xCC8E692B, 0xCC698E2B, 0xC682C9EB, 0xC862CE9B, 0xC8CE629B, 0xC6C982EB,
+0x9AA99F09, 0xAB8A5B85, 0xA6A9B721, 0xABA26791, 0x99A0AF99, 0xA588BBA5, 0x9AA990F9, 0xA8BA58B5,
+0xAA69B271, 0xAAB26971, 0x9A90A9F9, 0xA858BAB5, 0xAA698E4D, 0xAA8E694D, 0xA6A984ED, 0xA8AE649D,
+0xA864AE9D, 0xA684A9ED, 0x9A9FA909, 0xAB5B8A85, 0xA6B7A921, 0xAB67A291, 0x99AFA099, 0xA5BB88A5,
+0x3053CAFC, 0x5035ACFA, 0x0C47E2FC, 0x441DB8EE, 0x221BD8EE, 0x0A27E4FA, 0x3503CFAC, 0x5305AFCA,
+0x04C7EF2C, 0x414DBE8E, 0x212BDE8E, 0x02A7EF4A, 0x10D3FB38, 0x4171BEB2, 0x1D03F3B8, 0x4711BBE2,
+0x029BFB62, 0x092BF6B2, 0x2171DED4, 0x10B5FD58, 0x094DF6D4, 0x049DFD64, 0x2711DDE4, 0x1B05F5D8,
+0x30CA53FC, 0x50AC35FA, 0x0CE247FC, 0x44B81DEE, 0x22D81BEE, 0x0AE427FA, 0x35CF03AC, 0x53AF05CA,
+0x04EFC72C, 0x41BE4D8E, 0x21DE2B8E, 0x02EFA74A, 0x10FBD338, 0x41BE71B2, 0x1DF303B8, 0x47BB11E2,
+0x02FB9B62, 0x09F62BB2, 0x21DE71D4, 0x10FDB558, 0x09F64DD4, 0x04FD9D64, 0x27DD11E4, 0x1BF505D8,
+0x3C5F0A3C, 0x5A3F0C5A, 0x0E4FC27C, 0x4B1E48DE, 0x2D1E28BE, 0x0E2FA47A, 0x3C0A5F3C, 0x5A0C3F5A,
+0x0EC24F7C, 0x4B481EDE, 0x2D281EBE, 0x0EA42F7A, 0x1FD30B38, 0x4B7B1E12, 0x1F0BD338, 0x4B1E7B12,
+0x0F962BB2, 0x0F2B96B2, 0x2D7D1E14, 0x1FB50D58, 0x0F4D96D4, 0x0F964DD4, 0x2D1E7D14, 0x1F0DB558,
+0x3273C27C, 0x633660F6, 0x3C77223C, 0x663F3066, 0x323B986E, 0x393628BE, 0x3723C72C, 0x63366F06,
+0x37C7232C, 0x636F3606, 0x332B968E, 0x33962B8E, 0x32C2737C, 0x636036F6, 0x3C22773C, 0x66303F66,
+0x32983B6E, 0x392836BE, 0x337196D4, 0x339671D4, 0x397D3614, 0x379D3164, 0x37319D64, 0x39367D14,
+0x655660F6, 0x5475A47A, 0x595648DE, 0x545D986E, 0x665F5066, 0x5A77445A, 0x65566F06, 0x5745A74A,
+0x55964D8E, 0x554D968E, 0x656F5606, 0x57A7454A, 0x559671B2, 0x557196B2, 0x59567B12, 0x57519B62,
+0x579B5162, 0x597B5612, 0x656056F6, 0x54A4757A, 0x594856DE, 0x54985D6E, 0x66505F66, 0x5A44775A,
+0x533F0CCA, 0x355F0AAC, 0x473F30E2, 0x1D7722B8, 0x1B7744D8, 0x275F50E4, 0x437F3E02, 0x17D72B28,
+0x17B74D48, 0x257F5E04, 0x197F7610, 0x179F7160, 0x530C3FCA, 0x350A5FAC, 0x47303FE2, 0x1D2277B8,
+0x1B4477D8, 0x27505FE4, 0x433E7F02, 0x172BD728, 0x174DB748, 0x255E7F04, 0x19767F10, 0x17719F60,
+0x503C3CFA, 0x305A5AFC, 0x433E70F2, 0x127BD278, 0x147DB478, 0x255E70F4, 0x43703EF2, 0x12D27B78,
+0x14B47D78, 0x25705EF4, 0x177196F0, 0x179671F0, 0x433E4CCE, 0x066FC66C, 0x443C3CEE, 0x0C6666FC,
+0x19764CDC, 0x147D9C6C, 0x434C3ECE, 0x06C66F6C, 0x17964DCC, 0x174D96CC, 0x194C76DC, 0x149C7D6C,
+0x066FA66A, 0x255E2AAE, 0x127B9A6A, 0x19762ABA, 0x0A6666FA, 0x225A5AEE, 0x172B96AA, 0x17962BAA,
+0x06A66F6A, 0x252A5EAE, 0x192A76BA, 0x129A7B6A, 0xACC0F335, 0xCAA0F553, 0xB8C0CF1D, 0xE288DD47,
+0xE488BB27, 0xD8A0AF1B, 0xBC80C1FD, 0xE828D4D7, 0xE848B2B7, 0xDA80A1FB, 0xE68089EF, 0xE8608E9F,
+0xACF3C035, 0xCAF5A053, 0xB8CFC01D, 0xE2DD8847, 0xE4BB8827, 0xD8AFA01B, 0xBCC180FD, 0xE8D428D7,
+0xE8B248B7, 0xDAA180FB, 0xE68980EF, 0xE88E609F, 0xAFC3C305, 0xCFA5A503, 0xBCC18F0D, 0xED842D87,
+0xEB824B87, 0xDAA18F0B, 0xBC8FC10D, 0xED2D8487, 0xEB4B8287, 0xDA8FA10B, 0xE88E690F, 0xE8698E0F,
+0xBCC1B331, 0xF9903993, 0xBBC3C311, 0xF3999903, 0xE689B323, 0xEB826393, 0xBCB3C131, 0xF9399093,
+0xE869B233, 0xE8B26933, 0xE6B38923, 0xEB638293, 0xF9905995, 0xDAA1D551, 0xED846595, 0xE689D545,
+0xF5999905, 0xDDA5A511, 0xE8D46955, 0xE869D455, 0xF9599095, 0xDAD5A151, 0xE6D58945, 0xED658495,
+0xA33F0CC5, 0xC55F0AA3, 0x8B3F30D1, 0xD177228B, 0xB177448D, 0x8D5F50B1, 0x83BF3D01, 0xD717282B,
+0xB717484D, 0x85DF5B01, 0x91F76701, 0x9F176071, 0xA30C3FC5, 0xC50A5FA3, 0x8B303FD1, 0xD122778B,
+0xB144778D, 0x8D505FB1, 0x833DBF01, 0xD728172B, 0xB748174D, 0x855BDF01, 0x9167F701, 0x9F601771,
+0xA03C3CF5, 0xC05A5AF3, 0x833DB0F1, 0xD278127B, 0xB478147D, 0x855BD0F1, 0x83B03DF1, 0xD212787B,
+0xB414787D, 0x85D05BF1, 0x96F01771, 0x9617F071, 0x833D8CCD, 0xC66C066F, 0x883C3CDD, 0xC06666CF,
+0x9167C4CD, 0x9C6C147D, 0x838C3DCD, 0xC6066C6F, 0x9617CC4D, 0x96CC174D, 0x91C467CD, 0x9C146C7D,
+0xA66A066F, 0x855B8AAB, 0x9A6A127B, 0x9167A2AB, 0xA06666AF, 0x885A5ABB, 0x96AA172B, 0x9617AA2B,
+0xA6066A6F, 0x858A5BAB, 0x91A267AB, 0x9A126A7B, 0x5CC0F33A, 0x3AA0F55C, 0x74C0CF2E, 0x2E88DD74,
+0x4E88BB72, 0x72A0AF4E, 0x7C40C2FE, 0x28E8D7D4, 0x48E8B7B2, 0x7A20A4FE, 0x6E0898FE, 0x60E89F8E,
+0x5CF3C03A, 0x3AF5A05C, 0x74CFC02E, 0x2EDD8874, 0x4EBB8872, 0x72AFA04E, 0x7CC240FE, 0x28D7E8D4,
+0x48B7E8B2, 0x7AA420FE, 0x6E9808FE, 0x609FE88E, 0x5FC3C30A, 0x3FA5A50C, 0x7CC24F0E, 0x2D87ED84,
+0x4B87EB82, 0x7AA42F0E, 0x7C4FC20E, 0x2DED8784, 0x4BEB8782, 0x7A2FA40E, 0x690FE88E, 0x69E80F8E,
+0x7CC27332, 0x3993F990, 0x77C3C322, 0x3F999930, 0x6E983B32, 0x6393EB82, 0x7C73C232, 0x39F99390,
+0x69E833B2, 0x6933E8B2, 0x6E3B9832, 0x63EB9382, 0x5995F990, 0x7AA47554, 0x6595ED84, 0x6E985D54,
+0x5F999950, 0x77A5A544, 0x6955E8D4, 0x69E855D4, 0x59F99590, 0x7A75A454, 0x6E5D9854, 0x65ED9584,
+0x5CCF033A, 0x3AAF055C, 0x74F3032E, 0x2EBB1174, 0x4EDD1172, 0x72F5054E, 0x7F43023E, 0x2BEB1714,
+0x4DED1712, 0x7F25045E, 0x7F191076, 0x71F91706, 0x5C03CF3A, 0x3A05AF5C, 0x7403F32E, 0x2E11BB74,
+0x4E11DD72, 0x7205F54E, 0x7F02433E, 0x2B17EB14, 0x4D17ED12, 0x7F04255E, 0x7F101976, 0x7117F906,
+0x50C3C3FA, 0x30A5A5FC, 0x70F2433E, 0x21B7E1B4, 0x41D7E1D2, 0x70F4255E, 0x7043F23E, 0x21E1B7B4,
+0x41E1D7D2, 0x7025F45E, 0x7117F096, 0x71F01796, 0x4CCE433E, 0x099FC99C, 0x44C3C3EE, 0x0C9999FC,
+0x4CDC1976, 0x41D7C9C6, 0x4C43CE3E, 0x09C99F9C, 0x4DCC1796, 0x4D17CC96, 0x4C19DC76, 0x41C9D7C6,
+0x099FA99A, 0x2AAE255E, 0x21B7A9A6, 0x2ABA1976, 0x0A9999FA, 0x22A5A5EE, 0x2B17AA96, 0x2BAA1796,
+0x09A99F9A, 0x2A25AE5E, 0x2A19BA76, 0x21A9B7A6, 0xA330FCC5, 0xC550FAA3, 0x8B0CFCD1, 0xD144EE8B,
+0xB122EE8D, 0x8D0AFAB1, 0x80BCFDC1, 0xD414E8EB, 0xB212E8ED, 0x80DAFBA1, 0x80E6EF89, 0x8E06E8F9,
+0xA3FC30C5, 0xC5FA50A3, 0x8BFC0CD1, 0xD1EE448B, 0xB1EE228D, 0x8DFA0AB1, 0x80FDBCC1, 0xD4E814EB,
+0xB2E812ED, 0x80FBDAA1, 0x80EFE689, 0x8EE806F9, 0xAF3C3C05, 0xCF5A5A03, 0x8F0DBCC1, 0xDE481E4B,
+0xBE281E2D, 0x8F0BDAA1, 0x8FBC0DC1, 0xDE1E484B, 0xBE1E282D, 0x8FDA0BA1, 0x8EE80F69, 0x8E0FE869,
+0xB331BCC1, 0xF6603663, 0xBB3C3C11, 0xF3666603, 0xB323E689, 0xBE283639, 0xB3BC31C1, 0xF6366063,
+0xB233E869, 0xB2E83369, 0xB3E62389, 0xBE362839, 0xF6605665, 0xD551DAA1, 0xDE485659, 0xD545E689,
+0xF5666605, 0xDD5A5A11, 0xD4E85569, 0xD455E869, 0xF6566065, 0xD5DA51A1, 0xD5E64589, 0xDE564859,
+0xACCF0335, 0xCAAF0553, 0xB8F3031D, 0xE2BB1147, 0xE4DD1127, 0xD8F5051B, 0xBF83013D, 0xEB2B1417,
+0xED4D1217, 0xDF85015B, 0xF7910167, 0xF9710617, 0xAC03CF35, 0xCA05AF53, 0xB803F31D, 0xE211BB47,
+0xE411DD27, 0xD805F51B, 0xBF01833D, 0xEB142B17, 0xED124D17, 0xDF01855B, 0xF7019167, 0xF9067117,
+0xA0C3C3F5, 0xC0A5A5F3, 0xB0F1833D, 0xE1B421B7, 0xE1D241D7, 0xD0F1855B, 0xB083F13D, 0xE121B4B7,
+0xE141D2D7, 0xD085F15B, 0xF0967117, 0xF0719617, 0x8CCD833D, 0xC99C099F, 0x88C3C3DD, 0xC09999CF,
+0xC4CD9167, 0xC9C641D7, 0x8C83CD3D, 0xC9099C9F, 0xCC4D9617, 0xCC964D17, 0xC491CD67, 0xC941C6D7,
+0xA99A099F, 0x8AAB855B, 0xA9A621B7, 0xA2AB9167, 0xA09999AF, 0x88A5A5BB, 0xAA962B17, 0xAA2B9617,
+0xA9099A9F, 0x8A85AB5B, 0xA291AB67, 0xA921A6B7, 0x5330FCCA, 0x3550FAAC, 0x470CFCE2, 0x1D44EEB8,
+0x1B22EED8, 0x270AFAE4, 0x407CFEC2, 0x14D4EBE8, 0x12B2EDE8, 0x207AFEA4, 0x086EFE98, 0x068EF9E8,
+0x53FC30CA, 0x35FA50AC, 0x47FC0CE2, 0x1DEE44B8, 0x1BEE22D8, 0x27FA0AE4, 0x40FE7CC2, 0x14EBD4E8,
+0x12EDB2E8, 0x20FE7AA4, 0x08FE6E98, 0x06F98EE8, 0x5F3C3C0A, 0x3F5A5A0C, 0x4F0E7CC2, 0x1E4BDE48,
+0x1E2DBE28, 0x2F0E7AA4, 0x4F7C0EC2, 0x1EDE4B48, 0x1EBE2D28, 0x2F7A0EA4, 0x0F698EE8, 0x0F8E69E8,
+0x73327CC2, 0x3663F660, 0x773C3C22, 0x3F666630, 0x3B326E98, 0x3639BE28, 0x737C32C2, 0x36F66360,
+0x33B269E8, 0x3369B2E8, 0x3B6E3298, 0x36BE3928, 0x5665F660, 0x75547AA4, 0x5659DE48, 0x5D546E98,
+0x5F666650, 0x775A5A44, 0x5569D4E8, 0x55D469E8, 0x56F66560, 0x757A54A4, 0x5D6E5498, 0x56DE5948
+};
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define SDB_MAX_CUTSIZE    6
+#define SDB_MAX_CUTNUM     51
+#define SDB_MAX_TT_WORDS   ((SDB_MAX_CUTSIZE > 6) ? 1 << (SDB_MAX_CUTSIZE-6) : 1)
+
+#define SDB_CUT_NO_LEAF   0xF
+
+typedef struct Sdb_Cut_t_ Sdb_Cut_t; 
+struct Sdb_Cut_t_
+{
+    word            Sign;                      // signature
+    int             iFunc;                     // functionality
+    int             Cost;                      // cut cost
+    int             CostLev;                   // cut cost
+    unsigned        nTreeLeaves  : 28;         // tree leaves
+    unsigned        nLeaves      :  4;         // leaf count
+    int             pLeaves[SDB_MAX_CUTSIZE];  // leaves
+};
+
+typedef struct Sdb_Sto_t_ Sdb_Sto_t; 
+struct Sdb_Sto_t_
+{
+    int             nCutSize;
+    int             nCutNum;
+    int             fCutMin;
+    int             fVerbose;
+    Gia_Man_t *     pGia;                      // user's AIG manager (will be modified by adding nodes)
+    Vec_Int_t *     vRefs;                     // refs for each node
+    Vec_Wec_t *     vCuts;                     // cuts for each node
+    Vec_Mem_t *     vTtMem;                    // truth tables
+    Sdb_Cut_t       pCuts[3][SDB_MAX_CUTNUM];  // temporary cuts
+    Sdb_Cut_t *     ppCuts[SDB_MAX_CUTNUM];    // temporary cut pointers
+    int             nCutsR;                    // the number of cuts
+    int             Pivot;                     // current object
+    int             iCutBest;                  // best-delay cut
+    int             nCutsOver;                 // overflow cuts
+    double          CutCount[4];               // cut counters
+    abctime         clkStart;                  // starting time
+};
+
+static inline word * Sdb_CutTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut ) { return Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc));           }
+
+#define Sdb_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 2 )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Check correctness of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word Sdb_CutGetSign( Sdb_Cut_t * pCut )
+{
+    word Sign = 0; int i; 
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Sign |= ((word)1) << (pCut->pLeaves[i] & 0x3F);
+    return Sign;
+}
+static inline int Sdb_CutCheck( Sdb_Cut_t * pBase, Sdb_Cut_t * pCut ) // check if pCut is contained in pBase
+{
+    int nSizeB = pBase->nLeaves;
+    int nSizeC = pCut->nLeaves;
+    int i, * pB = pBase->pLeaves;
+    int k, * pC = pCut->pLeaves;
+    for ( i = 0; i < nSizeC; i++ )
+    {
+        for ( k = 0; k < nSizeB; k++ )
+            if ( pC[i] == pB[k] )
+                break;
+        if ( k == nSizeB )
+            return 0;
+    }
+    return 1;
+}
+static inline int Sdb_CutSetCheckArray( Sdb_Cut_t ** ppCuts, int nCuts )
+{
+    Sdb_Cut_t * pCut0, * pCut1; 
+    int i, k, m, n, Value;
+    assert( nCuts > 0 );
+    for ( i = 0; i < nCuts; i++ )
+    {
+        pCut0 = ppCuts[i];
+        assert( pCut0->nLeaves <= SDB_MAX_CUTSIZE );
+        assert( pCut0->Sign == Sdb_CutGetSign(pCut0) );
+        // check duplicates
+        for ( m = 0; m < (int)pCut0->nLeaves; m++ )
+        for ( n = m + 1; n < (int)pCut0->nLeaves; n++ )
+            assert( pCut0->pLeaves[m] < pCut0->pLeaves[n] );
+        // check pairs
+        for ( k = 0; k < nCuts; k++ )
+        {
+            pCut1 = ppCuts[k];
+            if ( pCut0 == pCut1 )
+                continue;
+            // check containments
+            Value = Sdb_CutCheck( pCut0, pCut1 );
+            assert( Value == 0 );
+        }
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sdb_CutMergeOrder( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, Sdb_Cut_t * pCut, int nCutSize )
+{ 
+    int nSize0   = pCut0->nLeaves;
+    int nSize1   = pCut1->nLeaves;
+    int i, * pC0 = pCut0->pLeaves;
+    int k, * pC1 = pCut1->pLeaves;
+    int c, * pC  = pCut->pLeaves;
+    // the case of the largest cut sizes
+    if ( nSize0 == nCutSize && nSize1 == nCutSize )
+    {
+        for ( i = 0; i < nSize0; i++ )
+        {
+            if ( pC0[i] != pC1[i] )  return 0;
+            pC[i] = pC0[i];
+        }
+        pCut->nLeaves = nCutSize;
+        pCut->iFunc = -1;
+        pCut->Sign = pCut0->Sign | pCut1->Sign;
+        return 1;
+    }
+    // compare two cuts with different numbers
+    i = k = c = 0;
+    if ( nSize0 == 0 ) goto FlushCut1;
+    if ( nSize1 == 0 ) goto FlushCut0;
+    while ( 1 )
+    {
+        if ( c == nCutSize ) return 0;
+        if ( pC0[i] < pC1[k] )
+        {
+            pC[c++] = pC0[i++];
+            if ( i >= nSize0 ) goto FlushCut1;
+        }
+        else if ( pC0[i] > pC1[k] )
+        {
+            pC[c++] = pC1[k++];
+            if ( k >= nSize1 ) goto FlushCut0;
+        }
+        else
+        {
+            pC[c++] = pC0[i++]; k++;
+            if ( i >= nSize0 ) goto FlushCut1;
+            if ( k >= nSize1 ) goto FlushCut0;
+        }
+    }
+
+FlushCut0:
+    if ( c + nSize0 > nCutSize + i ) return 0;
+    while ( i < nSize0 )
+        pC[c++] = pC0[i++];
+    pCut->nLeaves = c;
+    pCut->iFunc = -1;
+    pCut->Sign = pCut0->Sign | pCut1->Sign;
+    return 1;
+
+FlushCut1:
+    if ( c + nSize1 > nCutSize + k ) return 0;
+    while ( k < nSize1 )
+        pC[c++] = pC1[k++];
+    pCut->nLeaves = c;
+    pCut->iFunc = -1;
+    pCut->Sign = pCut0->Sign | pCut1->Sign;
+    return 1;
+}
+static inline int Sdb_CutMergeOrder2( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, Sdb_Cut_t * pCut, int nCutSize )
+{ 
+    int x0, i0 = 0, nSize0 = pCut0->nLeaves, * pC0 = pCut0->pLeaves;
+    int x1, i1 = 0, nSize1 = pCut1->nLeaves, * pC1 = pCut1->pLeaves;
+    int xMin, c = 0, * pC  = pCut->pLeaves;
+    while ( 1 )
+    {
+        x0 = (i0 == nSize0) ? ABC_INFINITY : pC0[i0];
+        x1 = (i1 == nSize1) ? ABC_INFINITY : pC1[i1];
+        xMin = Abc_MinInt(x0, x1);
+        if ( xMin == ABC_INFINITY ) break;
+        if ( c == nCutSize ) return 0;
+        pC[c++] = xMin;
+        if (x0 == xMin) i0++;
+        if (x1 == xMin) i1++;
+    }
+    pCut->nLeaves = c;
+    pCut->iFunc = -1;
+    pCut->Sign = pCut0->Sign | pCut1->Sign;
+    return 1;
+}
+static inline int Sdb_CutSetCutIsContainedOrder( Sdb_Cut_t * pBase, Sdb_Cut_t * pCut ) // check if pCut is contained in pBase
+{
+    int i, nSizeB = pBase->nLeaves;
+    int k, nSizeC = pCut->nLeaves;
+    if ( nSizeB == nSizeC )
+    {
+        for ( i = 0; i < nSizeB; i++ )
+            if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
+                return 0;
+        return 1;
+    }
+    assert( nSizeB > nSizeC ); 
+    if ( nSizeC == 0 )
+        return 1;
+    for ( i = k = 0; i < nSizeB; i++ )
+    {
+        if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
+            return 0;
+        if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
+        {
+            if ( ++k == nSizeC )
+                return 1;
+        }
+    }
+    return 0;
+}
+static inline int Sdb_CutSetLastCutIsContained( Sdb_Cut_t ** pCuts, int nCuts )
+{
+    int i;
+    for ( i = 0; i < nCuts; i++ )
+        if ( pCuts[i]->nLeaves <= pCuts[nCuts]->nLeaves && (pCuts[i]->Sign & pCuts[nCuts]->Sign) == pCuts[i]->Sign && Sdb_CutSetCutIsContainedOrder(pCuts[nCuts], pCuts[i]) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sdb_CutCompare( Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1 )
+{
+    if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves )  return -1;
+    if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves )  return  1;
+    if ( pCut0->nLeaves     < pCut1->nLeaves )      return -1;
+    if ( pCut0->nLeaves     > pCut1->nLeaves )      return  1;
+    return 0;
+}
+static inline int Sdb_CutSetLastCutContains( Sdb_Cut_t ** pCuts, int nCuts )
+{
+    int i, k, fChanges = 0;
+    for ( i = 0; i < nCuts; i++ )
+        if ( pCuts[nCuts]->nLeaves < pCuts[i]->nLeaves && (pCuts[nCuts]->Sign & pCuts[i]->Sign) == pCuts[nCuts]->Sign && Sdb_CutSetCutIsContainedOrder(pCuts[i], pCuts[nCuts]) )
+            pCuts[i]->nLeaves = SDB_CUT_NO_LEAF, fChanges = 1;
+    if ( !fChanges )
+        return nCuts;
+    for ( i = k = 0; i <= nCuts; i++ )
+    {
+        if ( pCuts[i]->nLeaves == SDB_CUT_NO_LEAF )
+            continue;
+        if ( k < i )
+            ABC_SWAP( Sdb_Cut_t *, pCuts[k], pCuts[i] );
+        k++;
+    }
+    return k - 1;
+}
+static inline void Sdb_CutSetSortByCost( Sdb_Cut_t ** pCuts, int nCuts )
+{
+    int i;
+    for ( i = nCuts; i > 0; i-- )
+    {
+        if ( Sdb_CutCompare(pCuts[i - 1], pCuts[i]) < 0 )//!= 1 )
+            return;
+        ABC_SWAP( Sdb_Cut_t *, pCuts[i - 1], pCuts[i] );
+    }
+}
+static inline int Sdb_CutSetAddCut( Sdb_Cut_t ** pCuts, int nCuts, int nCutNum )
+{
+    if ( nCuts == 0 )
+        return 1;
+    nCuts = Sdb_CutSetLastCutContains(pCuts, nCuts);
+    assert( nCuts >= 0 );
+    Sdb_CutSetSortByCost( pCuts, nCuts );
+    // add new cut if there is room
+    return Abc_MinInt( nCuts + 1, nCutNum - 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sdb_CutComputeTruth6( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, int fCompl0, int fCompl1, Sdb_Cut_t * pCutR, int fIsXor )
+{
+    int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t;
+    word t0 = *Sdb_CutTruth(p, pCut0);
+    word t1 = *Sdb_CutTruth(p, pCut1);
+    if ( Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 ) t0 = ~t0;
+    if ( Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 ) t1 = ~t1;
+    t0 = Abc_Tt6Expand( t0, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+    t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+    t =  fIsXor ? t0 ^ t1 : t0 & t1;
+    if ( (fCompl = (int)(t & 1)) ) t = ~t;
+    pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
+    assert( (int)(t & 1) == 0 );
+    truthId        = Vec_MemHashInsert(p->vTtMem, &t);
+    pCutR->iFunc   = Abc_Var2Lit( truthId, fCompl );
+    assert( (int)pCutR->nLeaves <= nOldSupp );
+    return (int)pCutR->nLeaves < nOldSupp;
+}
+static inline int Sdb_CutComputeTruth( Sdb_Sto_t * p, Sdb_Cut_t * pCut0, Sdb_Cut_t * pCut1, int fCompl0, int fCompl1, Sdb_Cut_t * pCutR, int fIsXor )
+{
+    if ( p->nCutSize <= 6 )
+        return Sdb_CutComputeTruth6( p, pCut0, pCut1, fCompl0, fCompl1, pCutR, fIsXor );
+    {
+    word uTruth[SDB_MAX_TT_WORDS], uTruth0[SDB_MAX_TT_WORDS], uTruth1[SDB_MAX_TT_WORDS];
+    int nOldSupp   = pCutR->nLeaves, truthId;
+    int nCutSize   = p->nCutSize, fCompl;
+    int nWords     = Abc_Truth6WordNum(nCutSize);
+    word * pTruth0 = Sdb_CutTruth(p, pCut0);
+    word * pTruth1 = Sdb_CutTruth(p, pCut1);
+    Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 );
+    Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 );
+    Abc_TtExpand( uTruth0, nCutSize, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+    Abc_TtExpand( uTruth1, nCutSize, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+    if ( fIsXor )
+        Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) );
+    else
+        Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) );
+    pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
+    assert( (uTruth[0] & 1) == 0 );
+//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
+    truthId        = Vec_MemHashInsert(p->vTtMem, uTruth);
+    pCutR->iFunc   = Abc_Var2Lit( truthId, fCompl );
+    assert( (int)pCutR->nLeaves <= nOldSupp );
+    return (int)pCutR->nLeaves < nOldSupp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sdb_CutCountBits( word i )
+{
+    i = i - ((i >> 1) & 0x5555555555555555);
+    i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
+    i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
+    return (i*(0x0101010101010101))>>56;
+}
+static inline void Sdb_CutAddUnit( Sdb_Sto_t * p, int iObj )
+{
+    Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+    if ( Vec_IntSize(vThis) == 0 )
+        Vec_IntPush( vThis, 1 );
+    else 
+        Vec_IntAddToEntry( vThis, 0, 1 );
+    Vec_IntPush( vThis, 1 );
+    Vec_IntPush( vThis, iObj );
+    Vec_IntPush( vThis, 2 );
+}
+static inline void Sdb_CutAddZero( Sdb_Sto_t * p, int iObj )
+{
+    Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+    assert( Vec_IntSize(vThis) == 0 );
+    Vec_IntPush( vThis, 1 );
+    Vec_IntPush( vThis, 0 );
+    Vec_IntPush( vThis, 0 );
+}
+static inline int Sdb_CutTreeLeaves( Sdb_Sto_t * p, Sdb_Cut_t * pCut )
+{
+    int i, Cost = 0;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
+    return Cost;
+}
+static inline int Sdb_StoPrepareSet( Sdb_Sto_t * p, int iObj, int Index )
+{
+    Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+    int i, v, * pCut, * pList = Vec_IntArray( vThis );
+    Sdb_ForEachCut( pList, pCut, i )
+    {
+        Sdb_Cut_t * pCutTemp = &p->pCuts[Index][i];
+        pCutTemp->nLeaves = pCut[0];
+        for ( v = 1; v <= pCut[0]; v++ )
+            pCutTemp->pLeaves[v-1] = pCut[v];
+        pCutTemp->iFunc = pCut[pCut[0]+1];
+        pCutTemp->Sign = Sdb_CutGetSign( pCutTemp );
+        pCutTemp->nTreeLeaves = Sdb_CutTreeLeaves( p, pCutTemp );
+    }
+    return pList[0];
+}
+static inline void Sdb_StoInitResult( Sdb_Sto_t * p )
+{
+    int i; 
+    for ( i = 0; i < SDB_MAX_CUTNUM; i++ )
+        p->ppCuts[i] = &p->pCuts[2][i];
+}
+static inline void Sdb_StoStoreResult( Sdb_Sto_t * p, int iObj, Sdb_Cut_t ** pCuts, int nCuts )
+{
+    int i, v;
+    Vec_Int_t * vList = Vec_WecEntry( p->vCuts, iObj );
+    Vec_IntPush( vList, nCuts );
+    for ( i = 0; i < nCuts; i++ )
+    {
+        Vec_IntPush( vList, pCuts[i]->nLeaves );
+        for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
+            Vec_IntPush( vList, pCuts[i]->pLeaves[v] );
+        Vec_IntPush( vList, pCuts[i]->iFunc );
+    }
+}
+static inline void Sdb_CutPrint( Sdb_Sto_t * p, int iObj, Sdb_Cut_t * pCut )
+{
+    int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia)); 
+    if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
+    printf( "%d  {", pCut->nLeaves );
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        printf( " %*d", nDigits, pCut->pLeaves[i] );
+    for ( ; i < (int)p->nCutSize; i++ )
+        printf( " %*s", nDigits, " " );
+    printf( "  }  Cost = %3d  CostL = %3d  Tree = %d  ", 
+        pCut->Cost, pCut->CostLev, pCut->nTreeLeaves );
+    printf( "\n" );
+}
+void Sdb_StoMergeCuts( Sdb_Sto_t * p, int iObj )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+    int fIsXor       = Gia_ObjIsXor(pObj);
+    int nCutSize     = p->nCutSize;
+    int nCutNum      = p->nCutNum;
+    int fComp0       = Gia_ObjFaninC0(pObj);
+    int fComp1       = Gia_ObjFaninC1(pObj);
+    int Fan0         = Gia_ObjFaninId0(pObj, iObj);
+    int Fan1         = Gia_ObjFaninId1(pObj, iObj);
+    int nCuts0       = Sdb_StoPrepareSet( p, Fan0, 0 );
+    int nCuts1       = Sdb_StoPrepareSet( p, Fan1, 1 );
+    int i, k, nCutsR = 0;
+    Sdb_Cut_t * pCut0, * pCut1, ** pCutsR = p->ppCuts;
+    assert( !Gia_ObjIsBuf(pObj) );
+    assert( !Gia_ObjIsMux(p->pGia, pObj) );
+    Sdb_StoInitResult( p );
+    p->CutCount[0] += nCuts0 * nCuts1;
+    for ( i = 0, pCut0 = p->pCuts[0]; i < nCuts0; i++, pCut0++ )
+    for ( k = 0, pCut1 = p->pCuts[1]; k < nCuts1; k++, pCut1++ )
+    {
+        if ( (int)(pCut0->nLeaves + pCut1->nLeaves) > nCutSize && Sdb_CutCountBits(pCut0->Sign | pCut1->Sign) > nCutSize )
+            continue;
+        p->CutCount[1]++; 
+        if ( !Sdb_CutMergeOrder(pCut0, pCut1, pCutsR[nCutsR], nCutSize) )
+            continue;
+        if ( Sdb_CutSetLastCutIsContained(pCutsR, nCutsR) )
+            continue;
+        p->CutCount[2]++;
+        if ( p->fCutMin && Sdb_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) )
+            pCutsR[nCutsR]->Sign = Sdb_CutGetSign(pCutsR[nCutsR]);
+        pCutsR[nCutsR]->nTreeLeaves = Sdb_CutTreeLeaves( p, pCutsR[nCutsR] );
+        nCutsR = Sdb_CutSetAddCut( pCutsR, nCutsR, nCutNum );
+    }
+    p->CutCount[3] += nCutsR;
+    p->nCutsOver += nCutsR == nCutNum-1;
+    p->nCutsR = nCutsR;
+    p->Pivot = iObj;
+    // debug printout
+    if ( 0 )
+    {
+        printf( "*** Obj = %4d  NumCuts = %4d\n", iObj, nCutsR );
+        for ( i = 0; i < nCutsR; i++ )
+            Sdb_CutPrint( p, iObj, pCutsR[i] );
+        printf( "\n" );
+    }
+    // verify
+    assert( nCutsR > 0 && nCutsR < nCutNum );
+    assert( Sdb_CutSetCheckArray(pCutsR, nCutsR) );
+    // store the cutset
+    Sdb_StoStoreResult( p, iObj, pCutsR, nCutsR );
+    if ( nCutsR > 1 || pCutsR[0]->nLeaves > 1 )
+        Sdb_CutAddUnit( p, iObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Iterate through the cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sdb_StoIterCutsOne( Sdb_Sto_t * p, int iObj )
+{
+    int fVerbose = 1;
+    Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+    int i, k, * pCut, * pList = Vec_IntArray( vThis );
+    word * pTruth;
+    Sdb_ForEachCut( pList, pCut, i )
+    {
+        if ( pCut[0] != 5 )
+            continue;
+        pTruth = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]));
+        for ( k = 0; k < 1920; k++ )
+            if ( s_FuncTruths[k] == (unsigned)*pTruth )
+                break;
+        if ( k < 1920 )
+        {
+            if ( fVerbose )
+            {
+                printf( "Object %d has 5-input cut:  ", iObj );
+                for ( k = 1; k <= pCut[0]; k++ )
+                    printf( "%d ", pCut[k] );
+                printf( "\n" );
+            }
+            return 1;
+        }
+    }
+    return 0;
+}
+void Sdb_StoIterCuts( Sdb_Sto_t * p )
+{
+    Gia_Obj_t * pObj;   
+    int iObj, Count = 0;
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+        Count += Sdb_StoIterCutsOne( p, iObj );
+    printf( "Detected %d cuts.\n", Count );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Incremental cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sdb_Sto_t * Sdb_StoAlloc( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fCutMin, int fVerbose )
+{
+    Sdb_Sto_t * p;
+    assert( nCutSize < SDB_CUT_NO_LEAF );
+    assert( nCutSize > 1 && nCutSize <= SDB_MAX_CUTSIZE );
+    assert( nCutNum > 1 && nCutNum < SDB_MAX_CUTNUM );
+    p = ABC_CALLOC( Sdb_Sto_t, 1 );
+    p->clkStart = Abc_Clock();
+    p->nCutSize = nCutSize;
+    p->nCutNum  = nCutNum;
+    p->fCutMin  = fCutMin;
+    p->fVerbose = fVerbose;
+    p->pGia     = pGia;
+    p->vRefs    = Vec_IntAlloc( Gia_ManObjNum(pGia) );
+    p->vCuts    = Vec_WecStart( Gia_ManObjNum(pGia) );
+    p->vTtMem   = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
+    return p;
+}
+void Sdb_StoFree( Sdb_Sto_t * p )
+{
+    Vec_IntFree( p->vRefs );
+    Vec_WecFree( p->vCuts );
+    if ( p->fCutMin )
+        Vec_MemHashFree( p->vTtMem );
+    if ( p->fCutMin )
+        Vec_MemFree( p->vTtMem );
+    ABC_FREE( p );
+}
+void Sdb_StoComputeCutsConst0( Sdb_Sto_t * p, int iObj )
+{
+    Sdb_CutAddZero( p, iObj );
+}
+void Sdb_StoComputeCutsCi( Sdb_Sto_t * p, int iObj )
+{
+    Sdb_CutAddUnit( p, iObj );
+}
+void Sdb_StoComputeCutsNode( Sdb_Sto_t * p, int iObj )
+{
+    Sdb_StoMergeCuts( p, iObj );
+}
+void Sdb_StoRefObj( Sdb_Sto_t * p, int iObj )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+    assert( iObj == Vec_IntSize(p->vRefs) );
+    Vec_IntPush( p->vRefs, 0 );
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
+        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId1(pObj, iObj), 1 );
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
+}
+void Sdb_StoComputeCutsTest( Gia_Man_t * pGia )
+{
+    Sdb_Sto_t * p = Sdb_StoAlloc( pGia, 6, 20, 1, 1 );
+    Gia_Obj_t * pObj;   
+    int i, iObj;
+    // prepare references
+    Gia_ManForEachObj( p->pGia, pObj, iObj )
+        Sdb_StoRefObj( p, iObj );
+    // compute cuts
+    Sdb_StoComputeCutsConst0( p, 0 );
+    Gia_ManForEachCiId( p->pGia, iObj, i )
+        Sdb_StoComputeCutsCi( p, iObj );
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+        Sdb_StoComputeCutsNode( p, iObj );
+    if ( p->fVerbose )
+    {
+        printf( "Running cut computation with CutSize = %d  CutNum = %d:\n", p->nCutSize, p->nCutNum );
+        printf( "CutPair = %.0f  ",         p->CutCount[0] );
+        printf( "Merge = %.0f (%.2f %%)  ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
+        printf( "Eval = %.0f (%.2f %%)  ",  p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
+        printf( "Cut = %.0f (%.2f %%)  ",   p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
+        printf( "Cut/Node = %.2f  ",        p->CutCount[3] / Gia_ManAndNum(p->pGia) );
+        printf( "\n" );
+        printf( "Over = %4d  ",             p->nCutsOver );
+        Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
+    }
+    Sdb_StoIterCuts( p );
+    Sdb_StoFree( p );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index f4c69892..2e62826d 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -15,4 +15,5 @@ SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecSt.c \
     src/proof/acec/acecTree.c \
     src/proof/acec/acecUtil.c \
+    src/proof/acec/acec2Mult.c \
     src/proof/acec/acecXor.c