Merge branch 'hamed' into brian

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index 6bbbbfc7cf1f5f5fd6cd554e23ad23c8101b8116..dbbd93f53d51e6143db4a1bdbda6bf1102c2f4df 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -1,5 +1,5 @@
 #include "cnfexpr.h"
-
+#include <stdio.h>
 /* 
 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -445,5 +445,21 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                deleteCNFExpr(expr);
 }
 
-
-
+void printCNFExpr(CNFExpr *This) {
+       for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+               if (i!=0)
+                       printf(" ^ ");
+               Literal l=getLiteralLitVector(&This->singletons,i);
+               printf ("%d",l);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+               LitVector *lv=getVectorLitVector(&This->clauses,i);
+               printf(" ^ (");
+               for(uint j=0;j<getSizeLitVector(lv);j++) {
+                       if (j!=0)
+                               printf(" v ");
+                       printf("%d", getLiteralLitVector(lv, j));
+               }
+               printf(")");
+       }
+}

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index 5f1f9077d93e21277ef13128e2d784dd539c5570..1b64528d87b787ccc5e8f1f3a0bfba9108ffd34e 100644 (file)
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -43,6 +43,7 @@ CNFExpr * allocCNFExprBool(bool isTrue);
 CNFExpr * allocCNFExprLiteral(Literal l);
 void deleteCNFExpr(CNFExpr *This);
 void clearCNFExpr(CNFExpr *This, bool isTrue);
+void printCNFExpr(CNFExpr *This);
 
 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
 static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 307114ef4782acca1ae992328d40a94fba176df9..935aff95af7dd1b7ca2aaa1c0e6c85192920df6f 100644 (file)
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -11,6 +11,7 @@
 #define SATSOLVER "sat_solver"
 #include <fcntl.h>
 #include "common.h"
+#include <string.h>
 
 IncrementalSolver * allocIncrementalSolver() {
        IncrementalSolver *This=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -44,16 +45,25 @@ void addClauseLiteral(IncrementalSolver * This, int literal) {
 }
 
 void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) {
-       for(uint i=0;i<numliterals; i++) {
-               This->buffer[This->offset++]=literals[i];
-               if (This->offset==IS_BUFFERSIZE) {
+       uint index=0;
+       while(true) {
+               uint bufferspace=IS_BUFFERSIZE-This->offset;
+               uint numtowrite=numliterals-index;
+               if (bufferspace > numtowrite) {
+                       memcpy(&This->buffer[This->offset], &literals[index], numtowrite*sizeof(int));
+                       This->offset+=numtowrite;
+                       This->buffer[This->offset++]=0; //have one extra spot always
+                       if (This->offset==IS_BUFFERSIZE) {//Check if full
+                               flushBufferSolver(This);
+                       }
+                       return;
+               } else {
+                       memcpy(&This->buffer[This->offset], &literals[index], bufferspace*sizeof(int));
+                       This->offset+=bufferspace;
+                       index+=bufferspace;
                        flushBufferSolver(This);
                }
        }
-       This->buffer[This->offset++]=0;
-       if (This->offset==IS_BUFFERSIZE) {
-               flushBufferSolver(This);
-       }
 }
 
 void finishedClauses(IncrementalSolver * This) {

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 9e85bfc41dd07536f0c019564053fc7300ad3181..9d6e855ef5e89b22a64e3b0371597c58ff9be380 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -167,7 +167,7 @@ Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
        Edge lneg=constraintNegate(left);
        Edge rneg=constraintNegate(right);
-       Edge eand=constraintAND2(cnf, left, right);
+       Edge eand=constraintAND2(cnf, lneg, rneg);
        return constraintNegate(eand);
 }
 

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index d5f4166796809b70dcbfcd5849be89f05208844d..ddad6d7334c4fc048a4aef5206c69ea157814548 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -10,13 +10,17 @@ int main(int numargs, char ** argv) {
        printCNF(nv1);
        printf("\n");
        Edge nv2=constraintNegate(v2);
+       Edge nv3=constraintNegate(v3);
        Edge iff1=constraintIFF(cnf, nv1, v2);
        printCNF(iff1);
        printf("\n");
-       Edge iff2=constraintIFF(cnf, nv2, v3);
+
+       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 cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+
        printCNF(cand);
        printf("\n");
        addConstraint(cnf, cand);