6 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
8 LitVector * allocLitVector() {
9 LitVector *This=ourmalloc(sizeof(LitVector));
14 void initLitVector(LitVector *This) {
16 This->capacity=LITCAPACITY;
17 This->literals=ourmalloc(This->capacity * sizeof(Literal));
20 LitVector *cloneLitVector(LitVector *orig) {
21 LitVector *This=ourmalloc(sizeof(LitVector));
22 This->size=orig->size;
23 This->capacity=orig->capacity;
24 This->literals=ourmalloc(This->capacity * sizeof(Literal));
25 memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
29 void clearLitVector(LitVector *This) {
33 void freeLitVector(LitVector *This) {
34 ourfree(This->literals);
37 void deleteLitVector(LitVector *This) {
42 Literal getLiteralLitVector(LitVector *This, uint index) {
43 return This->literals[index];
46 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
47 This->literals[index]=l;
50 void addLiteralLitVector(LitVector *This, Literal l) {
51 Literal labs = abs(l);
52 uint vec_size=This->size;
53 uint searchsize=boundedSize(vec_size);
55 for (; i < searchsize; i++) {
56 Literal curr = This->literals[i];
57 Literal currabs = abs(curr);
60 if (currabs == labs) {
62 This->size = 0; //either true or false now depending on whether this is a conj or disj
65 if ((++This->size) >= This->capacity) {
67 This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
70 if (vec_size < MERGESIZE) {
71 memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
74 This->literals[vec_size]=l;
79 CNFExpr * allocCNFExprBool(bool isTrue) {
80 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
83 allocInlineVectorLitVector(&This->clauses, 2);
84 initLitVector(&This->singletons);
88 CNFExpr * allocCNFExprLiteral(Literal l) {
89 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
92 allocInlineVectorLitVector(&This->clauses, 2);
93 initLitVector(&This->singletons);
94 addLiteralLitVector(&This->singletons, l);
98 void clearCNFExpr(CNFExpr *This, bool isTrue) {
99 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
100 deleteLitVector(getVectorLitVector(&This->clauses, i));
102 clearVectorLitVector(&This->clauses);
103 clearLitVector(&This->singletons);
108 void deleteCNFExpr(CNFExpr *This) {
109 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
110 deleteLitVector(getVectorLitVector(&This->clauses, i));
112 deleteVectorArrayLitVector(&This->clauses);
113 freeLitVector(&This->singletons);
117 void conjoinCNFLit(CNFExpr *This, Literal l) {
118 if (This->litSize==0 && !This->isTrue) //Handle False
121 This->litSize-=getSizeLitVector(&This->singletons);
122 addLiteralLitVector(&This->singletons, l);
123 uint newsize=getSizeLitVector(&This->singletons);
125 clearCNF(This, false); //We found a conflict
127 This->litSize+=getSizeLitVector(&This->singletons);
130 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
132 ourfree(This->singletons.literals);
133 ourfree(This->clauses.array);
134 This->litSize=expr->litSize;
135 This->singletons.literals=expr->singletons.literals;
136 This->singletons.capacity=expr->singletons.capacity;
137 This->clauses.size=expr->clauses.size;
138 This->clauses.array=expr->clauses.array;
139 This->clauses.capacity=expr->clauses.capacity;
142 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
143 Literal l=getLiteralLitVector(&expr->singletons,i);
144 addLiteralLitVector(&This->singletons, l);
146 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
147 LitVector *lv=getVectorLitVector(&expr->clauses,i);
148 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
150 This->litSize=expr->litSize;
154 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
155 if (expr->litSize==0) {
157 clearCNF(This, false);
164 if (This->litSize==0) {
166 copyCNF(This, expr, destroy);
167 } else if (destroy) {
172 uint litSize=This->litSize;
173 litSize-=getSizeLitVector(&expr->singletons);
174 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
175 Literal l=getLiteralLitVector(&expr->singletons,i);
176 addLiteralLitVector(&This->singletons, l);
177 if (getSizeLitVector(&This->singletons)==0) {
179 clearCNF(This, false);
186 litSize+=getSizeLitVector(&expr->singletons);
188 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
189 LitVector *lv=getVectorLitVector(&expr->clauses,i);
190 litSize+=getSizeLitVector(lv);
191 pushVectorLitVector(&This->clauses, lv);
193 clearVectorLitVector(&expr->clauses);
196 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
197 LitVector *lv=getVectorLitVector(&expr->clauses,i);
198 litSize+=getSizeLitVector(lv);
199 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
202 This->litSize=litSize;
205 void disjoinCNFLit(CNFExpr *This, Literal l) {
206 if (This->litSize==0) {
209 addLiteralLitVector(&This->singletons, l);
216 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
217 LitVector * lv=getVectorLitVector(&This->clauses, i);
218 addLiteralLitVector(lv, l);
219 uint newSize=getSizeLitVector(lv);
221 setVectorLitVector(&This->clauses, newindex++, lv);
227 setSizeVectorLitVector(&This->clauses, newindex);
229 bool hasSameSingleton=false;
230 for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
231 Literal lsing=getLiteralLitVector(&This->singletons, i);
233 hasSameSingleton=true;
234 } else if (lsing != -l) {
235 //Create new LitVector with both l and lsing
236 LitVector *newlitvec=allocLitVector();
237 addLiteralLitVector(newlitvec, l);
238 addLiteralLitVector(newlitvec, lsing);
240 pushVectorLitVector(&This->clauses, newlitvec);
243 clearLitVector(&This->singletons);
244 if (hasSameSingleton) {
245 addLiteralLitVector(&This->singletons, l);
247 } else if (litSize==0) {
248 This->isTrue=true;//we are true
250 This->litSize=litSize;
253 #define MERGETHRESHOLD 2
254 LitVector * mergeLitVectors(LitVector *This, LitVector *expr) {
255 uint maxsize=This->size+expr->size+MERGETHRESHOLD;
256 LitVector *merged=ourmalloc(sizeof(LitVector));
257 merged->literals=ourmalloc(sizeof(Literal)*maxsize);
258 merged->capacity=maxsize;
259 uint thisSize=boundedSize(This->size);
260 uint exprSize=boundedSize(expr->size);
261 uint iThis=0, iExpr=0, iMerge=0;
262 Literal lThis=This->literals[iThis];
263 Literal lExpr=expr->literals[iExpr];
264 Literal thisAbs=abs(lThis);
265 Literal exprAbs=abs(lExpr);
267 while(iThis<thisSize && iExpr<exprSize) {
268 if (thisAbs<exprAbs) {
269 merged->literals[iMerge++]=lThis;
270 lThis=This->literals[++iThis];
272 } else if(thisAbs>exprAbs) {
273 merged->literals[iMerge++]=lExpr;
274 lExpr=expr->literals[++iExpr];
276 } else if(lThis==lExpr) {
277 merged->literals[iMerge++]=lExpr;
278 lExpr=expr->literals[++iExpr];
280 lThis=This->literals[++iThis];
282 } else if(lThis==-lExpr) {
287 if (iThis < thisSize) {
288 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize-iThis) * sizeof(Literal));
289 iMerge += (thisSize-iThis);
291 if (iExpr < exprSize) {
292 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize-iExpr) * sizeof(Literal));
293 iMerge += (exprSize-iExpr);
299 LitVector * mergeLitVectorLiteral(LitVector *This, Literal l) {
300 LitVector *copy=cloneLitVector(This);
301 addLiteralLitVector(copy, l);
305 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
306 /** Handle the special cases */
307 if (expr->litSize == 0) {
309 clearCNF(This, true);
315 } else if (This->litSize == 0) {
317 copyCNF(This, expr, destroy);
318 } else if (destroy) {
322 } else if (expr->litSize == 1) {
323 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
328 } else if (destroy && This->litSize == 1) {
329 Literal l=getLiteralLitVector(&This->singletons,0);
330 copyCNF(This, expr, true);
331 disjoinCNFLit(This, l);
335 /** Handle the full cross product */
337 uint newCapacity=getClauseSizeCNF(This)*getClauseSizeCNF(expr);
338 LitVector ** mergeArray=ourmalloc(newCapacity*sizeof(LitVector*));
340 /** First do the singleton, clause pairs */
341 for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
342 Literal lThis=getLiteralLitVector(&This->singletons, i);
343 for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);j++) {
344 LitVector * lExpr=getVectorLitVector(&expr->clauses, j);
345 LitVector * copy=cloneLitVector(lExpr);
346 addLiteralLitVector(copy, lThis);
347 if (getSizeLitVector(copy)==0) {
348 deleteLitVector(copy);
350 mergeArray[mergeIndex++]=copy;
355 /** Next do the clause, singleton pairs */
356 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
357 Literal lExpr=getLiteralLitVector(&expr->singletons, i);
358 for(uint j=0;j<getSizeVectorLitVector(&This->clauses);j++) {
359 LitVector * lThis=getVectorLitVector(&This->clauses, j);
360 LitVector * copy=cloneLitVector(lThis);
361 addLiteralLitVector(copy, lExpr);
362 if (getSizeLitVector(copy)==0) {
363 deleteLitVector(copy);
365 mergeArray[mergeIndex++]=copy;
370 /** Next do the clause, clause pairs */
371 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
372 LitVector * lThis=getVectorLitVector(&This->clauses, i);
373 for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);j++) {
374 LitVector * lExpr=getVectorLitVector(&expr->clauses, j);
375 LitVector * merge=mergeLitVectors(lThis, lExpr);
376 if (getSizeLitVector(merge)==0) {
377 deleteLitVector(merge);
379 mergeArray[mergeIndex++]=merge;
382 deleteLitVector(lThis);//Done with this litVector
385 /** Finally do the singleton, singleton pairs */
386 for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
387 Literal lThis=getLiteralLitVector(&This->singletons, i);
388 for(uint j=0;j<getSizeLitVector(&expr->singletons);j++) {
389 Literal lExpr=getLiteralLitVector(&expr->singletons, j);
391 //We have a singleton still in the final result
392 setLiteralLitVector(&This->singletons, singleIndex++, lThis);
393 } else if (lThis!=-lExpr) {
394 LitVector *mergeLV=allocLitVector();
395 addLiteralLitVector(mergeLV, lThis);
396 addLiteralLitVector(mergeLV, lExpr);
397 mergeArray[mergeIndex++]=mergeLV;
402 ourfree(This->clauses.array);
403 setSizeLitVector(&This->singletons, singleIndex);
404 This->clauses.capacity=newCapacity;
405 This->clauses.array=mergeArray;
406 This->clauses.size=mergeIndex;