14 typedef struct LitVector LitVector;
16 VectorDef(LitVector, LitVector *)
21 VectorLitVector clauses;
25 typedef struct CNFExpr CNFExpr;
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);
35 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
37 CNFExpr * allocCNFExprBool(bool isTrue);
38 CNFExpr * allocCNFExprLiteral(Literal l);
39 void deleteCNFExpr(CNFExpr *This);
40 void clearCNFExpr(CNFExpr *This, bool isTrue);
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);