5 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
6 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
8 Permission is hereby granted, free of charge, to any person obtaining
9 a copy of this software and associated documentation files (the
10 "Software"), to deal in the Software without restriction, including
11 without limitation the rights to use, copy, modify, merge, publish,
12 distribute, sublicense, and/or sell copies of the Software, and to
13 permit persons to whom the Software is furnished to do so, subject to
14 the following conditions:
16 The above copyright notice and this permission notice shall be
17 included in all copies or substantial portions of the Software. If
18 you download or use the software, send email to Pete Manolios
19 (pete@ccs.neu.edu) with your name, contact information, and a short
20 note describing what you want to use BAT for. For any reuse or
21 distribution, you must make clear to others the license terms of this
24 Contact Pete Manolios if you want any of these conditions waived.
26 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
36 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
42 VectorImpl(LitVector, LitVector *, 4)
44 static inline uint boundedSize(uint x) { return (x > MERGESIZE) ? MERGESIZE : x; }
46 LitVector *allocLitVector() {
47 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
52 void initLitVector(LitVector *This) {
54 This->capacity = LITCAPACITY;
55 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
58 LitVector *cloneLitVector(LitVector *orig) {
59 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
60 This->size = orig->size;
61 This->capacity = orig->capacity;
62 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
63 memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
67 void clearLitVector(LitVector *This) {
71 void freeLitVector(LitVector *This) {
72 ourfree(This->literals);
75 void deleteLitVector(LitVector *This) {
80 Literal getLiteralLitVector(LitVector *This, uint index) {
81 return This->literals[index];
84 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
85 This->literals[index] = l;
88 void addLiteralLitVector(LitVector *This, Literal l) {
89 Literal labs = abs(l);
90 uint vec_size = This->size;
91 uint searchsize = boundedSize(vec_size);
93 for (; i < searchsize; i++) {
94 Literal curr = This->literals[i];
95 Literal currabs = abs(curr);
98 if (currabs == labs) {
100 This->size = 0; //either true or false now depending on whether this is a conj or disj
104 if ((++This->size) >= This->capacity) {
105 This->capacity <<= 1;
106 This->literals = (Literal *) ourrealloc(This->literals, This->capacity * sizeof(Literal));
109 if (vec_size < MERGESIZE) {
110 memmove(&This->literals[i + 1], &This->literals[i], (vec_size - i) * sizeof(Literal));
111 This->literals[i] = l;
113 This->literals[vec_size] = l;
117 CNFExpr *allocCNFExprBool(bool isTrue) {
118 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
120 This->isTrue = isTrue;
121 initVectorLitVector(&This->clauses, 2);
122 initLitVector(&This->singletons);
126 CNFExpr *allocCNFExprLiteral(Literal l) {
127 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
129 This->isTrue = false;
130 initVectorLitVector(&This->clauses, 2);
131 initLitVector(&This->singletons);
132 addLiteralLitVector(&This->singletons, l);
136 void clearCNFExpr(CNFExpr *This, bool isTrue) {
137 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
138 deleteLitVector(getVectorLitVector(&This->clauses, i));
140 clearVectorLitVector(&This->clauses);
141 clearLitVector(&This->singletons);
143 This->isTrue = isTrue;
146 void deleteCNFExpr(CNFExpr *This) {
147 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
148 deleteLitVector(getVectorLitVector(&This->clauses, i));
150 deleteVectorArrayLitVector(&This->clauses);
151 freeLitVector(&This->singletons);
155 void conjoinCNFLit(CNFExpr *This, Literal l) {
156 if (This->litSize == 0 && !This->isTrue)//Handle False
159 This->litSize -= getSizeLitVector(&This->singletons);
160 addLiteralLitVector(&This->singletons, l);
161 uint newsize = getSizeLitVector(&This->singletons);
163 clearCNFExpr(This, false);//We found a conflict
165 This->litSize += getSizeLitVector(&This->singletons);
168 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
170 ourfree(This->singletons.literals);
171 ourfree(This->clauses.array);
172 This->litSize = expr->litSize;
173 This->singletons.size = expr->singletons.size;
174 This->singletons.literals = expr->singletons.literals;
175 This->singletons.capacity = expr->singletons.capacity;
176 This->clauses.size = expr->clauses.size;
177 This->clauses.array = expr->clauses.array;
178 This->clauses.capacity = expr->clauses.capacity;
181 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
182 Literal l = getLiteralLitVector(&expr->singletons,i);
183 addLiteralLitVector(&This->singletons, l);
185 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
186 LitVector *lv = getVectorLitVector(&expr->clauses,i);
187 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
189 This->litSize = expr->litSize;
193 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
194 if (expr->litSize == 0) {
196 clearCNFExpr(This, false);
203 if (This->litSize == 0) {
205 copyCNF(This, expr, destroy);
206 } else if (destroy) {
211 uint litSize = This->litSize;
212 litSize -= getSizeLitVector(&expr->singletons);
213 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
214 Literal l = getLiteralLitVector(&expr->singletons,i);
215 addLiteralLitVector(&This->singletons, l);
216 if (getSizeLitVector(&This->singletons) == 0) {
218 clearCNFExpr(This, false);
225 litSize += getSizeLitVector(&expr->singletons);
227 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
228 LitVector *lv = getVectorLitVector(&expr->clauses,i);
229 litSize += getSizeLitVector(lv);
230 pushVectorLitVector(&This->clauses, lv);
232 clearVectorLitVector(&expr->clauses);
235 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
236 LitVector *lv = getVectorLitVector(&expr->clauses,i);
237 litSize += getSizeLitVector(lv);
238 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
241 This->litSize = litSize;
244 void disjoinCNFLit(CNFExpr *This, Literal l) {
245 if (This->litSize == 0) {
248 addLiteralLitVector(&This->singletons, l);
255 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
256 LitVector *lv = getVectorLitVector(&This->clauses, i);
257 addLiteralLitVector(lv, l);
258 uint newSize = getSizeLitVector(lv);
260 setVectorLitVector(&This->clauses, newindex++, lv);
266 setSizeVectorLitVector(&This->clauses, newindex);
268 bool hasSameSingleton = false;
269 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
270 Literal lsing = getLiteralLitVector(&This->singletons, i);
272 hasSameSingleton = true;
273 } else if (lsing != -l) {
274 //Create new LitVector with both l and lsing
275 LitVector *newlitvec = allocLitVector();
276 addLiteralLitVector(newlitvec, l);
277 addLiteralLitVector(newlitvec, lsing);
279 pushVectorLitVector(&This->clauses, newlitvec);
282 clearLitVector(&This->singletons);
283 if (hasSameSingleton) {
284 addLiteralLitVector(&This->singletons, l);
286 } else if (litSize == 0) {
287 This->isTrue = true;//we are true
289 This->litSize = litSize;
292 #define MERGETHRESHOLD 2
293 LitVector *mergeLitVectors(LitVector *This, LitVector *expr) {
294 uint maxsize = This->size + expr->size + MERGETHRESHOLD;
295 LitVector *merged = (LitVector *)ourmalloc(sizeof(LitVector));
296 merged->literals = (Literal *)ourmalloc(sizeof(Literal) * maxsize);
297 merged->capacity = maxsize;
298 uint thisSize = boundedSize(This->size);
299 uint exprSize = boundedSize(expr->size);
300 uint iThis = 0, iExpr = 0, iMerge = 0;
301 Literal lThis = This->literals[iThis];
302 Literal lExpr = expr->literals[iExpr];
303 Literal thisAbs = abs(lThis);
304 Literal exprAbs = abs(lExpr);
306 while (iThis < thisSize && iExpr < exprSize) {
307 if (thisAbs < exprAbs) {
308 merged->literals[iMerge++] = lThis;
309 lThis = This->literals[++iThis];
310 thisAbs = abs(lThis);
311 } else if (thisAbs > exprAbs) {
312 merged->literals[iMerge++] = lExpr;
313 lExpr = expr->literals[++iExpr];
314 exprAbs = abs(lExpr);
315 } else if (lThis == lExpr) {
316 merged->literals[iMerge++] = lExpr;
317 lExpr = expr->literals[++iExpr];
318 exprAbs = abs(lExpr);
319 lThis = This->literals[++iThis];
320 thisAbs = abs(lThis);
321 } else if (lThis == -lExpr) {
326 if (iThis < thisSize) {
327 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize - iThis) * sizeof(Literal));
328 iMerge += (thisSize - iThis);
330 if (iExpr < exprSize) {
331 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize - iExpr) * sizeof(Literal));
332 iMerge += (exprSize - iExpr);
334 merged->size = iMerge;
338 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l) {
339 LitVector *copy = cloneLitVector(This);
340 addLiteralLitVector(copy, l);
344 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
345 /** Handle the special cases */
346 if (expr->litSize == 0) {
348 clearCNFExpr(This, true);
354 } else if (This->litSize == 0) {
356 copyCNF(This, expr, destroy);
357 } else if (destroy) {
361 } else if (expr->litSize == 1) {
362 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
367 } else if (destroy && This->litSize == 1) {
368 Literal l = getLiteralLitVector(&This->singletons,0);
369 copyCNF(This, expr, true);
370 disjoinCNFLit(This, l);
374 /** Handle the full cross product */
376 uint newCapacity = getClauseSizeCNF(This) * getClauseSizeCNF(expr);
377 LitVector **mergeArray = (LitVector **)ourmalloc(newCapacity * sizeof(LitVector *));
378 uint singleIndex = 0;
379 /** First do the singleton, clause pairs */
380 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
381 Literal lThis = getLiteralLitVector(&This->singletons, i);
382 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
383 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
384 LitVector *copy = cloneLitVector(lExpr);
385 addLiteralLitVector(copy, lThis);
386 if (getSizeLitVector(copy) == 0) {
387 deleteLitVector(copy);
389 mergeArray[mergeIndex++] = copy;
394 /** Next do the clause, singleton pairs */
395 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
396 Literal lExpr = getLiteralLitVector(&expr->singletons, i);
397 for (uint j = 0; j < getSizeVectorLitVector(&This->clauses); j++) {
398 LitVector *lThis = getVectorLitVector(&This->clauses, j);
399 LitVector *copy = cloneLitVector(lThis);
400 addLiteralLitVector(copy, lExpr);
401 if (getSizeLitVector(copy) == 0) {
402 deleteLitVector(copy);
404 mergeArray[mergeIndex++] = copy;
409 /** Next do the clause, clause pairs */
410 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
411 LitVector *lThis = getVectorLitVector(&This->clauses, i);
412 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
413 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
414 LitVector *merge = mergeLitVectors(lThis, lExpr);
415 if (getSizeLitVector(merge) == 0) {
416 deleteLitVector(merge);
418 mergeArray[mergeIndex++] = merge;
421 deleteLitVector(lThis); //Done with this litVector
424 /** Finally do the singleton, singleton pairs */
425 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
426 Literal lThis = getLiteralLitVector(&This->singletons, i);
427 for (uint j = 0; j < getSizeLitVector(&expr->singletons); j++) {
428 Literal lExpr = getLiteralLitVector(&expr->singletons, j);
429 if (lThis == lExpr) {
430 //We have a singleton still in the final result
431 setLiteralLitVector(&This->singletons, singleIndex++, lThis);
432 } else if (lThis != -lExpr) {
433 LitVector *mergeLV = allocLitVector();
434 addLiteralLitVector(mergeLV, lThis);
435 addLiteralLitVector(mergeLV, lExpr);
436 mergeArray[mergeIndex++] = mergeLV;
441 ourfree(This->clauses.array);
442 setSizeLitVector(&This->singletons, singleIndex);
443 This->clauses.capacity = newCapacity;
444 This->clauses.array = mergeArray;
445 This->clauses.size = mergeIndex;
450 void printCNFExpr(CNFExpr *This) {
451 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
454 Literal l = getLiteralLitVector(&This->singletons,i);
457 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
458 LitVector *lv = getVectorLitVector(&This->clauses,i);
460 for (uint j = 0; j < getSizeLitVector(lv); j++) {
463 printf("%d", getLiteralLitVector(lv, j));