import choco.Problem;
import choco.Constraint;
import choco.Solver;
import choco.Solution;
import choco.ContradictionException;
import choco.integer.*;

import java.io.*;
import java.lang.*;
import java.util.*;

public class UMatrix {
    private int n,m;
    private IntDomainVar M[][];
    private Problem pb;
    private Dict d;
    private Vector constraints;
    private Vector optVars;

    public UMatrix(int m,Problem pb,Dict d,boolean best) {
        n = d.size();
        this.m  = m;
	this.pb = pb;
	this.d = d;
	constraints = new Vector();
	optVars     = new Vector();
	M = new IntDomainVar[n][n];
	for (int i=0;i<n;i++) M[i][i] = null;
	for (int i=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++){
		String s = "M[" + i + "][" + j + "]";
		M[i][j] = pb.makeBoundIntVar(s,1,m);
		M[j][i] = M[i][j];
	    }
	/*
	for (int i=0;i<n-2;i++)
	    for (int j=i+1;j<n-1;j++)
		for (int k=j+1;k<n;k++){
		    IntDomainVar ab = M[i][j];
		    IntDomainVar ac = M[i][k];
		    IntDomainVar bc = M[j][k];
		   
		    //Constraint U1 = pb.and(pb.eq(ab,ac),pb.and(pb.gt(bc,ac),pb.gt(bc,ab)));
		    //Constraint U2 = pb.and(pb.eq(ab,bc),pb.and(pb.gt(ac,bc),pb.gt(ac,ab)));
		    //Constraint U3 = pb.and(pb.eq(ac,bc),pb.and(pb.gt(ab,bc),pb.gt(ab,ac)));
		    //Constraint U4 = pb.and(pb.eq(ab,ac),pb.and(pb.eq(ac,bc),pb.eq(ab,bc)));
		    //Constraint U5 = pb.or(U1,pb.or(U2,pb.or(U3,U4)));		    
		    //pb.post(U5);
		    //Constraint U5 = pb.card(new Constraint[]{U1,U2,U3,U4},pb.makeConstantIntVar(1));
		    //pb.post(U5);		    
		    
		    pb.post(new BACUM(ab,ac,bc,false));
		}
	*/
	pb.post(new AC3BACMatrix(M,false));
    } 
  
    public Problem getProblem(){return pb;}
    public int getN(){return n;}
    public IntDomainVar [][] getM(){return M;}
    public IntDomainVar getVar(int i,int j){return M[i][j];}
    public int numbConstraints(){return constraints.size();}

    public IntDomainVar []  getOptVars(){
	int n = optVars.size();
	IntDomainVar [] D = new IntDomainVar[n];
	for (int i=0;i<n;i++) D[i] = (IntDomainVar)optVars.get(i);
	return D;
    }


    public IntDomainVar [] getDecisionVars(){
	int n = d.size();
	IntDomainVar [] D = new IntDomainVar [n*(n-1)/2];
	int k = 0;
	for (int i=0;i<n-1;i++)
	    for (int j=i+1;j<n;j++){
		D[k] = M[i][j];
		k++;
	    }
	//for (int i=0;i<k;i++) System.out.println(D[i].pretty());
	return D;
    }

    public void addTriple(Triple t1){
	boolean found = false;
	int i = 0;
	while (!found && i<constraints.size()){
	    Triple t2 = (Triple)constraints.get(i);
	    if (t1.equalFans(t2) || t1.equalTriples(t2)){
		//System.out.println("Duplicates: " + t1 + " " + t2);
		found = true;
	    }
	    else i++;
	}
	//constraints.add(t1);
	//optVars.add(t1.getVar());
	if (!found) {
	    constraints.add(t1);
	    optVars.add(t1.getVar());
	}
    }
	    

    public void showTriples(){
	for (int i=0;i<constraints.size();i++) System.out.println((Triple)constraints.get(i));
    }

    public void postTriples() throws ContradictionException {
	for (int i=0;i<constraints.size();i++) ((Triple)constraints.get(i)).post();
    }

    public ArrayList getTriples(Tree t){
	ArrayList A = new ArrayList();
	int n = constraints.size();
	for (int i=0;i<n;i++){
	    Triple t2 = (Triple)constraints.get(i);
	    if (t.equals(t2.getTree())) A.add(t2);}
	return A;
    }

    public ArrayList getTriples(){
	ArrayList A = new ArrayList();
	int n = constraints.size();
	for (int i=0;i<n;i++){
	    Triple t = (Triple)constraints.get(i);
	    A.add(t);
	}
	return A;
    }

    public String toString(){
	String s = "n: " + n + " m: " + m + "\n";
	for (int i=0;i<n;i++){
	    for (int j=0;j<n;j++){
		if (i == j) s = s + 0 + " ";
		else if (M[i][j].isInstantiated()) s = s + M[i][j].getVal() + " ";
		else s = s + "[" + M[i][j].getInf() + "," + M[i][j].getSup() + "]";
	    }
	    s = s + "\n";
	}
	for (int i=0;i<constraints.size();i++) s = s + ((Triple)constraints.get(i)) + "\n";
	return s;
    }

    private TreeSet cluster(int i,int v,TreeSet leafs){
	TreeSet S = new TreeSet();
	Iterator setIter = leafs.iterator();
	while (setIter.hasNext()) {
	    int j = ((Integer)setIter.next()).intValue();
	    if (M[i][j].getInf() == v) S.add(new Integer(j));
	}
	return S;
    }
    //
    // return all leaf nodes (index of) j  such that mrca(i,j) = v
    //

    
    private TreeSet mrcaValues(int i,TreeSet leafs) {
	TreeSet S = new TreeSet(new IntVarCompare());
	Iterator setIter = leafs.iterator();
	while (setIter.hasNext()) {
	    int j = ((Integer)setIter.next()).intValue();
	    S.add(M[i][j]);
	}
	//System.out.println(i + ": " + S);
	return S;
    }
    //
    // given row i of the matrix and a set of leafs
    // deliver the set of most recent common ancestors v
    // where v = mrca(i,j) and j is in leafs
    // {v | mrca(i,j)=v & j in leafs}
    //

    private void toTree(TreeSet leafs,Node N,Tree t){
	//System.out.println("toTree(" + leafs + ")");
	Integer x = (Integer)leafs.first();
	leafs.remove(x);
	int i = x.intValue();
	TreeSet S = mrcaValues(i,leafs);
	Iterator setIter = S.iterator();
	while (setIter.hasNext()) {
	    IntDomainVar y = (IntDomainVar)setIter.next();
	    int j = y.getInf();
	    N = N.interiorNode(y,t);
	    toTree(cluster(i,j,leafs),N,t);
	}
	N.leafNode(m+1,i,d,t);
    }

    public Tree toTree(){
	TreeSet leafs = new TreeSet();
	for (int i=0;i<n;i++) leafs.add(new Integer(i));
	Tree T = new Tree();
	Node N = new Node();
	toTree(leafs,N,T);
	T.setRoot(N.getChildren().elementAt(0));
	return T;
    }


    public void predates(String v,String w, String x,String y) throws ContradictionException {
	int i = d.indexOf(v);
	int j = d.indexOf(w);
	int k = d.indexOf(x);
	int l = d.indexOf(y);
	pb.post(pb.lt(M[i][j],M[k][l]));
    }
    //
    // div(v,w) < div(x,y)
    //
	
}