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 struct IncrementalSolver {
  22         int *buffer;
  23         int *solution;
  24         int solutionsize;
  25         uint offset;
  26         pid_t solver_pid;
  27         int to_solver_fd;
  28         int from_solver_fd;
  29 };
  30
  31 IncrementalSolver *allocIncrementalSolver();
  32 void deleteIncrementalSolver(IncrementalSolver *This);
  33 void addClauseLiteral(IncrementalSolver *This, int literal);
  34 void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *literals);
  35 void finishedClauses(IncrementalSolver *This);
  36 void freeze(IncrementalSolver *This, int variable);
  37 int solve(IncrementalSolver *This);
  38 void startSolve(IncrementalSolver *This);
  39 int getSolution(IncrementalSolver *This);
  40 bool getValueSolver(IncrementalSolver *This, int variable);
  41 void resetSolver(IncrementalSolver *This);
  42 void createSolver(IncrementalSolver *This);
  43 void killSolver(IncrementalSolver *This);
  44 void flushBufferSolver(IncrementalSolver *This);
  45 int readIntSolver(IncrementalSolver *This);
  46 void readSolver(IncrementalSolver *This, void *buffer, ssize_t size);
  47 #endif