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

  FileName    [msatQueue.c]

  PackageName [A C version of SAT solver MINISAT, originally developed 
  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]

  Synopsis    [The manager of the assignment propagation queue.]

  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 1, 2004.]

  Revision    [$Id: msatQueue.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]

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

#include "msatInt.h"

ABC_NAMESPACE_IMPL_START


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

struct Msat_Queue_t_ 
{
    int         nVars;
    int *       pVars;
    int         iFirst;
    int         iLast;
};

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

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

  Synopsis    [Allocates the variable propagation queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Msat_Queue_t * Msat_QueueAlloc( int nVars )
{
    Msat_Queue_t * p;
    p = ABC_ALLOC( Msat_Queue_t, 1 );
    memset( p, 0, sizeof(Msat_Queue_t) );
    p->nVars  = nVars;
    p->pVars  = ABC_ALLOC( int, nVars );
    return p;
}

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

  Synopsis    [Deallocate the variable propagation queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Msat_QueueFree( Msat_Queue_t * p )
{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
}

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

  Synopsis    [Reads the queue size.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Msat_QueueReadSize( Msat_Queue_t * p )
{
    return p->iLast - p->iFirst;
}

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

  Synopsis    [Insert an entry into the queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Msat_QueueInsert( Msat_Queue_t * p, int Lit )
{
    if ( p->iLast == p->nVars )
    {
        int i;
        assert( 0 );
        for ( i = 0; i < p->iLast; i++ )
            printf( "entry = %2d  lit = %2d  var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
    }
    assert( p->iLast < p->nVars );
    p->pVars[p->iLast++] = Lit;
}

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

  Synopsis    [Extracts an entry from the queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Msat_QueueExtract( Msat_Queue_t * p )
{
    if ( p->iFirst == p->iLast )
        return -1;
    return p->pVars[p->iFirst++];
}

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

  Synopsis    [Resets the queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Msat_QueueClear( Msat_Queue_t * p )
{
    p->iFirst = 0;
    p->iLast  = 0;
}


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


ABC_NAMESPACE_IMPL_END