6 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
8 LitVector * allocLitVector() {
9 LitVector *This=ourmalloc(sizeofLitVector);
14 void initLitVector(LitVector *This) {
16 This->capacity=LITCAPACITY;
17 This->literals=ourmalloc(This->capacity * sizeof(Literal));
20 void freeLitVector(LitVector *This) {
21 ourfree(This->literals);
24 void deleteLitVector(LitVector *This) {
29 void addLiteralLitVector(LitVector *This, Literal l) {
30 Literal labs = abs(l);
31 uint vec_size=This->size;
32 uint searchsize=boundedSize(vec_size);
34 for (; i < searchsize; i++) {
35 Literal curr = This->literals[i];
36 Literals currabs = abs(curr);
39 if (currabs == labs) {
41 size = 0; //either true or false now depending on whether this is a conj or disj
44 if ((++This->size) >= This->capacity) {
45 This->capacity << = 1;
46 This->literals=ourrealloc(This->capacity * sizeof(Literal));
49 if (vec_size < MERGESIZE) {
50 memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
53 This->literals[vec_size]=l;
58 CNFExpr * allocCNFExprBool(bool isTrue) {
59 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
62 allocInlineVectorLitVector(&This->clauses);
63 initLitVector(&This->singletons);
67 CNFExpr * allocCNFExprLiteral(Literal l) {
68 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
71 allocInlineVectorLitVector(&This->clauses);
72 initLitVector(&This->singletons);
73 addLiteralLitVector(This, l);
77 void deleteCNFExpr(CNFExpr *This) {
78 deleteVectorArray(&This->clauses);
79 freeLitVector(&This->singletons);