import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.DimacsReader;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import java.io.*;
import java.util.Scanner;

public class SATSolver {

	private APTA apta;
	private int colors;
	private int vertices;
	private IProblem problem;
	private String dimacsFile = null;
	private String satSolverFile = null;
	private String timeoutString = " ";
	private String ansLine = null;
	private int countClauses;
	private int countVars;
	private int timeout = 0;
	private boolean problemIsSatisfiableCalled = false;
	private boolean iterativeMode;
	private boolean iterativeSolver;
	private Process process;
	private boolean first;
	Scanner sc;
	BufferedWriter bw;

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile) throws ContradictionException,
			ParseFormatException, IOException {
		init(apta, colors, dimacsFile, null, false, false);
	}

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile, int timeout) throws ContradictionException,
			ParseFormatException, IOException {
		this.timeout = timeout;
		init(apta, colors, dimacsFile, null, false, false);
	}

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile, String satSolverFile)
			throws ContradictionException, ParseFormatException, IOException {
		init(apta, colors, dimacsFile, satSolverFile, false, false);
	}

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile, String satSolverFile, boolean iterativeMode, boolean iterativeSolver)
			throws ContradictionException, ParseFormatException, IOException {
		init(apta, colors, dimacsFile, satSolverFile, iterativeMode, iterativeSolver);
	}

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile, int timeout, String satSolverFile)
			throws ContradictionException, IOException {
		init(apta, colors, dimacsFile, satSolverFile, false, false);
		timeoutString = " -t " + timeout + " ";
	}

	public SATSolver(APTA apta, int colors,
	                 String dimacsFile, int timeout, String satSolverFile, boolean iterativeMode, boolean iterativeSolver)
			throws ContradictionException, IOException {
		init(apta, colors, dimacsFile, satSolverFile, iterativeMode, iterativeSolver);
		timeoutString = " -t " + timeout + " ";
	}

	private void init(APTA apta, int colors, String dimacsFile,
	                  String satSolverFile, boolean iterativeMode, boolean iterativeSolver) throws IOException {
		this.apta = apta;
		this.vertices = apta.getSize();
		this.dimacsFile = dimacsFile;
		this.colors = colors;
		this.satSolverFile = satSolverFile;
		this.iterativeMode = iterativeMode;
		this.iterativeSolver = iterativeSolver;
		this.first = true;
		try (BufferedReader br = new BufferedReader(new FileReader(dimacsFile))) {
			String line;
			while ((line = br.readLine()) != null) {
				if (line.startsWith("p cnf ")) {
					String[] tmp = line.split(" ");
					countVars = Integer.parseInt(tmp[2]);
					countClauses = Integer.parseInt(tmp[3]);
					break;
				}
			}
		}
	}

	private IProblem build() throws ContradictionException,
			ParseFormatException, IOException {
		ISolver solver = SolverFactory.newDefault();
		if (timeout > 0) {
			solver.setTimeout(timeout);
		}
		Reader reader = new DimacsReader(solver);
		return problem = reader.parseInstance(dimacsFile);
	}

	public boolean problemIsSatisfiable() throws TimeoutException, IOException, ParseFormatException, ContradictionException {
		problemIsSatisfiableCalled = true;
		if (satSolverFile == null) {
			problem = build();
			return problem.isSatisfiable();
		} else {
			if (!(iterativeMode || iterativeSolver)) {
				process = new ProcessBuilder((satSolverFile + timeoutString + dimacsFile).split(" ")).start();
				try (BufferedReader br = new BufferedReader(new InputStreamReader(
						process.getInputStream()))) {
					String line;
					while ((line = br.readLine()) != null) {
						if (line.equals("s SATISFIABLE")) {
							ansLine = "";
						}
						if (line.charAt(0) == 'v') {
							ansLine += line.substring(2, line.length()) + " ";
						}
						if (line.contains("c time limit") && line.contains("reached")) {
							throw new TimeoutException();
						}
					}
					return ansLine != null;
				}
			} else {
				if (first) {
					process = new ProcessBuilder((satSolverFile + " " + countVars).split(" ")).start();
					sc = new Scanner(new InputStreamReader(process.getInputStream()));
					bw = new BufferedWriter(new OutputStreamWriter(process.getOutputStream()));
					try (
							BufferedReader brDimacs = new BufferedReader(new FileReader(dimacsFile))
					) {
						String line;
						while ((line = brDimacs.readLine()) != null) {
							if (line.startsWith("p cnf ")) {
								continue;
							}
							bw.write(line + "\n");
						}
						bw.write("solve " + timeout + "\n");
						bw.flush();
						line = sc.nextLine();
						if (line.equals("SAT")) {
							line = sc.nextLine();
							ansLine = line.substring(2, line.length()) + " ";
							if (iterativeSolver) {
								bw.write("halt\n");
								bw.flush();
							}
						} else if (line.equals("UNKNOWN")) {
							bw.write("halt\n");
							bw.flush();
							throw new TimeoutException();
						} else if (line.equals("UNSAT")) {
							bw.write("halt\n");
							bw.flush();
						}
						first = false;
						return ansLine != null;
					}
				} else {
					try (
							BufferedReader brDimacs = new BufferedReader(new FileReader(dimacsFile))
					) {
						ansLine = null;
						String prevLine = "";
						String line = brDimacs.readLine();
						while (line != null) {
							prevLine = line;
							line = brDimacs.readLine();
						}
						bw.write(prevLine + "\n");
						bw.write("solve " + timeout + "\n");
						bw.flush();
						line = sc.nextLine();
						if (line.equals("SAT")) {
							line = sc.nextLine();
							ansLine = line.substring(2, line.length()) + " ";
						} else if (line.equals("UNKNOWN")) {
							bw.write("halt\n");
							bw.flush();
							throw new TimeoutException();
						} else if (line.equals("UNSAT")) {
							bw.write("halt\n");
							bw.flush();
						}
						return ansLine != null;
					}
				}
			}
		}
	}

	// must be called after problemIsSatisfiable
	public int[] getModel() throws Exception {
		if (!problemIsSatisfiableCalled) {
			throw new Exception("You should call problemIsSatisfiable first");
		}
		int[] model;
		if (satSolverFile == null) {
			model = problem.model();
		} else {
			String[] strings = ansLine.split(" ");
			model = new int[strings.length];
			for (int i = 0; i < strings.length; i++) {
				model[i] = Integer.parseInt(strings[i]);
			}
		}
		return model;
	}

	public void updateTL(int timeout) {
		this.timeout = timeout;
	}

	public int nVars() {
		return countVars;
	}

	public int nConstraints() {
		return countClauses;
	}

}
