X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Finc_solver.cc;h=72d34083dcd4b096b32aee4b51816a361f708600;hp=d295ceeecfeeb6d1c9e004eeb41af05db3459102;hb=081e954fa3566ad9a2522ca45bef8e29472d2a72;hpb=cd362e8c49a8ac25e3f0324e89d139285cb71c3d

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index d295cee..72d3408 100644
--- 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;
 }
@@ -90,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) {
@@ -101,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;
 }
@@ -111,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;