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 freeLitVector(LitVector *This) {
  21         ourfree(This->literals);
  22 }
  23
  24 void deleteLitVector(LitVector *This) {
  25         freeLitVector(This);
  26         ourfree(This);
  27 }
  28
  29 void addLiteralLitVector(LitVector *This, Literal l) {
  30         Literal labs = abs(l);
  31         uint vec_size=This->size;
  32         uint searchsize=boundedSize(vec_size);
  33         uint i=0;
  34         for (; i < searchsize; i++) {
  35                 Literal curr = This->literals[i];
  36                 Literal currabs = abs(curr);
  37                 if (currabs > labs)
  38                         break;
  39                 if (currabs == labs) {
  40                         if (curr == -l)
  41                                 This->size = 0; //either true or false now depending on whether this is a conj or disj
  42                         return;
  43                 }
  44                 if ((++This->size) >= This->capacity) {
  45                         This->capacity <<= 1;
  46                         This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
  47                 }
  48
  49                 if (vec_size < MERGESIZE) {
  50                         memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
  51                         This->literals[i]=l;
  52                 } else {
  53                         This->literals[vec_size]=l;
  54                 }
  55         }
  56 }
  57
  58 CNFExpr * allocCNFExprBool(bool isTrue) {
  59         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  60         This->litSize=0;
  61         This->isTrue=isTrue;
  62         allocInlineVectorLitVector(&This->clauses, 2);
  63         initLitVector(&This->singletons);
  64         return This;
  65 }
  66
  67 CNFExpr * allocCNFExprLiteral(Literal l) {
  68         CNFExpr *This=ourmalloc(sizeof(CNFExpr));
  69         This->litSize=1;
  70         This->isTrue=false;
  71         allocInlineVectorLitVector(&This->clauses, 2);
  72         initLitVector(&This->singletons);
  73         addLiteralLitVector(&This->singletons, l);
  74         return This;
  75 }
  76
  77 void deleteCNFExpr(CNFExpr *This) {
  78         deleteVectorArrayLitVector(&This->clauses);
  79         freeLitVector(&This->singletons);
  80         ourfree(This);
  81 }