9 #define MERGETHRESHOLD 2
17 typedef struct LitVector LitVector;
19 VectorDef(LitVector, LitVector *)
24 VectorLitVector clauses;
28 typedef struct CNFExpr CNFExpr;
30 LitVector *allocLitVector();
31 void initLitVector(LitVector *This);
32 void clearLitVector(LitVector *This);
33 void freeLitVector(LitVector *This);
34 LitVector *cloneLitVector(LitVector *orig);
35 void deleteLitVector(LitVector *This);
36 void addLiteralLitVector(LitVector *This, Literal l);
37 Literal getLiteralLitVector(LitVector *This, uint index);
38 void setLiteralLitVector(LitVector *This, uint index, Literal l);
39 LitVector *mergeLitVectorLiteral(LitVector *This, Literal l);
40 LitVector *mergeLitVectors(LitVector *This, LitVector *expr);
42 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
43 static inline void setSizeLitVector(LitVector *This, uint size) {This->size = size;}
45 CNFExpr *allocCNFExprBool(bool isTrue);
46 CNFExpr *allocCNFExprLiteral(Literal l);
47 void deleteCNFExpr(CNFExpr *This);
48 void clearCNFExpr(CNFExpr *This, bool isTrue);
49 void printCNFExpr(CNFExpr *This);
51 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
52 static inline bool alwaysTrueCNF(CNFExpr *This) {return (This->litSize == 0) && This->isTrue;}
53 static inline bool alwaysFalseCNF(CNFExpr *This) {return (This->litSize == 0) && !This->isTrue;}
54 static inline uint getLitSizeCNF(CNFExpr *This) {return This->litSize;}
55 static inline uint getClauseSizeCNF(CNFExpr *This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
56 void conjoinCNFLit(CNFExpr *This, Literal l);
57 void disjoinCNFLit(CNFExpr *This, Literal l);
58 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
59 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);