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