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 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);
39 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
40 static inline void setSizeLitVector(LitVector *This, uint size) {This->size=size;}
42 CNFExpr * allocCNFExprBool(bool isTrue);
43 CNFExpr * allocCNFExprLiteral(Literal l);
44 void deleteCNFExpr(CNFExpr *This);
45 void clearCNFExpr(CNFExpr *This, bool isTrue);
47 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
48 bool alwaysTrueCNF(CNFExpr * This);
49 bool alwaysFalseCNF(CNFExpr * This);
50 uint getLitSizeCNF(CNFExpr * This);
51 void clearCNF(CNFExpr *This, bool isTrue);
52 uint getClauseSizeCNF(CNFExpr * This);
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);