src/Backend/cnfexpr.cc

   1 #include "cnfexpr.h"
   2 #include <stdio.h>
   3 /*
   4    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
   5    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
   6
   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:
  14
  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
  21    work.
  22
  23    Contact Pete Manolios if you want any of these conditions waived.
  24
  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.
  32  */
  33
  34 /*
  35    C port of CNF SAT Conversion Copyright Brian Demsky 2017.
  36  */
  37
  38 #define LITCAPACITY 4
  39 #define MERGESIZE 5
  40
  41 VectorImpl(LitVector, LitVector *, 4)
  42
  43 static inline uint boundedSize(uint x) { return (x > MERGESIZE) ? MERGESIZE : x; }
  44
  45 LitVector *allocLitVector() {
  46         LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
  47         initLitVector(This);
  48         return This;
  49 }
  50
  51 void initLitVector(LitVector *This) {
  52         This->size = 0;
  53         This->capacity = LITCAPACITY;
  54         This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
  55 }
  56
  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);
  63         return This;
  64 }
  65
  66 void clearLitVector(LitVector *This) {
  67         This->size = 0;
  68 }
  69
  70 void freeLitVector(LitVector *This) {
  71         ourfree(This->literals);
  72 }
  73
  74 void deleteLitVector(LitVector *This) {
  75         freeLitVector(This);
  76         ourfree(This);
  77 }
  78
  79 Literal getLiteralLitVector(LitVector *This, uint index) {
  80         return This->literals[index];
  81 }
  82
  83 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
  84         This->literals[index] = l;
  85 }
  86
  87 void addLiteralLitVector(LitVector *This, Literal l) {
  88         Literal labs = abs(l);
  89         uint vec_size = This->size;
  90         uint searchsize = boundedSize(vec_size);
  91         uint i = 0;
  92         for (; i < searchsize; i++) {
  93                 Literal curr = This->literals[i];
  94                 Literal currabs = abs(curr);
  95                 if (currabs > labs)
  96                         break;
  97                 if (currabs == labs) {
  98                         if (curr == -l)
  99                                 This->size = 0; //either true or false now depending on whether this is a conj or disj
 100                         return;
 101                 }
 102         }
 103         if ((++This->size) >= This->capacity) {
 104                 This->capacity <<= 1;
 105                 This->literals = (Literal *) ourrealloc(This->literals, This->capacity * sizeof(Literal));
 106         }
 107
 108         if (vec_size < MERGESIZE) {
 109                 memmove(&This->literals[i + 1], &This->literals[i], (vec_size - i) * sizeof(Literal));
 110                 This->literals[i] = l;
 111         } else {
 112                 This->literals[vec_size] = l;
 113         }
 114 }
 115
 116 CNFExpr *allocCNFExprBool(bool isTrue) {
 117         CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
 118         This->litSize = 0;
 119         This->isTrue = isTrue;
 120         initVectorLitVector(&This->clauses, 2);
 121         initLitVector(&This->singletons);
 122         return This;
 123 }
 124
 125 CNFExpr *allocCNFExprLiteral(Literal l) {
 126         CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
 127         This->litSize = 1;
 128         This->isTrue = false;
 129         initVectorLitVector(&This->clauses, 2);
 130         initLitVector(&This->singletons);
 131         addLiteralLitVector(&This->singletons, l);
 132         return This;
 133 }
 134
 135 void clearCNFExpr(CNFExpr *This, bool isTrue) {
 136         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 137                 deleteLitVector(getVectorLitVector(&This->clauses, i));
 138         }
 139         clearVectorLitVector(&This->clauses);
 140         clearLitVector(&This->singletons);
 141         This->litSize = 0;
 142         This->isTrue = isTrue;
 143 }
 144
 145 void deleteCNFExpr(CNFExpr *This) {
 146         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 147                 deleteLitVector(getVectorLitVector(&This->clauses, i));
 148         }
 149         deleteVectorArrayLitVector(&This->clauses);
 150         freeLitVector(&This->singletons);
 151         ourfree(This);
 152 }
 153
 154 void conjoinCNFLit(CNFExpr *This, Literal l) {
 155         if (This->litSize == 0 && !This->isTrue)//Handle False
 156                 return;
 157
 158         This->litSize -= getSizeLitVector(&This->singletons);
 159         addLiteralLitVector(&This->singletons, l);
 160         uint newsize = getSizeLitVector(&This->singletons);
 161         if (newsize == 0)
 162                 clearCNFExpr(This, false);//We found a conflict
 163         else
 164                 This->litSize += getSizeLitVector(&This->singletons);
 165 }
 166
 167 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 168         if (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;
 178                 ourfree(expr);
 179         } else {
 180                 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
 181                         Literal l = getLiteralLitVector(&expr->singletons,i);
 182                         addLiteralLitVector(&This->singletons, l);
 183                 }
 184                 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
 185                         LitVector *lv = getVectorLitVector(&expr->clauses,i);
 186                         pushVectorLitVector(&This->clauses, cloneLitVector(lv));
 187                 }
 188                 This->litSize = expr->litSize;
 189         }
 190 }
 191
 192 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 193         if (expr->litSize == 0) {
 194                 if (!expr->isTrue) {
 195                         clearCNFExpr(This, false);
 196                 }
 197                 if (destroy) {
 198                         deleteCNFExpr(expr);
 199                 }
 200                 return;
 201         }
 202         if (This->litSize == 0) {
 203                 if (This->isTrue) {
 204                         copyCNF(This, expr, destroy);
 205                 } else if (destroy) {
 206                         deleteCNFExpr(expr);
 207                 }
 208                 return;
 209         }
 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) {
 216                         //Found conflict...
 217                         clearCNFExpr(This, false);
 218                         if (destroy) {
 219                                 deleteCNFExpr(expr);
 220                         }
 221                         return;
 222                 }
 223         }
 224         litSize += getSizeLitVector(&expr->singletons);
 225         if (destroy) {
 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);
 230                 }
 231                 clearVectorLitVector(&expr->clauses);
 232                 deleteCNFExpr(expr);
 233         } else {
 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));
 238                 }
 239         }
 240         This->litSize = litSize;
 241 }
 242
 243 void disjoinCNFLit(CNFExpr *This, Literal l) {
 244         if (This->litSize == 0) {
 245                 if (!This->isTrue) {
 246                         This->litSize++;
 247                         addLiteralLitVector(&This->singletons, l);
 248                 }
 249                 return;
 250         }
 251
 252         uint litSize = 0;
 253         uint newindex = 0;
 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);
 258                 if (newSize != 0) {
 259                         setVectorLitVector(&This->clauses, newindex++, lv);
 260                 } else {
 261                         deleteLitVector(lv);
 262                 }
 263                 litSize += newSize;
 264         }
 265         setSizeVectorLitVector(&This->clauses, newindex);
 266
 267         bool hasSameSingleton = false;
 268         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 269                 Literal lsing = getLiteralLitVector(&This->singletons, i);
 270                 if (lsing == l) {
 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);
 277                         litSize += 2;
 278                         pushVectorLitVector(&This->clauses, newlitvec);
 279                 }
 280         }
 281         clearLitVector(&This->singletons);
 282         if (hasSameSingleton) {
 283                 addLiteralLitVector(&This->singletons, l);
 284                 litSize++;
 285         } else if (litSize == 0) {
 286                 This->isTrue = true;//we are true
 287         }
 288         This->litSize = litSize;
 289 }
 290
 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);
 304
 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) {
 321                         merged->size = 0;
 322                         return merged;
 323                 }
 324         }
 325         if (iThis < thisSize) {
 326                 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize - iThis) * sizeof(Literal));
 327                 iMerge += (thisSize - iThis);
 328         }
 329         if (iExpr < exprSize) {
 330                 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize - iExpr) * sizeof(Literal));
 331                 iMerge += (exprSize - iExpr);
 332         }
 333         merged->size = iMerge;
 334         return merged;
 335 }
 336
 337 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l) {
 338         LitVector *copy = cloneLitVector(This);
 339         addLiteralLitVector(copy, l);
 340         return copy;
 341 }
 342
 343 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 344         /** Handle the special cases */
 345         if (expr->litSize == 0) {
 346                 if (expr->isTrue) {
 347                         clearCNFExpr(This, true);
 348                 }
 349                 if (destroy) {
 350                         deleteCNFExpr(expr);
 351                 }
 352                 return;
 353         } else if (This->litSize == 0) {
 354                 if (!This->isTrue) {
 355                         copyCNF(This, expr, destroy);
 356                 } else if (destroy) {
 357                         deleteCNFExpr(expr);
 358                 }
 359                 return;
 360         } else if (expr->litSize == 1) {
 361                 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
 362                 if (destroy) {
 363                         deleteCNFExpr(expr);
 364                 }
 365                 return;
 366         } else if (destroy && This->litSize == 1) {
 367                 Literal l = getLiteralLitVector(&This->singletons,0);
 368                 copyCNF(This, expr, true);
 369                 disjoinCNFLit(This, l);
 370                 return;
 371         }
 372
 373         /** Handle the full cross product */
 374         uint mergeIndex = 0;
 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);
 387                         } else {
 388                                 mergeArray[mergeIndex++] = copy;
 389                         }
 390                 }
 391         }
 392
 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);
 402                         } else {
 403                                 mergeArray[mergeIndex++] = copy;
 404                         }
 405                 }
 406         }
 407
 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);
 416                         } else {
 417                                 mergeArray[mergeIndex++] = merge;
 418                         }
 419                 }
 420                 deleteLitVector(lThis);//Done with this litVector
 421         }
 422
 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;
 436                         }
 437                 }
 438         }
 439
 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;
 445         if (destroy)
 446                 deleteCNFExpr(expr);
 447 }
 448
 449 void printCNFExpr(CNFExpr *This) {
 450         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 451                 if (i != 0)
 452                         printf(" ^ ");
 453                 Literal l = getLiteralLitVector(&This->singletons,i);
 454                 printf ("%d",l);
 455         }
 456         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 457                 LitVector *lv = getVectorLitVector(&This->clauses,i);
 458                 printf(" ^ (");
 459                 for (uint j = 0; j < getSizeLitVector(lv); j++) {
 460                         if (j != 0)
 461                                 printf(" v ");
 462                         printf("%d", getLiteralLitVector(lv, j));
 463                 }
 464                 printf(")");
 465         }
 466 }