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 #define LITCAPACITY 4
  40 #define MERGESIZE 5
  41
  42 VectorImpl(LitVector, LitVector *, 4)
  43
  44 static inline uint boundedSize(uint x) { return (x > MERGESIZE) ? MERGESIZE : x; }
  45
  46 LitVector *allocLitVector() {
  47         LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
  48         initLitVector(This);
  49         return This;
  50 }
  51
  52 void initLitVector(LitVector *This) {
  53         This->size = 0;
  54         This->capacity = LITCAPACITY;
  55         This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
  56 }
  57
  58 LitVector *cloneLitVector(LitVector *orig) {
  59         LitVector *This = (LitVector *)ourmalloc(sizeof(LitVector));
  60         This->size = orig->size;
  61         This->capacity = orig->capacity;
  62         This->literals = (Literal *)ourmalloc(This->capacity * sizeof(Literal));
  63         memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
  64         return This;
  65 }
  66
  67 void clearLitVector(LitVector *This) {
  68         This->size = 0;
  69 }
  70
  71 void freeLitVector(LitVector *This) {
  72         ourfree(This->literals);
  73 }
  74
  75 void deleteLitVector(LitVector *This) {
  76         freeLitVector(This);
  77         ourfree(This);
  78 }
  79
  80 Literal getLiteralLitVector(LitVector *This, uint index) {
  81         return This->literals[index];
  82 }
  83
  84 void setLiteralLitVector(LitVector *This, uint index, Literal l) {
  85         This->literals[index] = l;
  86 }
  87
  88 void addLiteralLitVector(LitVector *This, Literal l) {
  89         Literal labs = abs(l);
  90         uint vec_size = This->size;
  91         uint searchsize = boundedSize(vec_size);
  92         uint i = 0;
  93         for (; i < searchsize; i++) {
  94                 Literal curr = This->literals[i];
  95                 Literal currabs = abs(curr);
  96                 if (currabs > labs)
  97                         break;
  98                 if (currabs == labs) {
  99                         if (curr == -l)
 100                                 This->size = 0; //either true or false now depending on whether this is a conj or disj
 101                         return;
 102                 }
 103         }
 104         if ((++This->size) >= This->capacity) {
 105                 This->capacity <<= 1;
 106                 This->literals = (Literal *) ourrealloc(This->literals, This->capacity * sizeof(Literal));
 107         }
 108
 109         if (vec_size < MERGESIZE) {
 110                 memmove(&This->literals[i + 1], &This->literals[i], (vec_size - i) * sizeof(Literal));
 111                 This->literals[i] = l;
 112         } else {
 113                 This->literals[vec_size] = l;
 114         }
 115 }
 116
 117 CNFExpr *allocCNFExprBool(bool isTrue) {
 118         CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
 119         This->litSize = 0;
 120         This->isTrue = isTrue;
 121         initVectorLitVector(&This->clauses, 2);
 122         initLitVector(&This->singletons);
 123         return This;
 124 }
 125
 126 CNFExpr *allocCNFExprLiteral(Literal l) {
 127         CNFExpr *This = (CNFExpr *)ourmalloc(sizeof(CNFExpr));
 128         This->litSize = 1;
 129         This->isTrue = false;
 130         initVectorLitVector(&This->clauses, 2);
 131         initLitVector(&This->singletons);
 132         addLiteralLitVector(&This->singletons, l);
 133         return This;
 134 }
 135
 136 void clearCNFExpr(CNFExpr *This, bool isTrue) {
 137         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 138                 deleteLitVector(getVectorLitVector(&This->clauses, i));
 139         }
 140         clearVectorLitVector(&This->clauses);
 141         clearLitVector(&This->singletons);
 142         This->litSize = 0;
 143         This->isTrue = isTrue;
 144 }
 145
 146 void deleteCNFExpr(CNFExpr *This) {
 147         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 148                 deleteLitVector(getVectorLitVector(&This->clauses, i));
 149         }
 150         deleteVectorArrayLitVector(&This->clauses);
 151         freeLitVector(&This->singletons);
 152         ourfree(This);
 153 }
 154
 155 void conjoinCNFLit(CNFExpr *This, Literal l) {
 156         if (This->litSize == 0 && !This->isTrue)//Handle False
 157                 return;
 158
 159         This->litSize -= getSizeLitVector(&This->singletons);
 160         addLiteralLitVector(&This->singletons, l);
 161         uint newsize = getSizeLitVector(&This->singletons);
 162         if (newsize == 0)
 163                 clearCNFExpr(This, false);//We found a conflict
 164         else
 165                 This->litSize += getSizeLitVector(&This->singletons);
 166 }
 167
 168 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 169         if (destroy) {
 170                 ourfree(This->singletons.literals);
 171                 ourfree(This->clauses.array);
 172                 This->litSize = expr->litSize;
 173                 This->singletons.size = expr->singletons.size;
 174                 This->singletons.literals = expr->singletons.literals;
 175                 This->singletons.capacity = expr->singletons.capacity;
 176                 This->clauses.size = expr->clauses.size;
 177                 This->clauses.array = expr->clauses.array;
 178                 This->clauses.capacity = expr->clauses.capacity;
 179                 ourfree(expr);
 180         } else {
 181                 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
 182                         Literal l = getLiteralLitVector(&expr->singletons,i);
 183                         addLiteralLitVector(&This->singletons, l);
 184                 }
 185                 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
 186                         LitVector *lv = getVectorLitVector(&expr->clauses,i);
 187                         pushVectorLitVector(&This->clauses, cloneLitVector(lv));
 188                 }
 189                 This->litSize = expr->litSize;
 190         }
 191 }
 192
 193 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 194         if (expr->litSize == 0) {
 195                 if (!expr->isTrue) {
 196                         clearCNFExpr(This, false);
 197                 }
 198                 if (destroy) {
 199                         deleteCNFExpr(expr);
 200                 }
 201                 return;
 202         }
 203         if (This->litSize == 0) {
 204                 if (This->isTrue) {
 205                         copyCNF(This, expr, destroy);
 206                 } else if (destroy) {
 207                         deleteCNFExpr(expr);
 208                 }
 209                 return;
 210         }
 211         uint litSize = This->litSize;
 212         litSize -= getSizeLitVector(&expr->singletons);
 213         for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
 214                 Literal l = getLiteralLitVector(&expr->singletons,i);
 215                 addLiteralLitVector(&This->singletons, l);
 216                 if (getSizeLitVector(&This->singletons) == 0) {
 217                         //Found conflict...
 218                         clearCNFExpr(This, false);
 219                         if (destroy) {
 220                                 deleteCNFExpr(expr);
 221                         }
 222                         return;
 223                 }
 224         }
 225         litSize += getSizeLitVector(&expr->singletons);
 226         if (destroy) {
 227                 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
 228                         LitVector *lv = getVectorLitVector(&expr->clauses,i);
 229                         litSize += getSizeLitVector(lv);
 230                         pushVectorLitVector(&This->clauses, lv);
 231                 }
 232                 clearVectorLitVector(&expr->clauses);
 233                 deleteCNFExpr(expr);
 234         } else {
 235                 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
 236                         LitVector *lv = getVectorLitVector(&expr->clauses,i);
 237                         litSize += getSizeLitVector(lv);
 238                         pushVectorLitVector(&This->clauses, cloneLitVector(lv));
 239                 }
 240         }
 241         This->litSize = litSize;
 242 }
 243
 244 void disjoinCNFLit(CNFExpr *This, Literal l) {
 245         if (This->litSize == 0) {
 246                 if (!This->isTrue) {
 247                         This->litSize++;
 248                         addLiteralLitVector(&This->singletons, l);
 249                 }
 250                 return;
 251         }
 252
 253         uint litSize = 0;
 254         uint newindex = 0;
 255         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 256                 LitVector *lv = getVectorLitVector(&This->clauses, i);
 257                 addLiteralLitVector(lv, l);
 258                 uint newSize = getSizeLitVector(lv);
 259                 if (newSize != 0) {
 260                         setVectorLitVector(&This->clauses, newindex++, lv);
 261                 } else {
 262                         deleteLitVector(lv);
 263                 }
 264                 litSize += newSize;
 265         }
 266         setSizeVectorLitVector(&This->clauses, newindex);
 267
 268         bool hasSameSingleton = false;
 269         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 270                 Literal lsing = getLiteralLitVector(&This->singletons, i);
 271                 if (lsing == l) {
 272                         hasSameSingleton = true;
 273                 } else if (lsing != -l) {
 274                         //Create new LitVector with both l and lsing
 275                         LitVector *newlitvec = allocLitVector();
 276                         addLiteralLitVector(newlitvec, l);
 277                         addLiteralLitVector(newlitvec, lsing);
 278                         litSize += 2;
 279                         pushVectorLitVector(&This->clauses, newlitvec);
 280                 }
 281         }
 282         clearLitVector(&This->singletons);
 283         if (hasSameSingleton) {
 284                 addLiteralLitVector(&This->singletons, l);
 285                 litSize++;
 286         } else if (litSize == 0) {
 287                 This->isTrue = true;//we are true
 288         }
 289         This->litSize = litSize;
 290 }
 291
 292 #define MERGETHRESHOLD 2
 293 LitVector *mergeLitVectors(LitVector *This, LitVector *expr) {
 294         uint maxsize = This->size + expr->size + MERGETHRESHOLD;
 295         LitVector *merged = (LitVector *)ourmalloc(sizeof(LitVector));
 296         merged->literals = (Literal *)ourmalloc(sizeof(Literal) * maxsize);
 297         merged->capacity = maxsize;
 298         uint thisSize = boundedSize(This->size);
 299         uint exprSize = boundedSize(expr->size);
 300         uint iThis = 0, iExpr = 0, iMerge = 0;
 301         Literal lThis = This->literals[iThis];
 302         Literal lExpr = expr->literals[iExpr];
 303         Literal thisAbs = abs(lThis);
 304         Literal exprAbs = abs(lExpr);
 305
 306         while (iThis < thisSize && iExpr < exprSize) {
 307                 if (thisAbs < exprAbs) {
 308                         merged->literals[iMerge++] = lThis;
 309                         lThis = This->literals[++iThis];
 310                         thisAbs = abs(lThis);
 311                 } else if (thisAbs > exprAbs) {
 312                         merged->literals[iMerge++] = lExpr;
 313                         lExpr = expr->literals[++iExpr];
 314                         exprAbs = abs(lExpr);
 315                 } else if (lThis == lExpr) {
 316                         merged->literals[iMerge++] = lExpr;
 317                         lExpr = expr->literals[++iExpr];
 318                         exprAbs = abs(lExpr);
 319                         lThis = This->literals[++iThis];
 320                         thisAbs = abs(lThis);
 321                 } else if (lThis == -lExpr) {
 322                         merged->size = 0;
 323                         return merged;
 324                 }
 325         }
 326         if (iThis < thisSize) {
 327                 memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize - iThis) * sizeof(Literal));
 328                 iMerge += (thisSize - iThis);
 329         }
 330         if (iExpr < exprSize) {
 331                 memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize - iExpr) * sizeof(Literal));
 332                 iMerge += (exprSize - iExpr);
 333         }
 334         merged->size = iMerge;
 335         return merged;
 336 }
 337
 338 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l) {
 339         LitVector *copy = cloneLitVector(This);
 340         addLiteralLitVector(copy, l);
 341         return copy;
 342 }
 343
 344 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 345         /** Handle the special cases */
 346         if (expr->litSize == 0) {
 347                 if (expr->isTrue) {
 348                         clearCNFExpr(This, true);
 349                 }
 350                 if (destroy) {
 351                         deleteCNFExpr(expr);
 352                 }
 353                 return;
 354         } else if (This->litSize == 0) {
 355                 if (!This->isTrue) {
 356                         copyCNF(This, expr, destroy);
 357                 } else if (destroy) {
 358                         deleteCNFExpr(expr);
 359                 }
 360                 return;
 361         } else if (expr->litSize == 1) {
 362                 disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0));
 363                 if (destroy) {
 364                         deleteCNFExpr(expr);
 365                 }
 366                 return;
 367         } else if (destroy && This->litSize == 1) {
 368                 Literal l = getLiteralLitVector(&This->singletons,0);
 369                 copyCNF(This, expr, true);
 370                 disjoinCNFLit(This, l);
 371                 return;
 372         }
 373
 374         /** Handle the full cross product */
 375         uint mergeIndex = 0;
 376         uint newCapacity = getClauseSizeCNF(This) * getClauseSizeCNF(expr);
 377         LitVector **mergeArray = (LitVector **)ourmalloc(newCapacity * sizeof(LitVector *));
 378         uint singleIndex = 0;
 379         /** First do the singleton, clause pairs */
 380         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 381                 Literal lThis = getLiteralLitVector(&This->singletons, i);
 382                 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
 383                         LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
 384                         LitVector *copy = cloneLitVector(lExpr);
 385                         addLiteralLitVector(copy, lThis);
 386                         if (getSizeLitVector(copy) == 0) {
 387                                 deleteLitVector(copy);
 388                         } else {
 389                                 mergeArray[mergeIndex++] = copy;
 390                         }
 391                 }
 392         }
 393
 394         /** Next do the clause, singleton pairs */
 395         for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
 396                 Literal lExpr = getLiteralLitVector(&expr->singletons, i);
 397                 for (uint j = 0; j < getSizeVectorLitVector(&This->clauses); j++) {
 398                         LitVector *lThis = getVectorLitVector(&This->clauses, j);
 399                         LitVector *copy = cloneLitVector(lThis);
 400                         addLiteralLitVector(copy, lExpr);
 401                         if (getSizeLitVector(copy) == 0) {
 402                                 deleteLitVector(copy);
 403                         } else {
 404                                 mergeArray[mergeIndex++] = copy;
 405                         }
 406                 }
 407         }
 408
 409         /** Next do the clause, clause pairs */
 410         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 411                 LitVector *lThis = getVectorLitVector(&This->clauses, i);
 412                 for (uint j = 0; j < getSizeVectorLitVector(&expr->clauses); j++) {
 413                         LitVector *lExpr = getVectorLitVector(&expr->clauses, j);
 414                         LitVector *merge = mergeLitVectors(lThis, lExpr);
 415                         if (getSizeLitVector(merge) == 0) {
 416                                 deleteLitVector(merge);
 417                         } else {
 418                                 mergeArray[mergeIndex++] = merge;
 419                         }
 420                 }
 421                 deleteLitVector(lThis); //Done with this litVector
 422         }
 423
 424         /** Finally do the singleton, singleton pairs */
 425         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 426                 Literal lThis = getLiteralLitVector(&This->singletons, i);
 427                 for (uint j = 0; j < getSizeLitVector(&expr->singletons); j++) {
 428                         Literal lExpr = getLiteralLitVector(&expr->singletons, j);
 429                         if (lThis == lExpr) {
 430                                 //We have a singleton still in the final result
 431                                 setLiteralLitVector(&This->singletons, singleIndex++, lThis);
 432                         } else if (lThis != -lExpr) {
 433                                 LitVector *mergeLV = allocLitVector();
 434                                 addLiteralLitVector(mergeLV, lThis);
 435                                 addLiteralLitVector(mergeLV, lExpr);
 436                                 mergeArray[mergeIndex++] = mergeLV;
 437                         }
 438                 }
 439         }
 440
 441         ourfree(This->clauses.array);
 442         setSizeLitVector(&This->singletons, singleIndex);
 443         This->clauses.capacity = newCapacity;
 444         This->clauses.array = mergeArray;
 445         This->clauses.size = mergeIndex;
 446         if (destroy)
 447                 deleteCNFExpr(expr);
 448 }
 449
 450 void printCNFExpr(CNFExpr *This) {
 451         for (uint i = 0; i < getSizeLitVector(&This->singletons); i++) {
 452                 if (i != 0)
 453                         printf(" ^ ");
 454                 Literal l = getLiteralLitVector(&This->singletons,i);
 455                 printf ("%d",l);
 456         }
 457         for (uint i = 0; i < getSizeVectorLitVector(&This->clauses); i++) {
 458                 LitVector *lv = getVectorLitVector(&This->clauses,i);
 459                 printf(" ^ (");
 460                 for (uint j = 0; j < getSizeLitVector(lv); j++) {
 461                         if (j != 0)
 462                                 printf(" v ");
 463                         printf("%d", getLiteralLitVector(lv, j));
 464                 }
 465                 printf(")");
 466         }
 467 }