abcExact.c

/**CFile****************************************************************

  FileName    [abcExact.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Find minimum size networks with a SAT solver.]

  Author      [Mathias Soeken]

  Affiliation [EPFL]

  Date        [Ver. 1.0. Started - July 15, 2016.]

  Revision    [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

/* This implementation is based on Exercises 477 and 478 in
 * Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2
 */

#include "base/abc/abc.h"

#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecInt.h"
#include "misc/vec/vecPtr.h"
#include "proof/cec/cec.h"
#include "sat/bsat/satSolver.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

/***********************************************************************

  Synopsis    [Some truth table helper functions.]

***********************************************************************/

static word s_Truths8[32] = {
    ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA),
    ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC),
    ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
    ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
    ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
    ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
    ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
    ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
};

static word s_Truths8Neg[32] = {
    ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555),
    ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333),
    ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F),
    ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF),
    ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF),
    ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF),
    ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000),
    ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000)
};

static int Abc_TtIsSubsetWithMask( word * pSmall, word * pLarge, word * pMask, int nWords )
{
    int w;
    for ( w = 0; w < nWords; ++w )
        if ( ( pSmall[w] & pLarge[w] & pMask[w] ) != ( pSmall[w] & pMask[w] ) )
            return 0;
    return 1;
}

static int Abc_TtCofsOppositeWithMask( word * pTruth, word * pMask, int nWords, int iVar )
{
    if ( iVar < 6 )
    {
        int w, Shift = ( 1 << iVar );
        for ( w = 0; w < nWords; ++w )
            if ( ( ( pTruth[w] << Shift ) & s_Truths6[iVar] & pMask[w] ) != ( ~pTruth[w] & s_Truths6[iVar] & pMask[w] ) )
                return 0;
        return 1;
    }
    else
    {
        int w, Step = ( 1 << ( iVar - 6 ) );
        word * p = pTruth, * m = pMask, * pLimit = pTruth + nWords;
        for ( ; p < pLimit; p += 2 * Step, m += 2 * Step )
            for ( w = 0; w < Step; ++w )
                if ( ( p[w] & m[w] ) != ( ~p[w + Step] & m[w + Step] ) )
                    return 0;
        return 1;
    }
}

// checks whether we can decompose as OP(x^p, g) where OP in {AND, OR} and p in {0, 1}
// returns p if OP = AND, and 2 + p if OP = OR
static int Abc_TtIsTopDecomposable( word * pTruth, word * pMask, int nWords, int iVar )
{
    assert( iVar < 8 );

    if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8[iVar << 2], pMask, nWords ) ) return 1;
    if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8Neg[iVar << 2], pMask, nWords ) ) return 2;
    if ( Abc_TtIsSubsetWithMask( &s_Truths8[iVar << 2], pTruth, pMask, nWords ) ) return 3;
    if ( Abc_TtIsSubsetWithMask( &s_Truths8Neg[iVar << 2], pTruth, pMask, nWords ) ) return 4;
    if ( Abc_TtCofsOppositeWithMask( pTruth, pMask, nWords, iVar ) ) return 5;

    return 0;
}

// checks whether we can decompose as OP(x1, OP(x2, OP(x3, ...))) where pVars = {x1, x2, x3, ...}
// OP can be different and vars can be complemented
static int Abc_TtIsStairDecomposable( word * pTruth, int nWords, int * pVars, int nSize, int * pStairFunc )
{
    int i, d;
    word pMask[4];
    word pCopy[4];

    Abc_TtCopy( pCopy, pTruth, nWords, 0 );
    Abc_TtMask( pMask, nWords, nWords * 64 );

    for ( i = 0; i < nSize; ++i )
    {
        d = Abc_TtIsTopDecomposable( pCopy, pMask, nWords, pVars[i] );
        if ( !d )
            return 0; /* not decomposable */

        pStairFunc[i] = d;

        switch ( d )
        {
        case 1: /* AND(x, g) */
        case 4: /* OR(!x, g) */
            Abc_TtAnd( pMask, pMask, &s_Truths8[pVars[i] << 2], nWords, 0 );
            break;
        case 2: /* AND(!x, g) */
        case 3: /* OR(x, g) */
            Abc_TtAnd( pMask, pMask, &s_Truths8Neg[pVars[i] << 2], nWords, 0 );
            break;
        case 5:
            Abc_TtXor( pCopy, pCopy, &s_Truths8[pVars[i] << 2], nWords, 0 );
            break;
        }
    }

    return 1; /* decomposable */
}

/***********************************************************************

  Synopsis    [Some printing utilities.]

***********************************************************************/

static inline void Abc_DebugPrint( const char* str, int fCond )
{
    if ( fCond )
    {
        printf( "%s", str );
        fflush( stdout );
    }
}

static inline void Abc_DebugPrintInt( const char* fmt, int n, int fCond )
{
    if ( fCond )
    {
        printf( fmt, n );
        fflush( stdout );
    }
}

static inline void Abc_DebugPrintIntInt( const char* fmt, int n1, int n2, int fCond )
{
    if ( fCond )
    {
        printf( fmt, n1, n2 );
        fflush( stdout );
    }
}

static inline void Abc_DebugErase( int n, int fCond )
{
    int i;
    if ( fCond )
    {
        for ( i = 0; i < n; ++i )
            printf( "\b" );
        fflush( stdout );
    }
}

/***********************************************************************

  Synopsis    [BMS.]

***********************************************************************/

#define ABC_EXACT_SOL_NVARS  0
#define ABC_EXACT_SOL_NFUNC  1
#define ABC_EXACT_SOL_NGATES 2

#define ANSI_COLOR_RED     "\x1b[31m"
#define ANSI_COLOR_GREEN   "\x1b[32m"
#define ANSI_COLOR_YELLOW  "\x1b[33m"
#define ANSI_COLOR_BLUE    "\x1b[34m"
#define ANSI_COLOR_MAGENTA "\x1b[35m"
#define ANSI_COLOR_CYAN    "\x1b[36m"
#define ANSI_COLOR_RESET   "\x1b[0m"

typedef struct Ses_Man_t_ Ses_Man_t;
struct Ses_Man_t_
{
    sat_solver * pSat;                  /* SAT solver */

    word *       pSpec;                 /* specification */
    int          bSpecInv;              /* remembers whether spec was inverted for normalization */
    int          nSpecVars;             /* number of variables in specification */
    int          nSpecFunc;             /* number of functions to synthesize */
    int          nSpecWords;            /* number of words for function */
    int          nRows;                 /* number of rows in the specification (without 0) */
    int          nMaxDepth;             /* maximum depth (-1 if depth is not constrained) */
    int          nMaxDepthTmp;          /* temporary copy to modify nMaxDepth temporarily */
    int *        pArrTimeProfile;       /* arrival times of inputs (NULL if arrival times are ignored) */
    int          pArrTimeProfileTmp[8]; /* temporary copy to modify pArrTimeProfile temporarily */
    int          nArrTimeDelta;         /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */
    int          nArrTimeMax;           /* maximum normalized arrival time */
    int          nBTLimit;              /* conflict limit */
    int          fMakeAIG;              /* create AIG instead of general network */
    int          fVerbose;              /* be verbose */
    int          fVeryVerbose;          /* be very verbose */
    int          fExtractVerbose;       /* be verbose about solution extraction */
    int          fSatVerbose;           /* be verbose about SAT solving */
    int          fReasonVerbose;        /* be verbose about give-up reasons */
    word         pTtValues[4];          /* truth table values to assign */
    Vec_Int_t *  vPolar;                /* variables with positive polarity */
    Vec_Int_t *  vAssump;               /* assumptions */
    int          nRandRowAssigns;       /* number of random row assignments to initialize CEGAR */
    int          fKeepRowAssigns;       /* if 1, keep counter examples in CEGAR for next number of gates */

    int          nGates;                /* number of gates */
    int          nStartGates;           /* number of gates to start search (-1), i.e., to start from 1 gate, one needs to specify 0 */
    int          nMaxGates;             /* maximum number of gates given max. delay and arrival times */
    int          fDecStructure;         /* set to 1 or higher if nSpecFunc = 1 and f = x_i OP g(X \ {x_i}), otherwise 0 (determined when solving) */
    int          pDecVars;              /* mask of variables that can be decomposed at top-level */
    Vec_Int_t *  vStairDecVars;         /* list of stair decomposable variables */
    int          pStairDecFunc[8];      /* list of stair decomposable functions */
    word         pTtObjs[100];          /* temporary truth tables */

    int          nSimVars;              /* number of simulation vars x(i, t) */
    int          nOutputVars;           /* number of output variables g(h, i) */
    int          nGateVars;             /* number of gate variables f(i, p, q) */
    int          nSelectVars;           /* number of select variables s(i, j, k) */
    int          nDepthVars;            /* number of depth variables d(i, j) */

    int          nSimOffset;            /* offset where gate variables start */
    int          nOutputOffset;         /* offset where output variables start */
    int          nGateOffset;           /* offset where gate variables start */
    int          nSelectOffset;         /* offset where select variables start */
    int          nDepthOffset;          /* offset where depth variables start */

    int          fHitResLimit;          /* SAT solver gave up due to resource limit */

    abctime      timeSat;               /* SAT runtime */
    abctime      timeSatSat;            /* SAT runtime (sat instance) */
    abctime      timeSatUnsat;          /* SAT runtime (unsat instance) */
    abctime      timeSatUndef;          /* SAT runtime (undef instance) */
    abctime      timeInstance;          /* creating instance runtime */
    abctime      timeTotal;             /* all runtime */

    int          nSatCalls;             /* number of SAT calls */
    int          nUnsatCalls;           /* number of UNSAT calls */
    int          nUndefCalls;           /* number of UNDEF calls */

    int          nDebugOffset;          /* for debug printing */
};

/***********************************************************************

  Synopsis    [Store truth tables based on normalized arrival times.]

***********************************************************************/

// The hash table is a list of pointers to Ses_TruthEntry_t elements, which
// are arranged in a linked list, each of which pointing to a linked list
// of Ses_TimesEntry_t elements which contain the char* representation of the
// optimum netlist according to then normalized arrival times:

typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t;
struct Ses_TimesEntry_t_
{
    int                pArrTimeProfile[8]; /* normalized arrival time profile */
    int                fResLimit;          /* solution found after resource limit */
    Ses_TimesEntry_t * next;               /* linked list pointer */
    char *             pNetwork;           /* pointer to char array representation of optimum network */
};

typedef struct Ses_TruthEntry_t_ Ses_TruthEntry_t;
struct Ses_TruthEntry_t_
{
    word               pTruth[4]; /* truth table for comparison */
    int                nVars;     /* number of variables */
    Ses_TruthEntry_t * next;      /* linked list pointer */
    Ses_TimesEntry_t * head;      /* pointer to head of sub list with arrival times */
};

#define SES_STORE_TABLE_SIZE 1024
typedef struct Ses_Store_t_ Ses_Store_t;
struct Ses_Store_t_
{
    int                fMakeAIG;                       /* create AIG instead of general network */
    int                fVerbose;                       /* be verbose */
    int                fVeryVerbose;                   /* be very verbose */
    int                nBTLimit;                       /* conflict limit */
    int                nEntriesCount;                  /* number of entries */
    int                nValidEntriesCount;             /* number of entries with network */
    Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
    sat_solver       * pSat;                           /* own SAT solver instance to reuse when calling exact algorithm */
    FILE             * pDebugEntries;                  /* debug unsynth. (rl) entries */
    char             * szDBName;                       /* if given, database is written every time a new entry is added */

    /* statistics */
    unsigned long      nCutCount;                      /* number of cuts investigated */
    unsigned long      pCutCount[9];                   /* -> per cut size */
    unsigned long      nUnsynthesizedImp;              /* number of cuts which couldn't be optimized at all, opt. stopped because of imp. constraints */
    unsigned long      pUnsynthesizedImp[9];           /* -> per cut size */
    unsigned long      nUnsynthesizedRL;               /* number of cuts which couldn't be optimized at all, opt. stopped because of resource limits */
    unsigned long      pUnsynthesizedRL[9];            /* -> per cut size */
    unsigned long      nSynthesizedTrivial;            /* number of cuts which could be synthesized trivially (n < 2) */
    unsigned long      pSynthesizedTrivial[9];         /* -> per cut size */
    unsigned long      nSynthesizedImp;                /* number of cuts which could be synthesized, opt. stopped because of imp. constraints */
    unsigned long      pSynthesizedImp[9];             /* -> per cut size */
    unsigned long      nSynthesizedRL;                 /* number of cuts which could be synthesized, opt. stopped because of resource limits */
    unsigned long      pSynthesizedRL[9];              /* -> per cut size */
    unsigned long      nCacheHits;                     /* number of cache hits */
    unsigned long      pCacheHits[9];                  /* -> per cut size */

    unsigned long      nSatCalls;                      /* number of total SAT calls */
    unsigned long      nUnsatCalls;                    /* number of total UNSAT calls */
    unsigned long      nUndefCalls;                    /* number of total UNDEF calls */

    abctime            timeExact;                      /* Exact synthesis runtime */
    abctime            timeSat;                        /* SAT runtime */
    abctime            timeSatSat;                     /* SAT runtime (sat instance) */
    abctime            timeSatUnsat;                   /* SAT runtime (unsat instance) */
    abctime            timeSatUndef;                   /* SAT runtime (undef instance) */
    abctime            timeInstance;                   /* creating instance runtime */
    abctime            timeTotal;                      /* all runtime */
};

static Ses_Store_t * s_pSesStore = NULL;

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * maxNormalized )
{
    int * p = pArrTimeProfile, * pEnd = pArrTimeProfile + nVars;
    int delta = *p;

    while ( ++p < pEnd )
        if ( *p < delta )
            delta = *p;

    *maxNormalized = 0;
    p = pArrTimeProfile;
    while ( p < pEnd )
    {
        *p -= delta;
        if ( *p > *maxNormalized )
            *maxNormalized = *p;
        ++p;
    }

    *maxNormalized += 1;

    return delta;
}

static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
{
    Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
    pStore->fMakeAIG           = fMakeAIG;
    pStore->fVerbose           = fVerbose;
    pStore->nBTLimit           = nBTLimit;
    memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );

    pStore->pSat = sat_solver_new();

    return pStore;
}

static inline void Ses_StoreClean( Ses_Store_t * pStore )
{
    int i;
    Ses_TruthEntry_t * pTEntry, * pTEntry2;
    Ses_TimesEntry_t * pTiEntry, * pTiEntry2;

    for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
        if ( pStore->pEntries[i] )
        {
            pTEntry = pStore->pEntries[i];

            while ( pTEntry )
            {
                pTiEntry = pTEntry->head;
                while ( pTiEntry )
                {
                    ABC_FREE( pTiEntry->pNetwork );
                    pTiEntry2 = pTiEntry;
                    pTiEntry = pTiEntry->next;
                    ABC_FREE( pTiEntry2 );
                }
                pTEntry2 = pTEntry;
                pTEntry = pTEntry->next;
                ABC_FREE( pTEntry2 );
            }
        }

    sat_solver_delete( pStore->pSat );

    if ( pStore->szDBName )
        ABC_FREE( pStore->szDBName );
    ABC_FREE( pStore );
}

static inline int Ses_StoreTableHash( word * pTruth, int nVars )
{
    static int s_Primes[4] = { 1291, 1699, 1999, 2357 };
    int i;
    unsigned uHash = 0;
    for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
        uHash ^= pTruth[i] * s_Primes[i & 0xf];
    return (int)(uHash % SES_STORE_TABLE_SIZE );
}

static inline int Ses_StoreTruthEqual( Ses_TruthEntry_t * pEntry, word * pTruth, int nVars )
{
    int i;

    if ( pEntry->nVars != nVars )
        return 0;

    for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
        if ( pEntry->pTruth[i] != pTruth[i] )
            return 0;
    return 1;
}

static inline void Ses_StoreTruthCopy( Ses_TruthEntry_t * pEntry, word * pTruthSrc, int nVars )
{
    int i;
    pEntry->nVars = nVars;
    for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
        pEntry->pTruth[i] = pTruthSrc[i];
}

static inline int Ses_StoreTimesEqual( int * pTimes1, int * pTimes2, int nVars )
{
    int i;
    for ( i = 0; i < nVars; ++i )
        if ( pTimes1[i] != pTimes2[i] )
            return 0;
    return 1;
}

static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nVars )
{
    int i;
    for ( i = 0; i < nVars; ++i )
        pTimesDest[i] = pTimesSrc[i];
}

static inline void Ses_StorePrintEntry( Ses_TruthEntry_t * pEntry, Ses_TimesEntry_t * pTiEntry )
{
    int i;

    printf( "f = " );
    Abc_TtPrintHexRev( stdout, pEntry->pTruth, pEntry->nVars );
    printf( ", n = %d", pEntry->nVars );
    printf( ", arrival =" );
    for ( i = 0; i < pEntry->nVars; ++i )
        printf( " %d", pTiEntry->pArrTimeProfile[i] );
    printf( "\n" );
}

static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth, char * pSol, int nStartGates )
{
    int l;

    fprintf( pStore->pDebugEntries, "abc -c \"exact -v -C %d", pStore->nBTLimit );
    if ( s_pSesStore->fMakeAIG ) fprintf( pStore->pDebugEntries, " -a" );
    fprintf( pStore->pDebugEntries, " -S %d -D %d -A", nStartGates + 1, nMaxDepth );
    for ( l = 0; l < nVars; ++l )
        fprintf( pStore->pDebugEntries, "%c%d", ( l == 0 ? ' ' : ',' ), pNormalArrTime[l] );
    fprintf( pStore->pDebugEntries, " " );
    Abc_TtPrintHexRev( pStore->pDebugEntries, pTruth, nVars );
    fprintf( pStore->pDebugEntries, "\" # " );

    if ( !pSol )
        fprintf( pStore->pDebugEntries, "no " );
    fprintf( pStore->pDebugEntries, "solution found before\n" );
}

static void Abc_ExactNormalizeArrivalTimesForNetwork( int nVars, int * pArrTimeProfile, char * pSol )
{
    int nGates, i, j, k, nMax;
    Vec_Int_t * vLevels;

    nGates = pSol[ABC_EXACT_SOL_NGATES];

    /* printf( "NORMALIZE\n" ); */
    /* printf( "  #vars  = %d\n", nVars ); */
    /* printf( "  #gates = %d\n", nGates ); */

    vLevels = Vec_IntAllocArrayCopy( pArrTimeProfile, nVars );

    /* compute level of each gate based on arrival time profile (to compute depth) */
    for ( i = 0; i < nGates; ++i )
    {
        j = pSol[3 + i * 4 + 2];
        k = pSol[3 + i * 4 + 3];

        Vec_IntPush( vLevels, Abc_MaxInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, k ) ) + 1 );

        /* printf( "  gate %d = (%d,%d)\n", nVars + i, j, k ); */
    }

    /* Vec_IntPrint( vLevels ); */

    /* reset all levels except for the last one */
    for ( i = 0; i < nVars + nGates - 1; ++i )
        Vec_IntSetEntry( vLevels, i, Vec_IntEntry( vLevels, nVars + nGates - 1 ) );

    /* Vec_IntPrint( vLevels ); */

    /* compute levels from top to bottom */
    for ( i = nGates - 1; i >= 0; --i )
    {
        j = pSol[3 + i * 4 + 2];
        k = pSol[3 + i * 4 + 3];

        Vec_IntSetEntry( vLevels, j, Abc_MinInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) );
        Vec_IntSetEntry( vLevels, k, Abc_MinInt( Vec_IntEntry( vLevels, k ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) );
    }

    /* Vec_IntPrint( vLevels ); */

    /* normalize arrival times */
    Abc_NormalizeArrivalTimes( Vec_IntArray( vLevels ), nVars, &nMax );
    memcpy( pArrTimeProfile, Vec_IntArray( vLevels ), sizeof(int) * nVars );

    /* printf( "  nMax = %d\n", nMax ); */
    /* Vec_IntPrint( vLevels ); */

    Vec_IntFree( vLevels );
}

static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
{
    int i;
    char zero = '\0';
    unsigned long nEntries = 0;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
    FILE * pFile;

    pFile = fopen( pFilename, "wb" );
    if (pFile == NULL)
    {
        printf( "cannot open file \"%s\" for writing\n", pFilename );
        return;
    }

    if ( fSynthImp )   nEntries += pStore->nSynthesizedImp;
    if ( fSynthRL )    nEntries += pStore->nSynthesizedRL;
    if ( fUnsynthImp ) nEntries += pStore->nUnsynthesizedImp;
    if ( fUnsynthRL )  nEntries += pStore->nUnsynthesizedRL;
    fwrite( &nEntries, sizeof( unsigned long ), 1, pFile );

    for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
        if ( pStore->pEntries[i] )
        {
            pTEntry = pStore->pEntries[i];

            while ( pTEntry )
            {
                pTiEntry = pTEntry->head;
                while ( pTiEntry )
                {
                    if ( !fSynthImp && pTiEntry->pNetwork && !pTiEntry->fResLimit )    { pTiEntry = pTiEntry->next; continue; }
                    if ( !fSynthRL && pTiEntry->pNetwork && pTiEntry->fResLimit )      { pTiEntry = pTiEntry->next; continue; }
                    if ( !fUnsynthImp && !pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; }
                    if ( !fUnsynthRL && !pTiEntry->pNetwork && pTiEntry->fResLimit )   { pTiEntry = pTiEntry->next; continue; }

                    fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile );
                    fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
                    fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
                    fwrite( &pTiEntry->fResLimit, sizeof( int ), 1, pFile );

                    if ( pTiEntry->pNetwork )
                    {
                        fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile );
                    }
                    else
                    {
                        fwrite( &zero, sizeof( char ), 1, pFile );
                        fwrite( &zero, sizeof( char ), 1, pFile );
                        fwrite( &zero, sizeof( char ), 1, pFile );
                    }

                    pTiEntry = pTiEntry->next;
                }
                pTEntry = pTEntry->next;
            }
        }


    fclose( pFile );
}

// pArrTimeProfile is normalized
// returns 1 if and only if a new TimesEntry has been created
int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol, int fResLimit )
{
    int key, fAdded;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;

    if ( pSol )
        Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pArrTimeProfile, pSol );

    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];

    /* does truth table already exist? */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }

    /* entry does not yet exist, so create new one and enqueue */
    if ( !pTEntry )
    {
        pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 );
        Ses_StoreTruthCopy( pTEntry, pTruth, nVars );
        pTEntry->next = pStore->pEntries[key];
        pStore->pEntries[key] = pTEntry;
    }

    /* does arrival time already exist? */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }

    /* entry does not yet exist, so create new one and enqueue */
    if ( !pTiEntry )
    {
        pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
        Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
        pTiEntry->pNetwork = pSol;
        pTiEntry->fResLimit = fResLimit;
        pTiEntry->next = pTEntry->head;
        pTEntry->head = pTiEntry;

        /* item has been added */
        fAdded = 1;
        pStore->nEntriesCount++;
        if ( pSol )
            pStore->nValidEntriesCount++;
    }
    else
    {
        //assert( 0 );
        /* item was already present */
        fAdded = 0;
    }

    /* statistics */
    if ( pSol )
    {
        if ( fResLimit )
        {
            pStore->nSynthesizedRL++;
            pStore->pSynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nSynthesizedImp++;
            pStore->pSynthesizedImp[nVars]++;
        }
    }
    else
    {
        if ( fResLimit )
        {
            pStore->nUnsynthesizedRL++;
            pStore->pUnsynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nUnsynthesizedImp++;
            pStore->pUnsynthesizedImp[nVars]++;
        }
    }

    if ( fAdded && pStore->szDBName )
        Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 );

    return fAdded;
}

// pArrTimeProfile is normalized
// returns 1 if entry was in store, pSol may still be 0 if it couldn't be computed
int Ses_StoreGetEntrySimple( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
{
    int key;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;

    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];

    /* find truth table entry */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }

    /* no entry found? */
    if ( !pTEntry )
        return 0;

    /* find times entry */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }

    /* no entry found? */
    if ( !pTiEntry )
        return 0;

    *pSol = pTiEntry->pNetwork;
    return 1;
}

int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
{
    int key;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
    int pTimes[8];

    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];

    /* find truth table entry */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }

    /* no entry found? */
    if ( !pTEntry )
        return 0;

    /* find times entry */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        /* found after normalization wrt. to network */
        if ( pTiEntry->pNetwork )
        {
            memcpy( pTimes, pArrTimeProfile, sizeof(int) * nVars );
            Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pTimes, pTiEntry->pNetwork );

            if ( Ses_StoreTimesEqual( pTimes, pTiEntry->pArrTimeProfile, nVars ) )
                break;
        }
        /* found for non synthesized network */
        else if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }

    /* no entry found? */
    if ( !pTiEntry )
        return 0;

    *pSol = pTiEntry->pNetwork;
    return 1;
}

static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
{
    int i;
    unsigned long nEntries;
    word pTruth[4];
    int nVars, fResLimit;
    int pArrTimeProfile[8];
    char pHeader[3];
    char * pNetwork;
    FILE * pFile;
    int value;

    if ( pStore->szDBName )
    {
        printf( "cannot read from database when szDBName is set" );
        return;
    }

    pFile = fopen( pFilename, "rb" );
    if (pFile == NULL)
    {
        printf( "cannot open file \"%s\" for reading\n", pFilename );
        return;
    }

    value = fread( &nEntries, sizeof( unsigned long ), 1, pFile );

    for ( i = 0; i < (int)nEntries; ++i )
    {
        value = fread( pTruth, sizeof( word ), 4, pFile );
        value = fread( &nVars, sizeof( int ), 1, pFile );
        value = fread( pArrTimeProfile, sizeof( int ), 8, pFile );
        value = fread( &fResLimit, sizeof( int ), 1, pFile );
        value = fread( pHeader, sizeof( char ), 3, pFile );

        if ( pHeader[0] == '\0' )
            pNetwork = NULL;
        else
        {
            pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
            pNetwork[0] = pHeader[0];
            pNetwork[1] = pHeader[1];
            pNetwork[2] = pHeader[2];

            value = fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
        }

        if ( !fSynthImp && pNetwork && !fResLimit )    continue;
        if ( !fSynthRL && pNetwork && fResLimit )      continue;
        if ( !fUnsynthImp && !pNetwork && !fResLimit ) continue;
        if ( !fUnsynthRL && !pNetwork && fResLimit )   continue;

        Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork, fResLimit );
    }

    fclose( pFile );

    printf( "read %lu entries from file\n", (long)nEntries );
}

// computes top decomposition of variables wrt. to AND and OR
static inline void Ses_ManComputeTopDec( Ses_Man_t * pSes )
{
    int l;
    word pMask[4];

    Abc_TtMask( pMask, pSes->nSpecWords, pSes->nSpecWords * 64 );

    for ( l = 0; l < pSes->nSpecVars; ++l )
        if ( Abc_TtIsTopDecomposable( pSes->pSpec, pMask, pSes->nSpecWords, l ) )
            pSes->pDecVars |= ( 1 << l );
}

static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose )
{
    int h, i;

    Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 );
    p->pSat       = NULL;
    p->bSpecInv   = 0;
    for ( h = 0; h < nFunc; ++h )
        if ( pTruth[h << 2] & 1 )
        {
            for ( i = 0; i < 4; ++i )
                pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
            p->bSpecInv |= ( 1 << h );
        }
    p->pSpec           = pTruth;
    p->nSpecVars       = nVars;
    p->nSpecFunc       = nFunc;
    p->nSpecWords      = Abc_TtWordNum( nVars );
    p->nRows           = ( 1 << nVars ) - 1;
    p->nMaxDepth       = nMaxDepth;
    p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL;
    if ( p->pArrTimeProfile )
        p->nArrTimeDelta = Abc_NormalizeArrivalTimes( p->pArrTimeProfile, nVars, &p->nArrTimeMax );
    else
        p->nArrTimeDelta = p->nArrTimeMax = 0;
    p->fMakeAIG        = fMakeAIG;
    p->nBTLimit        = nBTLimit;
    p->fVerbose        = fVerbose;
    p->fVeryVerbose    = 0;
    p->fExtractVerbose = 0;
    p->fSatVerbose     = 0;
    p->vPolar          = Vec_IntAlloc( 100 );
    p->vAssump         = Vec_IntAlloc( 10 );
    p->vStairDecVars   = Vec_IntAlloc( nVars );
    p->nRandRowAssigns = 2 * nVars;
    p->fKeepRowAssigns = 0;

    if ( p->nSpecFunc == 1 )
        Ses_ManComputeTopDec( p );

    srand( 0xCAFE );

    return p;
}

static inline void Ses_ManCleanLight( Ses_Man_t * pSes )
{
    int h, i;
    for ( h = 0; h < pSes->nSpecFunc; ++h )
        if ( ( pSes->bSpecInv >> h ) & 1 )
            for ( i = 0; i < 4; ++i )
                pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] );

    if ( pSes->pArrTimeProfile )
        for ( i = 0; i < pSes->nSpecVars; ++i )
            pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta;

    Vec_IntFree( pSes->vPolar );
    Vec_IntFree( pSes->vAssump );
    Vec_IntFree( pSes->vStairDecVars );

    ABC_FREE( pSes );
}

static inline void Ses_ManClean( Ses_Man_t * pSes )
{
    if ( pSes->pSat )
        sat_solver_delete( pSes->pSat );
    Ses_ManCleanLight( pSes );
}

/**Function*************************************************************

  Synopsis    [Access variables based on indexes.]

***********************************************************************/
static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t )
{
    assert( i < pSes->nGates );
    assert( t < pSes->nRows );

    return pSes->nSimOffset + pSes->nRows * i + t;
}

static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i )
{
    assert( h < pSes->nSpecFunc );
    assert( i < pSes->nGates );

    return pSes->nOutputOffset + pSes->nGates * h + i;
}

static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q )
{
    assert( i < pSes->nGates );
    assert( p < 2 );
    assert( q < 2 );
    assert( p > 0 || q > 0 );

    return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1;
}

static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
{
    int a;
    int offset;

    assert( i < pSes->nGates );
    assert( k < pSes->nSpecVars + i );
    assert( j < k );

    offset = pSes->nSelectOffset;
    for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a )
        offset += a * ( a - 1 ) / 2;

    return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 );
}

static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j )
{
    assert( i < pSes->nGates );
    assert( j <= pSes->nArrTimeMax + i );

    return pSes->nDepthOffset + i * pSes->nArrTimeMax + ( ( i * ( i + 1 ) ) / 2 ) + j;
}

/**Function*************************************************************

  Synopsis    [Compute truth table from a solution.]

***********************************************************************/
static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert )
{
    int i, f, j, k, w, nGates = pSol[ABC_EXACT_SOL_NGATES];
    char * p;
    word * pTruth = NULL, * pTruth0, * pTruth1;
    assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );

    p = pSol + 3;

    memset( pSes->pTtObjs, 0, sizeof( word ) * 4 * nGates );

    for ( i = 0; i < nGates; ++i )
    {
        f = *p++;
        assert( *p++ == 2 );
        j = *p++;
        k = *p++;

        pTruth0 = j < pSes->nSpecVars ? &s_Truths8[j << 2] : &pSes->pTtObjs[( j - pSes->nSpecVars ) << 2];
        pTruth1 = k < pSes->nSpecVars ? &s_Truths8[k << 2] : &pSes->pTtObjs[( k - pSes->nSpecVars ) << 2];

        pTruth = &pSes->pTtObjs[i << 2];

        if ( f & 1 )
            for ( w = 0; w < pSes->nSpecWords; ++w )
                pTruth[w] |= ~pTruth0[w] & pTruth1[w];
        if ( ( f >> 1 ) & 1 )
            for ( w = 0; w < pSes->nSpecWords; ++w )
                pTruth[w] |= pTruth0[w] & ~pTruth1[w];
        if ( ( f >> 2 ) & 1 )
            for ( w = 0; w < pSes->nSpecWords; ++w )
                pTruth[w] |= pTruth0[w] & pTruth1[w];
    }

    assert( Abc_Lit2Var( *p ) == nGates - 1 );
    if ( fInvert && Abc_LitIsCompl( *p ) )
        Abc_TtNot( pTruth, pSes->nSpecWords );

    return pTruth;
}

/**Function*************************************************************

  Synopsis    [Setup variables to find network with nGates gates.]

***********************************************************************/
static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
{
    int i;

    if ( pSes->fSatVerbose )
    {
        printf( "create variables for network with %d functions over %d variables and %d/%d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates, pSes->nMaxGates );
    }

    pSes->nGates      = nGates;
    pSes->nSimVars    = nGates * pSes->nRows;
    pSes->nOutputVars = pSes->nSpecFunc * nGates;
    pSes->nGateVars   = nGates * 3;
    pSes->nSelectVars = 0;
    for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
        pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
    pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;

    /* pSes->nSimOffset    = 0; */
    /* pSes->nOutputOffset = pSes->nSimVars; */
    /* pSes->nGateOffset   = pSes->nSimVars + pSes->nOutputVars; */
    /* pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars; */
    /* pSes->nDepthOffset  = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars; */

    pSes->nDepthOffset  = 0;
    pSes->nSelectOffset = pSes->nDepthVars;
    pSes->nGateOffset   = pSes->nDepthVars + pSes->nSelectVars;
    pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars;
    pSes->nSimOffset    = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars + pSes->nOutputVars;

    /* pSes->nDepthOffset  = 0; */
    /* pSes->nSelectOffset = pSes->nDepthVars; */
    /* pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars; */
    /* pSes->nGateOffset   = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars; */
    /* pSes->nSimOffset    = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars + pSes->nGateVars; */

    /* if we already have a SAT solver, then restart it (this saves a lot of time) */
    if ( pSes->pSat )
        sat_solver_restart( pSes->pSat );
    else
        pSes->pSat = sat_solver_new();
    sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars + pSes->nDepthVars );
}

/**Function*************************************************************

  Synopsis    [Create clauses.]

***********************************************************************/
static inline void Ses_ManGateCannotHaveChild( Ses_Man_t * pSes, int i, int j )
{
    int k;

    for ( k = 0; k < j; ++k )
        Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 1 ) );
    for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
        Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ) );
}

static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c )
{
    int pLits[5], ctr = 0;

    pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
    pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a );

    if ( j < pSes->nSpecVars )
    {
        if ( ( ( ( t + 1 ) & ( 1 << j ) ) ? 1 : 0 ) != b )
            return;
    }
    else
        pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b );

    if ( k < pSes->nSpecVars )
    {
        if ( ( ( ( t + 1 ) & ( 1 << k ) ) ? 1 : 0 ) != c )
            return;
    }
    else
        pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c );

    if ( b > 0 || c > 0 )
        pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );

    sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
}

static int inline Ses_ManCreateTruthTableClause( Ses_Man_t * pSes, int t )
{
    int i, j, k, h;
    int pLits[3];

    for ( i = 0; i < pSes->nGates; ++i )
    {
        /* main clauses */
        for ( j = 0; j < pSes->nSpecVars + i; ++j )
            for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
            {
                Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 );
                Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 );
            }

        /* output clauses */
        if ( pSes->nSpecFunc != 1 )
            for ( h = 0; h < pSes->nSpecFunc; ++h )
            {
                pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
                pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
                if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
                    return 0;
            }
    }

    if ( pSes->nSpecFunc == 1 )
        Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ) );

    return 1;
}

static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
    extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );

    int h, i, j, k, t, ii, jj, kk, p, q;
    int pLits[3];
    Vec_Int_t * vLits = NULL;

    for ( t = 0; t < pSes->nRows; ++t )
    {
        if ( Abc_TtGetBit( pSes->pTtValues, t ) )
            if ( !Ses_ManCreateTruthTableClause( pSes, t ) )
                return 0;
    }

    /* if there is only one output, we know it must point to the last gate  */
    if ( pSes->nSpecFunc == 1 )
    {
        for ( i = 0; i < pSes->nGates - 1; ++i )
            Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ) );
        Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ) );

        vLits = Vec_IntAlloc( 0u );
    }
    else
    {
        vLits = Vec_IntAlloc( 0u );

        /* some output is selected */
        for ( h = 0; h < pSes->nSpecFunc; ++h )
        {
            Vec_IntGrowResize( vLits, pSes->nGates );
            for ( i = 0; i < pSes->nGates; ++i )
                Vec_IntSetEntry( vLits, i, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
            sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + pSes->nGates );
        }
    }

    /* each gate has two operands */
    for ( i = 0; i < pSes->nGates; ++i )
    {
        Vec_IntGrowResize( vLits, ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
        jj = 0;
        for ( j = 0; j < pSes->nSpecVars + i; ++j )
            for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
                Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
        sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
    }

    /* gate decomposition (makes it worse) */
    /* if ( fDecVariable >= 0 && pSes->nGates >= 2 ) */
    /* { */
    /*     pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, fDecVariable, pSes->nSpecVars + pSes->nGates - 2 ), 0 ); */
    /*     if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */
    /*     { */
    /*         Vec_IntFree( vLits ); */
    /*         return 0; */
    /*     } */

    /*     for ( k = 1; k < pSes->nSpecVars + pSes->nGates - 1; ++k ) */
    /*         for ( j = 0; j < k; ++j ) */
    /*             if ( j != fDecVariable || k != pSes->nSpecVars + pSes->nGates - 2 ) */
    /*             { */
    /*                 pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, j, k ), 1 ); */
    /*                 if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */
    /*                 { */
    /*                     Vec_IntFree( vLits ); */
    /*                     return 0; */
    /*                 } */
    /*             } */
    /* } */

    /* only AIG */
    if ( pSes->fMakeAIG )
    {
        for ( i = 0; i < pSes->nGates; ++i )
        {
            /* not 2 ones */
            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );

            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );

            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
        }
    }

    /* only binary clauses */
    if ( 1 ) /* TODO: add some meaningful parameter */
    {
        for ( i = 0; i < pSes->nGates; ++i )
        {
            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );

            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );

            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
        }

        for ( i = 0; i < pSes->nGates; ++i )
            for ( k = 1; k < pSes->nSpecVars + i; ++k )
                for ( j = 0; j < k; ++j )
                {
                    pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );

                    for ( kk = 1; kk < pSes->nSpecVars + i; ++kk )
                        for ( jj = 0; jj < kk; ++jj )
                        {
                            if ( k == kk && j == jj ) continue;
                            pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, jj, kk ), 1 );

                            if ( pLits[0] < pLits[1] )
                                sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                        }
                }

        /* Vec_IntGrowResize( vLits, pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) ); */

        /* for ( j = 0; j < pSes->nSpecVars; ++j ) */
        /* { */
        /*     jj = 0; */
        /*     for ( i = 0; i < pSes->nGates; ++i ) */
        /*     { */
        /*         for ( k = 0; k < j; ++k ) */
        /*             Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 0 ) ); */
        /*         for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) */
        /*             Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) ); */
        /*     } */
        /*     sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj ); */
        /* } */
    }

    /* EXTRA stair decomposition */
    if (Vec_IntSize( pSes->vStairDecVars ) )
    {
        Vec_IntForEachEntry( pSes->vStairDecVars, j, i )
        {
            if ( pSes->nGates - 2 - i < j )
            {
                continue;
            }
            Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1 - i, j, pSes->nSpecVars + pSes->nGates - 2 - i ), 0 ) );

            //printf( "dec %d for var %d\n", pSes->pStairDecFunc[i], j );

            switch ( pSes->pStairDecFunc[i] )
            {
            case 1: /* AND(x,g) */
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 1 ) );
                //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
                //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
                break;
            case 2: /* AND(!x,g) */
                //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
                break;
            case 3: /* OR(x,g) */
                //Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
                break;
            case 4: /* OR(!x,g) */
                ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
                ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
                ////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
                break;
            case 5: /* XOR(x,g) */
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
                break;
            default:
                printf( "func: %d\n", pSes->pStairDecFunc[i] );
                assert( 0 );
            }
        }
    }

    /* EXTRA clauses: use gate i at least once */
    Vec_IntGrowResize( vLits, pSes->nSpecFunc + pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) );
    for ( i = 0; i < pSes->nGates; ++i )
    {
        jj = 0;
        for ( h = 0; h < pSes->nSpecFunc; ++h )
            Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
        for ( ii = i + 1; ii < pSes->nGates; ++ii )
        {
            for ( j = 0; j < pSes->nSpecVars + i; ++j )
                Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
            for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j )
                Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
        }
        sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
    }
    Vec_IntFree( vLits );

    /* EXTRA clauses: no reapplying operand */
    if ( pSes->nGates > 1 )
        for ( i = 0; i < pSes->nGates - 1; ++i )
            for ( ii = i + 1; ii < pSes->nGates; ++ii )
                for ( k = 1; k < pSes->nSpecVars + i; ++k )
                    for ( j = 0; j < k; ++j )
                    {
                        pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
                        pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 1 );
                        sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );

                        pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, k, pSes->nSpecVars + i ), 1 );
                        sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                    }

    /* EXTRA clauses: co-lexicographic order */
    for ( i = 0; i < pSes->nGates - 1; ++i )
    {
        for ( k = 2; k < pSes->nSpecVars + i; ++k )
        {
            for ( j = 1; j < k; ++j )
                for ( jj = 0; jj < j; ++jj )
                {
                    pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
                    pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 );
                    sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                }

            for ( j = 0; j < k; ++j )
                for ( kk = 1; kk < k; ++kk )
                    for ( jj = 0; jj < kk; ++jj )
                    {
                        pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
                        pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 );
                        sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                    }
        }
    }

    /* EXTRA clauses: symmetric variables */
    if ( /*pSes->nMaxDepth == -1 &&*/ pSes->nSpecFunc == 1 ) /* only check if there is one output function */
        for ( q = 1; q < pSes->nSpecVars; ++q )
            for ( p = 0; p < q; ++p )
                if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) &&
                     ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] <= pSes->pArrTimeProfile[q] ) ) )
                {
                    if ( pSes->fSatVerbose )
                        printf( "variables %d and %d are symmetric\n", p, q );
                    for ( i = 0; i < pSes->nGates; ++i )
                        for ( j = 0; j < q; ++j )
                        {
                            if ( j == p ) continue;

                            vLits = Vec_IntAlloc( 0 );
                            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) );
                            for ( ii = 0; ii < i; ++ii )
                                for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk )
                                    for ( jj = 0; jj < kk; ++jj )
                                        if ( jj == p || kk == p )
                                            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
                            sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) );
                            Vec_IntFree( vLits );
                        }
                }

    return 1;
}

static int Ses_ManCreateDepthClauses( Ses_Man_t * pSes )
{
    int i, j, k, jj, kk, d, h;
    int pLits[3];

    for ( i = 0; i < pSes->nGates; ++i )
    {
        /* propagate depths from children */
        for ( k = 1; k < i; ++k )
            for ( j = 0; j < k; ++j )
            {
                pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 );
                for ( jj = 0; jj <= pSes->nArrTimeMax + j; ++jj )
                {
                    pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 );
                    pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 );
                    sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
                }
            }

        for ( k = 0; k < i; ++k )
            for ( j = 0; j < pSes->nSpecVars + k; ++j )
            {
                pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 );
                for ( kk = 0; kk <= pSes->nArrTimeMax + k; ++kk )
                {
                    pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 );
                    pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 );
                    sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
                }
            }

        /* propagate depths from arrival times at PIs */
        if ( pSes->pArrTimeProfile )
        {
            for ( k = 1; k < pSes->nSpecVars + i; ++k )
                for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j )
                {
                    d = pSes->pArrTimeProfile[j];
                    if ( k < pSes->nSpecVars && pSes->pArrTimeProfile[k] > d )
                        d = pSes->pArrTimeProfile[k];

                    pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
                    pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d ), 0 );
                    sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                }
        }
        else
            /* arrival times are 0 */
            Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ) );

        /* reverse order encoding of depth variables */
        for ( j = 1; j <= pSes->nArrTimeMax + i; ++j )
        {
            pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 );
            pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 );
            sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
        }

        /* constrain maximum depth */
        if ( pSes->nMaxDepth < pSes->nArrTimeMax + i )
            for ( h = 0; h < pSes->nSpecFunc; ++h )
            {
                pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
                pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 );
                if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
                    return 0;
            }
    }

    return 1;
}

/**Function*************************************************************

  Synopsis    [Solve.]

***********************************************************************/
static inline double Sat_Wrd2Dbl( word w )  { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); }

static inline int Ses_ManSolve( Ses_Man_t * pSes )
{
    int status;
    abctime timeStart, timeDelta;

    if ( pSes->fSatVerbose )
    {
        printf( "SAT   CL: %7d   VA: %5d", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
        fflush( stdout );
    }

    timeStart = Abc_Clock();
    status = sat_solver_solve( pSes->pSat, Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), pSes->nBTLimit, 0, 0, 0 );
    timeDelta = Abc_Clock() - timeStart;

    if ( pSes->fSatVerbose )
        printf( "   RE:   %2d   ST: %4.f   CO: %7.0f   DE: %6.0f    PR: %6.0f\n",
                status,
                Sat_Wrd2Dbl( pSes->pSat->stats.starts ), Sat_Wrd2Dbl( pSes->pSat->stats.conflicts ),
                Sat_Wrd2Dbl( pSes->pSat->stats.decisions ), Sat_Wrd2Dbl( pSes->pSat->stats.propagations ) );
        //Sat_SolverPrintStats( stdout, pSes->pSat );

    pSes->timeSat += timeDelta;

    if ( status == l_True )
    {
        pSes->nSatCalls++;
        pSes->timeSatSat += timeDelta;
        return 1;
    }
    else if ( status == l_False )
    {
        pSes->nUnsatCalls++;
        pSes->timeSatUnsat += timeDelta;
        return 0;
    }
    else
    {
        pSes->nUndefCalls++;
        pSes->timeSatUndef += timeDelta;
        if ( pSes->fSatVerbose )
        {
            printf( "resource limit reached\n" );
        }
        return 2;
    }
}

/**Function*************************************************************

  Synopsis    [Extract solution.]

***********************************************************************/
// char is an array of short integers that stores the synthesized network
// using the following format
// | nvars | nfunc | ngates | gate[1] | ... | gate[ngates] | func[1] | .. | func[nfunc] |
// nvars:       integer with number of variables
// nfunc:       integer with number of functions
// ngates:      integer with number of gates
// gate[i]:     | op | nfanin | fanin[1] | ... | fanin[nfanin] |
//   op:        integer of gate's truth table (divided by 2, because gate is normal)
//   nfanin:    integer with number of fanins
//   fanin[i]:  integer to primary input or other gate
// func[i]:     | fanin | delay | pin[1] | ... | pin[nvars] |
//   fanin:     integer as literal to some gate (not primary input), can be complemented
//   delay:     maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified
//   pin[i]:    pin to pin delay to input i or 0 if not specified or if there is no connection to input i
// NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0
static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
{
    int nSol, h, i, j, k, l, aj, ak, d, nOp;
    char * pSol, * p;
    int * pPerm = NULL; /* will be a 2d array [i][l] where is is gate id and l is PI id */

    /* compute length of solution, for now all gates have 2 inputs */
    nSol = 3 + pSes->nGates * 4 + pSes->nSpecFunc * ( 2 + pSes->nSpecVars );

    p = pSol = ABC_CALLOC( char, nSol );

    /* header */
    *p++ = pSes->nSpecVars;
    *p++ = pSes->nSpecFunc;
    *p++ = pSes->nGates;

    /* gates */
    for ( i = 0; i < pSes->nGates; ++i )
    {
        nOp  = sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) );
        nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) << 1;
        nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) << 2;

        *p++ = nOp;
        *p++ = 2;

        if ( pSes->fExtractVerbose )
            printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp );

        for ( k = 0; k < pSes->nSpecVars + i; ++k )
            for ( j = 0; j < k; ++j )
                if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
                {
                    if ( pSes->fExtractVerbose )
                        printf( " and operands %d and %d", j, k );
                    *p++ = j;
                    *p++ = k;
                    k = pSes->nSpecVars + i;
                    break;
                }

        if ( pSes->fExtractVerbose )
        {
            if ( pSes->nMaxDepth > 0 )
            {
                printf( " and depth vector " );
                for ( j = 0; j <= pSes->nArrTimeMax + i; ++j )
                    printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) );
            }
            printf( "\n" );
        }
    }

    /* pin-to-pin delay */
    if ( pSes->nMaxDepth != -1 )
    {
        pPerm = ABC_CALLOC( int, pSes->nGates * pSes->nSpecVars );
        for ( i = 0; i < pSes->nGates; ++i )
        {
            /* since all gates are binary for now */
            j = pSol[3 + i * 4 + 2];
            k = pSol[3 + i * 4 + 3];

            for ( l = 0; l < pSes->nSpecVars; ++l )
            {
                /* pin-to-pin delay to input l of child nodes */
                aj = j < pSes->nSpecVars ? 0 : pPerm[(j - pSes->nSpecVars) * pSes->nSpecVars + l];
                ak = k < pSes->nSpecVars ? 0 : pPerm[(k - pSes->nSpecVars) * pSes->nSpecVars + l];

                if ( aj == 0 && ak == 0 )
                    pPerm[i * pSes->nSpecVars + l] = ( l == j || l == k ) ? 1 : 0;
                else
                    pPerm[i * pSes->nSpecVars + l] = Abc_MaxInt( aj, ak ) + 1;
            }
        }
    }

    /* outputs */
    for ( h = 0; h < pSes->nSpecFunc; ++h )
        for ( i = 0; i < pSes->nGates; ++i )
            if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) )
            {
                *p++ = Abc_Var2Lit( i, ( pSes->bSpecInv >> h ) & 1 );
                d = 0;
                if ( pSes->nMaxDepth != -1 )
                    for ( l = 0; l < pSes->nSpecVars; ++l )
                    {
                        if ( pSes->pArrTimeProfile )
                            d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
                        else
                            d = Abc_MaxInt( d, pPerm[i * pSes->nSpecVars + l] );
                    }
                *p++ = d;
                if ( pSes->pArrTimeProfile && pSes->fExtractVerbose )
                    printf( "output %d points to gate %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, pSes->nSpecVars + i, d, pSes->nArrTimeDelta );
                for ( l = 0; l < pSes->nSpecVars; ++l )
                {
                    d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0;
                    if ( pSes->pArrTimeProfile && pSes->fExtractVerbose )
                        printf( "  pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
                    *p++ = d;
                }
            }

    /* pin-to-pin delays */
    if ( pSes->nMaxDepth != -1 )
        ABC_FREE( pPerm );

    /* have we used all the fields? */
    assert( ( p - pSol ) == nSol );

    /* printf( "found network: " ); */
    /* Abc_TtPrintHexRev( stdout, Ses_ManDeriveTruth( pSes, pSol, 1 ), pSes->nSpecVars ); */
    /* printf( "\n" ); */

    return pSol;
}

static Abc_Ntk_t * Ses_ManExtractNtk( char const * pSol )
{
    int h, i;
    char const * p;
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pObj;
    Vec_Ptr_t * pGates, * vNames;
    char pGateTruth[5];
    char * pSopCover;

    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
    pNtk->pName = Extra_UtilStrsav( "exact" );
    pGates = Vec_PtrAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
    pGateTruth[3] = '0';
    pGateTruth[4] = '\0';
    vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );

    /* primary inputs */
    Vec_PtrPush( pNtk->vObjs, NULL );
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
    {
        pObj = Abc_NtkCreatePi( pNtk );
        Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL );
        Vec_PtrPush( pGates, pObj );
    }

    /* gates */
    p = pSol + 3;
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
    {
        pGateTruth[2] = '0' + ( *p & 1 );
        pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
        pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
        ++p;

        assert( *p == 2 ); /* binary gate */
        ++p;

        pSopCover = Abc_SopFromTruthBin( pGateTruth );
        pObj = Abc_NtkCreateNode( pNtk );
        pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
        Vec_PtrPush( pGates, pObj );
        ABC_FREE( pSopCover );

        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
    }

    /* outputs */
    for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
    {
        pObj = Abc_NtkCreatePo( pNtk );
        Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ), NULL );
        if ( Abc_LitIsCompl( *p ) )
            Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) ) );
        else
            Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) );
        p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
    }
    Abc_NodeFreeNames( vNames );

    Vec_PtrFree( pGates );

    if ( !Abc_NtkCheck( pNtk ) )
        printf( "Ses_ManExtractSolution(): Network check has failed.\n" );

    return pNtk;
}

static Gia_Man_t * Ses_ManExtractGia( char const * pSol )
{
    int h, i;
    char const * p;
    Gia_Man_t * pGia;
    Vec_Int_t * pGates;
    Vec_Ptr_t * vNames;
    int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp;

    pGia = Gia_ManStart( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] + pSol[ABC_EXACT_SOL_NFUNC] + 1 );
    pGia->nConstrs = 0;
    pGia->pName = Extra_UtilStrsav( "exact" );

    pGates = Vec_IntAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
    vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );

    /* primary inputs */
    pGia->vNamesIn = Vec_PtrStart( pSol[ABC_EXACT_SOL_NVARS] );
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
    {
        nObj = Gia_ManAppendCi( pGia );
        Vec_IntPush( pGates, nObj );
        Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( vNames, i ) ) );
    }

    /* gates */
    p = pSol + 3;
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
    {
        assert( p[1] == 2 );
        nChild1 = Vec_IntEntry( pGates, p[2] );
        nChild2 = Vec_IntEntry( pGates, p[3] );
        fChild1Comp = fChild2Comp = 0;

        if ( *p & 1 )
        {
            nChild1 = Abc_LitNot( nChild1 );
            fChild1Comp = 1;
        }
        if ( ( *p >> 1 ) & 1 )
        {
            nChild2 = Abc_LitNot( nChild2 );
            fChild2Comp = 1;
        }
        nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 );
        if ( fChild1Comp && fChild2Comp )
        {
            assert( ( *p >> 2 ) & 1 );
            nObj = Abc_LitNot( nObj );
        }

        Vec_IntPush( pGates, nObj );

        p += 4;
    }

    /* outputs */
    pGia->vNamesOut = Vec_PtrStart( pSol[ABC_EXACT_SOL_NFUNC] );
    for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
    {
        nObj = Vec_IntEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) );
        if ( Abc_LitIsCompl( *p ) )
            nObj = Abc_LitNot( nObj );
        Gia_ManAppendCo( pGia, nObj );
        Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( (const char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ) ) );
        p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
    }
    Abc_NodeFreeNames( vNames );

    Vec_IntFree( pGates );

    return pGia;
}

/**Function*************************************************************

  Synopsis    [Debug.]

***********************************************************************/
static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
{
    printf( "Runtime breakdown:\n" );
    ABC_PRTP( "Sat     ",  pSes->timeSat,      pSes->timeTotal );
    ABC_PRTP( " Sat    ",  pSes->timeSatSat,   pSes->timeTotal );
    ABC_PRTP( " Unsat  ",  pSes->timeSatUnsat, pSes->timeTotal );
    ABC_PRTP( " Undef  ",  pSes->timeSatUndef, pSes->timeTotal );
    ABC_PRTP( "Instance", pSes->timeInstance,  pSes->timeTotal );
    ABC_PRTP( "ALL     ",  pSes->timeTotal,    pSes->timeTotal );
}

static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
{
    int h;

    printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars );
    for ( h = 0; h < pSes->nSpecFunc; ++h )
    {
        printf( "  func %d: ", h + 1 );
        Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars );
        printf( "\n" );
    }

    if ( pSes->nMaxDepth != -1 )
    {
        printf( "  max depth = %d\n", pSes->nMaxDepth );
        if ( pSes->pArrTimeProfile )
        {
            printf( "  arrival times =" );
            for ( h = 0; h < pSes->nSpecVars; ++h )
                printf( " %d", pSes->pArrTimeProfile[h] );
            printf( "\n" );
        }
    }
}

static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
{
    int h, i, j, k, p, q, t;

    for ( i = 0; i < pSes->nGates; ++i )
        for ( t = 0; t < pSes->nRows; ++t )
            printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) );

    for ( h = 0; h < pSes->nSpecFunc; ++h )
        for ( i = 0; i < pSes->nGates; ++i )
            printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) );

    for ( i = 0; i < pSes->nGates; ++i )
        for ( p = 0; p <= 1; ++p )
            for ( q = 0; q <= 1; ++ q)
            {
                if ( p == 0 && q == 0 ) { continue; }
                printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) );
            }

    for ( i = 0; i < pSes->nGates; ++i )
        for ( j = 0; j < pSes->nSpecVars + i; ++j )
            for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
                printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) );

    if ( pSes->nMaxDepth > 0 )
        for ( i = 0; i < pSes->nGates; ++i )
            for ( j = 0; j <= i; ++j )
                printf( "d(%d, %d) : %d\n", i, j, Ses_ManDepthVar( pSes, i, j ) );

}

/**Function*************************************************************

  Synopsis    [Synthesis algorithm.]

***********************************************************************/
static void Ses_ManComputeMaxGates( Ses_Man_t * pSes )
{
    int s = 1, lvl = pSes->nMaxDepth, avail = pSes->nSpecVars, l;

    pSes->nMaxGates = 0;

    /* s is the number of gates we have in the current level */
    while ( s && /* while there are nodes to branch from */
            lvl && /* while we are at some level */
            avail * 2 > s /* while there are still enough available nodes (heuristic) */ )
    {
        /* erase from s if we have arriving nodes */
        for ( l = 0; l < pSes->nSpecVars; ++l )
            if ( pSes->pArrTimeProfile[l] == lvl )
            {
                --s;
                --avail;
            }

        --lvl;
        pSes->nMaxGates += s;
        s *= 2;
    }
}

// returns 0, if current max depth and arrival times are not consistent
static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
{
    int l, i, fAdded, nLevel;
    int fMaxGatesLevel2 = 1;

    Vec_IntClear( pSes->vStairDecVars );
    pSes->fDecStructure = 0;

    for ( l = 0; l < pSes->nSpecVars; ++l )
    {
        if ( pSes->pArrTimeProfile[l] >= pSes->nMaxDepth )
        {
            if ( pSes->fReasonVerbose )
                printf( "give up due to impossible arrival time (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
            return 0;
        }
        else if ( pSes->nSpecFunc == 1 && pSes->pArrTimeProfile[l] + 1 == pSes->nMaxDepth )
        {
            if ( ( pSes->fDecStructure == 1 && pSes->nSpecVars > 2 ) || pSes->fDecStructure == 2 )
            {
                if ( pSes->fReasonVerbose )
                    printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
                return 0;
            }

            pSes->fDecStructure++;

            /* A subset B <=> A and B = A */
            if ( !( ( pSes->pDecVars >> l ) & 1 ) )
            {
                if ( pSes->fReasonVerbose )
                    printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
                return 0;
            }
        }
    }

    /* more complicated decomposition */
    if ( pSes->fDecStructure )
    {
        nLevel = 1;
        while ( 1 )
        {
            fAdded = 0;

            for ( l = 0; l < pSes->nSpecVars; ++l )
                if ( pSes->pArrTimeProfile[l] + nLevel == pSes->nMaxDepth )
                {
                    if ( fAdded )
                    {
                        assert( nLevel == Vec_IntSize( pSes->vStairDecVars ) );
                        if ( fAdded > 1 || ( nLevel + 1 < pSes->nSpecVars ) )
                        {
                            if ( pSes->fReasonVerbose )
                                printf( "give up due to impossible decomposition at level %d", nLevel );
                            return 0;
                        }
                    }
                    else
                    {
                        Vec_IntPush( pSes->vStairDecVars, l );
                    }
                    fAdded++;
                }

            if ( !fAdded ) break;
            ++nLevel;
        }

        if ( Vec_IntSize( pSes->vStairDecVars ) && !Abc_TtIsStairDecomposable( pSes->pSpec, pSes->nSpecWords, Vec_IntArray( pSes->vStairDecVars ), Vec_IntSize( pSes->vStairDecVars ), pSes->pStairDecFunc ) )
        {
            if ( pSes->fReasonVerbose )
            {
                printf( "give up due to impossible stair decomposition at level %d: ", nLevel );
                Vec_IntPrint( pSes->vStairDecVars );
            }
            return 0;
        }
    }

    /* check if depth's match with structure at second level from top */
    if ( pSes->fDecStructure )
        fMaxGatesLevel2 = ( pSes->nSpecVars == 3 ) ? 2 : 1;
    else
        fMaxGatesLevel2 = ( pSes->nSpecVars == 4 ) ? 4 : 3;

    i = 0;
    for ( l = 0; l < pSes->nSpecVars; ++l )
        if ( pSes->pArrTimeProfile[l] + 2 == pSes->nMaxDepth )
            if ( ++i > fMaxGatesLevel2 )
            {
                if ( pSes->fReasonVerbose )
                    printf( "give up due to impossible decomposition at second level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
                return 0;
            }

    /* check if depth's match with structure at third level from top */
    if ( pSes->nSpecVars > 4 && pSes->fDecStructure && i == 1 ) /* we have f = AND(x_i, AND(x_j, g)) (x_i and x_j may be complemented) */
    {
        i = 0;
        for ( l = 0; l < pSes->nSpecVars; ++l )
            if ( pSes->pArrTimeProfile[l] + 3 == pSes->nMaxDepth )
                if ( ++i > 1 )
                {
                    if ( pSes->fReasonVerbose )
                        printf( "give up due to impossible decomposition at third level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
                    return 0;
                }
    }

    return 1;
}

// returns 0, if current max depth and #gates are not consistent
static int Ses_CheckGatesConsistency( Ses_Man_t * pSes, int nGates )
{
    /* give up if number of gates is impossible for given depth */
    if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) )
    {
        if ( pSes->fReasonVerbose )
            printf( "give up due to impossible depth (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
        return 0;
    }

    /* give up if number of gates is impossible for given depth and arrival times */
    if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile && nGates > pSes->nMaxGates )
    {
        if ( pSes->fReasonVerbose )
            printf( "give up due to impossible depth and arrival times (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
        return 0;
    }

    if ( pSes->fDecStructure && nGates >= ( 1 << ( pSes->nMaxDepth - 1 ) ) + 1 )
    {
        if ( pSes->fReasonVerbose )
            printf( "give up due to impossible depth in AND-dec structure (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
        return 0;
    }

    /* give up if number of gates gets practically too large */
    if ( nGates >= ( 1 << pSes->nSpecVars ) )
    {
        if ( pSes->fReasonVerbose )
            printf( "give up due to impossible number of gates" );
        return 0;
    }

    return 1;
}

static void Abc_ExactCopyDepthAndArrivalTimes( int nVars, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo )
{
    int l;

    *nDepthTo = nDepthFrom;
    for ( l = 0; l < nVars; ++l )
        pTimesTo[l] = pTimesFrom[l];
}

static void Ses_ManStoreDepthAndArrivalTimes( Ses_Man_t * pSes )
{
    if ( pSes->nMaxDepth == -1 ) return;
    Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepth, &pSes->nMaxDepthTmp, pSes->pArrTimeProfile, pSes->pArrTimeProfileTmp );
}

static void Ses_ManRestoreDepthAndArrivalTimes( Ses_Man_t * pSes )
{
    if ( pSes->nMaxDepth == -1 ) return;
    Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile );
}

static void Abc_ExactAdjustDepthAndArrivalTimes( int nVars, int nGates, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo, int nTimesMax )
{
    int l;

    *nDepthTo = Abc_MinInt( nDepthFrom, nGates );
    for ( l = 0; l < nVars; ++l )
        pTimesTo[l] = Abc_MinInt( pTimesFrom[l], Abc_MaxInt( 0, nGates - 1 - nTimesMax + pTimesFrom[l] ) );
}

static void Ses_AdjustDepthAndArrivalTimes( Ses_Man_t * pSes, int nGates )
{
    Abc_ExactAdjustDepthAndArrivalTimes( pSes->nSpecVars, nGates, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile, pSes->nArrTimeMax - 1 );
}

/* return: (2: continue, 1: found, 0: gave up) */
static int Ses_ManFindNetworkExact( Ses_Man_t * pSes, int nGates )
{
    int f, fSat;
    abctime timeStart;

    /* solve */
    timeStart = Abc_Clock();
    Vec_IntClear( pSes->vPolar );
    Vec_IntClear( pSes->vAssump );
    Ses_ManCreateVars( pSes, nGates );

    if ( pSes->nMaxDepth != -1 )
    {
        f = Ses_ManCreateDepthClauses( pSes );
        pSes->timeInstance += ( Abc_Clock() - timeStart );
        if ( !f ) return 2; /* proven UNSAT while creating clauses */
    }

    sat_solver_set_polarity( pSes->pSat, Vec_IntArray( pSes->vPolar ), Vec_IntSize( pSes->vPolar ) );

    /* first solve */
    fSat = Ses_ManSolve( pSes );
    if ( fSat == 0 )
        return 2; /* UNSAT, continue with next # of gates */
    else if ( fSat == 2 )
    {
        pSes->fHitResLimit = 1;
        return 0;
    }

    timeStart = Abc_Clock();
    f = Ses_ManCreateClauses( pSes );
    pSes->timeInstance += ( Abc_Clock() - timeStart );
    if ( !f ) return 2; /* proven UNSAT while creating clauses */

    fSat = Ses_ManSolve( pSes );
    if ( fSat == 1 )
        return 1;
    else if ( fSat == 2 )
    {
        pSes->fHitResLimit = 1;
        return 0;
    }

    return 2; /* UNSAT continue */
}

// is there a network for a given number of gates
/* return: (3: impossible, 2: continue, 1: found, 0: gave up) */
static int Ses_ManFindNetworkExactCEGAR( Ses_Man_t * pSes, int nGates, char ** pSol )
{
    int fRes, iMint, fSat, i;
    word pTruth[4];

    /* debug */
    Abc_DebugErase( pSes->nDebugOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose );
    Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );

    /* do #gates and max depth allow for a network? */
    if ( !Ses_CheckGatesConsistency( pSes, nGates ) )
        return 3;

    for ( i = 0; i < pSes->nRandRowAssigns; ++i )
        Abc_TtSetBit( pSes->pTtValues, rand() % pSes->nRows );

    fRes = Ses_ManFindNetworkExact( pSes, nGates );
    if ( fRes != 1 ) return fRes;

    while ( true )
    {
        *pSol = Ses_ManExtractSolution( pSes );
        Abc_TtXor( pTruth, Ses_ManDeriveTruth( pSes, *pSol, 0 ), pSes->pSpec, pSes->nSpecWords, 0 );
        iMint = Abc_TtFindFirstBit( pTruth, pSes->nSpecVars );

        if ( iMint == -1 || (pSes->nSpecVars < 6 && iMint > pSes->nRows) )
        {
            assert( fRes == 1 );
            return 1;
        }
        ABC_FREE( *pSol );

        if ( pSes->fKeepRowAssigns )
            Abc_TtSetBit( pSes->pTtValues, iMint - 1 );
        if ( !Ses_ManCreateTruthTableClause( pSes, iMint - 1 ) ) /* UNSAT, continue */
            return 2;

        if ( ( fSat = Ses_ManSolve( pSes ) ) == 1 ) continue;

        return ( fSat == 2 ) ? 0 : 2;
    }
}

// find minimum size by increasing the number of gates
static char * Ses_ManFindMinimumSizeBottomUp( Ses_Man_t * pSes )
{
    int nGates = pSes->nStartGates, fRes;
    char * pSol = NULL;

    /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */
    pSes->fHitResLimit = 0;

    pSes->nDebugOffset = pSes->nMaxGates >= 10 ? 3 : 2;

    /* adjust number of gates if there is a stair decomposition */
    if ( Vec_IntSize( pSes->vStairDecVars ) )
        nGates = Abc_MaxInt( nGates, Vec_IntSize( pSes->vStairDecVars ) - 1 );

    //Ses_ManStoreDepthAndArrivalTimes( pSes );

    memset( pSes->pTtValues, 0, 4 * sizeof( word ) );

    Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );

    while ( true )
    {
        ++nGates;

        fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol );

        if ( fRes == 0 )
        {
            pSes->fHitResLimit = 1;
            break;
        }
        else if ( fRes == 1 || fRes == 3 )
            break;
    }

    Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );

    return pSol;
}

static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates )
{
    int nGates = pSes->nMaxGates, fRes;
    char * pSol = NULL, * pSol2 = NULL;

    pSes->fHitResLimit = 0;

    Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );

    while ( true )
    {
        fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol2 );

        if ( fRes == 0 )
        {
            pSes->fHitResLimit = 1;
            break;
        }
        else if ( fRes == 2 || fRes == 3 )
            break;

        pSol = pSol2;

        if ( nGates == nMinGates )
            break;

        --nGates;
    }

    Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );

    return pSol;
}

static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
{
    char * pSol = NULL;

    /* do the arrival times allow for a network? */
    if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile )
    {
        if ( !Ses_CheckDepthConsistency( pSes ) )
            return 0;
        Ses_ManComputeMaxGates( pSes );
    }

    pSol = Ses_ManFindMinimumSizeBottomUp( pSes );

    if ( !pSol && pSes->nMaxDepth != -1 && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates )
        return Ses_ManFindMinimumSizeTopDown( pSes, pSes->nGates + 1 );
    else
        return pSol;
}


/**Function*************************************************************

  Synopsis    [Find minimum size networks with a SAT solver.]

  Description [If nMaxDepth is -1, then depth constraints are ignored.
               If nMaxDepth is not -1, one can set pArrTimeProfile which should have the length of nVars.
               One can ignore pArrTimeProfile by setting it to NULL.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
{
    Ses_Man_t * pSes;
    char * pSol;
    Abc_Ntk_t * pNtk = NULL;
    abctime timeStart;

    /* some checks */
    assert( nVars >= 2 && nVars <= 8 );

    timeStart = Abc_Clock();

    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
    pSes->nStartGates = nStartGates;
    pSes->fReasonVerbose = 0;
    pSes->fSatVerbose = 0;
    if ( fVerbose )
        Ses_ManPrintFuncs( pSes );

    if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
    {
        pNtk = Ses_ManExtractNtk( pSol );
        ABC_FREE( pSol );
    }

    pSes->timeTotal = Abc_Clock() - timeStart;

    if ( fVerbose )
        Ses_ManPrintRuntime( pSes );

    /* cleanup */
    Ses_ManClean( pSes );

    return pNtk;
}

Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
{
    Ses_Man_t * pSes;
    char * pSol;
    Gia_Man_t * pGia = NULL;
    abctime timeStart;

    /* some checks */
    assert( nVars >= 2 && nVars <= 8 );

    timeStart = Abc_Clock();

    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
    pSes->nStartGates = nStartGates;
    pSes->fVeryVerbose = 1;
    pSes->fExtractVerbose = 0;
    pSes->fSatVerbose = 0;
    pSes->fReasonVerbose = 1;
    if ( fVerbose )
        Ses_ManPrintFuncs( pSes );

    if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
    {
        pGia = Ses_ManExtractGia( pSol );
        ABC_FREE( pSol );
    }

    pSes->timeTotal = Abc_Clock() - timeStart;

    if ( fVerbose )
        Ses_ManPrintRuntime( pSes );

    /* cleanup */
    Ses_ManClean( pSes );

    return pGia;
}

/**Function*************************************************************

  Synopsis    [Some test cases.]

***********************************************************************/

Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars )
{
    Abc_Ntk_t * pNtk;
    Mem_Flex_t * pMan;
    char * pSopCover;

    pMan = Mem_FlexStart();
    pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
    pNtk = Abc_NtkCreateWithNode( pSopCover );
    Abc_NtkShortNames( pNtk );
    Mem_FlexStop( pMan, 0 );

    return pNtk;
}

void Abc_ExactTestSingleOutput( int fVerbose )
{
    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );

    word pTruth[4] = {0xcafe, 0, 0, 0};
    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
    int pArrTimeProfile[4] = {6, 2, 8, 5};

    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );

    pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
    Abc_NtkShortNames( pNtk2 );
    Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
    assert( pNtk2 );
    assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
    Abc_NtkDelete( pNtk2 );

    pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
    Abc_NtkShortNames( pNtk3 );
    Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
    assert( pNtk3 );
    assert( Abc_NtkLevel( pNtk3 ) <= 3 );
    Abc_NtkDelete( pNtk3 );

    pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
    Abc_NtkShortNames( pNtk4 );
    Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
    assert( pNtk4 );
    assert( Abc_NtkLevel( pNtk4 ) <= 9 );
    Abc_NtkDelete( pNtk4 );

    assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );

    assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );

    Abc_NtkDelete( pNtk );
}

void Abc_ExactTestSingleOutputAIG( int fVerbose )
{
    word pTruth[4] = {0xcafe, 0, 0, 0};
    Abc_Ntk_t * pNtk;
    Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
    int pArrTimeProfile[4] = {6, 2, 8, 5};

    Cec_ManCecSetDefaultParams( pPars );

    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
    Abc_NtkToAig( pNtk );
    pGia = Abc_NtkAigToGia( pNtk, 1 );

    pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );

    pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );

    pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );

    assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );

    assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );

    Gia_ManStop( pGia );
    Gia_ManStop( pGia2 );
    Gia_ManStop( pGia3 );
    Gia_ManStop( pGia4 );
}

void Abc_ExactTest( int fVerbose )
{
    Abc_ExactTestSingleOutput( fVerbose );
    Abc_ExactTestSingleOutputAIG( fVerbose );

    printf( "\n" );
}


/**Function*************************************************************

  Synopsis    [APIs for integraging with the mapper.]

***********************************************************************/
// may need to have a static pointer to the SAT-based synthesis engine and/or loaded library
// this procedure should return 1, if the engine/library are available, and 0 otherwise
int Abc_ExactIsRunning()
{
    return s_pSesStore != NULL;
}
// this procedure returns the number of inputs of the library
// for example, somebody may try to map into 10-cuts while the library only contains 8-functions
int Abc_ExactInputNum()
{
    return 8;
}
// start exact store manager
void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char * pFilename )
{
    if ( !s_pSesStore )
    {
        s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
        s_pSesStore->fVeryVerbose = fVeryVerbose;
        if ( pFilename )
        {
            Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );

            s_pSesStore->szDBName = ABC_CALLOC( char, strlen( pFilename ) + 1 );
            strcpy( s_pSesStore->szDBName, pFilename );
        }
        if ( s_pSesStore->fVeryVerbose )
        {
            s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
        }
    }
    else
        printf( "BMS manager already started\n" );
}
// stop exact store manager
void Abc_ExactStop( const char * pFilename )
{
    if ( s_pSesStore )
    {
        if ( pFilename )
            Ses_StoreWrite( s_pSesStore, pFilename, 1, 0, 0, 0 );
        if ( s_pSesStore->pDebugEntries )
            fclose( s_pSesStore->pDebugEntries );
        Ses_StoreClean( s_pSesStore );
    }
    else
        printf( "BMS manager has not been started\n" );
}
// show statistics about store manager
void Abc_ExactStats()
{
    int i;

    if ( !s_pSesStore )
    {
        printf( "BMS manager has not been started\n" );
        return;
    }

    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "                                    0         1         2         3         4         5         6         7         8     total\n" );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of considered cuts :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pCutCount[i] );
    printf( "%10lu\n", s_pSesStore->nCutCount );
    printf( " - trivial                :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedTrivial[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedTrivial );
    printf( " - synth (imp)            :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedImp[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedImp );
    printf( " - synth (res)            :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedRL[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedRL );
    printf( " - not synth (imp)        :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pUnsynthesizedImp[i] );
    printf( "%10lu\n", s_pSesStore->nUnsynthesizedImp );
    printf( " - not synth (res)        :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pUnsynthesizedRL[i] );
    printf( "%10lu\n", s_pSesStore->nUnsynthesizedRL );
    printf( " - cache hits             :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pCacheHits[i] );
    printf( "%10lu\n", s_pSesStore->nCacheHits );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of entries         : %d\n", s_pSesStore->nEntriesCount );
    printf( "number of valid entries   : %d\n", s_pSesStore->nValidEntriesCount );
    printf( "number of invalid entries : %d\n", s_pSesStore->nEntriesCount - s_pSesStore->nValidEntriesCount );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of SAT calls       : %lu\n", s_pSesStore->nSatCalls );
    printf( "number of UNSAT calls     : %lu\n", s_pSesStore->nUnsatCalls );
    printf( "number of UNDEF calls     : %lu\n", s_pSesStore->nUndefCalls );

    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "Runtime breakdown:\n" );
    ABC_PRTP( "Exact    ", s_pSesStore->timeExact,                          s_pSesStore->timeTotal );
    ABC_PRTP( " Sat     ", s_pSesStore->timeSat,                            s_pSesStore->timeTotal );
    ABC_PRTP( "  Sat    ", s_pSesStore->timeSatSat,                         s_pSesStore->timeTotal );
    ABC_PRTP( "  Unsat  ", s_pSesStore->timeSatUnsat,                       s_pSesStore->timeTotal );
    ABC_PRTP( "  Undef  ", s_pSesStore->timeSatUndef,                       s_pSesStore->timeTotal );
    ABC_PRTP( " Instance", s_pSesStore->timeInstance,                       s_pSesStore->timeTotal );
    ABC_PRTP( "Other    ", s_pSesStore->timeTotal - s_pSesStore->timeExact, s_pSesStore->timeTotal );
    ABC_PRTP( "ALL      ", s_pSesStore->timeTotal,                          s_pSesStore->timeTotal );
}
// this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
// it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
{
    int i, nMaxArrival, nDelta, l;
    Ses_Man_t * pSes = NULL;
    char * pSol = NULL, * pSol2 = NULL, * p;
    int pNormalArrTime[8];
    int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
    abctime timeStart = Abc_Clock(), timeStartExact;

    /* some checks */
    if ( nVars < 0 || nVars > 8 )
    {
        printf( "invalid truth table size %d\n", nVars );
        assert( 0 );
    }

    /* statistics */
    s_pSesStore->nCutCount++;
    s_pSesStore->pCutCount[nVars]++;

    if ( nVars == 0 )
    {
        s_pSesStore->nSynthesizedTrivial++;
        s_pSesStore->pSynthesizedTrivial[0]++;

        *Cost = 0;
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return 0;
    }

    if ( nVars == 1 )
    {
        s_pSesStore->nSynthesizedTrivial++;
        s_pSesStore->pSynthesizedTrivial[1]++;

        *Cost = 0;
        pPerm[0] = (char)0;
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return pArrTimeProfile[0];
    }

    for ( l = 0; l < nVars; ++l )
        pNormalArrTime[l] = pArrTimeProfile[l];

    nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );

    *Cost = ABC_INFINITY;

    if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
    {
        s_pSesStore->nCacheHits++;
        s_pSesStore->pCacheHits[nVars]++;
    }
    else
    {
        if ( s_pSesStore->fVeryVerbose )
        {
            printf( ANSI_COLOR_CYAN );
            Abc_TtPrintHexRev( stdout, pTruth, nVars );
            printf( ANSI_COLOR_RESET );
            printf( " [%d", pNormalArrTime[0] );
            for ( l = 1; l < nVars; ++l )
                printf( " %d", pNormalArrTime[l] );
            printf( "]@%d:", AigLevel );
            fflush( stdout );
        }

        nMaxDepth = pNormalArrTime[0];
        for ( i = 1; i < nVars; ++i )
            nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] );
        nMaxDepth += nVars + 1;
        if ( AigLevel != -1 )
            nMaxDepth = Abc_MinInt( AigLevel - nDelta, nMaxDepth + nVars + 1 );

        timeStartExact = Abc_Clock();

        pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose );
        pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
        pSes->pSat = s_pSesStore->pSat;
        pSes->nStartGates = nVars - 2;

        while ( pSes->nMaxDepth ) /* there is improvement */
        {
            if ( s_pSesStore->fVeryVerbose )
            {
                printf( " %d", pSes->nMaxDepth );
                fflush( stdout );
            }

            if ( ( pSol2 = Ses_ManFindMinimumSize( pSes ) ) != NULL )
            {
                if ( s_pSesStore->fVeryVerbose )
                {
                    if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
                    printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth );
                }
                if ( pSol )
                    ABC_FREE( pSol );
                pSol = pSol2;
                pSes->nMaxDepth--;
            }
            else
            {
                if ( s_pSesStore->fVeryVerbose )
                {
                    if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
                    printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth );
                }
                break;
            }
        }

        if ( s_pSesStore->fVeryVerbose )
            printf( "        \n" );

        /* log unsuccessful case for debugging */
        if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit )
            Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth, pSol, nVars - 2 );

        pSes->timeTotal = Abc_Clock() - timeStartExact;

        /* statistics */
        s_pSesStore->nSatCalls += pSes->nSatCalls;
        s_pSesStore->nUnsatCalls += pSes->nUnsatCalls;
        s_pSesStore->nUndefCalls += pSes->nUndefCalls;

        s_pSesStore->timeSat += pSes->timeSat;
        s_pSesStore->timeSatSat += pSes->timeSatSat;
        s_pSesStore->timeSatUnsat += pSes->timeSatUnsat;
        s_pSesStore->timeSatUndef += pSes->timeSatUndef;
        s_pSesStore->timeInstance += pSes->timeInstance;
        s_pSesStore->timeExact += pSes->timeTotal;

        /* cleanup (we need to clean before adding since pTruth may have been modified by pSes) */
        fResLimit = pSes->fHitResLimit;
        Ses_ManCleanLight( pSes );

        /* store solution */
        Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol, fResLimit );
    }

    if ( pSol )
    {
        *Cost = pSol[ABC_EXACT_SOL_NGATES];
        p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1;
        Delay = *p++;
        for ( l = 0; l < nVars; ++l )
            pPerm[l] = *p++;
    }

    if ( pSol )
    {
        int Delay2 = 0;
        for ( l = 0; l < nVars; ++l )
        {
            //printf( "%d ", pPerm[l] );
            Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] );
        }
        //printf( "  output arrival = %d    recomputed = %d\n", Delay, Delay2 );
        //if ( Delay != Delay2 )
        //{
        //    printf( "^--- BUG!\n" );
        //    assert( 0 );
        //}

        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return Delay2;
    }
    else
    {
        assert( *Cost == ABC_INFINITY );

        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return ABC_INFINITY;
    }
}
// this procedure returns a new node whose output in terms of the given fanins
// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
{
    char * pSol = NULL;
    int i, j, nMaxArrival;
    int pNormalArrTime[8];
    char const * p;
    Abc_Obj_t * pObj;
    Vec_Ptr_t * pGates;
    char pGateTruth[5];
    char * pSopCover;
    abctime timeStart = Abc_Clock();

    if ( nVars == 0 )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
    }
    if ( nVars == 1 )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
    }

    for ( i = 0; i < nVars; ++i )
        pNormalArrTime[i] = pArrTimeProfile[i];
    Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
    assert( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) );
    if ( !pSol )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return NULL;
    }

    assert( pSol[ABC_EXACT_SOL_NVARS] == nVars );
    assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );

    pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] );
    pGateTruth[3] = '0';
    pGateTruth[4] = '\0';

    /* primary inputs */
    for ( i = 0; i < nVars; ++i )
    {
        assert( pFanins[i] );
        Vec_PtrPush( pGates, pFanins[i] );
    }

    /* gates */
    p = pSol + 3;
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
    {
        pGateTruth[2] = '0' + ( *p & 1 );
        pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
        pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
        ++p;

        assert( *p == 2 ); /* binary gate */
        ++p;

        /* invert truth table if we are last gate and inverted */
        if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
            for ( j = 0; j < 4; ++j )
                pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';

        pSopCover = Abc_SopFromTruthBin( pGateTruth );
        pObj = Abc_NtkCreateNode( pNtk );
        assert( pObj );
        pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
        Vec_PtrPush( pGates, pObj );
        ABC_FREE( pSopCover );

        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
    }

    /* output */
    pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );

    Vec_PtrFree( pGates );

    s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
    return pObj;
}

void Abc_ExactStoreTest( int fVerbose )
{
    int i;
    word pTruth[4] = {0xcafe, 0, 0, 0};
    int pArrTimeProfile[4] = {6, 2, 8, 5};
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pFanins[4];
    Vec_Ptr_t * vNames;
    char pPerm[4];
    int Cost;

    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
    pNtk->pName = Extra_UtilStrsav( "exact" );
    vNames = Abc_NodeGetFakeNames( 4u );

    /* primary inputs */
    Vec_PtrPush( pNtk->vObjs, NULL );
    for ( i = 0; i < 4; ++i )
    {
        pFanins[i] = Abc_NtkCreatePi( pNtk );
        Abc_ObjAssignName( pFanins[i], (char*)Vec_PtrEntry( vNames, i ), NULL );
    }
    Abc_NodeFreeNames( vNames );

    Abc_ExactStart( 10000, 1, fVerbose, 0, NULL );

    assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );

    assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 );

    assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );

    (*pArrTimeProfile)++;
    assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
    (*pArrTimeProfile)--;

    Abc_ExactStop( NULL );

    Abc_NtkDelete( pNtk );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END