//package de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2;

import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Map.Entry;

import org.apache.log4j.Logger;
import org.apache.log4j.SimpleLayout;
import org.apache.log4j.WriterAppender;

import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
import de.uni_freiburg.informatik.ultimate.logic.NoopScript;
import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException;
import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.smtinterpol.Config;

public class LraSolver extends NoopScript {

	private Logger m_Logger;
	private SimpleLayout m_Layout;
	private WriterAppender m_Appender;
	private PrintWriter m_Err = new PrintWriter(System.err);

	ArrayList<String> basics = new ArrayList<String>();
	ArrayList<String> nonBasics = null;
	
	HashMap<String,Double> bs = new HashMap<String,Double>();
	
	double[][] tab;
	double[] basicValues;
	double[] nonBasicValues;
	
	int varNr = 0;
	HashMap<String,Integer> variableOrdering = new HashMap<String,Integer>();
	
	String helpVarId = "%%y";//may not occur as (part of a) variable name in the SMTLIB file
	
	ArrayList<Double[]> tableau = new ArrayList<Double[]>();
	
	public LraSolver(Logger logger) {
		m_Logger = logger;
		m_Layout = new SimpleLayout();
		m_Appender = new WriterAppender(m_Layout, m_Err);
		m_Logger.addAppender(m_Appender);
		m_Logger.setLevel(Config.DEFAULT_LOG_LEVEL);
        reset();
	}

	@Override
	public void declareFun(String fun, Sort[] paramSorts, Sort resultSort)
			throws SMTLIBException {
		assert resultSort.toString().equals("Real") && paramSorts.length == 0;
		variableOrdering.put(fun, varNr++);
		super.declareFun(fun, paramSorts, resultSort);
	}

	@Override
	public LBool assertTerm(Term term) throws SMTLIBException {
		if (nonBasics == null) {
			nonBasics = new ArrayList<String>(variableOrdering.size());
			for (int i = 0; i < variableOrdering.size(); i++) {
				nonBasics.add("");
			}
			for (Entry<String,Integer> en : variableOrdering.entrySet()) {
				nonBasics.set(en.getValue(), en.getKey());
			}
		}
		
		assert term instanceof ApplicationTerm && 
			((ApplicationTerm) term).getParameters().length == 2;
		
		ApplicationTerm at = (ApplicationTerm) term;

		assert at.getFunction().getName() == "<="; 
		assert at.getParameters()[0] instanceof ApplicationTerm;

		Double[] tableauLine = new Double[nonBasics.size()];
		
		BoundConstr bound = readLeqTerm((ApplicationTerm) at.getParameters()[0], at.getParameters()[1]);
		String newY = helpVarId + basics.size();
		variableOrdering.put(newY, varNr++);
		basics.add(newY);
		
		for (int i = 0; i < bound.linearTerm.coefficients.size(); i++) {
			tableauLine[variableOrdering.get(bound.linearTerm.variables.get(i))] = 
					bound.linearTerm.coefficients.get(i);
		}
		
		tableau.add(tableauLine);
		bs.put(newY,bound.bound);
		
		return super.assertTerm(term);
	}

	private BoundConstr readLeqTerm(ApplicationTerm linTerm, Term constant) {
		LinearTerm aft = new LinearTerm();
		if (linTerm.getParameters().length == 0) {
			aft.addSummand(1d, linTerm.toString());
		} else if (linTerm.getFunction().getName() == "-" && linTerm.getParameters().length == 1) {
			aft.addSummand(-1d, linTerm.getParameters()[0].toString());
		} else if (linTerm.getFunction().getName() == "+") {
			for (Term summand : linTerm.getParameters()) {
				if (summand instanceof ApplicationTerm) {
					ApplicationTerm smnd = (ApplicationTerm) summand;
					if(smnd.getFunction().getName() == "*" && smnd.getParameters().length == 2 &&
							((ApplicationTerm) smnd.getParameters()[1]).getParameters().length == 0) {
						aft.addSummand(readDoubleFromTerm(smnd.getParameters()[0]), smnd.getParameters()[1].toString());
					} else if (smnd.getFunction().getName() == "-" && smnd.getParameters().length == 1 && 
							smnd.getParameters()[0] instanceof ApplicationTerm && 
							((ApplicationTerm) smnd.getParameters()[0]).getParameters().length == 0) {
						aft.addSummand(-1d, smnd.getParameters()[0].toString());
					} else if (smnd.getParameters().length == 0) {
						aft.addSummand(1d, smnd.toString());
					} else
						assert false;
				} else
					assert false;
			}
		} else {
			assert false;
		}
		return new BoundConstr(aft, readDoubleFromTerm(constant));
	}

	private Double readDoubleFromTerm(Term term) {
		Double toReturn = 0d;
		if (term instanceof ConstantTerm) {
			toReturn = Double.parseDouble(term.toString());
		} else if (term instanceof ApplicationTerm) {
			ApplicationTerm aterm = (ApplicationTerm) term;
			String func = aterm.getFunction().getName();
			if (func.equals("+")) 
				for (Term t : aterm.getParameters()) 
					toReturn += readDoubleFromTerm(t);
			else if (func.equals("-")) 
				for (Term t : aterm.getParameters()) 
					toReturn -= readDoubleFromTerm(t);
			else 
				assert false;
		} else {
			assert false;
		}
		return toReturn;
	}

	@Override
	public LBool checkSat() {
		LBool result = LBool.UNKNOWN;
		//LBool is the return type
		//use
		// LBool.SAT
		// LBool.UNSAT
		// in their obvious meaning

		int n = nonBasics.size();
		int m = basics.size();
		
		String[] nba = new String[n]; 
		String[] ba = new String[m];
		nonBasics.toArray(nba);
		basics.toArray(ba);
		
		tab = new double[m][n];
		for (int i = 0; i < m; i++)
			for (int j = 0; j < n; j++)
				tab[i][j] = tableau.get(i)[j] == null ? 0d : tableau.get(i)[j];
		
		//at this point all the values from the constraints 
		//are put into the initial tableau "tab"
		//the ArrayLists<String> "nonBasics"/"basics" contain the variable names
		//for each column/line
		//the HashMap<String,Double> "bs" contains the bound for each initially basic variable 
		//in the matrix (i.e. the pairs (y_i,b_i) in the lecture's notation)
		//all these data structures are supposed to be for your convenience, you may change them
		//if you do not like them
		
		
		//TODO: add decision procedure
		
		return result;
	}

	class LinearTerm {
		
		ArrayList<Double> coefficients = new ArrayList<Double>();
		ArrayList<String> variables = new ArrayList<String>();
		
		public void addSummand(Double coefficient, String variable) {
			coefficients.add(coefficient);
			variables.add(variable);
		}
		
		public String toString() {
			String toReturn = "";
			for (int i = 0; i < coefficients.size(); i++) {
				toReturn += coefficients.get(i) + "*" + variables.get(i) + " ";
			}
			return toReturn;
		}
	}
	
	class BoundConstr {
		LinearTerm linearTerm;
		Double bound;

		public BoundConstr(LinearTerm affineTerm, Double bound) {
			super();
			this.linearTerm = affineTerm;
			this.bound = bound;
		}
	}
}