src/sat/msat/msatClauseVec.c File Reference

#include "msatInt.h"

Include dependency graph for msatClauseVec.c:

Go to the source code of this file.

Functions
Msat_ClauseVec_t *	Msat_ClauseVecAlloc (int nCap)
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_ClauseVec_t* Msat_ClauseVecAlloc

(

int

nCap

)

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 <alanmi@eecs.berkeley.edu>]

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

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

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file msatClauseVec.c.

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

void Msat_ClauseVecClear

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file msatClauseVec.c.

{
    p->nSize = 0;
}

void Msat_ClauseVecFree

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file msatClauseVec.c.

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

void Msat_ClauseVecGrow	(	Msat_ClauseVec_t *	p,
		int	nCapMin
	)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file msatClauseVec.c.

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

Msat_Clause_t* Msat_ClauseVecPop

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file msatClauseVec.c.

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

void Msat_ClauseVecPush	(	Msat_ClauseVec_t *	p,
		Msat_Clause_t *	Entry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 166 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;
}

Msat_Clause_t** Msat_ClauseVecReadArray

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file msatClauseVec.c.

{
    return p->pArray;
}

Msat_Clause_t* Msat_ClauseVecReadEntry	(	Msat_ClauseVec_t *	p,
		int	i
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file msatClauseVec.c.

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

int Msat_ClauseVecReadSize

(

Msat_ClauseVec_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file msatClauseVec.c.

{
    return p->nSize;
}

void Msat_ClauseVecShrink	(	Msat_ClauseVec_t *	p,
		int	nSizeNew
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatClauseVec.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file msatClauseVec.c.

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