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

  FileName    [xsatSolverAPI.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 external API 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 "xsatSolver.h"

ABC_NAMESPACE_IMPL_START

xSAT_SolverOptions_t DefaultConfig =
{
    1,     //.fVerbose = 1,

    0,     //.nConfLimit = 0,
    0,     //.nInsLimit = 0,
    0,     //.nRuntimeLimit = 0,

    0.8,   //.K = 0.8,
    1.4,   //.R = 1.4,
    10000, //.nFirstBlockRestart = 10000,
    50,    //.nSizeLBDQueue = 50,
    5000,  //.nSizeTrailQueue = 5000,

    2000,  //.nConfFirstReduce = 2000,
    300,   //.nIncReduce = 300,
    1000,  //.nSpecialIncReduce = 1000,

    30     //.nLBDFrozenClause = 30
};


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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
xSAT_Solver_t* xSAT_SolverCreate()
{
    xSAT_Solver_t * s = (xSAT_Solver_t *) ABC_CALLOC( char, sizeof( xSAT_Solver_t ) );
    s->Config = DefaultConfig;

    s->pMemory = xSAT_MemAlloc(0);
    s->vClauses = Vec_IntAlloc(0);
    s->vLearnts = Vec_IntAlloc(0);
    s->vWatches = xSAT_VecWatchListAlloc( 0 );
    s->vBinWatches = xSAT_VecWatchListAlloc( 0 );

    s->vTrailLim = Vec_IntAlloc(0);
    s->vTrail = Vec_IntAlloc( 0 );

    s->vActivity = Vec_IntAlloc( 0 );
    s->hOrder = xSAT_HeapAlloc( s->vActivity );

    s->vPolarity = Vec_StrAlloc( 0 );
    s->vTags = Vec_StrAlloc( 0 );
    s->vAssigns = Vec_StrAlloc( 0 );
    s->vLevels = Vec_IntAlloc( 0 );
    s->vReasons = Vec_IntAlloc( 0 );
    s->vStamp = Vec_IntAlloc( 0 );

    s->vTagged = Vec_IntAlloc(0);
    s->vStack  = Vec_IntAlloc(0);

    s->vSeen = Vec_StrAlloc( 0 );
    s->vLearntClause = Vec_IntAlloc(0);
    s->vLastDLevel = Vec_IntAlloc(0);


    s->bqTrail = xSAT_BQueueNew( s->Config.nSizeTrailQueue );
    s->bqLBD = xSAT_BQueueNew( s->Config.nSizeLBDQueue );

    s->nVarActInc = (1 <<  5);
    s->nClaActInc = (1 << 11);

    s->nConfBeforeReduce = s->Config.nConfFirstReduce;
    s->nRC1 = 1;
    s->nRC2 = s->Config.nConfFirstReduce;
    return s;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverDestroy( xSAT_Solver_t * s )
{
    xSAT_MemFree( s->pMemory );
    Vec_IntFree( s->vClauses );
    Vec_IntFree( s->vLearnts );
    xSAT_VecWatchListFree( s->vWatches );
    xSAT_VecWatchListFree( s->vBinWatches );

    xSAT_HeapFree(s->hOrder);
    Vec_IntFree( s->vTrailLim );
    Vec_IntFree( s->vTrail );
    Vec_IntFree( s->vTagged );
    Vec_IntFree( s->vStack );

    Vec_StrFree( s->vSeen );
    Vec_IntFree( s->vLearntClause );
    Vec_IntFree( s->vLastDLevel );

    Vec_IntFree( s->vActivity );
    Vec_StrFree( s->vPolarity );
    Vec_StrFree( s->vTags );
    Vec_StrFree( s->vAssigns );
    Vec_IntFree( s->vLevels );
    Vec_IntFree( s->vReasons );
    Vec_IntFree( s->vStamp );

    xSAT_BQueueFree(s->bqLBD);
    xSAT_BQueueFree(s->bqTrail);

    ABC_FREE(s);
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int xSAT_SolverSimplify( xSAT_Solver_t * s )
{
    int i, j;
    unsigned CRef;
    assert( xSAT_SolverDecisionLevel(s) == 0 );

    if ( xSAT_SolverPropagate(s) != CRefUndef )
        return false;

    if ( s->nAssignSimplify == Vec_IntSize( s->vTrail ) || s->nPropSimplify > 0 )
        return true;

    j = 0;
    Vec_IntForEachEntry( s->vClauses, CRef, i )
    {
        xSAT_Clause_t * pCla = xSAT_SolverReadClause( s, CRef );
        if ( xSAT_SolverIsClauseSatisfied( s, pCla ) )
        {
            pCla->fMark = 1;
            s->Stats.nClauseLits -= pCla->nSize;

            if ( pCla->nSize == 2 )
            {
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef );
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef );
            }
            else
            {
                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
            Vec_IntWriteEntry( s->vClauses, j++, CRef );
    }
    Vec_IntShrink( s->vClauses, j );
    xSAT_SolverRebuildOrderHeap( s );

    s->nAssignSimplify = Vec_IntSize( s->vTrail );
    s->nPropSimplify = s->Stats.nClauseLits + s->Stats.nLearntLits;

    return true;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverAddVariable( xSAT_Solver_t* s, int Sign )
{
    int Var = Vec_IntSize( s->vActivity );

    xSAT_VecWatchListPush( s->vWatches );
    xSAT_VecWatchListPush( s->vWatches );
    xSAT_VecWatchListPush( s->vBinWatches );
    xSAT_VecWatchListPush( s->vBinWatches );

    Vec_IntPush( s->vActivity, 0 );
    Vec_IntPush( s->vLevels, 0 );
    Vec_StrPush( s->vAssigns, VarX );
    Vec_StrPush( s->vPolarity, 1 );
    Vec_StrPush( s->vTags, 0 );
    Vec_IntPush( s->vReasons, ( int ) CRefUndef );
    Vec_IntPush( s->vStamp, 0 );
    Vec_StrPush( s->vSeen, 0 );

    xSAT_HeapInsert( s->hOrder, Var );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int xSAT_SolverAddClause( xSAT_Solver_t * s, Vec_Int_t * vLits )
{
    int i, j;
    int Lit, PrevLit;
    int MaxVar;

    Vec_IntSort( vLits, 0 );
    MaxVar = xSAT_Lit2Var( Vec_IntEntryLast( vLits ) );
    while ( MaxVar >= Vec_IntSize( s->vActivity ) )
        xSAT_SolverAddVariable( s, 1 );

    j = 0;
    PrevLit = LitUndef;
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        if ( Lit == xSAT_NegLit( PrevLit ) || Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == xSAT_LitSign( Lit ) )
            return true;
        else if ( Lit != PrevLit && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX )
        {
            PrevLit = Lit;
            Vec_IntWriteEntry( vLits, j++, Lit );
        }
    }
    Vec_IntShrink( vLits, j );

    if ( Vec_IntSize( vLits ) == 0 )
        return false;
    if ( Vec_IntSize( vLits ) == 1 )
    {
        xSAT_SolverEnqueue( s, Vec_IntEntry( vLits, 0 ), CRefUndef );
        return ( xSAT_SolverPropagate( s ) == CRefUndef );
    }

    xSAT_SolverClaNew( s, vLits, 0 );
    return true;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int xSAT_SolverSolve( xSAT_Solver_t* s )
{
    char status = LBoolUndef;

    assert(s);
    if ( s->Config.fVerbose )
    {
        printf( "==========================================[ BLACK MAGIC ]================================================\n" );
        printf( "|                                |                                |                                     |\n" );
        printf( "| - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |\n" );
        printf( "|   * LBD Queue    : %6d      |   * First     : %6d         |    * size < %3d                     |\n",       s->Config.nSizeLBDQueue, s->Config.nConfFirstReduce, 0 );
        printf( "|   * Trail Queue  : %6d      |   * Inc       : %6d         |    * lbd  < %3d                     |\n",       s->Config.nSizeTrailQueue, s->Config.nIncReduce, 0 );
        printf( "|   * K            : %6.2f      |   * Special   : %6d         |                                     |\n",     s->Config.K, s->Config.nSpecialIncReduce );
        printf( "|   * R            : %6.2f      |   * Protected :  (lbd)< %2d     |                                     |\n", s->Config.R, s->Config.nLBDFrozenClause );
        printf( "|                                |                                |                                     |\n" );
        printf( "=========================================================================================================\n" );
    }

    while ( status == LBoolUndef )
        status = xSAT_SolverSearch( s );

    if ( s->Config.fVerbose )
        printf( "=========================================================================================================\n" );

    xSAT_SolverCancelUntil( s, 0 );
    return status;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void xSAT_SolverPrintStats( xSAT_Solver_t * s )
{
    printf( "starts        : %10d\n", s->Stats.nStarts );
    printf( "conflicts     : %10ld\n", s->Stats.nConflicts );
    printf( "decisions     : %10ld\n", s->Stats.nDecisions );
    printf( "propagations  : %10ld\n", s->Stats.nPropagations );
}

ABC_NAMESPACE_IMPL_END