Another bug fix

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 634945365956d9441f14a59da127bdd9e7e582b6..9e85bfc41dd07536f0c019564053fc7300ad3181 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -245,7 +245,7 @@ Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 }
 
 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
-       bool negate=sameSignEdge(left, right);
+       bool negate=!sameSignEdge(left, right);
        Edge lpos=getNonNeg(left);
        Edge rpos=getNonNeg(right);
 
@@ -314,13 +314,19 @@ Edge constraintNewVar(CNF *cnf) {
        return e;
 }
 
-void solveCNF(CNF *cnf) {
+int solveCNF(CNF *cnf) {
        countPass(cnf);
        convertPass(cnf, false);
        finishedClauses(cnf->solver);
-       solve(cnf->solver);
+       return solve(cnf->solver);
 }
 
+bool getValueCNF(CNF *cnf, Edge var) {
+       Literal l=getEdgeVar(var);
+       bool isneg=(l<0);
+       l=abs(l);
+       return isneg ^ getValueSolver(cnf->solver, l);
+}
 
 void countPass(CNF *cnf) {
        uint numConstraints=getSizeVectorEdge(&cnf->constraints);
@@ -681,6 +687,43 @@ CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
        return largest;
 }
 
+void printCNF(Edge e) {
+       if (edgeIsVarConst(e)) {
+               Literal l=getEdgeVar(e);
+               printf ("%d", l);
+               return;
+       }
+       bool isNeg=isNegEdge(e);
+       if (edgeIsConst(e)) {
+               if (isNeg)
+                       printf("T");
+               else
+                       printf("F");
+               return;
+       }
+       Node *n=getNodePtrFromEdge(e);
+       if (isNeg)
+               printf("!");
+       switch(getNodeType(e)) {
+       case NodeType_AND:
+               printf("and");
+               break;
+       case NodeType_ITE:
+               printf("ite");
+               break;
+       case NodeType_IFF:
+               printf("iff");
+               break;
+       }
+       printf("(");
+       for(uint i=0;i<n->numEdges;i++) {
+               Edge e=n->edges[i];
+               if (i!=0)
+                       printf(" ");
+               printCNF(e);
+       }
+       printf(")");
+}
 
 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
        Edge largestEdge;

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 95ee530ab880f9f2b2f3b9b04ae37e31d5a6d480..89ea40f512d0d947fc0c98b390f0ce962071d3ee 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -191,8 +191,9 @@ Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 void addConstraint(CNF *cnf, Edge constraint);
-void solveCNF(CNF *cnf);
-
+int solveCNF(CNF *cnf);
+bool getValueCNF(CNF *cnf, Edge var);
+void printCNF(Edge e);
 
 void convertPass(CNF *cnf, bool backtrackLit);
 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 5b638e9458a26b5480d5cc92664076b1766e3dee..e0ebebd035ac76afe61573a902f184109a8d69c6 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -35,7 +35,7 @@
                Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
                tmp->size = 0;                                                      \
                tmp->capacity = capacity;                                           \
-               tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity);          \
+               tmp->array = (type *) ourmalloc(sizeof(type) * capacity);                                               \
                return tmp;                                                         \
        }                                                                     \
        Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
@@ -65,6 +65,7 @@
                if (vector->size >= vector->capacity) {                                                                                                                 \
                        uint newcap=vector->capacity << 1;                                                                                                                              \
                        vector->array=(type *)ourrealloc(vector->array, newcap * sizeof(type)); \
+                       vector->capacity=newcap;                                                                                                                                                                        \
                }                                                                   \
                vector->array[vector->size++] = item;                               \
        }                                                                     \
@@ -93,7 +94,7 @@
        void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
                vector->size = 0;                                                      \
                vector->capacity = capacity;                                                                                                                                                                                    \
-               vector->array = (type *) ourcalloc(1, sizeof(type) * capacity);                 \
+               vector->array = (type *) ourmalloc(sizeof(type) * capacity);                            \
        }                                                                                                                                                                                                                                                                                       \
        void allocInlineDefVector ## name(Vector ## name * vector) {                                    \
                allocInlineVector ## name(vector, defcap);                                                                                                      \

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 940500934efcdf1e7560846afa71098de6113cce..d5f4166796809b70dcbfcd5849be89f05208844d 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -1,4 +1,5 @@
 #include "nodeedge.h"
+#include <stdio.h>
 
 int main(int numargs, char ** argv) {
        CNF *cnf=createCNF();
@@ -6,13 +7,26 @@ int main(int numargs, char ** argv) {
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
        Edge nv1=constraintNegate(v1);
+       printCNF(nv1);
+       printf("\n");
        Edge nv2=constraintNegate(v2);
        Edge iff1=constraintIFF(cnf, nv1, v2);
+       printCNF(iff1);
+       printf("\n");
        Edge iff2=constraintIFF(cnf, nv2, v3);
-       //      Edge iff3=constraintIFF(cnf, v3, nv1);
-       //Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
-       Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+       Edge iff3=constraintIFF(cnf, v3, nv1);
+       Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+       //Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+       printCNF(cand);
+       printf("\n");
        addConstraint(cnf, cand);
-       solveCNF(cnf);
+       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);
+       } else
+               printf("%d\n",value);
        deleteCNF(cnf);
 }