src/Backend/cnfexpr.cc

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