src/Backend/cnfexpr.c

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