Bug fix

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 6065e5f5c13e49e6a6965dbfe3dd048c02a5217d..7f65364f357945557178915547e194ede587a797 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -232,7 +232,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
                        return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
                }
        }
-       
+
        return createNode(cnf, NodeType_AND, lowindex, edges);
 }
 
@@ -397,8 +397,8 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
                                n->intAnnot[polarity]=1;
                                for (uint i=0;i<n->numEdges;i++) {
                                        Edge succ=n->edges[i];
-                                       succ=constraintNegateIf(succ, polarity);
                                        if(!edgeIsVarConst(succ)) {
+                                               succ=constraintNegateIf(succ, polarity);
                                                pushVectorEdge(stack, succ);
                                        }
                                }
@@ -605,7 +605,7 @@ void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
        if (exp->litSize == 1) {
                Literal l = getLiteralLitVector(&exp->singletons, 0);
                deleteCNFExpr(exp);
-               n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+               n->ptrAnnot[sign] = (void*) ((((intptr_t) l) << 1) | 1);
        } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
                introProxy(cnf, e, exp, sign);
        } else {
@@ -625,7 +625,7 @@ void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
        for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
                Literal l=getLiteralLitVector(&expr->singletons,i);
                Literal clause[] = {-lcond, l};
-               addArrayClauseLiteral(cnf->solver, 1, clause);
+               addArrayClauseLiteral(cnf->solver, 2, clause);
        }
        for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
                LitVector *lv=getVectorLitVector(&expr->clauses,i);
@@ -654,7 +654,8 @@ CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
        Node *n=getNodePtrFromEdge(e);
        int i = n->numEdges;
        while (i != 0) {
-               Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+               Edge arg = n->edges[--i];
+               arg=constraintNegateIf(arg, isNeg);
                Node * narg = getNodePtrFromEdge(arg);
                
                if (edgeIsVarConst(arg)) {
@@ -734,7 +735,8 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) {
        Edge largestEdge;
        
        CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
-       if (accum == NULL) accum = allocCNFExprBool(true);
+       if (accum == NULL)
+               accum = allocCNFExprBool(true);
        
        int i = getSizeVectorEdge(&cnf->args);
        while (i != 0) {
@@ -750,7 +752,8 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) {
                                conjoinCNFLit(accum, getProxy(argExp));
                        } else {
                                conjoinCNFExpr(accum, argExp, destroy);
-                               if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+                               if (destroy)
+                                       narg->ptrAnnot[isNegEdge(arg)] = NULL;
                        }
                }
        }

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 23d943c7344137bb068dbe3ff5344bad4a97dcb8..222d4a11c74aec994f48ca90dc3e512d4c196656 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -14,7 +14,7 @@ int main(int numargs, char ** argv) {
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
        addBoolean(solver, oc);
-       /*      
+               
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
        Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
@@ -38,7 +38,7 @@ int main(int numargs, char ** argv) {
        Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addBoolean(solver, pred);
-       */
+       
        startEncoding(solver);
        deleteSolver(solver);
 }

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 06b83bb171545ea44b58fd473465cb17d40738c6..ebd79f52f9a788a460d0119e879eec4c8f3a75af 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -6,30 +6,29 @@ int main(int numargs, char ** argv) {
        Edge v1=constraintNewVar(cnf);
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
+       Edge v4=constraintNewVar(cnf);
+       Edge v5=constraintNewVar(cnf);
+
        Edge nv1=constraintNegate(v1);
-       printCNF(nv1);
-       printf("\n");
        Edge nv2=constraintNegate(v2);
        Edge nv3=constraintNegate(v3);
-       Edge iff1=constraintIFF(cnf, nv1, v2);
-       printCNF(iff1);
-       printf("\n");
-
-       Edge iff2=constraintOR2(cnf, constraintAND2(cnf, v2, v3), constraintAND2(cnf, nv2, nv3));
-       printCNF(iff2);
-       printf("\n");
-       Edge iff3=constraintIFF(cnf, v3, nv1);
-       Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+       Edge nv4=constraintNegate(v4);
 
-       printCNF(cand);
+       Edge c1=constraintAND2(cnf, v1, nv2);
+       Edge c2=constraintAND2(cnf, v3, nv4);
+       Edge c3=constraintAND2(cnf, nv1, v2);
+       Edge c4=constraintAND2(cnf, nv3, v4);
+       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+       printCNF(cor);
        printf("\n");
-       addConstraint(cnf, cand);
+       addConstraint(cnf, cor);
        int value=solveCNF(cnf);
        if (value==1) {
                bool v1v=getValueCNF(cnf, v1);
                bool v2v=getValueCNF(cnf, v2);
                bool v3v=getValueCNF(cnf, v3);
-               printf("%d %u %u %u\n", value, v1v, v2v, v3v);
+               bool v4v=getValueCNF(cnf, v4);
+               printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
        } else
                printf("%d\n",value);
        deleteCNF(cnf);