inc_solver.h

   1 #ifndef INC_SOLVER_H
   2 #define INC_SOLVER_H
   3 #include <sys/types.h>
   4 #include <unistd.h>
   5 #include <stdio.h>
   6 #include <stdlib.h>
   7 #include <signal.h>
   8
   9
  10 #define IS_UNSAT 0
  11 #define IS_SAT 1
  12 #define IS_INDETER 2
  13 #define IS_RUNSOLVER 3
  14 #define IS_FREEZE 3
  15
  16 #define BUFFERSIZE 1024
  17
  18 class IncrementalSolver {
  19  public:
  20   IncrementalSolver();
  21   ~IncrementalSolver();
  22   void addClauseLiteral(int literal);
  23   void finishedClauses();
  24   void freeze(int variable);
  25   int solve();
  26   bool getValue(int variable);
  27   void reset();
  28
  29  private:
  30   void createSolver();
  31   void killSolver();
  32   void flushBuffer();
  33   int readIntSolver();
  34   void readSolver(void * buffer, ssize_t size);
  35   int * buffer;
  36   int * solution;
  37   int solutionsize;
  38   int offset;
  39   pid_t solver_pid;
  40   int to_solver_fd;
  41   int from_solver_fd;
  42 };
  43 #endif