//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 java.math.BigDecimal;
import java.math.BigInteger;

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;
import de.uni_freiburg.informatik.ultimate.logic.Rational;

public class LraSolverRationals 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,Rational> bs = new HashMap<String,Rational>();
	
	Rational[][] tab;
	Rational[] basicValues;
	Rational[] 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<Rational[]> tableau = new ArrayList<Rational[]>();
	
	public LraSolverRationals(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;

		Rational[] tableauLine = new Rational[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(Rational.ONE, linTerm.toString());
		} else if (linTerm.getFunction().getName() == "-" && linTerm.getParameters().length == 1) {
			aft.addSummand(Rational.MONE, 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(readRationalFromTerm(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(Rational.MONE, smnd.getParameters()[0].toString());
					} else if (smnd.getParameters().length == 0) {
						aft.addSummand(Rational.ONE, smnd.toString());
					} else
						assert false;
				} else
					assert false;
			}
		} else {
			assert false;
		}
		return new BoundConstr(aft, readRationalFromTerm(constant));
	}

	private Rational readRationalFromTerm(Term term) {
		Rational toReturn = Rational.ZERO;
		if (term instanceof ConstantTerm) {
			Object value = ((ConstantTerm) term).getValue();
			if (value instanceof Rational)
				toReturn = (Rational) ((ConstantTerm) term).getValue();
			else if (value instanceof BigInteger)
				toReturn = Rational.ONE.mul((BigInteger) value);
			else if (value instanceof BigDecimal) 
				toReturn = Rational.ONE.mul(((BigDecimal) value).unscaledValue())
						.div(Rational.ONE.mul(BigInteger.TEN.pow(((BigDecimal) value).scale())));
			else
				assert false;
		} else if (term instanceof ApplicationTerm) {
			ApplicationTerm aterm = (ApplicationTerm) term;
			String func = aterm.getFunction().getName();
			if (func.equals("+")) 
				for (Term t : aterm.getParameters()) 
					toReturn = toReturn.add(readRationalFromTerm(t));
			else if (func.equals("-")) 
				for (Term t : aterm.getParameters()) 
					toReturn = toReturn.sub(readRationalFromTerm(t));
			else 
				assert false;
		} else {
			assert false;
		}
		return toReturn;
	}

	@Override
	public LBool checkSat() {
		//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 Rational[m][n];
		for (int i = 0; i < m; i++)
			for (int j = 0; j < n; j++)
				tab[i][j] = tableau.get(i)[j] == null ? Rational.ZERO : tableau.get(i)[j];
		
		nonBasicValues = new Rational[n];
		for (int i = 0; i < n; i++) 
			nonBasicValues[i] = Rational.ZERO;

		basicValues = new Rational[m];
		for (int i = 0; i < m; i++) 
			basicValues[i] = Rational.ZERO;
		
		//at this point all the values from the constraints 
		//are stored in the initial tableau "tab"
		//the ArrayLists<String> "nonBasics"/"basics" contain the variable names
		//for each column/line
		//for their values there are arrays (non)BasicValues 
		//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 and helper methods are supposed to be for your convenience, you may change them
		//if you do not like them
		
		//Note: should you run into an assertion Error in your execution, probably the smt2-file contains
		// some syntax which can not (yet) be parsed -> either stick to the given syntax or just add
		// the case in the above code.
		
		
		//TODO: add decision procedure
		
		return LBool.UNKNOWN;
	}
	
	private boolean isInitiallyBasic(String var) {
		if(var.startsWith(helpVarId))
			return true;
		else
			return false;
	}

	public String printTableau(ArrayList<Rational[]> tableau) {
		StringBuilder toReturn = new StringBuilder();
		
		for (Rational[] line : tableau) {
			for (int i = 0; i < line.length; i++) {
				toReturn.append(line[i] + "\t");
			}
			toReturn.append("\n");
		}
		
		return toReturn.toString();
	}
	
	public String printTableau(Rational[][] tableau) {
		StringBuilder toReturn = new StringBuilder();
		
		for (int i = 0; i < tableau.length; i++) {
			Rational[] line = tableau[i];
			for (int j = 0; j < line.length; j++) {
				toReturn.append(/*trimRational(*/line[j] + "\t");
			}
			toReturn.append("\n");
		}
		
		return toReturn.toString();
	}
	
	public String printArray(Rational[] array) {
		StringBuilder sb = new StringBuilder();
		for (int i = 0; i < array.length; i++) {
			sb.append(array[i] + " ");
		}
		return sb.toString();
	}
	
	class LinearTerm {
		
		ArrayList<Rational> coefficients = new ArrayList<Rational>();
		ArrayList<String> variables = new ArrayList<String>();
		
		public LinearTerm() {
			
		}
		
		public void addSummand(Rational 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;
		Rational bound;

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