diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/msat/msatQueue.c | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/sat/msat/msatQueue.c')
-rw-r--r-- | src/sat/msat/msatQueue.c | 157 |
1 files changed, 0 insertions, 157 deletions
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c deleted file mode 100644 index 5938e042..00000000 --- a/src/sat/msat/msatQueue.c +++ /dev/null @@ -1,157 +0,0 @@ -/**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" - -//////////////////////////////////////////////////////////////////////// -/// 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 = ALLOC( Msat_Queue_t, 1 ); - memset( p, 0, sizeof(Msat_Queue_t) ); - p->nVars = nVars; - p->pVars = ALLOC( int, nVars ); - return p; -} - -/**Function************************************************************* - - Synopsis [Deallocate the variable propagation queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_QueueFree( Msat_Queue_t * p ) -{ - free( p->pVars ); - 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 /// -//////////////////////////////////////////////////////////////////////// - - |