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

  FileName    [xsatSolver.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [xSAT - A SAT solver written in C.
               Read the license file for more info.]

  Synopsis    [Solver internal functions implementation.]

  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]

  Affiliation [UC Berkeley / UFRGS]

  Date        [Ver. 1.0. Started - November 10, 2016.]

  Revision    []

***********************************************************************/
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>

#include "xsatHeap.h"
#include "xsatSolver.h"
#include "xsatUtils.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DECLARATIONS                        ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int xSAT_SolverDecide( xSAT_Solver_t * s )
{
    int NextVar = VarUndef;

    while ( NextVar == VarUndef || Vec_StrEntry( s->vAssigns, NextVar ) != VarX )
    {
        if ( xSAT_HeapSize( s->hOrder ) == 0 )
        {
            NextVar = VarUndef;
            break;
        }
        else
            NextVar = xSAT_HeapRemoveMin( s->hOrder );
    }
    return NextVar;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t * s )
{
    Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) );
    int Var;

    for ( Var = 0; Var < Vec_StrSize( s->vAssigns ); Var++ )
        if ( Vec_StrEntry( s->vAssigns, Var ) == VarX )
            Vec_IntPush( vTemp, Var );

    xSAT_HeapBuild( s->hOrder, vTemp );
    Vec_IntFree( vTemp );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
{
    int i;
    unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );

    for ( i = 0; i < Vec_IntSize( s->vActivity ); i++ )
        pActivity[i] >>= 19;

    s->nVarActInc >>= 19;
    s->nVarActInc = Abc_MaxInt( s->nVarActInc, ( 1 << 5 ) );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverVarActBump( xSAT_Solver_t * s, int Var )
{
    unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );

    pActivity[Var] += s->nVarActInc;
    if ( pActivity[Var] & 0x80000000 )
        xSAT_SolverVarActRescale( s );

    if ( xSAT_HeapInHeap( s->hOrder, Var ) )
        xSAT_HeapDecrease( s->hOrder, Var );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverVarActDecay( xSAT_Solver_t * s )
{
    s->nVarActInc += ( s->nVarActInc >> 4 );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s )
{
    xSAT_Clause_t * pC;
    int i, CRef;

    Vec_IntForEachEntry( s->vLearnts, CRef, i )
    {
        pC = xSAT_SolverReadClause( s, ( unsigned ) CRef );
        pC->pData[pC->nSize].Act >>= 14;
    }
    s->nClaActInc >>= 14;
    s->nClaActInc = Abc_MaxInt( s->nClaActInc, ( 1 << 10 ) );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverClaActBump( xSAT_Solver_t* s, xSAT_Clause_t * pCla )
{
    pCla->pData[pCla->nSize].Act += s->nClaActInc;
    if ( pCla->pData[pCla->nSize].Act & 0x80000000 )
        xSAT_SolverClaActRescale( s );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverClaActDecay( xSAT_Solver_t * s )
{
    s->nClaActInc += ( s->nClaActInc >> 10 );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
{
    int i;
    int nLBD = 0;

    s->nStamp++;
    for ( i = 0; i < pCla->nSize; i++ )
    {
        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) );
        if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
        {
            Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
            nLBD++;
        }
    }
    return nLBD;
}

static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits )
{
    int i;
    int nLBD = 0;

    s->nStamp++;
    for ( i = 0; i < Vec_IntSize( vLits ); i++ )
    {
        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Vec_IntEntry( vLits, i ) ) );
        if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
        {
            Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
            nLBD++;
        }
    }
    return nLBD;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
{
    unsigned CRef;
    xSAT_Clause_t * pCla;
    xSAT_Watcher_t w1;
    xSAT_Watcher_t w2;
    unsigned nWords;

    assert( Vec_IntSize( vLits ) > 1);
    assert( fLearnt == 0 || fLearnt == 1 );

    nWords = 3 + fLearnt + Vec_IntSize( vLits );
    CRef = xSAT_MemAppend( s->pMemory, nWords );
    pCla = xSAT_SolverReadClause( s, CRef );
    pCla->fLearnt = fLearnt;
    pCla->fMark = 0;
    pCla->fReallocd = 0;
    pCla->fCanBeDel = fLearnt;
    pCla->nSize = Vec_IntSize( vLits );
    memcpy( &( pCla->pData[0].Lit ), Vec_IntArray( vLits ), sizeof( int ) * Vec_IntSize( vLits ) );

    if ( fLearnt )
    {
        Vec_IntPush( s->vLearnts, CRef );
        pCla->nLBD = xSAT_SolverClaCalcLBD2( s, vLits );
        pCla->pData[pCla->nSize].Act = 0;
        s->Stats.nLearntLits += Vec_IntSize( vLits );
        xSAT_SolverClaActBump(s, pCla);
    }
    else
    {
        Vec_IntPush( s->vClauses, CRef );
        s->Stats.nClauseLits += Vec_IntSize( vLits );
    }

    w1.CRef = CRef;
    w2.CRef = CRef;
    w1.Blocker = pCla->pData[1].Lit;
    w2.Blocker = pCla->pData[0].Lit;

    if ( Vec_IntSize( vLits ) == 2 )
    {
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
    }
    else
    {
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
    }
    return CRef;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int xSAT_SolverEnqueue( xSAT_Solver_t * s, int Lit, unsigned Reason )
{
    int Var = xSAT_Lit2Var( Lit );

    Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) );
    Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
    Vec_IntWriteEntry( s->vReasons, Var, ( int ) Reason );
    Vec_IntPush( s->vTrail, Lit );

    return true;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_SolverNewDecision( xSAT_Solver_t * s, int Lit )
{
    assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX );
    s->Stats.nDecisions++;
    Vec_IntPush( s->vTrailLim, Vec_IntSize( s->vTrail ) );
    xSAT_SolverEnqueue( s, Lit, CRefUndef );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverCancelUntil( xSAT_Solver_t * s, int Level )
{
    int c;

    if ( xSAT_SolverDecisionLevel( s ) <= Level )
        return;

    for ( c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- )
    {
        int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) );

        Vec_StrWriteEntry( s->vAssigns, Var, VarX );
        Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef );
        Vec_StrWriteEntry( s->vPolarity, Var, ( char )xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) );

        if ( !xSAT_HeapInHeap( s->hOrder, Var ) )
            xSAT_HeapInsert( s->hOrder, Var );
    }

    s->iQhead = Vec_IntEntry( s->vTrailLim, Level );
    Vec_IntShrink( s->vTrail, Vec_IntEntry( s->vTrailLim, Level ) );
    Vec_IntShrink( s->vTrailLim, Level );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
{
    int top = Vec_IntSize( s->vTagged );

    assert( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
    Vec_IntClear( s->vStack );
    Vec_IntPush( s->vStack, xSAT_Lit2Var( Lit ) );

    while ( Vec_IntSize( s->vStack ) )
    {
        int i;
        int v = Vec_IntPop(  s->vStack );
        xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( unsigned ) Vec_IntEntry( s->vReasons, v ) );
        int * Lits = &( c->pData[0].Lit );

        assert( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
        if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
        {
            assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
            ABC_SWAP( int, Lits[0], Lits[1] );
        }

        for ( i = 1; i < c->nSize; i++ )
        {
            int v = xSAT_Lit2Var( Lits[i] );
            if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) )
            {
                if ( ( unsigned ) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ( ( 1 << (Vec_IntEntry( s->vLevels, v ) & 31 ) ) & MinLevel ) )
                {
                    Vec_IntPush( s->vStack, v );
                    Vec_IntPush( s->vTagged, Lits[i] );
                    Vec_StrWriteEntry( s->vSeen, v, 1 );
                }
                else
                {
                    int Lit;
                    Vec_IntForEachEntryStart( s->vTagged, Lit, i, top )
                        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
                    Vec_IntShrink( s->vTagged, top );
                    return 0;
                }
            }
        }
    }
    return 1;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
{
    int * pLits = Vec_IntArray( vLits );
    int MinLevel = 0;
    int i, j;

    for ( i = 1; i < Vec_IntSize( vLits ); i++ )
    {
        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pLits[i] ) );
        MinLevel |= 1 << ( Level & 31 );
    }

    /* Remove reduntant literals */
    Vec_IntAppend( s->vTagged, vLits );
    for ( i = j = 1; i < Vec_IntSize( vLits ); i++ )
        if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
            pLits[j++] = pLits[i];
    Vec_IntShrink( vLits, j );

    /* Binary Resolution */
    if( Vec_IntSize( vLits ) <= 30 && xSAT_SolverClaCalcLBD2( s, vLits ) <= 6 )
    {
        int nb, l;
        int Lit;
        int FlaseLit = xSAT_NegLit( pLits[0] );
        xSAT_WatchList_t * ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
        xSAT_Watcher_t * begin = xSAT_WatchListArray( ws );
        xSAT_Watcher_t * end   = begin + xSAT_WatchListSize( ws );
        xSAT_Watcher_t * pWatcher;

        s->nStamp++;
        Vec_IntForEachEntry( vLits, Lit, i )
            Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), ( int ) s->nStamp );

        nb = 0;
        for ( pWatcher = begin; pWatcher < end; pWatcher++ )
        {
            int ImpLit = pWatcher->Blocker;

            if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
            {
                nb++;
                Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), ( int )( s->nStamp - 1 ) );
            }
        }

        l = Vec_IntSize( vLits ) - 1;
        if ( nb > 0 )
        {
            for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ )
                if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp )
                {
                    int TempLit = pLits[l];
                    pLits[l] = pLits[i];
                    pLits[i] = TempLit;
                    i--; l--;
                }

            Vec_IntShrink( vLits, Vec_IntSize( vLits ) - nb );
        }
    }
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static void xSAT_SolverAnalyze( xSAT_Solver_t* s, unsigned ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD )
{
    int * trail = Vec_IntArray( s->vTrail );
    int Count   = 0;
    int p       = LitUndef;
    int Idx     = Vec_IntSize( s->vTrail ) - 1;
    int * Lits;
    int Lit;
    int i, j;

    Vec_IntPush( vLearnt, LitUndef );
    do
    {
        xSAT_Clause_t * pCla;

        assert( ConfCRef != CRefUndef );
        pCla = xSAT_SolverReadClause(s, ConfCRef);
        Lits = &( pCla->pData[0].Lit );

        if( p != LitUndef && pCla->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
        {
            assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
            ABC_SWAP( int, Lits[0], Lits[1] );
        }

        if ( pCla->fLearnt )
            xSAT_SolverClaActBump( s, pCla );

        if ( pCla->fLearnt && pCla->nLBD > 2 )
        {
            unsigned int nLevels = xSAT_SolverClaCalcLBD( s, pCla );
            if ( nLevels + 1 < pCla->nLBD )
            {
                if ( pCla->nLBD <= s->Config.nLBDFrozenClause )
                    pCla->fCanBeDel = 0;
                pCla->nLBD = nLevels;
            }
        }

        for ( j = ( p == LitUndef ? 0 : 1 ); j < pCla->nSize; j++ )
        {
            int Var = xSAT_Lit2Var( Lits[j] );

            if ( Vec_StrEntry( s->vSeen, Var ) == 0 && Vec_IntEntry( s->vLevels, Var ) > 0 )
            {
                Vec_StrWriteEntry( s->vSeen, Var, 1 );
                xSAT_SolverVarActBump( s, Var );
                if ( Vec_IntEntry( s->vLevels, Var ) >= xSAT_SolverDecisionLevel( s ) )
                {
                    Count++;
                    if (  Vec_IntEntry( s->vReasons, Var ) != CRefUndef && xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->fLearnt )
                        Vec_IntPush( s->vLastDLevel, Var );
                }
                else
                    Vec_IntPush( vLearnt, Lits[j] );
            }
        }

        while ( !Vec_StrEntry( s->vSeen, xSAT_Lit2Var( trail[Idx--] ) ) );

        // Next clause to look at
        p = trail[Idx+1];
        ConfCRef = ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( p ), 0 );
        Count--;

    } while ( Count > 0 );

    Vec_IntArray( vLearnt )[0] = xSAT_NegLit( p );
    xSAT_SolverClaMinimisation( s, vLearnt );

    // Find the backtrack level
    Lits = Vec_IntArray( vLearnt );
    if ( Vec_IntSize( vLearnt ) == 1 )
        *OutBtLevel = 0;
    else
    {
        int iMax = 1;
        int Max   = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) );
        int Tmp;

        for (i = 2; i < Vec_IntSize( vLearnt ); i++)
            if ( Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) ) > Max)
            {
                Max   = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) );
                iMax = i;
            }

        Tmp         = Lits[1];
        Lits[1]     = Lits[iMax];
        Lits[iMax]  = Tmp;
        *OutBtLevel = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) );
    }

    *nLBD = xSAT_SolverClaCalcLBD2( s, vLearnt );
    if ( Vec_IntSize( s->vLastDLevel ) > 0 )
    {
        int Var;
        Vec_IntForEachEntry( s->vLastDLevel, Var, i )
        {
            if ( xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->nLBD < *nLBD )
                xSAT_SolverVarActBump( s, Var );
        }

        Vec_IntClear( s->vLastDLevel );
    }

    Vec_IntForEachEntry( s->vTagged, Lit, i )
        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
    Vec_IntClear( s->vTagged );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
{
    unsigned hConfl = CRefUndef;
    int * Lits;
    int NegLit;
    int nProp = 0;

    while ( s->iQhead < Vec_IntSize( s->vTrail ) )
    {
        int p = Vec_IntEntry( s->vTrail, s->iQhead++ );
        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p );
        xSAT_Watcher_t* begin = xSAT_WatchListArray( ws );
        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize( ws );
        xSAT_Watcher_t *i, *j;

        nProp++;
        for ( i = begin; i < end; i++ )
        {
            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
                xSAT_SolverEnqueue( s, i->Blocker, i->CRef );
            else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) )
                return i->CRef;
        }

        ws    = xSAT_VecWatchListEntry( s->vWatches, p );
        begin = xSAT_WatchListArray( ws );
        end   = begin + xSAT_WatchListSize( ws );

        for ( i = j = begin; i < end; )
        {
            xSAT_Clause_t * pCla;
            xSAT_Watcher_t w;
            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
            {
                *j++ = *i++;
                continue;
            }

            pCla = xSAT_SolverReadClause( s, i->CRef );
            Lits = &( pCla->pData[0].Lit );

            // Make sure the false literal is data[1]:
            NegLit = xSAT_NegLit( p );
            if ( Lits[0] == NegLit )
            {
                Lits[0] = Lits[1];
                Lits[1] = NegLit;
            }
            assert( Lits[1] == NegLit );

            w.CRef = i->CRef;
            w.Blocker = Lits[0];

            // If 0th watch is true, then clause is already satisfied.
            if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) )
                *j++ = w;
            else
            {
                // Look for new watch:
                int * stop = Lits + pCla->nSize;
                int * k;
                for ( k = Lits + 2; k < stop; k++ )
                {
                    if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) )
                    {
                        Lits[1] = *k;
                        *k = NegLit;
                        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( Lits[1] ) ), w );
                        goto next;
                    }
                }

                *j++ = w;

                // Clause is unit under assignment:
                if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
                {
                    hConfl = i->CRef;
                    i++;
                    s->iQhead = Vec_IntSize( s->vTrail );
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
                else
                    xSAT_SolverEnqueue( s, Lits[0], i->CRef );
            }
        next:
            i++;
        }

        s->Stats.nInspects += j - xSAT_WatchListArray( ws );
        xSAT_WatchListShrink( ws, j - xSAT_WatchListArray( ws ) );
    }

    s->Stats.nPropagations += nProp;
    s->nPropSimplify -= nProp;

    return hConfl;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverReduceDB( xSAT_Solver_t * s )
{
    static abctime TimeTotal = 0;
    abctime clk = Abc_Clock();
    int nLearnedOld = Vec_IntSize( s->vLearnts );
    int i, limit;
    unsigned CRef;
    xSAT_Clause_t * pCla;
    xSAT_Clause_t ** learnts_cls;

    learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld );
    Vec_IntForEachEntry( s->vLearnts, CRef, i )
        learnts_cls[i] = xSAT_SolverReadClause(s, CRef);

    limit = nLearnedOld / 2;

    xSAT_UtilSort((void **) learnts_cls, nLearnedOld,
                  (int (*)( const void *, const void * )) xSAT_ClauseCompare);

    if ( learnts_cls[nLearnedOld / 2]->nLBD <= 3 )
        s->nRC2 += s->Config.nSpecialIncReduce;
    if ( learnts_cls[nLearnedOld - 1]->nLBD <= 5 )
        s->nRC2 += s->Config.nSpecialIncReduce;

    Vec_IntClear( s->vLearnts );
    for ( i = 0; i < nLearnedOld; i++ )
    {
        unsigned CRef;

        pCla = learnts_cls[i];
        CRef = xSAT_MemCRef( s->pMemory, ( unsigned * ) pCla );
        assert( pCla->fMark == 0 );
        if ( pCla->fCanBeDel && pCla->nLBD > 2 && pCla->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pCla->pData[0].Lit ) ) != CRef && ( i < limit ) )
        {
            pCla->fMark = 1;
            s->Stats.nLearntLits -= pCla->nSize;
            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), CRef );
            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), CRef );
        }
        else
        {
            if ( !pCla->fCanBeDel )
                limit++;
            pCla->fCanBeDel = 1;
            Vec_IntPush( s->vLearnts, CRef );
        }
    }
    ABC_FREE( learnts_cls );

    TimeTotal += Abc_Clock() - clk;
    if ( s->Config.fVerbose )
    {
        Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
            Vec_IntSize( s->vLearnts ), nLearnedOld, 100.0 * Vec_IntSize( s->vLearnts ) / nLearnedOld );
        Abc_PrintTime( 1, "Time", TimeTotal );
    }
    xSAT_SolverGarbageCollect(s);
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
char xSAT_SolverSearch( xSAT_Solver_t * s )
{
    iword conflictC  = 0;

    s->Stats.nStarts++;
    for (;;)
    {
        unsigned hConfl = xSAT_SolverPropagate( s );

        if ( hConfl != CRefUndef )
        {
            /* Conflict */
            int BacktrackLevel;
            unsigned nLBD;
            unsigned CRef;

            s->Stats.nConflicts++;
            conflictC++;

            if ( xSAT_SolverDecisionLevel( s ) == 0 )
                return LBoolFalse;

            xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) );
            if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * ( iword ) xSAT_BQueueAvg( s->bqTrail ) ) ) )
                xSAT_BQueueClean(s->bqLBD);

            Vec_IntClear( s->vLearntClause );
            xSAT_SolverAnalyze( s, hConfl, s->vLearntClause, &BacktrackLevel, &nLBD );

            s->nSumLBD += nLBD;
            xSAT_BQueuePush( s->bqLBD, nLBD );
            xSAT_SolverCancelUntil( s, BacktrackLevel );

            CRef = Vec_IntSize( s->vLearntClause ) == 1 ? CRefUndef : xSAT_SolverClaNew( s, s->vLearntClause , 1 );
            xSAT_SolverEnqueue( s, Vec_IntEntry( s->vLearntClause , 0 ), CRef );

            xSAT_SolverVarActDecay( s );
            xSAT_SolverClaActDecay( s );
        }
        else
        {
            /* No conflict */
            int NextVar;
            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( ( iword )xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
            {
                xSAT_BQueueClean( s->bqLBD );
                xSAT_SolverCancelUntil( s, 0 );
                return LBoolUndef;
            }

            // Simplify the set of problem clauses:
            if ( xSAT_SolverDecisionLevel( s ) == 0 )
                xSAT_SolverSimplify( s );

            // Reduce the set of learnt clauses:
            if ( s->Stats.nConflicts >= s->nConfBeforeReduce )
            {
                s->nRC1 = ( s->Stats.nConflicts / s->nRC2 ) + 1;
                xSAT_SolverReduceDB(s);
                s->nRC2 += s->Config.nIncReduce;
                s->nConfBeforeReduce = s->nRC1 * s->nRC2;
            }

            // New variable decision:
            NextVar = xSAT_SolverDecide( s );

            if ( NextVar == VarUndef )
                return LBoolTrue;

            xSAT_SolverNewDecision( s, xSAT_Var2Lit( NextVar, ( int ) Vec_StrEntry( s->vPolarity, NextVar ) ) );
        }
    }

    return LBoolUndef; // cannot happen
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, unsigned * pCRef )
{
    unsigned nNewCRef;
    xSAT_Clause_t * pNewCla;
    xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );

    if ( pOldCla->fReallocd )
    {
        *pCRef = ( unsigned ) pOldCla->nSize;
        return;
    }
    nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
    pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
    memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
    pOldCla->fReallocd = 1;
    pOldCla->nSize = ( unsigned ) nNewCRef;
    *pCRef = nNewCRef;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
{
    int i;
    unsigned * pArray;
    xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc(  xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) );

    for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ )
    {
        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vWatches, i);
        xSAT_Watcher_t* begin = xSAT_WatchListArray(ws);
        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize(ws);
        xSAT_Watcher_t *w;

        for ( w = begin; w != end; w++ )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );

        ws = xSAT_VecWatchListEntry( s->vBinWatches, i);
        begin = xSAT_WatchListArray(ws);
        end   = begin + xSAT_WatchListSize(ws);
        for ( w = begin; w != end; w++ )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );
    }

    for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
        if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, ( unsigned * ) &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );

    pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
    for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );

    pArray = ( unsigned * ) Vec_IntArray( s->vClauses );
    for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ )
        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );

    xSAT_MemFree( s->pMemory );
    s->pMemory = pNewMemMngr;
}

ABC_NAMESPACE_IMPL_END