src/Backend/inc_solver.h

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #ifndef INC_SOLVER_H
  11 #define INC_SOLVER_H
  12 #include <sys/types.h>
  13 #include <sys/wait.h>
  14 #include <unistd.h>
  15 #include <stdio.h>
  16 #include <stdlib.h>
  17 #include <signal.h>
  18 #include "solver_interface.h"
  19 #include "classlist.h"
  20
  21 #define NOTIMEOUT -1
  22
  23 struct IncrementalSolver {
  24         int *buffer;
  25         int *solution;
  26         int solutionsize;
  27         uint offset;
  28         pid_t solver_pid;
  29         int to_solver_fd;
  30         int from_solver_fd;
  31         long timeout;
  32 };
  33
  34 IncrementalSolver *allocIncrementalSolver();
  35 void deleteIncrementalSolver(IncrementalSolver *This);
  36 void addClauseLiteral(IncrementalSolver *This, int literal);
  37 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals);
  38 void finishedClauses(IncrementalSolver *This);
  39 void freeze(IncrementalSolver *This, int variable);
  40 int solve(IncrementalSolver *This);
  41 void startSolve(IncrementalSolver *This);
  42 int getSolution(IncrementalSolver *This);
  43 bool getValueSolver(IncrementalSolver *This, int variable);
  44 void resetSolver(IncrementalSolver *This);
  45 void createSolver(IncrementalSolver *This);
  46 void killSolver(IncrementalSolver *This);
  47 void flushBufferSolver(IncrementalSolver *This);
  48 int readIntSolver(IncrementalSolver *This);
  49 int readStatus(IncrementalSolver *This);
  50 void readSolver(IncrementalSolver *This, void *buffer, ssize_t size);
  51 #endif