abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatQueue.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatQueue.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [The manager of the assignment propagation queue.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatQueue.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 struct Msat_Queue_t_
31 {
32  int nVars;
33  int * pVars;
34  int iFirst;
35  int iLast;
36 };
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis [Allocates the variable propagation queue.]
45 
46  Description []
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 Msat_Queue_t * Msat_QueueAlloc( int nVars )
54 {
55  Msat_Queue_t * p;
56  p = ABC_ALLOC( Msat_Queue_t, 1 );
57  memset( p, 0, sizeof(Msat_Queue_t) );
58  p->nVars = nVars;
59  p->pVars = ABC_ALLOC( int, nVars );
60  return p;
61 }
62 
63 /**Function*************************************************************
64 
65  Synopsis [Deallocate the variable propagation queue.]
66 
67  Description []
68 
69  SideEffects []
70 
71  SeeAlso []
72 
73 ***********************************************************************/
74 void Msat_QueueFree( Msat_Queue_t * p )
75 {
76  ABC_FREE( p->pVars );
77  ABC_FREE( p );
78 }
79 
80 /**Function*************************************************************
81 
82  Synopsis [Reads the queue size.]
83 
84  Description []
85 
86  SideEffects []
87 
88  SeeAlso []
89 
90 ***********************************************************************/
91 int Msat_QueueReadSize( Msat_Queue_t * p )
92 {
93  return p->iLast - p->iFirst;
94 }
95 
96 /**Function*************************************************************
97 
98  Synopsis [Insert an entry into the queue.]
99 
100  Description []
101 
102  SideEffects []
103 
104  SeeAlso []
105 
106 ***********************************************************************/
107 void Msat_QueueInsert( Msat_Queue_t * p, int Lit )
108 {
109  if ( p->iLast == p->nVars )
110  {
111  int i;
112  assert( 0 );
113  for ( i = 0; i < p->iLast; i++ )
114  printf( "entry = %2d lit = %2d var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
115  }
116  assert( p->iLast < p->nVars );
117  p->pVars[p->iLast++] = Lit;
118 }
119 
120 /**Function*************************************************************
121 
122  Synopsis [Extracts an entry from the queue.]
123 
124  Description []
125 
126  SideEffects []
127 
128  SeeAlso []
129 
130 ***********************************************************************/
131 int Msat_QueueExtract( Msat_Queue_t * p )
132 {
133  if ( p->iFirst == p->iLast )
134  return -1;
135  return p->pVars[p->iFirst++];
136 }
137 
138 /**Function*************************************************************
139 
140  Synopsis [Resets the queue.]
141 
142  Description []
143 
144  SideEffects []
145 
146  SeeAlso []
147 
148 ***********************************************************************/
149 void Msat_QueueClear( Msat_Queue_t * p )
150 {
151  p->iFirst = 0;
152  p->iLast = 0;
153 }
154 
155 
156 ////////////////////////////////////////////////////////////////////////
157 /// END OF FILE ///
158 ////////////////////////////////////////////////////////////////////////
159 
160 
161 ABC_NAMESPACE_IMPL_END
162 
memset
char * memset()
Msat_QueueFree
void Msat_QueueFree(Msat_Queue_t *p)
Definition: msatQueue.c:74
Msat_QueueAlloc
Msat_Queue_t * Msat_QueueAlloc(int nVars)
FUNCTION DEFINITIONS ///.
Definition: msatQueue.c:53
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_Queue_t_::iFirst
int iFirst
Definition: msatQueue.c:34
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_Queue_t_::nVars
int nVars
Definition: msatQueue.c:32
Msat_Queue_t_::pVars
int * pVars
Definition: msatQueue.c:33
Msat_QueueReadSize
int Msat_QueueReadSize(Msat_Queue_t *p)
Definition: msatQueue.c:91
Msat_QueueInsert
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
Definition: msatQueue.c:107
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Msat_QueueExtract
int Msat_QueueExtract(Msat_Queue_t *p)
Definition: msatQueue.c:131
Msat_Queue_t_
DECLARATIONS ///.
Definition: msatQueue.c:30
Msat_QueueClear
void Msat_QueueClear(Msat_Queue_t *p)
Definition: msatQueue.c:149
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
assert
#define assert(ex)
Definition: util_old.h:213
Msat_Queue_t_::iLast
int iLast
Definition: msatQueue.c:35