<commit_before>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);
		}<commit_msg>Use assert+ and retract for queries<commit_after>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 int queryCount = 1;
	
	private SolverResult query(String str) {
		/**
		 * Using assert+ and retract seems to be much more efficient than push
		 * and pop for some reason.
		 */

		send("(assert+ (not " + str + "))");
		send("(check)");
		send("(echo \"" + DONE + "\\n\")");
		send("(retract " + queryCount + ")");
		queryCount++;

		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 if (line.startsWith("unsat core ids")) {
					continue;
				} 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);
		}
{'fraction_non_alphanumeric': 0.1329177897574124, 'fraction_numerical': 0.00016846361185983828, 'mean_word_length': 3.8229082047116165, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5881130', 'n_tokens_mistral': 2197, 'n_tokens_neox': 1904, 'n_words': 485}