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 void deleteLitVector(LitVector *This);
  32 void addLiteralLitVector(LitVector *This, Literal l);
  33 Literal getLiteralLitVector(LitVector *This, uint index);
  34
  35 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
  36
  37 CNFExpr * allocCNFExprBool(bool isTrue);
  38 CNFExpr * allocCNFExprLiteral(Literal l);
  39 void deleteCNFExpr(CNFExpr *This);
  40 void clearCNFExpr(CNFExpr *This, bool isTrue);
  41
  42
  43 bool alwaysTrueCNF(CNFExpr * This);
  44 bool alwaysFalseCNF(CNFExpr * This);
  45 uint getLitSizeCNF(CNFExpr * This);
  46 void clearCNF(CNFExpr *This, bool isTrue);
  47 uint getClauseSizeCNF(CNFExpr * This);
  48 void conjoinCNFLit(CNFExpr *This, Literal l);
  49 void disjoinCNFLit(CNFExpr *This, Literal l);
  50 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
  51 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
  52
  53 #endif