src/Backend/cnfexpr.h

   1 #ifndef CNFEXPR_H
   2 #define CNFEXPR_H
   3 #include "classlist.h"
   4 #include "vector.h"
   5
   6 typedef int Literal;
   7 #define LITCAPACITY 4
   8 #define MERGESIZE 5
   9 #define MERGETHRESHOLD 2
  10
  11
  12 struct LitVector {
  13         uint size;
  14         uint capacity;
  15         Literal *literals;
  16 };
  17 typedef struct LitVector LitVector;
  18
  19 VectorDef(LitVector, LitVector *)
  20
  21 struct CNFExpr {
  22         uint litSize;
  23         bool isTrue;
  24         VectorLitVector clauses;
  25         LitVector singletons;
  26 };
  27
  28 typedef struct CNFExpr CNFExpr;
  29
  30 LitVector *allocLitVector();
  31 void initLitVector(LitVector *This);
  32 void clearLitVector(LitVector *This);
  33 void freeLitVector(LitVector *This);
  34 LitVector *cloneLitVector(LitVector *orig);
  35 void deleteLitVector(LitVector *This);
  36 void addLiteralLitVector(LitVector *This, Literal l);
  37 Literal getLiteralLitVector(LitVector *This, uint index);
  38 void setLiteralLitVector(LitVector *This, uint index, Literal l);
  39 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l);
  40 LitVector *mergeLitVectors(LitVector *This, LitVector *expr);
  41
  42 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
  43 static inline void setSizeLitVector(LitVector *This, uint size) {This->size = size;}
  44
  45 CNFExpr *allocCNFExprBool(bool isTrue);
  46 CNFExpr *allocCNFExprLiteral(Literal l);
  47 void deleteCNFExpr(CNFExpr *This);
  48 void clearCNFExpr(CNFExpr *This, bool isTrue);
  49 void printCNFExpr(CNFExpr *This);
  50
  51 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
  52 static inline bool alwaysTrueCNF(CNFExpr *This) {return (This->litSize == 0) && This->isTrue;}
  53 static inline bool alwaysFalseCNF(CNFExpr *This) {return (This->litSize == 0) && !This->isTrue;}
  54 static inline uint getLitSizeCNF(CNFExpr *This) {return This->litSize;}
  55 static inline uint getClauseSizeCNF(CNFExpr *This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
  56 void conjoinCNFLit(CNFExpr *This, Literal l);
  57 void disjoinCNFLit(CNFExpr *This, Literal l);
  58 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
  59 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
  60
  61 #endif