Base Commit
[satune.git] / 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