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 static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}
49 static inline bool alwaysFalseCNF(CNFExpr * This) {return (This->litSize==0) && !This->isTrue;}
50 static inline uint getLitSizeCNF(CNFExpr * This) {return This->litSize;}
51 static inline uint getClauseSizeCNF(CNFExpr * This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
52 void conjoinCNFLit(CNFExpr *This, Literal l);
53 void disjoinCNFLit(CNFExpr *This, Literal l);
54 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
55 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);