4 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
5 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
7 Permission is hereby granted, free of charge, to any person obtaining
8 a copy of this software and associated documentation files (the
9 "Software"), to deal in the Software without restriction, including
10 without limitation the rights to use, copy, modify, merge, publish,
11 distribute, sublicense, and/or sell copies of the Software, and to
12 permit persons to whom the Software is furnished to do so, subject to
13 the following conditions:
15 The above copyright notice and this permission notice shall be
16 included in all copies or substantial portions of the Software. If
17 you download or use the software, send email to Pete Manolios
18 (pete@ccs.neu.edu) with your name, contact information, and a short
19 note describing what you want to use BAT for. For any reuse or
20 distribution, you must make clear to others the license terms of this
23 Contact Pete Manolios if you want any of these conditions waived.
25 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
26 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
27 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
28 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
29 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
30 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
31 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
41 VectorImpl(LitVector, LitVector *, 4)
43 static inline uint boundedSize(uint x) { return (x > MERGESIZE) ? MERGESIZE : x; }
45 LitVector *allocLitVector() {
46 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
51 void initLitVector(LitVector *This) {
53 This->capacity = LITCAPACITY;
54 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
57 LitVector *cloneLitVector(LitVector *orig) {
58 LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
59 This->size = orig->size;
60 This->capacity = orig->capacity;
61 This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
62 memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
66 void clearLitVector(LitVector *This) {
70 void freeLitVector(LitVector *This) {
71 ourfree(This->literals);
74 void deleteLitVector(LitVector *This) {
79 Literal getLiteralLitVector(LitVector *This, uint index) {
80 return This->literals[index];
83 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
84 This->literals[index] = l;
87 void addLiteralLitVector(LitVector *This, Literal l) {
88 Literal labs = abs(l);
89 uint vec_size = This->size;
90 uint searchsize = boundedSize(vec_size);
92 for (; i < searchsize; i++) {
93 Literal curr = This->literals[i];
94 Literal currabs = abs(curr);
97 if (currabs == labs) {
99 This->size = 0; //either true or false now depending on whether this is a conj or disj
103 if ((++This->size) >= This->capacity) {
104 This->capacity <<= 1;
105 This->literals = (Literal *) ourrealloc(This->literals, This->capacity * sizeof(Literal));
108 if (vec_size < MERGESIZE) {
109 memmove(&This->literals[i + 1], &This->literals[i], (vec_size - i) * sizeof(Literal));
110 This->literals[i] = l;
112 This->literals[vec_size] = l;
116 CNFExpr *allocCNFExprBool(bool isTrue) {
117 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
119 This->isTrue = isTrue;
120 initVectorLitVector(&This->clauses, 2);
121 initLitVector(&This->singletons);
125 CNFExpr *allocCNFExprLiteral(Literal l) {
126 CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
128 This->isTrue = false;
129 initVectorLitVector(&This->clauses, 2);
130 initLitVector(&This->singletons);
131 addLiteralLitVector(&This->singletons, l);
135 void clearCNFExpr(CNFExpr *This, bool isTrue) {
136 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
137 deleteLitVector(getVectorLitVector(&This->clauses, i));
139 clearVectorLitVector(&This->clauses);
140 clearLitVector(&This->singletons);
142 This->isTrue = isTrue;
145 void deleteCNFExpr(CNFExpr *This) {
146 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
147 deleteLitVector(getVectorLitVector(&This->clauses, i));
149 deleteVectorArrayLitVector(&This->clauses);
150 freeLitVector(&This->singletons);
154 void conjoinCNFLit(CNFExpr *This, Literal l) {
155 if (This->litSize == 0 && !This->isTrue)//Handle False
158 This->litSize -= getSizeLitVector(&This->singletons);
159 addLiteralLitVector(&This->singletons, l);
160 uint newsize = getSizeLitVector(&This->singletons);
162 clearCNFExpr(This, false);//We found a conflict
164 This->litSize += getSizeLitVector(&This->singletons);
167 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
169 ourfree(This->singletons.literals);
170 ourfree(This->clauses.array);
171 This->litSize = expr->litSize;
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;
290 #define MERGETHRESHOLD 2
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));