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 void clearLitVector(LitVector *This) {
  21         This->size=0;
  22 }
  23
  24 void freeLitVector(LitVector *This) {
  25         ourfree(This->literals);
  26 }
  27
  28 void deleteLitVector(LitVector *This) {
  29         freeLitVector(This);
  30         ourfree(This);
  31 }
  32
  33 Literal getLiteralLitVector(LitVector *This, uint index) {
  34         return This->literals[index];
  35 }
  36
  37 void addLiteralLitVector(LitVector *This, Literal l) {
  38         Literal labs = abs(l);
  39         uint vec_size=This->size;
  40         uint searchsize=boundedSize(vec_size);
  41         uint i=0;
  42         for (; i < searchsize; i++) {
  43                 Literal curr = This->literals[i];
  44                 Literal currabs = abs(curr);
  45                 if (currabs > labs)
  46                         break;
  47                 if (currabs == labs) {
  48                         if (curr == -l)
  49                                 This->size = 0; //either true or false now depending on whether this is a conj or disj
  50                         return;
  51                 }
  52                 if ((++This->size) >= This->capacity) {
  53                         This->capacity <<= 1;
  54                         This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
  55                 }
  56
  57                 if (vec_size < MERGESIZE) {
  58                         memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
  59                         This->literals[i]=l;
  60                 } else {
  61                         This->literals[vec_size]=l;
  62                 }
  63         }
  64 }
  65
  66 CNFExpr * allocCNFExprBool(bool isTrue) {
  67         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  68         This->litSize=0;
  69         This->isTrue=isTrue;
  70         allocInlineVectorLitVector(&This->clauses, 2);
  71         initLitVector(&This->singletons);
  72         return This;
  73 }
  74
  75 CNFExpr * allocCNFExprLiteral(Literal l) {
  76         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  77         This->litSize=1;
  78         This->isTrue=false;
  79         allocInlineVectorLitVector(&This->clauses, 2);
  80         initLitVector(&This->singletons);
  81         addLiteralLitVector(&This->singletons, l);
  82         return This;
  83 }
  84
  85 void clearCNFExpr(CNFExpr *This, bool isTrue) {
  86         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
  87                 deleteLitVector(getVectorLitVector(&This->clauses, i));
  88         }
  89         clearVectorLitVector(&This->clauses);
  90         clearLitVector(&This->singletons);
  91         This->litSize=0;
  92         This->isTrue=isTrue;
  93 }
  94
  95 void deleteCNFExpr(CNFExpr *This) {
  96         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
  97                 deleteLitVector(getVectorLitVector(&This->clauses, i));
  98         }
  99         deleteVectorArrayLitVector(&This->clauses);
 100         freeLitVector(&This->singletons);
 101         ourfree(This);
 102 }
 103
 104 void conjoinCNFLit(CNFExpr *This, Literal l) {
 105         if (This->litSize==0 && !This->isTrue) //Handle False
 106                 return;
 107
 108         This->litSize-=getSizeLitVector(&This->singletons);
 109         addLiteralLitVector(&This->singletons, l);
 110         uint newsize=getSizeLitVector(&This->singletons);
 111         if (newsize==0)
 112                 clearCNF(This, false); //We found a conflict
 113         else
 114                 This->litSize+=getSizeLitVector(&This->singletons);
 115 }
 116
 117 void disjoinCNFLit(CNFExpr *This, Literal l) {
 118         if (This->litSize==0) {
 119                 if (!This->isTrue) {
 120                         This->litSize++;
 121                         addLiteralLitVector(&This->singletons, l);
 122                 }
 123                 return;
 124         }
 125         uint litSize=0;
 126         uint newindex=0;
 127         for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
 128                 LitVector * lv=getVectorLitVector(&This->clauses, i);
 129                 addLiteralLitVector(lv, l);
 130                 uint newSize=getSizeLitVector(lv);
 131                 if (newSize!=0) {
 132                         setVectorLitVector(&This->clauses, newindex++, lv);
 133                 } else {
 134                         deleteLitVector(lv);
 135                 }
 136                 litSize+=newSize;
 137         }
 138         setSizeVectorLitVector(&This->clauses, newindex);
 139
 140         bool hasSameSingleton=false;
 141         for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
 142                 Literal lsing=getLiteralLitVector(&This->singletons, i);
 143                 if (lsing == l) {
 144                         hasSameSingleton=true;
 145                 } else if (lsing != -l) {
 146                         //Create new LitVector with both l and lsing
 147                         LitVector *newlitvec=allocLitVector();
 148                         addLiteralLitVector(newlitvec, l);
 149                         addLiteralLitVector(newlitvec, lsing);
 150                         litSize+=2;
 151                         pushVectorLitVector(&This->clauses, newlitvec);
 152                 }
 153         }
 154         clearLitVector(&This->singletons);
 155         if (hasSameSingleton) {
 156                 addLiteralLitVector(&This->singletons, l);
 157                 litSize++;
 158         }
 159         This->litSize=litSize;
 160 }