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 ***********************************************************************/
Msat_QueueAlloc(int nVars)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 ***********************************************************************/
Msat_QueueFree(Msat_Queue_t * p)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 ***********************************************************************/
Msat_QueueReadSize(Msat_Queue_t * p)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 ***********************************************************************/
Msat_QueueInsert(Msat_Queue_t * p,int Lit)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 ***********************************************************************/
Msat_QueueExtract(Msat_Queue_t * p)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 ***********************************************************************/
Msat_QueueClear(Msat_Queue_t * p)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
163