src/sat/msat/msatQueue.c File Reference

#include "msatInt.h"

Include dependency graph for msatQueue.c:

Go to the source code of this file.

Data Structures
struct	Msat_Queue_t_
Functions
Msat_Queue_t *	Msat_QueueAlloc (int nVars)
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 50 of file msatQueue.c.

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

void Msat_QueueClear

(

Msat_Queue_t *

p

)

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

Synopsis [Resets the queue.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 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 128 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 71 of file msatQueue.c.

{
    free( p->pVars );
    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 104 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 88 of file msatQueue.c.

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