+
+void conjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0 && !This->isTrue) //Handle False
+ return;
+
+ This->litSize-=getSizeLitVector(&This->singletons);
+ addLiteralLitVector(&This->singletons, l);
+ uint newsize=getSizeLitVector(&This->singletons);
+ if (newsize==0)
+ clearCNF(This, false); //We found a conflict
+ else
+ This->litSize+=getSizeLitVector(&This->singletons);
+}
+
+void disjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0) {
+ if (!This->isTrue) {
+ This->litSize++;
+ addLiteralLitVector(&This->singletons, l);
+ }
+ return;
+ }
+ uint litSize=0;
+ uint newindex=0;
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ LitVector * lv=getVectorLitVector(&This->clauses, i);
+ addLiteralLitVector(lv, l);
+ uint newSize=getSizeLitVector(lv);
+ if (newSize!=0) {
+ setVectorLitVector(&This->clauses, newindex++, lv);
+ } else {
+ deleteLitVector(lv);
+ }
+ litSize+=newSize;
+ }
+ setSizeVectorLitVector(&This->clauses, newindex);
+
+ bool hasSameSingleton=false;
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ Literal lsing=getLiteralLitVector(&This->singletons, i);
+ if (lsing == l) {
+ hasSameSingleton=true;
+ } else if (lsing != -l) {
+ //Create new LitVector with both l and lsing
+ LitVector *newlitvec=allocLitVector();
+ addLiteralLitVector(newlitvec, l);
+ addLiteralLitVector(newlitvec, lsing);
+ litSize+=2;
+ pushVectorLitVector(&This->clauses, newlitvec);
+ }
+ }
+ clearLitVector(&This->singletons);
+ if (hasSameSingleton) {
+ addLiteralLitVector(&This->singletons, l);
+ litSize++;
+ }
+ This->litSize=litSize;
+}