mirror of https://github.com/YosysHQ/abc.git
163 lines
4.0 KiB
C
163 lines
4.0 KiB
C
/**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
|
|
|