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

  FileName    [xsatClause.h]

  SystemName  [ABC: Logic synthesis and verification system.]

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

  Synopsis    [Clause data type definition.]

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

  Affiliation [UC Berkeley / UFRGS]

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

  Revision    []

***********************************************************************/
#ifndef ABC__sat__xSAT__xsatClause_h
#define ABC__sat__xSAT__xsatClause_h

////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////
#include "misc/util/abc_global.h"

ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
typedef struct xSAT_Clause_t_ xSAT_Clause_t;
struct xSAT_Clause_t_
{
    unsigned fLearnt   :  1;
    unsigned fMark     :  1;
    unsigned fReallocd :  1;
    unsigned fCanBeDel :  1;
    unsigned nLBD      : 28;
    int nSize;
    union {
        int Lit;
        unsigned Act;
    } pData[0];
};

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int xSAT_ClauseCompare( const void * p1, const void * p2 )
{
    xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1;
    xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2;

    if ( pC1->nSize > 2 && pC2->nSize == 2 )
        return 1;
    if ( pC1->nSize == 2 && pC2->nSize > 2 )
        return 0;
    if ( pC1->nSize == 2 && pC2->nSize == 2 )
        return 0;

    if ( pC1->nLBD > pC2->nLBD )
        return 1;
    if ( pC1->nLBD < pC2->nLBD )
        return 0;

    return pC1->pData[pC1->nSize].Act < pC2->pData[pC2->nSize].Act;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void xSAT_ClausePrint( xSAT_Clause_t * pCla )
{
    int i;

    printf("{ ");
    for ( i = 0; i < pCla->nSize; i++ )
        printf("%d ", pCla->pData[i].Lit );
    printf("}\n");
}

ABC_NAMESPACE_HEADER_END

#endif
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////