package formulae.cltloc.converters;

import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;

import org.apache.commons.lang3.StringUtils;

import com.google.common.base.Preconditions;

import formulae.cltloc.CLTLocFormula;
import formulae.cltloc.atoms.BoundedVariable;
import formulae.cltloc.atoms.CLTLocClock;
import formulae.cltloc.atoms.Signal;
import formulae.cltloc.atoms.Variable;
import formulae.cltloc.visitor.CLTLoc2ZotVisitor;
import formulae.cltloc.visitor.GetBoundedVariablesVisitor;
import formulae.cltloc.visitor.GetClocksVisitor;
import formulae.cltloc.visitor.GetSignalVisitor;
import formulae.cltloc.visitor.GetVariablesVisitor;
import formulae.cltloc.visitor.ZotPlugin;

public class CLTLoc2zot implements Function<CLTLocFormula, String> {

	private final int bound;
	private final int maxConstant;

	private final ZotPlugin plugin;

	public CLTLoc2zot(int bound, ZotPlugin pluginName) {
		Preconditions.checkArgument(bound > 0, "The bound must be grather than zero");
		this.bound = bound;
		this.maxConstant = bound;
		this.plugin = pluginName;
	}

	public CLTLoc2zot(int bound, int maxConstant, ZotPlugin plugin) {
		Preconditions.checkArgument(bound > 0, "The bound must be grather than zero");
		this.bound = Math.max(10, bound);
		this.maxConstant = maxConstant;
		this.plugin = plugin;
	}

	public String apply(CLTLocFormula formula) {
		final StringBuilder builder = new StringBuilder();
		builder.append("(asdf:operate 'asdf:load-op '" + plugin + ")\n");

		builder.append("(use-package :trio-utils)\n");

		Set<CLTLocClock> clocks = formula.accept(new GetClocksVisitor());
		clocks.forEach(clock -> builder.append("(define-tvar " + clock.toString() + " *real*)\n"));

		Set<Signal> signals = formula.accept(new GetSignalVisitor());
		signals.forEach(signal -> builder.append("(define-tvar " + signal.toString() + " *real*)\n"));

		Set<Variable> variables = formula.accept(new GetVariablesVisitor());
		variables.forEach(variable -> builder.append("(define-tvar " + variable.toString() + " *int*)\n"));

		Set<BoundedVariable> boundedvariables=null;
		if (plugin.equals(ZotPlugin.AE2SBVZOT) || plugin.equals(ZotPlugin.AE2ZOT)) {
			boundedvariables = formula.accept(new GetBoundedVariablesVisitor());
			boundedvariables.forEach(variable -> {
				builder.append("(define-item " + variable.toString() + " '("
						+ StringUtils.join(variable.getValues(), ' ') + "))\n");
			});
		} else {
			Set<String> variablesString=variables.stream().map(v -> v.toString()).collect(Collectors.toSet());
			
			boundedvariables = formula.accept(new GetBoundedVariablesVisitor());
			boundedvariables.forEach(variable -> {
				if(!variablesString.contains(variable.toString())){
					builder.append("(define-tvar " + variable.toString() + " *int*)\n");
				}
			}
			);

		}

		// ae2sbvzot
		// ae2zot
		builder.append("(" + plugin + ":zot " + bound + " (&&" + formula.accept(new CLTLoc2ZotVisitor(plugin)) + ")\n\n"
				+ ":smt-lib :smt2 \n" + ":over-clocks " + maxConstant + "\n"
				+ ":logic :QF_UFLRA" + "\n" 
				+ ":gen-symbolic-val nil\n");

		if (plugin.equals(ZotPlugin.AE2SBVZOT) || plugin.equals(ZotPlugin.AE2ZOT)) {
			builder.append(":parametric-regions t\n");
			final StringBuilder footerBuilder = new StringBuilder();
			footerBuilder.append(":discrete-counters '(" + StringUtils.join(variables, ' ') + ")");
			builder.append(footerBuilder.toString() + "");
		}
		else{
			final StringBuilder footerBuilder = new StringBuilder();
			Set<String> variablesString=variables.stream().map(v -> v.toString()).collect(Collectors.toSet());
			variablesString.addAll(boundedvariables.stream().map(v -> v.toString()).collect(Collectors.toSet()));
			footerBuilder.append(":discrete-counters '(" + StringUtils.join(variablesString, ' ') + ")");
			builder.append(footerBuilder.toString() + "");
		}

		builder.append(")\n");

		return builder.toString();
	}
}
