Get rid of silly macros
[satune.git] / 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 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);
38
39 static inline uint getSizeLitVector(LitVector *This) {return This->size;}
40 static inline void setSizeLitVector(LitVector *This, uint size) {This->size = size;}
41
42 CNFExpr *allocCNFExprBool(bool isTrue);
43 CNFExpr *allocCNFExprLiteral(Literal l);
44 void deleteCNFExpr(CNFExpr *This);
45 void clearCNFExpr(CNFExpr *This, bool isTrue);
46 void printCNFExpr(CNFExpr *This);
47
48 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
49 static inline bool alwaysTrueCNF(CNFExpr *This) {return (This->litSize == 0) && This->isTrue;}
50 static inline bool alwaysFalseCNF(CNFExpr *This) {return (This->litSize == 0) && !This->isTrue;}
51 static inline uint getLitSizeCNF(CNFExpr *This) {return This->litSize;}
52 static inline uint getClauseSizeCNF(CNFExpr *This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
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);
57
58 #endif