msatQueue.c File Reference

#include "msatInt.h"

Go to the source code of this file.

Data Structures
struct	Msat_Queue_t_
	DECLARATIONS ///. More...

Functions
Msat_Queue_t *	Msat_QueueAlloc (int nVars)
	FUNCTION DEFINITIONS ///. More...
void	Msat_QueueFree (Msat_Queue_t *p)
int	Msat_QueueReadSize (Msat_Queue_t *p)
void	Msat_QueueInsert (Msat_Queue_t *p, int Lit)
int	Msat_QueueExtract (Msat_Queue_t *p)
void	Msat_QueueClear (Msat_Queue_t *p)

Function Documentation

Msat_Queue_t* Msat_QueueAlloc

(

int

nVars

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Allocates the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file msatQueue.c.

{
    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;
}

void Msat_QueueClear

(

Msat_Queue_t *

p

)

Function*************************************************************

Synopsis [Resets the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file msatQueue.c.

{
    p->iFirst = 0;
    p->iLast  = 0;
}

int Msat_QueueExtract

(

Msat_Queue_t *

p

)

Function*************************************************************

Synopsis [Extracts an entry from the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file msatQueue.c.

{
    if ( p->iFirst == p->iLast )
        return -1;
    return p->pVars[p->iFirst++];
}

void Msat_QueueFree

(

Msat_Queue_t *

p

)

Function*************************************************************

Synopsis [Deallocate the variable propagation queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file msatQueue.c.

{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
}

void Msat_QueueInsert	(	Msat_Queue_t *	p,
		int	Lit
	)

Function*************************************************************

Synopsis [Insert an entry into the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file msatQueue.c.

{
    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;
}

int Msat_QueueReadSize

(

Msat_Queue_t *

p

)

Function*************************************************************

Synopsis [Reads the queue size.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file msatQueue.c.

{
    return p->iLast - p->iFirst;
}