package jkind.solvers;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.util.List;

import jkind.JKindException;
import jkind.sexp.Sexp;

import org.antlr.runtime.ANTLRStringStream;
import org.antlr.runtime.CharStream;
import org.antlr.runtime.CommonTokenStream;
import org.antlr.runtime.RecognitionException;

public class YicesSolver extends Solver {
	private Process process;
	private BufferedWriter toYices;
	private BufferedReader fromYices;
	private boolean debug = false;

	final private static String DONE = "@DONE";
	
	public YicesSolver() {
		ProcessBuilder pb = new ProcessBuilder("yices");
		pb.redirectErrorStream(true);
		try {
			process = pb.start();
		} catch (IOException e) {
			throw new JKindException("Unable to start yices", e);
		}
		toYices = new BufferedWriter(new OutputStreamWriter(process.getOutputStream()));
		fromYices = new BufferedReader(new InputStreamReader(process.getInputStream()));
	}
	
	@Override
	public void initialize() {
		send("(set-evidence! true)");
	}
	
	@Override
	public void send(Sexp sexp) {
		send(sexp.toString());
	}
	
	@Override
	public void send(List<Sexp> sexps) {
		for (Sexp sexp : sexps) {
			send(sexp);
		}
	}
	
	private void send(String str) {
		if (debug) {
			System.out.println("Sending: " + str);
		}
		try {
			toYices.append(str);
			toYices.newLine();
			toYices.flush();
		} catch (IOException e) {
			throw new JKindException("Unable to write to yices", e);
		}
	}

	@Override
	public SolverResult query(Sexp sexp) {
		return query(sexp.toString());
	}
	
	private SolverResult query(String str) {
		push();
		send("(assert (not " + str + "))");
		send("(check)");
		send("(echo \"" + DONE + "\\n\")");
		pop();

		SolverResult result = readResult();
		if (result.getResult() == null) {
			throw new JKindException("Unknown result from yices");
		}
		return result;
	}

	private SolverResult readResult() {
		try {
			String line;
			StringBuilder content = new StringBuilder();
			while (true) {
				line = fromYices.readLine();
				if (debug) {
					System.out.println("Read: " + line);
				}
				if (line == null) {
					throw new JKindException("Yices terminated unexpectedly");
				} else if (line.contains("Error:")) {
					throw new JKindException("Yices error: " + line);
				} else if (line.startsWith("Logical context")) {
					continue;
				} else if (line.equals(DONE)) {
					break;
				} else {
					content.append(line);
					content.append("\n");
				}
			}

			return parseYices(content.toString());
		} catch (RecognitionException e) {
			throw new JKindException("Error parsing Yices output", e);
		} catch (IOException e) {
			throw new JKindException("Unable to read from yices", e);
		}
	}
	
	private static SolverResult parseYices(String string) throws IOException, RecognitionException {
		CharStream stream = new ANTLRStringStream(string);
		YicesLexer lexer = new YicesLexer(stream);
		CommonTokenStream tokens = new CommonTokenStream(lexer);
		YicesParser parser = new YicesParser(tokens);
		SolverResult result = parser.solverResult();
		if (parser.getNumberOfSyntaxErrors() > 0) {
			throw new JKindException("Error parsing Yices output");
		}
		return result;
	}

	@Override
	public void push() {
		send("(push)");
	}

	@Override
	public void pop() {
		send("(pop)");
	}
	
	@Override
	public void stop() {
		try {
			toYices.close();
			fromYices.close();
		} catch (IOException e) {
		}
		process.destroy();
		process = null;
	}
}

@@ -1709,32 +1709,64 @@
 ing());%0D%0A%09%7D%0D%0A%09%0D%0A
+%09private int queryCount = 1;%0D%0A%09%0A
 %09private SolverR
@@ -1798,15 +1798,125 @@
 %0D%0A%09%09
-push();
+/**%0D%0A%09%09 * Using assert+ and retract seems to be much more efficient than push%0D%0A%09%09 * and pop for some reason.%0D%0A%09%09 */%0D%0A
 %0D%0A%09%09
@@ -1928,16 +1928,17 @@
 %22(assert
++
  (not %22 
@@ -2014,21 +2014,69 @@
 )%22);%0D%0A%09%09
-pop()
+send(%22(retract %22 + queryCount + %22)%22);%0D%0A%09%09queryCount++
 ;%0D%0A%0D%0A%09%09S
@@ -2779,16 +2779,85 @@
 break;%0D%0A
+%09%09%09%09%7D else if (line.startsWith(%22unsat core ids%22)) %7B%0D%0A%09%09%09%09%09continue;%0D%0A
 %09%09%09%09%7D el

Use assert+ and retract for queries