This->literals=ourmalloc(This->capacity * sizeof(Literal));
}
+void clearLitVector(LitVector *This) {
+ This->size=0;
+}
+
void freeLitVector(LitVector *This) {
ourfree(This->literals);
}
ourfree(This);
}
+Literal getLiteralLitVector(LitVector *This, uint index) {
+ return This->literals[index];
+}
+
void addLiteralLitVector(LitVector *This, Literal l) {
Literal labs = abs(l);
uint vec_size=This->size;
return This;
}
+void clearCNFExpr(CNFExpr *This, bool isTrue) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
+ clearVectorLitVector(&This->clauses);
+ clearLitVector(&This->singletons);
+ This->litSize=0;
+ This->isTrue=isTrue;
+}
+
void deleteCNFExpr(CNFExpr *This) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
deleteVectorArrayLitVector(&This->clauses);
freeLitVector(&This->singletons);
ourfree(This);
}
+
+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;
+}
LitVector * allocLitVector();
void initLitVector(LitVector *This);
+void clearLitVector(LitVector *This);
void freeLitVector(LitVector *This);
void deleteLitVector(LitVector *This);
void addLiteralLitVector(LitVector *This, Literal l);
+Literal getLiteralLitVector(LitVector *This, uint index);
+
+static inline uint getSizeLitVector(LitVector *This) {return This->size;}
CNFExpr * allocCNFExprBool(bool isTrue);
CNFExpr * allocCNFExprLiteral(Literal l);
void deleteCNFExpr(CNFExpr *This);
-
+void clearCNFExpr(CNFExpr *This, bool isTrue);
bool alwaysTrueCNF(CNFExpr * This);
uint getLitSizeCNF(CNFExpr * This);
void clearCNF(CNFExpr *This, bool isTrue);
uint getClauseSizeCNF(CNFExpr * This);
+void conjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFLit(CNFExpr *This, Literal l);
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
+
#endif
}
}
-//DONE
+
Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
Literal l = 0;
Node * n = getNodePtrFromEdge(e);
}
}
-
-//DONE
bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
if (dest == NULL) {
dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
} else {
- clearCNF(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
}
return true;
}
if (exp == NULL || isProxy(exp)) return;
if (exp->litSize == 1) {
- Literal l = exp->singletons()[0];
+ Literal l = getLiteralLitVector(&exp->singletons, 0);
deleteCNFExpr(exp);
n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
- } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->isVarForced())) {
+ } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
introProxy(cnf, e, exp, sign);
} else {
n->ptrAnnot[sign] = exp;
CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
clearVectorEdge(&cnf->args);
- *largestEdge = (void*) NULL;
+ *largestEdge = (Edge) {(Node*) NULL};
CNFExpr* largest = NULL;
- int i = e->size();
+ Node *n=getNodePtrFromEdge(e);
+ int i = n->numEdges;
while (i != 0) {
- Edge arg = (*e)[--i]; arg.negateIf(isNeg);
+ Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
Node * narg = getNodePtrFromEdge(arg);
- if (arg.isVar()) {
+ if (edgeIsVarConst(arg)) {
pushVectorEdge(&cnf->args, arg);
continue;
}
}
if (largest != NULL) {
- largestEdge->ptrAnnot(isNegEdge(*largestEdge)) = NULL;
+ Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
+ nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
}
return largest;
int i = getSizeVectorEdge(&cnf->args);
while (i != 0) {
Edge arg = getVectorEdge(&cnf->args, --i);
- if (arg.isVar()) {
- accum->conjoin(atomLit(arg));
+ if (edgeIsVarConst(arg)) {
+ conjoinCNFLit(accum, getEdgeVar(arg));
} else {
- CNFExpr* argExp = (CNFExpr*) arg->ptrAnnot(isNegEdge(arg));
+ Node *narg=getNodePtrFromEdge(arg);
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
- bool destroy = (--arg->intAnnot(isNegEdge(arg)) == 0);
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
if (isProxy(argExp)) { // variable has been introduced
- accum->conjoin(getProxy(argExp));
+ conjoinCNFLit(accum, getProxy(argExp));
} else {
- accum->conjoin(argExp, destroy);
- if (destroy) arg->ptrAnnot(isNegEdge(arg)) = NULL;
+ conjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
}
}
}
/// be possible to use the correct proxy. That should be fixed.
// at this point, we will either have NULL, or a destructible expression
- if (accum->clauseSize() > CLAUSE_MAX)
+ if (getClauseSizeCNF(accum) > CLAUSE_MAX)
accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
int i = getSizeVectorEdge(&cnf->args);
while (i != 0) {
Edge arg=getVectorEdge(&cnf->args, --i);
Node *narg=getNodePtrFromEdge(arg);
- if (arg.isVar()) {
- accum->disjoin(atomLit(arg));
+ if (edgeIsVarConst(arg)) {
+ disjoinCNFLit(accum, getEdgeVar(arg));
} else {
CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
if (isProxy(argExp)) { // variable has been introduced
- accum->disjoin(getProxy(argExp));
+ disjoinCNFLit(accum, getProxy(argExp));
} else if (argExp->litSize == 0) {
- accum->disjoin(argExp, destroy);
+ disjoinCNFExpr(accum, argExp, destroy);
} else {
// check to see if we should introduce a proxy
int aL = accum->litSize; // lits in accum
int eC = getClauseSizeCNF(argExp); // clauses in argument
if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
- accum->disjoin(introProxy(cnf, arg, argExp, isNegEdge(arg)));
+ disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
} else {
- accum->disjoin(argExp, destroy);
+ disjoinCNFExpr(accum, argExp, destroy);
if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
}
}
void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
-
-
Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
#endif
type getVector ## name(Vector ## name *vector, uint index); \
void setVector ## name(Vector ## name *vector, uint index, type item); \
uint getSizeVector ## name(Vector ## name *vector); \
+ void setSizeVector ## name(Vector ## name *vector, uint size); \
void deleteVector ## name(Vector ## name *vector); \
void clearVector ## name(Vector ## name *vector); \
void deleteVectorArray ## name(Vector ## name *vector); \
type lastVector ## name(Vector ## name *vector) { \
return vector->array[vector->size]; \
} \
+ void setSizeVector ## name(Vector ## name *vector, uint size) { \
+ if (size <= vector->size) { \
+ vector->size=size; \
+ return; \
+ } else if (size > vector->capacity) { \
+ vector->array=(type *)ourrealloc(vector->array, size); \
+ vector->capacity=size; \
+ } \
+ bzero(&vector->array[vector->size], (size-vector->size)*sizeof(type)); \
+ vector->size=size; \
+ } \
void pushVector ## name(Vector ## name *vector, type item) { \
if (vector->size >= vector->capacity) { \
uint newcap=vector->capacity * 2; \