src/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