This->solution = NULL;
This->solutionsize = 0;
This->offset = 0;
+ This->timeout = NOTIMEOUT;
createSolver(This);
return 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) {
}
readSolver(This, &This->solution[1], numVars * sizeof(int));
This->solutionsize = numVars;
+ } else if (result == IS_INDETER){
+ return result;
+ } 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;
}
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;