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;

    public UMatrix(int m,Problem pb,Dict d,boolean best) {
        n = d.size();
	if (m < 1) m = n;
        this.m  = m;
	this.pb = pb;
	this.d = d;
	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);
		}
    } 
  
    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 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 + "? ";
	    }
	    s = s + "\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;
    }
	
}
