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

  FileName    [bmcFx.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT-based bounded model checking.]

  Synopsis    [INT-FX: Interpolation-based logic sharing extraction.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

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

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

#include "bmc.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Create hash table to hash divisors.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
#define TAB_UNUSED 0x7FFF
typedef struct Tab_Obj_t_ Tab_Obj_t; // 16 bytes
struct Tab_Obj_t_
{
    int         Table;
    int         Next;
    unsigned    Cost : 17;
    unsigned    LitA : 15;
    unsigned    LitB : 15;
    unsigned    LitC : 15;
    unsigned    Func :  2;
};
typedef struct Tab_Tab_t_ Tab_Tab_t; // 16 bytes
struct Tab_Tab_t_
{
    int         SizeMask;
    int         nBins;
    Tab_Obj_t * pBins;
};
static inline Tab_Tab_t * Tab_TabAlloc( int LogSize )
{
    Tab_Tab_t * p = ABC_CALLOC( Tab_Tab_t, 1 );
    assert( LogSize >= 4 && LogSize <= 31 );
    p->SizeMask = (1 << LogSize) - 1;
    p->pBins = ABC_CALLOC( Tab_Obj_t, p->SizeMask + 1 );
    p->nBins = 1;
    return p;
}
static inline void Tab_TabFree( Tab_Tab_t * p )
{
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}
static inline Vec_Int_t * Tab_TabFindBest( Tab_Tab_t * p, int nDivs )
{
    char * pNames[5] = {"const1", "and", "xor", "mux", "none"};
    int * pOrder, i;
    Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); 
    Vec_Int_t * vCosts = Vec_IntAlloc( p->nBins ); 
    Tab_Obj_t * pEnt, * pLimit = p->pBins + p->nBins;
    for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ )
        Vec_IntPush( vCosts, -(int)pEnt->Cost );
    pOrder = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
    for ( i = 0; i < Vec_IntSize(vCosts); i++ )
    {
        pEnt = p->pBins + pOrder[i];
        if ( i == nDivs || pEnt->Cost == 1 )
            break;
        printf( "Lit0 = %5d.  Lit1 = %5d.  Lit2 = %5d.  Func = %s.  Cost = %3d.\n",
            pEnt->LitA, pEnt->LitB, pEnt->LitC, pNames[pEnt->Func], pEnt->Cost );
        Vec_IntPushTwo( vDivs, pEnt->Func, pEnt->LitA );
        Vec_IntPushTwo( vDivs, pEnt->LitB, pEnt->LitC );
    }
    Vec_IntFree( vCosts );
    ABC_FREE( pOrder );
    return vDivs;
}
static inline int Tab_Hash( int LitA, int LitB, int LitC, int Func, int Mask )
{
    return (LitA * 50331653 + LitB * 100663319 + LitC * 201326611 + Func * 402653189) & Mask;
}
static inline void Tab_TabRehash( Tab_Tab_t * p )
{
    Tab_Obj_t * pEnt, * pLimit, * pBin;
    assert( p->nBins == p->SizeMask + 1 );
    // realloc memory
    p->pBins = ABC_REALLOC( Tab_Obj_t, p->pBins, 2 * (p->SizeMask + 1) );
    memset( p->pBins + p->SizeMask + 1, 0, sizeof(Tab_Obj_t) * (p->SizeMask + 1) );
    // clean entries
    pLimit = p->pBins + p->SizeMask + 1;
    for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ )
        pEnt->Table = pEnt->Next = 0;
    // rehash entries
    p->SizeMask = 2 * p->SizeMask + 1;
    for ( pEnt = p->pBins + 1; pEnt < pLimit; pEnt++ )
    {
        pBin = p->pBins + Tab_Hash( pEnt->LitA, pEnt->LitB, pEnt->LitC, pEnt->Func, p->SizeMask );
        pEnt->Next  = pBin->Table;
        pBin->Table = pEnt - p->pBins;
        assert( !pEnt->Next || pEnt->Next != pBin->Table );
    }
}
static inline Tab_Obj_t * Tab_TabEntry( Tab_Tab_t * p, int i ) { return i ? p->pBins + i : NULL; }
static inline int         Tab_TabHashAdd( Tab_Tab_t * p, int * pLits, int Func, int Cost )
{
    if ( p->nBins == p->SizeMask + 1 )
        Tab_TabRehash( p );
    assert( p->nBins < p->SizeMask + 1 );
    {
        Tab_Obj_t * pEnt, * pBin = p->pBins + Tab_Hash(pLits[0], pLits[1], pLits[2], Func, p->SizeMask);
        for ( pEnt = Tab_TabEntry(p, pBin->Table); pEnt; pEnt = Tab_TabEntry(p, pEnt->Next) )
            if ( (int)pEnt->LitA == pLits[0] && (int)pEnt->LitB == pLits[1] && (int)pEnt->LitC == pLits[2] && (int)pEnt->Func == Func )
                {  pEnt->Cost += Cost; return 1; }
        pEnt = p->pBins + p->nBins;
        pEnt->LitA  = pLits[0];
        pEnt->LitB  = pLits[1];
        pEnt->LitC  = pLits[2];
        pEnt->Func  = Func;
        pEnt->Cost  = Cost;
        pEnt->Next  = pBin->Table;
        pBin->Table = p->nBins++;
        assert( !pEnt->Next || pEnt->Next != pBin->Table );
        return 0;
    }
}


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

  Synopsis    [Input is four literals. Output is type, polarity and fanins.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
// name types
typedef enum { 
    DIV_CST = 0,   // 0: constant 1
    DIV_AND,       // 1: and (ordered fanins)
    DIV_XOR,       // 2: xor (ordered fanins)
    DIV_MUX,       // 3: mux (c, d1, d0)
    DIV_NONE       // 4: not used
} Div_Type_t; 

static inline Div_Type_t Bmc_FxDivOr( int LitA, int LitB, int * pLits, int * pPhase )
{
    assert( LitA != LitB );
    if ( Abc_Lit2Var(LitA) == Abc_Lit2Var(LitB) )
        return DIV_CST;
    if ( LitA > LitB )
        ABC_SWAP( int, LitA, LitB );
    pLits[0] = Abc_LitNot(LitA);
    pLits[1] = Abc_LitNot(LitB);
    *pPhase = 1;
    return DIV_AND;
}
static inline Div_Type_t Bmc_FxDivXor( int LitA, int LitB, int * pLits, int * pPhase )
{
    assert( LitA != LitB );
    *pPhase ^= Abc_LitIsCompl(LitA);
    *pPhase ^= Abc_LitIsCompl(LitB);
    pLits[0] = Abc_LitRegular(LitA);
    pLits[1] = Abc_LitRegular(LitB);
    return DIV_XOR;
}
static inline Div_Type_t Bmc_FxDivMux( int LitC, int LitCn, int LitT, int LitE, int * pLits, int * pPhase )
{
    assert( LitC != LitCn );
    assert( Abc_Lit2Var(LitC) == Abc_Lit2Var(LitCn) );
    assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitT) );
    assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) );
    assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) );
    if ( Abc_LitIsCompl(LitC) )
    {
        LitC = Abc_LitRegular(LitC);
        ABC_SWAP( int, LitT, LitE );
    }
    if ( Abc_LitIsCompl(LitT) )
    {
        *pPhase ^= 1;
        LitT = Abc_LitNot(LitT);
        LitE = Abc_LitNot(LitE);
    }
    pLits[0] = LitC;
    pLits[1] = LitT;
    pLits[2] = LitE;
    return DIV_MUX;
}
static inline Div_Type_t Div_FindType( int LitA[2], int LitB[2], int * pLits, int * pPhase )
{
    *pPhase = 0;
    pLits[0] = pLits[1] = pLits[2] = TAB_UNUSED;
    if ( LitA[0] == -1 && LitA[1] == -1 ) return DIV_CST;
    if ( LitB[0] == -1 && LitB[1] == -1 ) return DIV_CST;
    assert( LitA[0] >= 0 && LitB[0] >= 0 );
    assert( LitA[0] != LitB[0] );
    if ( LitA[1] == -1 && LitB[1] == -1 )
        return Bmc_FxDivOr( LitA[0], LitB[0], pLits, pPhase );
    assert( LitA[1] != LitB[1] );
    if ( LitA[1] == -1 || LitB[1] == -1 )
    {
        if ( LitA[1] == -1 )
        {
            ABC_SWAP( int, LitA[0], LitB[0] );
            ABC_SWAP( int, LitA[1], LitB[1] );
        }
        assert( LitA[0] >= 0 && LitA[1] >= 0 );
        assert( LitB[0] >= 0 && LitB[1] == -1 );
        if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[0]) )
            return Bmc_FxDivOr( LitB[0], LitA[1], pLits, pPhase );
        if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[1]) )
            return Bmc_FxDivOr( LitB[0], LitA[0], pLits, pPhase );
        return DIV_NONE;
    }
    if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) && Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) )
        return Bmc_FxDivXor( LitA[0], LitB[1], pLits, pPhase );
    if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) )
        return Bmc_FxDivMux( LitA[0], LitB[0], LitA[1], LitB[1], pLits, pPhase );
    if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[1]) )
        return Bmc_FxDivMux( LitA[0], LitB[1], LitA[1], LitB[0], pLits, pPhase );
    if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[0]) )
        return Bmc_FxDivMux( LitA[1], LitB[0], LitA[0], LitB[1], pLits, pPhase );
    if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) )
        return Bmc_FxDivMux( LitA[1], LitB[1], LitA[0], LitB[0], pLits, pPhase );
    return DIV_NONE;
}

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

  Synopsis    [Returns the number of shared variables, or -1 if failed.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Div_AddLit( int Lit, int pLits[2] )
{
    if ( pLits[0] == -1 )
        pLits[0] = Lit;
    else if ( pLits[1] == -1 )
        pLits[1] = Lit;
    else return 1;
    return 0;
}
int Div_FindDiv( Vec_Int_t * vA, Vec_Int_t * vB, int pLitsA[2], int pLitsB[2] )
{
    int Counter = 0;
    int * pBegA = vA->pArray, * pEndA = vA->pArray + vA->nSize;
    int * pBegB = vB->pArray, * pEndB = vB->pArray + vB->nSize; 
    pLitsA[0] = pLitsA[1] = pLitsB[0] = pLitsB[1] = -1;
    while ( pBegA < pEndA && pBegB < pEndB )
    {
        if ( *pBegA == *pBegB )
            pBegA++, pBegB++, Counter++;
        else if ( *pBegA < *pBegB )
        {
            if ( Div_AddLit( *pBegA++, pLitsA ) )
                return -1;
        }
        else  
        {
            if ( Div_AddLit( *pBegB++, pLitsB ) )
                return -1;
        }
    }
    while ( pBegA < pEndA )
        if ( Div_AddLit( *pBegA++, pLitsA ) )
            return -1;
    while ( pBegB < pEndB )
        if ( Div_AddLit( *pBegB++, pLitsB ) )
            return -1;
    return Counter;
}

void Div_CubePrintOne( Vec_Int_t * vCube, Vec_Str_t * vStr, int nVars )
{
    int i, Lit;
    Vec_StrFill( vStr, nVars, '-' );
    Vec_IntForEachEntry( vCube, Lit, i )
        Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
    printf( "%s\n", Vec_StrArray(vStr) );
}
void Div_CubePrint( Vec_Wec_t * p, int nVars )
{
    Vec_Int_t * vCube; int i;
    Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
    Vec_WecForEachLevel( p, vCube, i )
        Div_CubePrintOne( vCube, vStr, nVars );
    Vec_StrFree( vStr );
}

Vec_Int_t * Div_CubePairs( Vec_Wec_t * p, int nVars, int nDivs )
{
    int fVerbose = 0;
    char * pNames[5] = {"const1", "and", "xor", "mux", "none"};
    Vec_Int_t * vCube1, * vCube2, * vDivs; 
    int i1, i2, i, k, pLitsA[2], pLitsB[2], pLits[4], Type, Phase, nBase, Count = 0;
    Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
    Tab_Tab_t * pTab = Tab_TabAlloc( 5 );
    Vec_WecForEachLevel( p, vCube1, i )
    {
        // add lit pairs
        pLits[2] = TAB_UNUSED;
        Vec_IntForEachEntry( vCube1, pLits[0], i1 )
        Vec_IntForEachEntryStart( vCube1, pLits[1], i2, i1+1 )
        {
            Tab_TabHashAdd( pTab, pLits, DIV_AND, 1 );
        }

        Vec_WecForEachLevelStart( p, vCube2, k, i+1 )
        {
            nBase = Div_FindDiv( vCube1, vCube2, pLitsA, pLitsB );
            if ( nBase == -1 )
                continue;
            Type = Div_FindType(pLitsA, pLitsB, pLits, &Phase);
            if ( Type >= DIV_AND && Type <= DIV_MUX )
                Tab_TabHashAdd( pTab, pLits, Type, nBase );

            if ( fVerbose )
            {
                printf( "Pair %d:\n", Count++ );
                Div_CubePrintOne( vCube1, vStr, nVars );
                Div_CubePrintOne( vCube2, vStr, nVars );
                printf( "Result = %d   ", nBase );
                assert( nBase > 0 );

                printf( "Type = %s  ", pNames[Type] );
                printf( "LitA = %d ",  pLits[0] );
                printf( "LitB = %d ",  pLits[1] );
                printf( "LitC = %d ",  pLits[2] );
                printf( "Phase = %d ", Phase );
                printf( "\n" );
            }
        }
    }
    // print the table
    printf( "Divisors = %d.\n", pTab->nBins );
    vDivs = Tab_TabFindBest( pTab, nDivs );
    // cleanup
    Vec_StrFree( vStr );
    Tab_TabFree( pTab );
    return vDivs;
}

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

  Synopsis    [Solve the enumeration problem.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, int fDumpPla, int fVerbose, int * pCounter, Vec_Wec_t * vCubes )
{
    int nBTLimit = 1000000;
    int fUseOrder = 1;
    Vec_Int_t * vLevel  = NULL;
    Vec_Int_t * vLits   = Vec_IntAlloc( Vec_IntSize(vVars) );
    Vec_Int_t * vLits2  = Vec_IntAlloc( Vec_IntSize(vVars) );
    Vec_Str_t * vCube   = Vec_StrStart( Vec_IntSize(vVars)+1 );
    int status, i, k, n, Lit, Lit2, iVar, nFinal, * pFinal, pLits[2], nIter = 0, RetValue = 0;
    int Before, After, Total = 0, nLits = 0;
    pLits[0] = Abc_Var2Lit( iOut + 1, 0 ); // F = 1
    pLits[1] = Abc_Var2Lit( iAuxVar, 0 );  // iNewLit
    if ( vCubes )
        Vec_WecClear( vCubes );
    if ( fDumpPla )
    printf( ".i %d\n", Vec_IntSize(vVars) );
    if ( fDumpPla )
    printf( ".o %d\n", 1 );
    while ( 1 ) 
    {
        // find onset minterm
        status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            { RetValue = -1; break; }
        if ( status == l_False )
            { RetValue = 1; break; }
        assert( status == l_True );
        // collect divisor literals
        Vec_IntClear( vLits );
        Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0
//        Vec_IntForEachEntryReverse( vVars, iVar, i )
        Vec_IntForEachEntry( vVars, iVar, i )
            Vec_IntPush( vLits, sat_solver_var_literal(pSat, iVar) );

        if ( fUseOrder )
        {
            //////////////////////////////////////////////////////////////
            // save these literals
            Vec_IntClear( vLits2 );
            Vec_IntAppend( vLits2, vLits );
            Before = Vec_IntSize(vLits2);

            // try removing literals from the cube
            Vec_IntForEachEntry( vLits2, Lit2, k )
            {
                if ( Lit2 == Abc_LitNot(pLits[0]) )
                    continue;
                Vec_IntClear( vLits );
                Vec_IntForEachEntry( vLits2, Lit, n )
                    if ( Lit != -1 && Lit != Lit2 )
                        Vec_IntPush( vLits, Lit );
                // call sat
                status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
                if ( status == l_Undef )
                    assert( 0 );
                if ( status == l_True ) // SAT
                    continue;
                // Lit2 can be removed
                Vec_IntWriteEntry( vLits2, k, -1 );
            }

            // make one final run
            Vec_IntClear( vLits );
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    Vec_IntPush( vLits, Lit2 );
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );

            // get subset of literals
            nFinal = sat_solver_final( pSat, &pFinal );
            //////////////////////////////////////////////////////////////
        }
        else
        {
            ///////////////////////////////////////////////////////////////
            // check against offset
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            if ( status == l_Undef )
                { RetValue = -1; break; }
            if ( status == l_True )
                break;
            assert( status == l_False );
            // get subset of literals
            nFinal = sat_solver_final( pSat, &pFinal );
            Before = nFinal;
            //printf( "Before %d. ", nFinal );

/*
            // save these literals
            Vec_IntClear( vLits );
            for ( i = 0; i < nFinal; i++ )
                Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) );
            Vec_IntReverseOrder( vLits );

            // make one final run
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );
            nFinal = sat_solver_final( pSat, &pFinal );
*/

            // save these literals
            Vec_IntClear( vLits2 );
            for ( i = 0; i < nFinal; i++ )
                Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) );
            Vec_IntSort( vLits2, 1 );

            // try removing literals from the cube
            Vec_IntForEachEntry( vLits2, Lit2, k )
            {
                if ( Lit2 == Abc_LitNot(pLits[0]) )
                    continue;
                Vec_IntClear( vLits );
                Vec_IntForEachEntry( vLits2, Lit, n )
                    if ( Lit != -1 && Lit != Lit2 )
                        Vec_IntPush( vLits, Lit );
                // call sat
                status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
                if ( status == l_Undef )
                    assert( 0 );
                if ( status == l_True ) // SAT
                    continue;
                // Lit2 can be removed
                Vec_IntWriteEntry( vLits2, k, -1 );
            }

            // make one final run
            Vec_IntClear( vLits );
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    Vec_IntPush( vLits, Lit2 );
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );

            // put them back
            nFinal = 0;
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    pFinal[nFinal++] = Abc_LitNot(Lit2);        
            /////////////////////////////////////////////////////////
        }


        //printf( "After %d. \n", nFinal );
        After  = nFinal;
        Total += Before - After;

        // get subset of literals
        //nFinal = sat_solver_final( pSat, &pFinal );
        // compute cube and add clause
        Vec_IntClear( vLits );
        Vec_IntPush( vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
        if ( fDumpPla )
            Vec_StrFill( vCube, Vec_IntSize(vVars), '-' );
        if ( vCubes )
            vLevel = Vec_WecPushLevel( vCubes );
        for ( i = 0; i < nFinal; i++ )
        {
            if ( pFinal[i] == pLits[0] )
                continue;
            Vec_IntPush( vLits, pFinal[i] );
            iVar = Vec_IntFind( vVars, Abc_Lit2Var(pFinal[i]) );   
            assert( iVar >= 0 && iVar < Vec_IntSize(vVars) );
            //printf( "%s%d ", Abc_LitIsCompl(pFinal[i]) ? "+":"-", iVar );
            if ( fDumpPla )
                Vec_StrWriteEntry( vCube, iVar, (char)(!Abc_LitIsCompl(pFinal[i]) ? '0' : '1') );
            if ( vLevel )
                Vec_IntPush( vLevel, Abc_Var2Lit(iVar, !Abc_LitIsCompl(pFinal[i])) );
        }
        if ( vCubes )
            Vec_IntSort( vLevel, 0 );
        if ( fDumpPla )
            printf( "%s 1\n", Vec_StrArray(vCube) );
        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
        assert( status );
        nLits += Vec_IntSize(vLevel);
        nIter++;
    }
    if ( fDumpPla )
    printf( ".e\n" );
    if ( fDumpPla )
    printf( ".p %d\n\n", nIter );
    if ( fVerbose )
    printf( "Cubes = %d.  Reduced = %d.  Lits = %d\n", nIter, Total, nLits );
    if ( pCounter )
        *pCounter = nIter;
//    assert( status == l_True );
    Vec_IntFree( vLits );
    Vec_IntFree( vLits2 );
    Vec_StrFree( vCube );
    return RetValue;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bmc_FxCompute( Gia_Man_t * p )
{
    // create dual-output circuit with on-set/off-set
    extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p );
    Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p );
    // create SAT solver
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p2, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // compute parameters
    int nOuts = Gia_ManCoNum(p);
    int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1;
    int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat );
    int nCubes[2][2] = {{0}};
    // create variables
    Vec_Int_t * vVars = Vec_IntAlloc( nCiVars );
    for ( n = 0; n < nCiVars; n++ )
        Vec_IntPush( vVars, iCiVarBeg + n );
    sat_solver_setnvars( pSat, iAuxVarStart + 4*nOuts );
    // iterate through outputs
    for ( o = 0; o < nOuts; o++ )
    for ( i = 0; i < 2; i++ )
    for ( n = 0; n < 2; n++ ) // 0=onset, 1=offset
//    for ( n = 1; n >= 0; n-- ) // 0=onset, 1=offset
    {
        printf( "Out %3d %sset ", o, n ? "off" : " on" );
        RetValue = Bmc_FxSolve( pSat, Abc_Var2Lit(o, n), iAuxVarStart + 2*i*nOuts + Abc_Var2Lit(o, n), vVars, 0, 0, &nCounter, NULL );
        if ( RetValue == 0 )
            printf( "Mismatch\n" );
        if ( RetValue == -1 )
            printf( "Timeout\n" );
        nCubes[i][n] += nCounter;
    }
    // cleanup
    Vec_IntFree( vVars );
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Gia_ManStop( p2 );
    printf( "Onset = %5d.   Offset = %5d.      Onset = %5d.   Offset = %5d.\n", nCubes[0][0], nCubes[0][1], nCubes[1][0], nCubes[1][1] );
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bmc_FxAddClauses( sat_solver * pSat, Vec_Int_t * vDivs, int iCiVarBeg, int iVarStart )
{
    int i, Func, pLits[3], nDivs = Vec_IntSize(vDivs)/4;
    assert( Vec_IntSize(vDivs) % 4 == 0 );
    // create new var for each divisor
    for ( i = 0; i < nDivs; i++ )
    {
        Func     = Vec_IntEntry(vDivs, 4*i+0);
        pLits[0] = Vec_IntEntry(vDivs, 4*i+1);
        pLits[1] = Vec_IntEntry(vDivs, 4*i+2);
        pLits[2] = Vec_IntEntry(vDivs, 4*i+3);
        //printf( "Adding clause with vars %d %d -> %d\n", iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iVarStart + nDivs - 1 - i );
        if ( Func == DIV_AND )
            sat_solver_add_and( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 
                Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), 0 );
        else if ( Func == DIV_XOR )
            sat_solver_add_xor( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 0 );
        else if ( Func == DIV_MUX )
            sat_solver_add_mux( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iCiVarBeg + Abc_Lit2Var(pLits[2]), 
                Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), Abc_LitIsCompl(pLits[2]), 0 );
        else assert( 0 );
    }
}
int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add )
{
    int Extra    = 1000;
    // create SAT solver
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // compute parameters
    int nCiVars   = Gia_ManCiNum(p);             // PI count
    int iCiVarBeg = pCnf->nVars - nCiVars;//- 1;   // first PI var
    int iCiVarCur = iCiVarBeg + nCiVars;         // current unused PI var
    int n, Iter, RetValue;
    // create variables
    int iAuxVarStart = sat_solver_nvars(pSat) + Extra; // the aux var
    sat_solver_setnvars( pSat, iAuxVarStart + 1 + nIterMax );
    for ( Iter = 0; Iter < nIterMax; Iter++ )
    {
        Vec_Wec_t * vCubes = Vec_WecAlloc( 1000 );
        // collect variables
        Vec_Int_t * vVar2Sat = Vec_IntAlloc( iCiVarCur-iCiVarBeg ), * vDivs;
//        for ( n = iCiVarCur - 1; n >= iCiVarBeg; n-- )
        for ( n = iCiVarBeg; n < iCiVarCur; n++ )
            Vec_IntPush( vVar2Sat, n );
        // iterate through outputs
        printf( "\nIteration %d (Aux = %d)\n", Iter, iAuxVarStart + Iter );
        RetValue = Bmc_FxSolve( pSat, 0, iAuxVarStart + Iter, vVar2Sat, 1, 1, NULL, vCubes );
        if ( RetValue == 0 )
            printf( "Mismatch\n" );
        if ( RetValue == -1 )
            printf( "Timeout\n" );
        // print cubes
        //Div_CubePrint( vCubes, nCiVars );
        vDivs = Div_CubePairs( vCubes, nCiVars, nDiv2Add );
        Vec_WecFree( vCubes );
        // add clauses and update variables
        Bmc_FxAddClauses( pSat, vDivs, iCiVarBeg, iCiVarCur );
        iCiVarCur += Vec_IntSize(vDivs)/4;
        Vec_IntFree( vDivs );
        // cleanup
        assert( Vec_IntSize(vVar2Sat) <= nCiVars + Extra );
        Vec_IntFree( vVar2Sat );
    }
    // cleanup
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    return 1;
}


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


ABC_NAMESPACE_IMPL_END