more edits

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index 0f0aef4af4c8c526676d971887ffdb1892f0b507..b2d3ca9301f6b0a8a37ab1b3c66466a89ea3be84 100644 (file)
--- 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;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;
+}

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index 1d12f6bf5e214c73142fc553f291e8ecfd0efe0c..18f5ff573538f3bb0af2f3de2a07b81db82cce27 100644 (file)
--- 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 801351dcf42d764bec29e84b2b2268177e878ad7..fd805b44db1208a92ab9e5e8b816ff7237f40e1e 100644 (file)
--- 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 559c05822732b6f694ef96ec973f80c1440c259e..bc0eb5cec3fe55530147a09e55f064dd7be03373 100644 (file)
--- 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 00696f1a4f0ef900bb3e627b4f476767be74b60f..fdaf0f416d84a9e079770eef4b13069b9eb0f375 100644 (file)
--- 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;                                 \