summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatQueue.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
commite54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch)
treede3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/msat/msatQueue.c
parent7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff)
downloadabc-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.c157
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 ///
-////////////////////////////////////////////////////////////////////////
-
-