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 80c4e4c9f6b4b4857e4add875aff110f1990932d..72d34083dcd4b096b32aee4b51816a361f708600 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -12,7 +12,6 @@
 #include <fcntl.h>
 #include "common.h"
 #include <string.h>
-#include <stdexcept>
 
 IncrementalSolver *allocIncrementalSolver() {
        IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -20,6 +19,7 @@ IncrementalSolver *allocIncrementalSolver() {
        This->solution = NULL;
        This->solutionsize = 0;
        This->offset = 0;
+       This->timeout = NOTIMEOUT;
        createSolver(This);
        return This;
 }
@@ -91,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) {
@@ -102,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;
 }
@@ -112,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;
@@ -120,7 +157,7 @@ void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
                ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
                if (n == -1) {
                        model_print("Read failure\n");
-                       throw std::runtime_error("Read failure\n");
+                       exit(-1);
                }
                bytestoread -= n;
                bytesread += n;