ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
msatQueue.c
Go to the documentation of this file.
1
20
21#include "msatInt.h"
22
24
25
29
31{
32 int nVars;
33 int * pVars;
34 int iFirst;
35 int iLast;
36};
37
41
54{
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
75{
76 ABC_FREE( p->pVars );
77 ABC_FREE( p );
78}
79
92{
93 return p->iLast - p->iFirst;
94}
95
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
132{
133 if ( p->iFirst == p->iLast )
134 return -1;
135 return p->pVars[p->iFirst++];
136}
137
150{
151 p->iFirst = 0;
152 p->iLast = 0;
153}
154
155
159
160
162
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
struct Msat_Queue_t_ Msat_Queue_t
Definition msatInt.h:58
void Msat_QueueFree(Msat_Queue_t *p)
Definition msatQueue.c:74
int Msat_QueueReadSize(Msat_Queue_t *p)
Definition msatQueue.c:91
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
Definition msatQueue.c:107
void Msat_QueueClear(Msat_Queue_t *p)
Definition msatQueue.c:149
Msat_Queue_t * Msat_QueueAlloc(int nVars)
FUNCTION DEFINITIONS ///.
Definition msatQueue.c:53
int Msat_QueueExtract(Msat_Queue_t *p)
Definition msatQueue.c:131
DECLARATIONS ///.
Definition msatQueue.c:31
#define assert(ex)
Definition util_old.h:213
char * memset()