src/Backend/cnfexpr.c

   1 #include "cnfexpr.h"
   2
   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=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=ourmalloc(This->capacity * sizeof(Literal));
  55 }
  56
  57 LitVector *cloneLitVector(LitVector *orig) {
  58         LitVector *This=ourmalloc(sizeof(LitVector));
  59         This->size=orig->size;
  60         This->capacity=orig->capacity;
  61         This->literals=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=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=ourmalloc(sizeof(CNFExpr));
 118         This->litSize=0;
 119         This->isTrue=isTrue;
 120         allocInlineVectorLitVector(&This->clauses, 2);
 121         initLitVector(&This->singletons);
 122         return This;
 123 }
 124
 125 CNFExpr * allocCNFExprLiteral(Literal l) {
 126         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
 127         This->litSize=1;
 128         This->isTrue=false;
 129         allocInlineVectorLitVector(&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.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 (!This->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 #define MERGETHRESHOLD 2
 291 LitVector * mergeLitVectors(LitVector *This, LitVector *expr) {
 292         uint maxsize=This->size+expr->size+MERGETHRESHOLD;
 293         LitVector *merged=ourmalloc(sizeof(LitVector));
 294         merged->literals=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=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
 449