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 class IncrementalSolver {
  22  public:
  23   IncrementalSolver();
  24   ~IncrementalSolver();
  25   void addClauseLiteral(int literal);
  26   void finishedClauses();
  27   void freeze(int variable);
  28   int solve();
  29         void startSolve();
  30         int getSolution();
  31
  32         bool getValue(int variable);
  33   void reset();
  34         MEMALLOC;
  35
  36  private:
  37   void createSolver();
  38   void killSolver();
  39   void flushBuffer();
  40   int readIntSolver();
  41   void readSolver(void * buffer, ssize_t size);
  42   int * buffer;
  43   int * solution;
  44   int solutionsize;
  45   int offset;
  46   pid_t solver_pid;
  47   int to_solver_fd;
  48   int from_solver_fd;
  49 };
  50 #endif