6 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
8 LitVector * allocLitVector() {
9 LitVector *This=ourmalloc(sizeof(LitVector));
14 void initLitVector(LitVector *This) {
16 This->capacity=LITCAPACITY;
17 This->literals=ourmalloc(This->capacity * sizeof(Literal));
20 void clearLitVector(LitVector *This) {
24 void freeLitVector(LitVector *This) {
25 ourfree(This->literals);
28 void deleteLitVector(LitVector *This) {
33 Literal getLiteralLitVector(LitVector *This, uint index) {
34 return This->literals[index];
37 void addLiteralLitVector(LitVector *This, Literal l) {
38 Literal labs = abs(l);
39 uint vec_size=This->size;
40 uint searchsize=boundedSize(vec_size);
42 for (; i < searchsize; i++) {
43 Literal curr = This->literals[i];
44 Literal currabs = abs(curr);
47 if (currabs == labs) {
49 This->size = 0; //either true or false now depending on whether this is a conj or disj
52 if ((++This->size) >= This->capacity) {
54 This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
57 if (vec_size < MERGESIZE) {
58 memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
61 This->literals[vec_size]=l;
66 CNFExpr * allocCNFExprBool(bool isTrue) {
67 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
70 allocInlineVectorLitVector(&This->clauses, 2);
71 initLitVector(&This->singletons);
75 CNFExpr * allocCNFExprLiteral(Literal l) {
76 CNFExpr *This=ourmalloc(sizeof(CNFExpr));
79 allocInlineVectorLitVector(&This->clauses, 2);
80 initLitVector(&This->singletons);
81 addLiteralLitVector(&This->singletons, l);
85 void clearCNFExpr(CNFExpr *This, bool isTrue) {
86 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
87 deleteLitVector(getVectorLitVector(&This->clauses, i));
89 clearVectorLitVector(&This->clauses);
90 clearLitVector(&This->singletons);
95 void deleteCNFExpr(CNFExpr *This) {
96 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
97 deleteLitVector(getVectorLitVector(&This->clauses, i));
99 deleteVectorArrayLitVector(&This->clauses);
100 freeLitVector(&This->singletons);
104 void conjoinCNFLit(CNFExpr *This, Literal l) {
105 if (This->litSize==0 && !This->isTrue) //Handle False
108 This->litSize-=getSizeLitVector(&This->singletons);
109 addLiteralLitVector(&This->singletons, l);
110 uint newsize=getSizeLitVector(&This->singletons);
112 clearCNF(This, false); //We found a conflict
114 This->litSize+=getSizeLitVector(&This->singletons);
117 void disjoinCNFLit(CNFExpr *This, Literal l) {
118 if (This->litSize==0) {
121 addLiteralLitVector(&This->singletons, l);
127 for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
128 LitVector * lv=getVectorLitVector(&This->clauses, i);
129 addLiteralLitVector(lv, l);
130 uint newSize=getSizeLitVector(lv);
132 setVectorLitVector(&This->clauses, newindex++, lv);
138 setSizeVectorLitVector(&This->clauses, newindex);
140 bool hasSameSingleton=false;
141 for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
142 Literal lsing=getLiteralLitVector(&This->singletons, i);
144 hasSameSingleton=true;
145 } else if (lsing != -l) {
146 //Create new LitVector with both l and lsing
147 LitVector *newlitvec=allocLitVector();
148 addLiteralLitVector(newlitvec, l);
149 addLiteralLitVector(newlitvec, lsing);
151 pushVectorLitVector(&This->clauses, newlitvec);
154 clearLitVector(&This->singletons);
155 if (hasSameSingleton) {
156 addLiteralLitVector(&This->singletons, l);
159 This->litSize=litSize;