package solvers;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.PrintStream;
import java.nio.file.Files;
import java.util.concurrent.TimeUnit;

import com.google.common.base.Stopwatch;

import formulae.cltloc.CLTLocFormula;
import formulae.cltloc.converters.CLTLoc2zot;
import formulae.cltloc.visitor.CLTLoc2StringVisitor;
import formulae.cltloc.visitor.CLTLocGetMaxBound;
import formulae.cltloc.visitor.ZotPlugin;
import zotrunner.ZotException;
import zotrunner.ZotRunner;

public class CLTLocsolver {
	private final CLTLocFormula formula;
	private final PrintStream out;
	private final int bound;

	private float checkingtime;

	private double checkingspace;

	private long cltloc2zottime;

	private long sattime;

	public CLTLocsolver(CLTLocFormula formula, PrintStream out, int bound) {

		this.formula = formula;
		this.out = out;
		this.bound = bound;

	}

	public boolean solve() throws IOException, ZotException {
		Stopwatch timer = Stopwatch.createUnstarted();
		timer.start();
		out.println("Converting the CLTLoc formula in zot");

		// String zotEncoding = new CLTLoc2Ae2sbvzot(bound).apply(formula);

		
		File f = new File("solver.txt");
		ZotPlugin p = null;
		if (f.exists()) {
			BufferedReader reader = new BufferedReader(new FileReader(f));
			String solver = reader.readLine();
			p = ZotPlugin.valueOf(solver.toUpperCase());
			reader.close();
		} else {
			p = ZotPlugin.AE2ZOT;
		}

		String zotEncoding = new CLTLoc2zot(bound, formula.accept(new CLTLocGetMaxBound()), p).apply(formula);
		timer.stop();
		cltloc2zottime = timer.elapsed(TimeUnit.MILLISECONDS);

		out.println("Formula converted in zot");
		timer.reset();
		timer.start();

		ZotRunner zotRunner = new ZotRunner(zotEncoding, out);
		boolean sat = zotRunner.run();

		timer.stop();
		this.sattime = zotRunner.getSatTime();
		this.checkingspace = zotRunner.getCheckingspace();
		this.checkingtime = zotRunner.getCheckingtime();

		return sat;
	}

	public long getSattime() {
		return sattime;
	}

	public long getCltloc2zottime() {
		return cltloc2zottime;
	}

	public float getCheckingtime() {
		return checkingtime;
	}

	public double getCheckingspace() {
		return checkingspace;
	}
}
