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.
40 VectorImpl(LitVector, LitVector *, 4)
42 static inline uint boundedSize(uint x) { return (x > MERGESIZE) ? MERGESIZE : x; }
44 LitVector *allocLitVector() {
45 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
50 void initLitVector(LitVector *This) {
52 This->capacity = LITCAPACITY;
53 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
56 LitVector *cloneLitVector(LitVector *orig) {
57 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
58 This->size = orig->size;
59 This->capacity = orig->capacity;
60 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
61 memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
65 void clearLitVector(LitVector *This) {
69 void freeLitVector(LitVector *This) {
70 ourfree(This->literals);
73 void deleteLitVector(LitVector *This) {
78 Literal getLiteralLitVector(LitVector *This, uint index) {
79 return This->literals[index];
82 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
83 This->literals[index] = l;
86 void addLiteralLitVector(LitVector *This, Literal l) {
87 Literal labs = abs(l);
88 uint vec_size = This->size;
89 uint searchsize = boundedSize(vec_size);
91 for (; i < searchsize; i++) {
92 Literal curr = This->literals[i];
93 Literal currabs = abs(curr);
96 if (currabs == labs) {
98 This->size = 0; //either true or false now depending on whether this is a conj or disj
102 if ((++This->size) >= This->capacity) {
103 This->capacity <<= 1;
104 This->literals = (Literal *) ourrealloc(This->literals, This->capacity * sizeof(Literal));
107 if (vec_size < MERGESIZE) {
108 memmove(&This->literals[i + 1], &This->literals[i], (vec_size - i) * sizeof(Literal));
109 This->literals[i] = l;
111 This->literals[vec_size] = l;
115 CNFExpr *allocCNFExprBool(bool isTrue) {
116 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
118 This->isTrue = isTrue;
119 initVectorLitVector(&This->clauses, 2);
120 initLitVector(&This->singletons);
124 CNFExpr *allocCNFExprLiteral(Literal l) {
125 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
127 This->isTrue = false;
128 initVectorLitVector(&This->clauses, 2);
129 initLitVector(&This->singletons);
130 addLiteralLitVector(&This->singletons, l);
134 void clearCNFExpr(CNFExpr *This, bool isTrue) {
135 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
136 deleteLitVector(getVectorLitVector(&This->clauses, i));
138 clearVectorLitVector(&This->clauses);
139 clearLitVector(&This->singletons);
141 This->isTrue = isTrue;
144 void deleteCNFExpr(CNFExpr *This) {
145 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
146 deleteLitVector(getVectorLitVector(&This->clauses, i));
148 deleteVectorArrayLitVector(&This->clauses);
149 freeLitVector(&This->singletons);
153 void conjoinCNFLit(CNFExpr *This, Literal l) {
154 if (This->litSize == 0 && !This->isTrue)//Handle False
157 This->litSize -= getSizeLitVector(&This->singletons);
158 addLiteralLitVector(&This->singletons, l);
159 uint newsize = getSizeLitVector(&This->singletons);
161 clearCNFExpr(This, false);//We found a conflict
163 This->litSize += getSizeLitVector(&This->singletons);
166 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
168 ourfree(This->singletons.literals);
169 ourfree(This->clauses.array);
170 This->litSize = expr->litSize;
171 This->singletons.size = expr->singletons.size;
172 This->singletons.literals = expr->singletons.literals;
173 This->singletons.capacity = expr->singletons.capacity;
174 This->clauses.size = expr->clauses.size;
175 This->clauses.array = expr->clauses.array;
176 This->clauses.capacity = expr->clauses.capacity;
179 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
180 Literal l = getLiteralLitVector(&expr->singletons,i);
181 addLiteralLitVector(&This->singletons, l);
183 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
184 LitVector *lv = getVectorLitVector(&expr->clauses,i);
185 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
187 This->litSize = expr->litSize;
191 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
192 if (expr->litSize == 0) {
194 clearCNFExpr(This, false);
201 if (This->litSize == 0) {
203 copyCNF(This, expr, destroy);
204 } else if (destroy) {
209 uint litSize = This->litSize;
210 litSize -= getSizeLitVector(&expr->singletons);
211 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
212 Literal l = getLiteralLitVector(&expr->singletons,i);
213 addLiteralLitVector(&This->singletons, l);
214 if (getSizeLitVector(&This->singletons) == 0) {
216 clearCNFExpr(This, false);
223 litSize += getSizeLitVector(&expr->singletons);
225 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
226 LitVector *lv = getVectorLitVector(&expr->clauses,i);
227 litSize += getSizeLitVector(lv);
228 pushVectorLitVector(&This->clauses, lv);
230 clearVectorLitVector(&expr->clauses);
233 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
234 LitVector *lv = getVectorLitVector(&expr->clauses,i);
235 litSize += getSizeLitVector(lv);
236 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
239 This->litSize = litSize;
242 void disjoinCNFLit(CNFExpr *This, Literal l) {
243 if (This->litSize == 0) {
246 addLiteralLitVector(&This->singletons, l);
253 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
254 LitVector *lv = getVectorLitVector(&This->clauses, i);
255 addLiteralLitVector(lv, l);
256 uint newSize = getSizeLitVector(lv);
258 setVectorLitVector(&This->clauses, newindex++, lv);
264 setSizeVectorLitVector(&This->clauses, newindex);
266 bool hasSameSingleton = false;
267 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
268 Literal lsing = getLiteralLitVector(&This->singletons, i);
270 hasSameSingleton = true;
271 } else if (lsing != -l) {
272 //Create new LitVector with both l and lsing
273 LitVector *newlitvec = allocLitVector();
274 addLiteralLitVector(newlitvec, l);
275 addLiteralLitVector(newlitvec, lsing);
277 pushVectorLitVector(&This->clauses, newlitvec);
280 clearLitVector(&This->singletons);
281 if (hasSameSingleton) {
282 addLiteralLitVector(&This->singletons, l);
284 } else if (litSize == 0) {
285 This->isTrue = true;//we are true
287 This->litSize = litSize;
291 LitVector *mergeLitVectors(LitVector *This, LitVector *expr) {
292 uint maxsize = This->size + expr->size + MERGETHRESHOLD;
293 LitVector *merged = (LitVector *)ourmalloc(sizeof(LitVector));
294 merged->literals = (Literal *)ourmalloc(sizeof(Literal) * maxsize);
295 merged->capacity = maxsize;
296 uint thisSize = boundedSize(This->size);
297 uint exprSize = boundedSize(expr->size);
298 uint iThis = 0, iExpr = 0, iMerge = 0;
299 Literal lThis = This->literals[iThis];
300 Literal lExpr = expr->literals[iExpr];
301 Literal thisAbs = abs(lThis);
302 Literal exprAbs = abs(lExpr);
304 while (iThis < thisSize && iExpr < exprSize) {
305 if (thisAbs < exprAbs) {
306 merged->literals[iMerge++] = lThis;
307 lThis = This->literals[++iThis];
308 thisAbs = abs(lThis);
309 } else if (thisAbs > exprAbs) {
310 merged->literals[iMerge++] = lExpr;
311 lExpr = expr->literals[++iExpr];
312 exprAbs = abs(lExpr);
313 } else if (lThis == lExpr) {
314 merged->literals[iMerge++] = lExpr;
315 lExpr = expr->literals[++iExpr];
316 exprAbs = abs(lExpr);
317 lThis = This->literals[++iThis];
318 thisAbs = abs(lThis);
319 } else if (lThis == -lExpr) {
324 if (iThis < thisSize) {
325 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize - iThis) * sizeof(Literal));
326 iMerge += (thisSize - iThis);
328 if (iExpr < exprSize) {
329 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize - iExpr) * sizeof(Literal));
330 iMerge += (exprSize - iExpr);
332 merged->size = iMerge;
336 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l) {
337 LitVector *copy = cloneLitVector(This);
338 addLiteralLitVector(copy, l);
342 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
343 /** Handle the special cases */
344 if (expr->litSize == 0) {
346 clearCNFExpr(This, true);
352 } else if (This->litSize == 0) {
354 copyCNF(This, expr, destroy);
355 } else if (destroy) {
359 } else if (expr->litSize == 1) {
360 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
365 } else if (destroy && This->litSize == 1) {
366 Literal l = getLiteralLitVector(&This->singletons,0);
367 copyCNF(This, expr, true);
368 disjoinCNFLit(This, l);
372 /** Handle the full cross product */
374 uint newCapacity = getClauseSizeCNF(This) * getClauseSizeCNF(expr);
375 LitVector **mergeArray = (LitVector **)ourmalloc(newCapacity * sizeof(LitVector *));
376 uint singleIndex = 0;
377 /** First do the singleton, clause pairs */
378 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
379 Literal lThis = getLiteralLitVector(&This->singletons, i);
380 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
381 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
382 LitVector *copy = cloneLitVector(lExpr);
383 addLiteralLitVector(copy, lThis);
384 if (getSizeLitVector(copy) == 0) {
385 deleteLitVector(copy);
387 mergeArray[mergeIndex++] = copy;
392 /** Next do the clause, singleton pairs */
393 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
394 Literal lExpr = getLiteralLitVector(&expr->singletons, i);
395 for (uint j = 0; j < getSizeVectorLitVector(&This->clauses); j++) {
396 LitVector *lThis = getVectorLitVector(&This->clauses, j);
397 LitVector *copy = cloneLitVector(lThis);
398 addLiteralLitVector(copy, lExpr);
399 if (getSizeLitVector(copy) == 0) {
400 deleteLitVector(copy);
402 mergeArray[mergeIndex++] = copy;
407 /** Next do the clause, clause pairs */
408 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
409 LitVector *lThis = getVectorLitVector(&This->clauses, i);
410 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
411 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
412 LitVector *merge = mergeLitVectors(lThis, lExpr);
413 if (getSizeLitVector(merge) == 0) {
414 deleteLitVector(merge);
416 mergeArray[mergeIndex++] = merge;
419 deleteLitVector(lThis); //Done with this litVector
422 /** Finally do the singleton, singleton pairs */
423 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
424 Literal lThis = getLiteralLitVector(&This->singletons, i);
425 for (uint j = 0; j < getSizeLitVector(&expr->singletons); j++) {
426 Literal lExpr = getLiteralLitVector(&expr->singletons, j);
427 if (lThis == lExpr) {
428 //We have a singleton still in the final result
429 setLiteralLitVector(&This->singletons, singleIndex++, lThis);
430 } else if (lThis != -lExpr) {
431 LitVector *mergeLV = allocLitVector();
432 addLiteralLitVector(mergeLV, lThis);
433 addLiteralLitVector(mergeLV, lExpr);
434 mergeArray[mergeIndex++] = mergeLV;
439 ourfree(This->clauses.array);
440 setSizeLitVector(&This->singletons, singleIndex);
441 This->clauses.capacity = newCapacity;
442 This->clauses.array = mergeArray;
443 This->clauses.size = mergeIndex;
448 void printCNFExpr(CNFExpr *This) {
449 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
452 Literal l = getLiteralLitVector(&This->singletons,i);
455 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
456 LitVector *lv = getVectorLitVector(&This->clauses,i);
458 for (uint j = 0; j < getSizeLitVector(lv); j++) {
461 printf("%d", getLiteralLitVector(lv, j));