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.size = expr->singletons.size;
173 This->singletons.literals = expr->singletons.literals;
174 This->singletons.capacity = expr->singletons.capacity;
175 This->clauses.size = expr->clauses.size;
176 This->clauses.array = expr->clauses.array;
177 This->clauses.capacity = expr->clauses.capacity;
180 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
181 Literal l = getLiteralLitVector(&expr->singletons,i);
182 addLiteralLitVector(&This->singletons, l);
184 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
185 LitVector *lv = getVectorLitVector(&expr->clauses,i);
186 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
188 This->litSize = expr->litSize;
192 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
193 if (expr->litSize == 0) {
195 clearCNFExpr(This, false);
202 if (This->litSize == 0) {
204 copyCNF(This, expr, destroy);
205 } else if (destroy) {
210 uint litSize = This->litSize;
211 litSize -= getSizeLitVector(&expr->singletons);
212 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
213 Literal l = getLiteralLitVector(&expr->singletons,i);
214 addLiteralLitVector(&This->singletons, l);
215 if (getSizeLitVector(&This->singletons) == 0) {
217 clearCNFExpr(This, false);
224 litSize += getSizeLitVector(&expr->singletons);
226 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
227 LitVector *lv = getVectorLitVector(&expr->clauses,i);
228 litSize += getSizeLitVector(lv);
229 pushVectorLitVector(&This->clauses, lv);
231 clearVectorLitVector(&expr->clauses);
234 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
235 LitVector *lv = getVectorLitVector(&expr->clauses,i);
236 litSize += getSizeLitVector(lv);
237 pushVectorLitVector(&This->clauses, cloneLitVector(lv));
240 This->litSize = litSize;
243 void disjoinCNFLit(CNFExpr *This, Literal l) {
244 if (This->litSize == 0) {
247 addLiteralLitVector(&This->singletons, l);
254 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
255 LitVector *lv = getVectorLitVector(&This->clauses, i);
256 addLiteralLitVector(lv, l);
257 uint newSize = getSizeLitVector(lv);
259 setVectorLitVector(&This->clauses, newindex++, lv);
265 setSizeVectorLitVector(&This->clauses, newindex);
267 bool hasSameSingleton = false;
268 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
269 Literal lsing = getLiteralLitVector(&This->singletons, i);
271 hasSameSingleton = true;
272 } else if (lsing != -l) {
273 //Create new LitVector with both l and lsing
274 LitVector *newlitvec = allocLitVector();
275 addLiteralLitVector(newlitvec, l);
276 addLiteralLitVector(newlitvec, lsing);
278 pushVectorLitVector(&This->clauses, newlitvec);
281 clearLitVector(&This->singletons);
282 if (hasSameSingleton) {
283 addLiteralLitVector(&This->singletons, l);
285 } else if (litSize == 0) {
286 This->isTrue = true;//we are true
288 This->litSize = litSize;
291 #define MERGETHRESHOLD 2
292 LitVector *mergeLitVectors(LitVector *This, LitVector *expr) {
293 uint maxsize = This->size + expr->size + MERGETHRESHOLD;
294 LitVector *merged = (LitVector *)ourmalloc(sizeof(LitVector));
295 merged->literals = (Literal *)ourmalloc(sizeof(Literal) * maxsize);
296 merged->capacity = maxsize;
297 uint thisSize = boundedSize(This->size);
298 uint exprSize = boundedSize(expr->size);
299 uint iThis = 0, iExpr = 0, iMerge = 0;
300 Literal lThis = This->literals[iThis];
301 Literal lExpr = expr->literals[iExpr];
302 Literal thisAbs = abs(lThis);
303 Literal exprAbs = abs(lExpr);
305 while (iThis < thisSize && iExpr < exprSize) {
306 if (thisAbs < exprAbs) {
307 merged->literals[iMerge++] = lThis;
308 lThis = This->literals[++iThis];
309 thisAbs = abs(lThis);
310 } else if (thisAbs > exprAbs) {
311 merged->literals[iMerge++] = lExpr;
312 lExpr = expr->literals[++iExpr];
313 exprAbs = abs(lExpr);
314 } else if (lThis == lExpr) {
315 merged->literals[iMerge++] = lExpr;
316 lExpr = expr->literals[++iExpr];
317 exprAbs = abs(lExpr);
318 lThis = This->literals[++iThis];
319 thisAbs = abs(lThis);
320 } else if (lThis == -lExpr) {
325 if (iThis < thisSize) {
326 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize - iThis) * sizeof(Literal));
327 iMerge += (thisSize - iThis);
329 if (iExpr < exprSize) {
330 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize - iExpr) * sizeof(Literal));
331 iMerge += (exprSize - iExpr);
333 merged->size = iMerge;
337 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l) {
338 LitVector *copy = cloneLitVector(This);
339 addLiteralLitVector(copy, l);
343 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
344 /** Handle the special cases */
345 if (expr->litSize == 0) {
347 clearCNFExpr(This, true);
353 } else if (This->litSize == 0) {
355 copyCNF(This, expr, destroy);
356 } else if (destroy) {
360 } else if (expr->litSize == 1) {
361 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
366 } else if (destroy && This->litSize == 1) {
367 Literal l = getLiteralLitVector(&This->singletons,0);
368 copyCNF(This, expr, true);
369 disjoinCNFLit(This, l);
373 /** Handle the full cross product */
375 uint newCapacity = getClauseSizeCNF(This) * getClauseSizeCNF(expr);
376 LitVector **mergeArray = (LitVector **)ourmalloc(newCapacity * sizeof(LitVector *));
377 uint singleIndex = 0;
378 /** First do the singleton, clause pairs */
379 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
380 Literal lThis = getLiteralLitVector(&This->singletons, i);
381 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
382 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
383 LitVector *copy = cloneLitVector(lExpr);
384 addLiteralLitVector(copy, lThis);
385 if (getSizeLitVector(copy) == 0) {
386 deleteLitVector(copy);
388 mergeArray[mergeIndex++] = copy;
393 /** Next do the clause, singleton pairs */
394 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
395 Literal lExpr = getLiteralLitVector(&expr->singletons, i);
396 for (uint j = 0; j < getSizeVectorLitVector(&This->clauses); j++) {
397 LitVector *lThis = getVectorLitVector(&This->clauses, j);
398 LitVector *copy = cloneLitVector(lThis);
399 addLiteralLitVector(copy, lExpr);
400 if (getSizeLitVector(copy) == 0) {
401 deleteLitVector(copy);
403 mergeArray[mergeIndex++] = copy;
408 /** Next do the clause, clause pairs */
409 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
410 LitVector *lThis = getVectorLitVector(&This->clauses, i);
411 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
412 LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
413 LitVector *merge = mergeLitVectors(lThis, lExpr);
414 if (getSizeLitVector(merge) == 0) {
415 deleteLitVector(merge);
417 mergeArray[mergeIndex++] = merge;
420 deleteLitVector(lThis);//Done with this litVector
423 /** Finally do the singleton, singleton pairs */
424 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
425 Literal lThis = getLiteralLitVector(&This->singletons, i);
426 for (uint j = 0; j < getSizeLitVector(&expr->singletons); j++) {
427 Literal lExpr = getLiteralLitVector(&expr->singletons, j);
428 if (lThis == lExpr) {
429 //We have a singleton still in the final result
430 setLiteralLitVector(&This->singletons, singleIndex++, lThis);
431 } else if (lThis != -lExpr) {
432 LitVector *mergeLV = allocLitVector();
433 addLiteralLitVector(mergeLV, lThis);
434 addLiteralLitVector(mergeLV, lExpr);
435 mergeArray[mergeIndex++] = mergeLV;
440 ourfree(This->clauses.array);
441 setSizeLitVector(&This->singletons, singleIndex);
442 This->clauses.capacity = newCapacity;
443 This->clauses.array = mergeArray;
444 This->clauses.size = mergeIndex;
449 void printCNFExpr(CNFExpr *This) {
450 for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
453 Literal l = getLiteralLitVector(&This->singletons,i);
456 for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
457 LitVector *lv = getVectorLitVector(&This->clauses,i);
459 for (uint j = 0; j < getSizeLitVector(lv); j++) {
462 printf("%d", getLiteralLitVector(lv, j));