From 68e2982593fbf881adc716b7548207a1b3171f8f Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 8 Jul 2017 20:13:09 -0700 Subject: [PATCH] more edits --- src/Backend/cnfexpr.c | 79 ++++++++++++++++++++++++++++++++++++++++ src/Backend/cnfexpr.h | 11 +++++- src/Backend/nodeedge.c | 51 +++++++++++++------------- src/Backend/nodeedge.h | 2 - src/Collections/vector.h | 12 ++++++ 5 files changed, 127 insertions(+), 28 deletions(-) diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c index 0f0aef4..b2d3ca9 100644 --- a/src/Backend/cnfexpr.c +++ b/src/Backend/cnfexpr.c @@ -17,6 +17,10 @@ void initLitVector(LitVector *This) { This->literals=ourmalloc(This->capacity * sizeof(Literal)); } +void clearLitVector(LitVector *This) { + This->size=0; +} + void freeLitVector(LitVector *This) { ourfree(This->literals); } @@ -26,6 +30,10 @@ void deleteLitVector(LitVector *This) { 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; @@ -74,8 +82,79 @@ CNFExpr * allocCNFExprLiteral(Literal l) { return This; } +void clearCNFExpr(CNFExpr *This, bool isTrue) { + for(uint i=0;iclauses);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;iclauses);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;iclauses);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;isingletons);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; +} diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h index 1d12f6b..18f5ff5 100644 --- a/src/Backend/cnfexpr.h +++ b/src/Backend/cnfexpr.h @@ -26,14 +26,18 @@ typedef struct CNFExpr CNFExpr; 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); @@ -41,4 +45,9 @@ bool alwaysFalseCNF(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 diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c index 801351d..fd805b4 100644 --- a/src/Backend/nodeedge.c +++ b/src/Backend/nodeedge.c @@ -434,7 +434,7 @@ void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit } } -//DONE + Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) { Literal l = 0; Node * n = getNodePtrFromEdge(e); @@ -507,8 +507,6 @@ void produceCNF(CNF * cnf, Edge e) { } } - -//DONE bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) { if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) { if (dest == NULL) { @@ -525,7 +523,7 @@ bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) { dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); } else { - clearCNF(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); + clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src)); } return true; } @@ -538,10 +536,10 @@ void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) { 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; @@ -567,14 +565,15 @@ void outputCNF(CNF *cnf, CNFExpr *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; } @@ -602,7 +601,8 @@ CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) { } if (largest != NULL) { - largestEdge->ptrAnnot(isNegEdge(*largestEdge)) = NULL; + Node *nlargestEdge=getNodePtrFromEdge(*largestEdge); + nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL; } return largest; @@ -618,17 +618,18 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) { 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; } } } @@ -655,23 +656,23 @@ CNFExpr* produceDisjunction(CNF *cnf, Edge e) { /// 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 @@ -680,9 +681,9 @@ CNFExpr* produceDisjunction(CNF *cnf, Edge e) { 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; } } diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h index 559c058..bc0eb5c 100644 --- a/src/Backend/nodeedge.h +++ b/src/Backend/nodeedge.h @@ -193,8 +193,6 @@ bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate); 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 diff --git a/src/Collections/vector.h b/src/Collections/vector.h index 00696f1..fdaf0f4 100644 --- a/src/Collections/vector.h +++ b/src/Collections/vector.h @@ -18,6 +18,7 @@ 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); \ @@ -49,6 +50,17 @@ 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; \ -- 2.34.1