New SAT-based optimization package.

7 files changed, 821 insertions, 43 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4dcea33a..25bcc306 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -55,6 +55,7 @@
 #include "sat/bmc/bmc.h"
 #include "proof/ssc/ssc.h"
 #include "opt/sfm/sfm.h"
+#include "opt/sbd/sbd.h"
 #include "bool/rpo/rpo.h"
 #include "map/mpm/mpm.h"
 #include "opt/fret/fretime.h"
@@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Mfsd               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&mfsd",         Abc_CommandAbc9Mfsd,         0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -40829,6 +40832,132 @@ usage:
   Synopsis    []
 
   Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars );
+    Gia_Man_t * pTemp; int c;
+    Sbd_Par_t Pars, * pPars = &Pars;
+    Sbd_ParSetDefault( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoLevels = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoLevels < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoFanMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoFanMax < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWinSizeMax < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManBufNum(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
+        return 1;
+    }
+    if ( Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
+        return 0;
+    }
+    pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-avwh]\n" );
+    Abc_Print( -2, "\t           performs SAT-based delay-oriented AIG optimization\n" );
+    Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n",         pPars->nLutSize );
+    Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevels );
+    Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nTfoFanMax );
+    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
+    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
 
   SideEffects []
 
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 7de6bd81..3431c761 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -74,7 +74,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     Abc_Obj_t * pNode, * pFanin;
     char * pSopString;
     int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
-    int Limit = 300;
+    int Limit = 500;
 
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
 
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 5a4ef545..b8a34da7 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -266,6 +266,28 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
         for ( w = 0; w < nWords; w++ )
             pOut[w] = pIn1[w] & pIn2[w];
 }
+static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords )
+{
+    int w;
+    if ( fCompl1 )
+    {
+        if ( fCompl2 )
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = ~pIn1[w] & ~pIn2[w];
+        else
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = ~pIn1[w] & pIn2[w];
+    }
+    else
+    {
+        if ( fCompl2 )
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = pIn1[w] & ~pIn2[w];
+        else
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = pIn1[w] & pIn2[w];
+    }
+}
 static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -288,6 +310,12 @@ static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
     for ( w = 0; w < nWords; w++ )
         pOut[w] = pIn1[w] | pIn2[w];
 }
+static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] |= pIn1[w] ^ pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index 946a2ee4..e1e39a3b 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -35,42 +35,21 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Sbd_Ntk_t_ Sbd_Ntk_t;
 typedef struct Sbd_Par_t_ Sbd_Par_t;
 struct Sbd_Par_t_
 {
-    int             nTfoLevMax;    // the maximum fanout levels
-    int             nTfiLevMax;    // the maximum fanin levels
-    int             nFanoutMax;    // the maximum number of fanouts
-    int             nDepthMax;     // the maximum depth to try
-    int             nVarMax;       // the maximum variable count
-    int             nMffcMin;      // the minimum MFFC size
-    int             nMffcMax;      // the maximum MFFC size
-    int             nDecMax;       // the maximum number of decompositions
-    int             nWinSizeMax;   // the maximum window size
-    int             nGrowthLevel;  // the maximum allowed growth in level
-    int             nBTLimit;      // the maximum number of conflicts in one SAT run
-    int             nNodesMax;     // the maximum number of nodes to try
-    int             iNodeOne;      // one particular node to try
-    int             nFirstFixed;   // the number of first nodes to be treated as fixed
-    int             nTimeWin;      // the size of timing window in percents
-    int             DeltaCrit;     // delay delta in picoseconds
-    int             DelAreaRatio;  // delay/area tradeoff (how many ps we trade for a unit of area)
-    int             fRrOnly;       // perform redundance removal
-    int             fArea;         // performs optimization for area
-    int             fAreaRev;      // performs optimization for area in reverse order
-    int             fMoreEffort;   // performs high-affort minimization
-    int             fUseAndOr;     // enable internal detection of AND/OR gates
-    int             fZeroCost;     // enable zero-cost replacement
-    int             fUseSim;       // enable simulation
-    int             fPrintDecs;    // enable printing decompositions
-    int             fAllBoxes;     // enable preserving all boxes
-    int             fLibVerbose;   // enable library stats
-    int             fDelayVerbose; // enable delay stats
-    int             fVerbose;      // enable basic stats
-    int             fVeryVerbose;  // enable detailed stats
+    int             nLutSize;     // target LUT size
+    int             nTfoLevels;   // the number of TFO levels (windowing)
+    int             nTfoFanMax;   // the max number of fanouts (windowing)
+    int             nWinSizeMax;  // maximum window size (windowing)
+    int             nBTLimit;     // maximum number of SAT conflicts 
+    int             nWords;       // simulation word count
+    int             fArea;        // area-oriented optimization
+    int             fVerbose;     // verbose flag
+    int             fVeryVerbose; // verbose flag
 };
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,16 +61,7 @@ struct Sbd_Par_t_
 /*=== sbdCnf.c ==========================================================*/
 /*=== sbdCore.c ==========================================================*/
 extern void         Sbd_ParSetDefault( Sbd_Par_t * pPars );
-extern int          Sbd_NtkPerform( Sbd_Ntk_t * p, Sbd_Par_t * pPars );
-/*=== sbdNtk.c ==========================================================*/
-extern Sbd_Ntk_t *  Sbd_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths );
-extern void         Sbd_NtkFree( Sbd_Ntk_t * p );
-extern Vec_Int_t *  Sbd_NodeReadFanins( Sbd_Ntk_t * p, int i );
-extern word *       Sbd_NodeReadTruth( Sbd_Ntk_t * p, int i );
-extern int          Sbd_NodeReadFixed( Sbd_Ntk_t * p, int i );
-extern int          Sbd_NodeReadUsed( Sbd_Ntk_t * p, int i );
-/*=== sbdWin.c ==========================================================*/
-extern Vec_Int_t *  Sbd_NtkDfs( Sbd_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes );
+extern Gia_Man_t *  Sbd_NtkPerform( Gia_Man_t * p, Sbd_Par_t * pPars );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index 4d86d2ee..2120a8f9 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -19,14 +19,44 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SBD_MAX_LUTSIZE 6
+
+
+typedef struct Sbd_Man_t_ Sbd_Man_t;
+struct Sbd_Man_t_
+{
+    Sbd_Par_t *     pPars;       // user's parameters
+    Gia_Man_t *     pGia;        // user's AIG manager (will be modified by adding nodes)
+    Vec_Wec_t *     vTfos;       // TFO for each node (roots are marked) (windowing)
+    Vec_Int_t *     vLutLevs;    // LUT level for each node after resynthesis
+    Vec_Int_t *     vLutCuts;    // LUT cut for each nodes after resynthesis
+    Vec_Int_t *     vMirrors;    // alternative node
+    Vec_Wrd_t *     vSims[3];    // simulation information (main, backup, controlability)
+    Vec_Int_t *     vCover;      // temporary
+    // target node
+    int             Pivot;       // target node
+    int             nTfiLeaves;  // TFI leaves
+    int             nTfiNodes;   // TFI nodes
+    Vec_Int_t *     vTfo;        // TFO (excludes node, includes roots)
+    Vec_Int_t *     vLeaves;     // leaves (TFI leaves + extended leaves)
+    Vec_Int_t *     vTfi;        // TFI (TFI + node + extended TFI)
+    Vec_Int_t *     vCounts[2];  // counters of zeros and ones
+};
+
+static inline int *  Sbd_ObjCut( Sbd_Man_t * p, int i )  { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
+
+static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i );         }
+static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i );         }
+static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i );         }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,7 +72,454 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Sbd_ParSetDefault( Sbd_Par_t * pPars )
+{
+    memset( pPars, 0, sizeof(Sbd_Par_t) );
+    pPars->nLutSize     = 4;  // target LUT size
+    pPars->nTfoLevels   = 4;  // the number of TFO levels (windowing)
+    pPars->nTfoFanMax   = 4;  // the max number of fanouts (windowing)
+    pPars->nWinSizeMax  = 0;  // maximum window size (windowing)
+    pPars->nBTLimit     = 0;  // maximum number of SAT conflicts 
+    pPars->nWords       = 1;  // simulation word count
+    pPars->fArea        = 0;  // area-oriented optimization
+    pPars->fVerbose     = 0;  // verbose flag
+    pPars->fVeryVerbose = 0;  // verbose flag
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes window roots for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
+{
+    Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked
+    Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage
+    Vec_Int_t * vNodes, * vNodes0, * vNodes1;
+    int i, k, k2, Id, Fan;
+    Gia_ManLevelNum( p );
+    Gia_ManCreateRefs( p );
+    Gia_ManCleanMark0( p );
+    Gia_ManForEachCiId( p, Id, i )
+    {
+        vNodes = Vec_WecEntry( vTemp, Id );
+        Vec_IntGrow( vNodes, 1 );
+        Vec_IntPush( vNodes, Id );
+    }
+    Gia_ManForEachAndId( p, Id )
+    {
+        int fAlwaysRoot = Gia_ObjRefNumId(p, Id) >= nTfoFanMax;
+        vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) );
+        vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) );
+        vNodes = Vec_WecEntry( vTemp, Id );
+        Vec_IntTwoMerge2( vNodes, vNodes0, vNodes1 );
+        k2 = 0;
+        Vec_IntForEachEntry( vNodes, Fan, k )
+        {
+            int fRoot = fAlwaysRoot || (Gia_ObjLevelId(p, Id) - Gia_ObjLevelId(p, Fan) >= nTfoLevels);
+            Vec_WecPush( vTfos, Fan, Abc_Var2Lit(Id, fRoot) );
+            if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan );
+        }
+        Vec_IntShrink( vNodes, k2 );
+        Vec_IntPush( vNodes, Id );
+    }
+    Vec_WecFree( vTemp );
+    // print the results
+    Vec_WecForEachLevel( vTfos, vNodes, i )
+    {
+        if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
+            continue;
+        printf( "Node %3d : ", i );
+        Vec_IntForEachEntry( vNodes, Fan, k )
+            printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" );
+        printf( "\n" );
+
+    }
+    return vTfos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Manager manipulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
+{
+    int i, w, Id;
+    Sbd_Man_t * p = ABC_CALLOC( Sbd_Man_t, 1 );  
+    p->pPars      = pPars;
+    p->pGia       = pGia;
+    p->vTfos      = Sbd_ManWindowRoots( pGia, pPars->nTfoLevels, pPars->nTfoFanMax );
+    p->vLutLevs   = Vec_IntStart( Gia_ManObjNum(pGia) );
+    p->vLutCuts   = Vec_IntStart( Gia_ManObjNum(pGia) * (p->pPars->nLutSize + 1) );
+    p->vMirrors   = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+    for ( i = 0; i < 3; i++ )
+        p->vSims[i] = Vec_WrdStart( Gia_ManObjNum(pGia) * p->pPars->nWords );
+    // target node
+    p->vCover     = Vec_IntStart( 100 );
+    p->vLeaves    = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vTfi       = Vec_IntAlloc( Gia_ManAndNum(pGia) );
+    p->vCounts[0] = Vec_IntAlloc( 100 );
+    p->vCounts[1] = Vec_IntAlloc( 100 );
+    // start input cuts
+    Gia_ManForEachCiId( pGia, Id, i )
+    {
+        int * pCut = Sbd_ObjCut( p, Id );
+        pCut[0] = 1;
+        pCut[1] = Id;
+    }
+    // generate random input
+    Gia_ManRandom( 1 );
+    Gia_ManForEachCiId( pGia, Id, i )
+        for ( w = 0; w < p->pPars->nWords; w++ )
+            Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
+    return p;
+}
+void Sbd_ManStop( Sbd_Man_t * p )
+{
+    int i;
+    Vec_WecFree( p->vTfos );
+    Vec_IntFree( p->vLutLevs );
+    Vec_IntFree( p->vLutCuts );
+    Vec_IntFree( p->vMirrors );
+    for ( i = 0; i < 3; i++ )
+        Vec_WrdFree( p->vSims[i] );
+    Vec_IntFree( p->vCover  );
+    Vec_IntFree( p->vLeaves );
+    Vec_IntFree( p->vTfi );
+    Vec_IntFree( p->vCounts[0] );
+    Vec_IntFree( p->vCounts[1] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructing window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node )
+{
+    Gia_Obj_t * pObj;
+    if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
+        Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) );
+    if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) || Node == 0 )
+        return;
+    Gia_ObjSetTravIdCurrentId(p->pGia, Node);
+    pObj = Gia_ManObj( p->pGia, Node );
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( p->vLeaves, Node );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) );
+    Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
+    Vec_IntPush( p->vTfi, Node );
+    // simulate
+    Abc_TtAndCompl( Sbd_ObjSim0(p, Node), 
+        Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+        Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+        p->pPars->nWords );
+    if ( pObj->fMark0 )
+        Abc_TtAndCompl( Sbd_ObjSim1(p, Node), 
+            Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+            Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+            p->pPars->nWords );
+}
+void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
+{
+    int iObj0 = Gia_ObjFaninId0(Gia_ManObj(p->pGia, Node), Node);
+    int iObj1 = Gia_ObjFaninId1(Gia_ManObj(p->pGia, Node), Node);
+    word * pCtrl  = Sbd_ObjSim2(p, Node);
+    word * pCtrl0 = Sbd_ObjSim2(p, iObj0);
+    word * pCtrl1 = Sbd_ObjSim2(p, iObj1);
+    word * pSims  = Sbd_ObjSim0(p, Node);
+    word * pSims0 = Sbd_ObjSim0(p, iObj0);
+    word * pSims1 = Sbd_ObjSim0(p, iObj1);
+    int w;
+    for ( w = 0; w < p->pPars->nWords; w++ )
+    {
+        pCtrl0[w] = pCtrl[w] & (pSims[w] | pSims1[w]);
+        pCtrl1[w] = pCtrl[w] & (pSims[w] | pSims0[w] | (~pSims0[w] & ~pSims1[w]));
+    }
+}
+void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
+{
+    int i, Node;
+    // assign pivot and TFO (assume siminfo is assigned at the PIs)
+    p->Pivot = Pivot;
+    p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
+    Vec_IntClear( p->vLeaves );
+    Vec_IntClear( p->vTfi );
+    // simulate TFI cone
+    Gia_ManIncrementTravId( p->pGia );
+    Sbd_ManWindowSim_rec( p, Pivot );
+    p->nTfiLeaves = Vec_IntSize( p->vLeaves );
+    p->nTfiNodes = Vec_IntSize( p->vTfi );
+    // simulate node
+    Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
+    Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
+    // simulate extended TFI cone
+    Vec_IntForEachEntry( p->vTfo, Node, i )
+    {
+        Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1;
+        if ( Abc_LitIsCompl(Node) ) 
+            Sbd_ManWindowSim_rec( p, Node );
+    }
+    // remove marks
+    Gia_ManObj(p->pGia, Pivot)->fMark0 = 0;
+    Vec_IntForEachEntry( p->vTfo, Node, i )
+        Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 0;
+    // compute controlability for node
+    Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
+    Vec_IntForEachEntry( p->vTfo, Node, i )
+        if ( Abc_LitIsCompl(Node) ) // root
+            Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Node), Sbd_ObjSim1(p, Node), p->pPars->nWords );
+    // propagate controlability to TFI
+    for ( i = p->nTfiNodes; i >= 0 && (Node = Vec_IntEntry(p->vTfi, i)); i-- )
+        Sbd_ManPropagateControl( p, Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Profiling divisor candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
+{
+    int i, k, k0, k1, Id, Bit0, Bit1;
+    assert( p->Pivot == Pivot );
+    Vec_IntClear( p->vCounts[0] );
+    Vec_IntClear( p->vCounts[1] );
+    // sampling matrix
+    for ( k = 0; k < p->pPars->nWords * 64; k++ )
+    {
+        printf( "%3d : ", k );
+        Vec_IntForEachEntry( p->vTfi, Id, i )
+        {
+            word * pSims = Sbd_ObjSim0( p, Id );
+            word * pCtrl = Sbd_ObjSim2( p, Id );
+            if ( i == Vec_IntSize(p->vTfi)-1 )
+            {
+                if ( Abc_TtGetBit(pCtrl, k) )
+                    Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
+                printf( " " );
+            }
+            printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' );
+        }
+        printf( "\n" );
+    }
+    // covering table
+    printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) );
+    Vec_IntForEachEntry( p->vCounts[0], Bit0, k0 )
+    Vec_IntForEachEntry( p->vCounts[1], Bit1, k1 )
+    {
+        printf( "%3d %3d : ", Bit0, Bit1 );
+        Vec_IntForEachEntry( p->vTfi, Id, i )
+        {
+            word * pSims = Sbd_ObjSim0( p, Id );
+            word * pCtrl = Sbd_ObjSim2( p, Id );
+            if ( i == Vec_IntSize(p->vTfi)-1 )
+                printf( " " );
+            printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' );
+        }
+        printf( "\n" );
+    }
+}
+int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, int * pCut, word * pTruth )
+{
+    Sbd_ManPrintObj( p, Pivot );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay-oriented k-feasible cut at the node.]
+
+  Description [Return 1 if node's LUT level does not exceed those of the fanins.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_CutMergeSimple( Sbd_Man_t * p, int * pCut1, int * pCut2, int * pCut )
+{
+    int * pBeg  = pCut + 1;
+    int * pBeg1 = pCut1 + 1;
+    int * pBeg2 = pCut2 + 1;
+    int * pEnd1 = pCut1 + 1 + pCut1[0];
+    int * pEnd2 = pCut2 + 1 + pCut2[0];
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg++ = *pBeg1++;
+        else 
+            *pBeg++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg++ = *pBeg2++;
+    return (pCut[0] = pBeg - pCut - 1);
+}
+int Sbd_ManComputeCut( Sbd_Man_t * p, int Node )
+{
+    int pCut[2*SBD_MAX_LUTSIZE];     
+    int iFan0   = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
+    int iFan1   = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
+    int Level0  = Vec_IntEntry( p->vLutLevs, iFan0 );
+    int Level1  = Vec_IntEntry( p->vLutLevs, iFan1 );
+    int LevMax  = Abc_MaxInt( Level0, Level1 );
+    int * pCut0 = Sbd_ObjCut( p, iFan0 );
+    int * pCut1 = Sbd_ObjCut( p, iFan1 );
+    int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0; 
+    int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1; 
+    int nSize   = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut );
+    int Result  = 1; // no need to resynthesize
+    assert( iFan0 != iFan1 );
+    if ( nSize > p->pPars->nLutSize )
+    {
+        pCut[0] = 2;
+        pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1;
+        pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0;
+        Result  = LevMax ? 0 : 1;
+        LevMax++;
+    }
+    assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+    Vec_IntWriteEntry( p->vLutLevs, Node, LevMax );
+    memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
+    return Result;
+}
+int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, int * pCut, word Truth )
+{
+    Vec_Int_t vLeaves = { pCut[0], pCut[0], pCut+1 };
+    int iLit = Dsm_ManTruthToGia( p->pGia, &Truth, &vLeaves, p->vCover );
+    int i, k, w, iObjLast = Gia_ManObjNum(p->pGia);
+    assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
+    Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
+    assert( Vec_IntSize(p->vLutLevs) == iObjLast );
+    for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
+    {
+        Vec_IntPush( p->vLutLevs, 0 );
+        Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
+        Sbd_ManComputeCut( p, i );
+        for ( k = 0; k < 3; k++ )
+            for ( w = 0; w < p->pPars->nWords; w++ )
+                Vec_WrdPush( p->vSims[k], 0 );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new AIG after resynthesis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
+{
+    Gia_Obj_t * pObj;
+    int Obj = Node;
+    if ( Vec_IntEntry(vMirrors, Node) >= 0 )
+        Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
+    pObj = Gia_ManObj( p, Obj );
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
+    Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
+    if ( Gia_ObjIsXor(pObj) )
+        pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    else
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // set the original node as well
+    if ( Obj != Node )
+        Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
+} 
+Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAndId( p, i )
+        Sbd_ManDerive_rec( pNew, p, i, vMirrors );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
 
+/**Function*************************************************************
+
+  Synopsis    [Performs delay optimization for the given LUT size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
+{
+    Gia_Man_t * pNew;  word Truth;
+    Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
+    int Pivot, pCut[2*SBD_MAX_LUTSIZE];     
+    assert( pPars->nLutSize <= 6 );
+    Gia_ManForEachAndId( pGia, Pivot )
+    {
+        if ( Sbd_ManComputeCut( p, Pivot ) )
+            continue;
+        Sbd_ManWindow( p, Pivot );
+        if ( Sbd_ManExplore( p, Pivot, pCut, &Truth ) )
+            Sbd_ManImplement( p, Pivot, pCut, Truth );
+    }
+    pNew = Sbd_ManDerive( pGia, p->vMirrors );
+    Sbd_ManStop( p );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 1157d02c..8211610c 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -34,6 +34,7 @@
 #include "misc/vec/vec.h"
 #include "sat/bsat/satSolver.h"
 #include "misc/util/utilNam.h"
+#include "misc/util/utilTruth.h"
 #include "map/scl/sclLib.h"
 #include "map/scl/sclCon.h"
 #include "bool/kit/kit.h"
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
index bd49c50e..ae865627 100644
--- a/src/opt/sbd/sbdSat.c
+++ b/src/opt/sbd/sbdSat.c
@@ -37,6 +37,179 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SBD_LUTS_MAX   2
+#define SBD_SIZE_MAX   4
+#define SBD_DIV_MAX   16
+
+// new AIG manager
+typedef struct Sbd_Pro_t_ Sbd_Pro_t;
+struct Sbd_Pro_t_
+{
+    int             nLuts;  // LUT count
+    int             nSize;  // LUT size
+    int             nDivs;  // divisor count
+    int             nVars;  // intermediate variables (nLuts * nSize)
+    int             nPars;  // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs) 
+    int             pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX];            // lut parameters
+    int             pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX];  // topo parameters
+    int             pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1];              // internal variables
+    int             pDivs[SBD_DIV_MAX];                               // divisor variables (external)
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
+{
+    Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
+    int i, k, d, v, n, iVar = 0;
+    assert( nLuts >= 1 && nLuts <= 2 );
+    memset( p, 0, sizeof(Sbd_Pro_t) );
+    p->nLuts = nLuts;
+    p->nSize = nSize;
+    p->nDivs = nDivs;
+    p->nVars = nLuts * nSize;
+    p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
+    // set parameters
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < (1 << nSize); k++ )
+        p->pPars1[i][k] = iVar++;
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+        p->pPars2[i][k][d] = iVar++;
+    // set intermediate variables
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < nSize; k++ )
+        p->pVars[i][k] = iVar++;
+    // set top variables 
+    for ( i = 1; i < nLuts; i++ )
+        p->pVars[i][nSize] = p->pVars[i-1][0];
+    // set divisor variables
+    for ( d = 0; d < nDivs; d++ )
+        p->pDivs[d] = iVar++;
+    assert( iVar == p->nPars + p->nVars + p->nDivs );
+
+    // input compatiblity clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = (i > 0); k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+    for ( n = 0; n < nDivs; n++ )
+    {
+        if ( n < d )
+        {
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
+            Vec_IntPush( vCnf, -1 );
+        }
+        else if ( k < nSize-1 )
+        {
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
+            Vec_IntPush( vCnf, -1 );
+        }
+    }
+
+    // create LUT clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < (1 << nSize); k++ )
+    for ( n = 0; n < 2; n++ )
+    {
+        for ( v = 0; v < nSize; v++ )
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
+        Vec_IntPush( vCnf, -1 );
+    }
+
+    // create input clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = (i > 0); k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
+        Vec_IntPush( vCnf, -1 );
+    }
+
+    return vCnf;
+}
+// add clauses to the don't-care computation solver
+void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
+{
+    int pLits[8], nLits, i, k, iLit, RetValue;
+    int ThisTopVar = p->pVars[0][p->nSize];
+    int FirstDivVar = p->nPars + p->nVars;
+    // add clauses
+    for ( i = 0; i < Vec_IntSize(vCnf); i++ )
+    {
+        assert( Vec_IntEntry(vCnf, i) != -1 );
+        for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
+            if ( Vec_IntEntry(vCnf, i) == -1 )
+                break;
+        nLits = 0;
+        Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
+            if ( Abc_Lit2Var(iLit) == ThisTopVar )
+                pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
+            else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+                pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
+            else
+                pLits[nLits++] = iLit + 2 * iStartVar;
+        }
+        assert( nLits <= 8 );
+        RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+        assert( RetValue );
+    }
+}
+// add clauses to the functionality evaluation solver
+void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
+{
+    Vec_Int_t * vLevel;
+    int pLits[8], nLits, i, k, iLit, RetValue;
+    int ThisTopVar = p->pVars[0][p->nSize];
+    int FirstDivVar = p->nPars + p->nVars;
+    int FirstIntVar = p->nPars;
+    // add clauses
+    Vec_WecForEachLevel( vCnf, vLevel, i )
+    {
+        nLits = 0;
+        Vec_IntForEachEntry( vLevel, iLit, k ) {
+            if ( Abc_Lit2Var(iLit) == ThisTopVar )
+            {
+                if ( Abc_LitIsCompl(iLit) == iTopVarValue )
+                    break;
+                continue;
+            }
+            else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+            {
+                if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
+                    break;
+                continue;
+            }
+            else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
+                pLits[nLits++] = iLit + 2 * iStartVar;
+            else
+                pLits[nLits++] = iLit;
+        }
+        if ( k < Vec_IntSize(vLevel) )
+            continue;
+        assert( nLits <= 8 );
+        RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+        assert( RetValue );
+    }
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []