Bug fixes for Java API + Exactly one constraints + Adding support for getting the...

[satune.git] / src / Backend / inc_solver.cc

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 7d0fd6513d86379fb96385db7c67d654a157133f..72d34083dcd4b096b32aee4b51816a361f708600 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -19,6 +19,7 @@ IncrementalSolver *allocIncrementalSolver() {
        This->solution = NULL;
        This->solutionsize = 0;
        This->offset = 0;
+       This->timeout = NOTIMEOUT;
        createSolver(This);
        return This;
 }
@@ -67,7 +68,10 @@ void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *liter
 }
 
 void finishedClauses(IncrementalSolver *This) {
-       addClauseLiteral(This, 0);
+       This->buffer[This->offset++] = 0;
+       if (This->offset == IS_BUFFERSIZE) {
+               flushBufferSolver(This);
+       }
 }
 
 void freeze(IncrementalSolver *This, int variable) {
@@ -87,7 +91,7 @@ void startSolve(IncrementalSolver *This) {
 }
 
 int getSolution(IncrementalSolver *This) {
-       int result = readIntSolver(This);
+       int result = readStatus(This);
        if (result == IS_SAT) {
                int numVars = readIntSolver(This);
                if (numVars > This->solutionsize) {
@@ -98,6 +102,16 @@ int getSolution(IncrementalSolver *This) {
                }
                readSolver(This, &This->solution[1], numVars * sizeof(int));
                This->solutionsize = numVars;
+       } else { //Reading unsat explanation
+               int numVars = readIntSolver(This);
+               if (numVars > This->solutionsize) {
+                       if (This->solution != NULL)
+                               ourfree(This->solution);
+                       This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
+                       This->solution[0] = 0;
+               }
+               readSolver(This, &This->solution[1], numVars * sizeof(int));
+               This->solutionsize = numVars;
        }
        return result;
 }
@@ -108,6 +122,33 @@ int readIntSolver(IncrementalSolver *This) {
        return value;
 }
 
+int readStatus(IncrementalSolver *This) {
+       int retval;
+       fd_set rfds;
+       FD_ZERO(&rfds);
+       FD_SET(This->from_solver_fd, &rfds);
+       fd_set *temp;
+       if (This->timeout == NOTIMEOUT) {
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
+       } else {
+               struct timeval tv;
+               tv.tv_sec = This->timeout;
+               tv.tv_usec = 0;
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
+       }
+       if (retval == -1) {
+               perror("Error in select()");
+               exit(EXIT_FAILURE);
+       }
+       else if (retval) {
+               printf("Data is available now.\n");
+               return readIntSolver(This);
+       } else {
+               printf("Timeout for the solver\n");
+               return IS_INDETER;
+       }
+}
+
 void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
        char *result = (char *) tmp;
        ssize_t bytestoread = size;