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 addLiteralLitVector(LitVector *This, Literal l) {
  47         Literal labs = abs(l);
  48         uint vec_size=This->size;
  49         uint searchsize=boundedSize(vec_size);
  50         uint i=0;
  51         for (; i < searchsize; i++) {
  52                 Literal curr = This->literals[i];
  53                 Literal currabs = abs(curr);
  54                 if (currabs > labs)
  55                         break;
  56                 if (currabs == labs) {
  57                         if (curr == -l)
  58                                 This->size = 0; //either true or false now depending on whether this is a conj or disj
  59                         return;
  60                 }
  61                 if ((++This->size) >= This->capacity) {
  62                         This->capacity <<= 1;
  63                         This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
  64                 }
  65
  66                 if (vec_size < MERGESIZE) {
  67                         memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
  68                         This->literals[i]=l;
  69                 } else {
  70                         This->literals[vec_size]=l;
  71                 }
  72         }
  73 }
  74
  75 CNFExpr * allocCNFExprBool(bool isTrue) {
  76         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  77         This->litSize=0;
  78         This->isTrue=isTrue;
  79         allocInlineVectorLitVector(&This->clauses, 2);
  80         initLitVector(&This->singletons);
  81         return This;
  82 }
  83
  84 CNFExpr * allocCNFExprLiteral(Literal l) {
  85         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  86         This->litSize=1;
  87         This->isTrue=false;
  88         allocInlineVectorLitVector(&This->clauses, 2);
  89         initLitVector(&This->singletons);
  90         addLiteralLitVector(&This->singletons, l);
  91         return This;
  92 }
  93
  94 void clearCNFExpr(CNFExpr *This, bool isTrue) {
  95         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
  96                 deleteLitVector(getVectorLitVector(&This->clauses, i));
  97         }
  98         clearVectorLitVector(&This->clauses);
  99         clearLitVector(&This->singletons);
 100         This->litSize=0;
 101         This->isTrue=isTrue;
 102 }
 103
 104 void deleteCNFExpr(CNFExpr *This) {
 105         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
 106                 deleteLitVector(getVectorLitVector(&This->clauses, i));
 107         }
 108         deleteVectorArrayLitVector(&This->clauses);
 109         freeLitVector(&This->singletons);
 110         ourfree(This);
 111 }
 112
 113 void conjoinCNFLit(CNFExpr *This, Literal l) {
 114         if (This->litSize==0 && !This->isTrue) //Handle False
 115                 return;
 116
 117         This->litSize-=getSizeLitVector(&This->singletons);
 118         addLiteralLitVector(&This->singletons, l);
 119         uint newsize=getSizeLitVector(&This->singletons);
 120         if (newsize==0)
 121                 clearCNF(This, false); //We found a conflict
 122         else
 123                 This->litSize+=getSizeLitVector(&This->singletons);
 124 }
 125
 126 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 127         if (destroy) {
 128                 ourfree(This->singletons.literals);
 129                 ourfree(This->clauses.array);
 130                 This->litSize=expr->litSize;
 131                 This->singletons.literals=expr->singletons.literals;
 132                 This->singletons.capacity=expr->singletons.capacity;
 133                 This->clauses.size=expr->clauses.size;
 134                 This->clauses.array=expr->clauses.array;
 135                 This->clauses.capacity=expr->clauses.capacity;
 136                 ourfree(expr);
 137         } else {
 138                 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 139                         Literal l=getLiteralLitVector(&expr->singletons,i);
 140                         addLiteralLitVector(&This->singletons, l);
 141                 }
 142                 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 143                         LitVector *lv=getVectorLitVector(&expr->clauses,i);
 144                         pushVectorLitVector(&This->clauses, cloneLitVector(lv));
 145                 }
 146                 This->litSize=expr->litSize;
 147         }
 148 }
 149
 150 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 151         if (expr->litSize==0) {
 152                 if (!This->isTrue) {
 153                         clearCNF(This, false);
 154                 }
 155                 if (destroy) {
 156                         deleteCNFExpr(expr);
 157                 }
 158                 return;
 159         }
 160         if (This->litSize==0) {
 161                 if (This->isTrue) {
 162                         copyCNF(This, expr, destroy);
 163                 } else if (destroy) {
 164                         deleteCNFExpr(expr);
 165                 }
 166                 return;
 167         }
 168         uint litSize=This->litSize;
 169         litSize-=getSizeLitVector(&expr->singletons);
 170         for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 171                 Literal l=getLiteralLitVector(&expr->singletons,i);
 172                 addLiteralLitVector(&This->singletons, l);
 173                 if (getSizeLitVector(&This->singletons)==0) {
 174                         //Found conflict...
 175                         clearCNF(This, false);
 176                         if (destroy) {
 177                                 deleteCNFExpr(expr);
 178                         }
 179                         return;
 180                 }
 181         }
 182         litSize+=getSizeLitVector(&expr->singletons);
 183         if (destroy) {
 184                 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 185                         LitVector *lv=getVectorLitVector(&expr->clauses,i);
 186                         litSize+=getSizeLitVector(lv);
 187                         pushVectorLitVector(&This->clauses, lv);
 188                 }
 189                 clearVectorLitVector(&expr->clauses);
 190                 deleteCNFExpr(expr);
 191         } else {
 192                 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 193                         LitVector *lv=getVectorLitVector(&expr->clauses,i);
 194                         litSize+=getSizeLitVector(lv);
 195                         pushVectorLitVector(&This->clauses, cloneLitVector(lv));
 196                 }
 197         }
 198         This->litSize=litSize;
 199 }
 200
 201 void disjoinCNFLit(CNFExpr *This, Literal l) {
 202         if (This->litSize==0) {
 203                 if (!This->isTrue) {
 204                         This->litSize++;
 205                         addLiteralLitVector(&This->singletons, l);
 206                 }
 207                 return;
 208         }
 209
 210         uint litSize=0;
 211         uint newindex=0;
 212         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
 213                 LitVector * lv=getVectorLitVector(&This->clauses, i);
 214                 addLiteralLitVector(lv, l);
 215                 uint newSize=getSizeLitVector(lv);
 216                 if (newSize!=0) {
 217                         setVectorLitVector(&This->clauses, newindex++, lv);
 218                 } else {
 219                         deleteLitVector(lv);
 220                 }
 221                 litSize+=newSize;
 222         }
 223         setSizeVectorLitVector(&This->clauses, newindex);
 224
 225         bool hasSameSingleton=false;
 226         for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
 227                 Literal lsing=getLiteralLitVector(&This->singletons, i);
 228                 if (lsing == l) {
 229                         hasSameSingleton=true;
 230                 } else if (lsing != -l) {
 231                         //Create new LitVector with both l and lsing
 232                         LitVector *newlitvec=allocLitVector();
 233                         addLiteralLitVector(newlitvec, l);
 234                         addLiteralLitVector(newlitvec, lsing);
 235                         litSize+=2;
 236                         pushVectorLitVector(&This->clauses, newlitvec);
 237                 }
 238         }
 239         clearLitVector(&This->singletons);
 240         if (hasSameSingleton) {
 241                 addLiteralLitVector(&This->singletons, l);
 242                 litSize++;
 243         } else if (litSize==0) {
 244                 This->isTrue=true;//we are true
 245         }
 246         This->litSize=litSize;
 247 }
 248
 249 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 250
 251 }
 252
 253
 254