msatClauseVec.c File Reference

#include "msatInt.h"

Include dependency graph for msatClauseVec.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Msat_ClauseVec_t *	Msat_ClauseVecAlloc (int nCap)
	DECLARATIONS ///.
void	Msat_ClauseVecFree (Msat_ClauseVec_t *p)
Msat_Clause_t **	Msat_ClauseVecReadArray (Msat_ClauseVec_t *p)
int	Msat_ClauseVecReadSize (Msat_ClauseVec_t *p)
void	Msat_ClauseVecGrow (Msat_ClauseVec_t *p, int nCapMin)
void	Msat_ClauseVecShrink (Msat_ClauseVec_t *p, int nSizeNew)
void	Msat_ClauseVecClear (Msat_ClauseVec_t *p)
void	Msat_ClauseVecPush (Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
Msat_Clause_t *	Msat_ClauseVecPop (Msat_ClauseVec_t *p)
void	Msat_ClauseVecWriteEntry (Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
Msat_Clause_t *	Msat_ClauseVecReadEntry (Msat_ClauseVec_t *p, int i)

Function Documentation

Msat_ClauseVecAlloc()

ABC_NAMESPACE_IMPL_START Msat_ClauseVec_t * Msat_ClauseVecAlloc

(

int

nCap

)

DECLARATIONS ///.

CFile****************************************************************

FileName [msatClauseVec.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 [Procedures working with arrays of SAT clauses.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

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

Revision [

Id

msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatClauseVec.c.

{
    Msat_ClauseVec_t * p;
    p = ABC_ALLOC( Msat_ClauseVec_t, 1 );
    if ( nCap > 0 && nCap < 16 )
        nCap = 16;
    p->nSize  = 0;
    p->nCap   = nCap;
    p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
    return p;
}

Here is the caller graph for this function:

Msat_ClauseVecClear()

void Msat_ClauseVecClear

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file msatClauseVec.c.

{
    p->nSize = 0;
}

Here is the caller graph for this function:

Msat_ClauseVecFree()

void Msat_ClauseVecFree

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file msatClauseVec.c.

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

Here is the caller graph for this function:

Msat_ClauseVecGrow()

void Msat_ClauseVecGrow	(	Msat_ClauseVec_t *	p,
		int	nCapMin )

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file msatClauseVec.c.

{
    if ( p->nCap >= nCapMin )
        return;
    p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
    p->nCap   = nCapMin;
}

Here is the caller graph for this function:

Msat_ClauseVecPop()

Msat_Clause_t * Msat_ClauseVecPop

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file msatClauseVec.c.

{
    return p->pArray[--p->nSize];
}

Here is the caller graph for this function:

Msat_ClauseVecPush()

void Msat_ClauseVecPush	(	Msat_ClauseVec_t *	p,
		Msat_Clause_t *	Entry )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 169 of file msatClauseVec.c.

{
    if ( p->nSize == p->nCap )
    {
        if ( p->nCap < 16 )
            Msat_ClauseVecGrow( p, 16 );
        else
            Msat_ClauseVecGrow( p, 2 * p->nCap );
    }
    p->pArray[p->nSize++] = Entry;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Msat_ClauseVecReadArray()

Msat_Clause_t ** Msat_ClauseVecReadArray

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file msatClauseVec.c.

{
    return p->pArray;
}

Here is the caller graph for this function:

Msat_ClauseVecReadEntry()

Msat_Clause_t * Msat_ClauseVecReadEntry	(	Msat_ClauseVec_t *	p,
		int	i )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file msatClauseVec.c.

{
    assert( i >= 0 && i < p->nSize );
    return p->pArray[i];
}

Here is the caller graph for this function:

Msat_ClauseVecReadSize()

int Msat_ClauseVecReadSize

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file msatClauseVec.c.

{
    return p->nSize;
}

Here is the caller graph for this function:

Msat_ClauseVecShrink()

void Msat_ClauseVecShrink	(	Msat_ClauseVec_t *	p,
		int	nSizeNew )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatClauseVec.c.

{
    assert( p->nSize >= nSizeNew );
    p->nSize = nSizeNew;
}

Here is the caller graph for this function:

Msat_ClauseVecWriteEntry()

void Msat_ClauseVecWriteEntry	(	Msat_ClauseVec_t *	p,
		int	i,
		Msat_Clause_t *	Entry )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file msatClauseVec.c.

{
    assert( i >= 0 && i < p->nSize );
    p->pArray[i] = Entry;
}