/**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