import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.Model;
import choco.kernel.solver.Solver;
import choco.kernel.solver.ContradictionException;
import choco.kernel.solver.constraints.integer.AbstractLargeIntSConstraint;
import choco.kernel.solver.variables.integer.IntDomainVar;
import choco.kernel.memory.IStateInt;
import choco.kernel.memory.IStateIntVector;
import choco.kernel.memory.trailing.StoredInt;
import choco.kernel.memory.trailing.StoredIntVector;
import choco.kernel.model.variables.integer.IntegerExpressionVariable;
import choco.kernel.model.variables.integer.IntegerVariable;
import java.util.Stack;

//
// Clique Cost Constraint
// see Fahle ESA2002
// This uses a maintenance technique based on ac4
// An initial colouring is maintained, by downdating 
// saturations when a vertex is selected and removed from the
// candidate set. It is SLOOOOOOOOOOOOOOOOOOOOOOOOW
//

public class CliqueOptimize extends AbstractLargeIntSConstraint {  

    private IStateInt[] deg;        // number of vertices adjacent to v[i] in candidate set, reversible
    private IStateInt K;            // size of current clique, reversible
    private ReversibleVector P;     // set of candidates, reversible
    private int maxK;               // size of largest clique found so far
    private int n;                  // number of vertices
    private int[] solution;         // as it says ...
    private ReversibleVector[] adj; // adjacency list for each vertex
    private IStateInt[] candidate;  // candidate[i] = 1 <-> i \in P
    private int[][] A;              // adjacency matrix
    private int[] col;              // 0 <= col[i] < n, the colour of vertex i
    private int[] saturation;       // number of differently coloured vertices adjacent to vertex i
    private boolean[][] dom;        // domain of colours, dom[i][j] true <-> vertex i can have jth colour
    private int model;              // 1 -> simple, 2 -> Fahle, 3 -> Fahle + Brelaz
    private MonitorObject monitor;
    private IStateInt[][] revDom;   // reversible domain of colours
    private IStateInt[] revSatur;   // reversible saturation
	

    public CliqueOptimize(Solver s,IntDomainVar[] v,IStateInt[] deg,int[] saturation,int[] colour,ReversibleVector candidateSet,
			  int[] solution,int[][] A,int model,MonitorObject monitor) { 
	super(v);
	n               = v.length;
	this.deg        = deg; 
	K               = s.getEnvironment().makeInt(0);
	P               = candidateSet;
	maxK            = 0;
	this.solution   = solution;
	this.adj        = adj;
	this.A          = A;
	this.model      = model;
	this.monitor    = monitor;
	candidate       = new IStateInt[n];
	adj             = new ReversibleVector[n];
	col             = colour; //new int[n];
	this.saturation = saturation; //new int[n];
	dom             = new boolean[n][n];
	revDom          = new IStateInt[n][n];
	revSatur        = new IStateInt[n];
	for (int i=0;i<n;i++){
	    candidate[i] = s.getEnvironment().makeInt(1);
	    adj[i]       = new ReversibleVector(s);
	    col[i]       = -1;
	    revSatur[i]  =  s.getEnvironment().makeInt(0);
	    for (int j=0;j<n;j++){
		if (A[i][j] == 1) adj[i].add(j);
		dom[i][j] = true;
		revDom[i][j] = s.getEnvironment().makeInt(0);
	    }
	}
    }

    public boolean isSatisfied(){return true;}
    
    public void awake() throws ContradictionException {
	if (model > 1)
	    for (int i=0;i<n;i++) if (deg[i].get() == n-1) vars[i].setVal(1);
	brelaz();
	initializeReversibles();
    }
    //
    // if a vertex is adjacent to everything then it is in every possible clique
    //
    

    public void propagate() throws ContradictionException {}
    public void awakeOnInf(int idx) throws ContradictionException {}
    public void awakeOnSup(int idx) throws ContradictionException {}
    public void awakeOnRem(int idx,int x) throws ContradictionException {}

    private void saveSolution(){
	for (int i=0;i<n;i++) 
	    if (vars[i].isInstantiated() && vars[i].getVal() == 1) 
		solution[i] = 1;
	    else 
		solution[i] = 0;
    }

    private void initializeReversibles(){
	for (int k=0;k<P.size();k++){          // select from candidate set
	    int i = P.get(k);
	    for (int l=0;l<adj[i].size();l++){ // remove colour from adjacent vertices
		int j = adj[i].get(l);         // j is lth adjacent vertex to i
		if (revDom[j][col[i]].get() == 0) revSatur[j].add(1);
		revDom[j][col[i]].add(1);      // remove colour from domain of vertex j
	    }
	}
	for (int k=0;k<P.size();k++){ // select from candidate set
	    int i = P.get(k);
	    if (saturation[i] != revSatur[i].get()) System.out.println("blip1");
	}
    }

    private void removeColouredVertex(int i){
	for (int k=0;k<adj[i].size();k++){    // return colour if possible to adjacent vertices
	    int j = adj[i].get(k);            // j is kth adjacent vertex to i
	    revDom[j][col[i]].add(-1);        // one less colour thief
	    if (revDom[j][col[i]].get() < 0) System.out.println("blip2");
	    if (revDom[j][col[i]].get() == 0) // if colour is now free saturation falls
		revSatur[j].add(-1);
	    if (revSatur[j].get() < 0) System.out.println("blip3");
	    //int calcSatur = 0;
	    //for (int l=0;l<n;l++) if (revDom[j][l].get() > 0) calcSatur++;
	    //if (calcSatur != revSatur[j].get()) System.out.println("blip4");
	    saturation[j] = revSatur[j].get();
	}
    }
    
    private int getMaxSatur(){
	int maxSatur = -1;
	for (int k=0;k<P.size();k++){          // select from candidate set
	    int i = P.get(k);
	    maxSatur = Math.max(maxSatur,revSatur[i].get());
	}
	return maxSatur + 1;
    }
	

    private int selectMaxSaturatedUncolouredVertex(){
	int maxSaturation = -1,
	    maxDegree     = -1,
	    selected      = -1;
	for (int k=0;k<P.size();k++){ // select unColVar: uncoloured with maximum saturation, tie break on max degree
	    int i = P.get(k);
	    if (col[i] == -1)
		if (saturation[i] > maxSaturation || saturation[i] == maxSaturation && deg[i].get() > maxDegree){
		    maxSaturation = saturation[i];
		    maxDegree     = deg[i].get();
		    selected      = i;
		}
	}
	return selected;
    }
    //
    // Classic Brelaz
    //

    private int selectFirstUncolouredVertex(){
	for (int k=0;k<n;k++) if (col[k] == -1) return k;
	return -1;
    } 
    //
    // as a straw man
    //

    private int colourVertex(int i){
	for (int j=0;j<n;j++)              // get minimum colour for vertex i
	    if (dom[i][j]){col[i] = j; break;}
	for (int k=0;k<adj[i].size();k++){ // remove colour from adjacent vertices
	    int j = adj[i].get(k);         // j is kth adjacent vertex to i
	    if (dom[j][col[i]]){           // does j have same colour available?
		dom[j][col[i]] = false;    // remove colour from domain of vertex j
		saturation[j]++;           // increase saturation of vertex
	    }
	}
	return col[i];
    }

    
    private int brelaz(){
	int n = P.size();       // downsizing n, locally
	for (int k=0;k<n;k++){
	    int i         = P.get(k);
	    col[i]        = -1;
	    saturation[i] = 0;
	    for (int j=0;j<n;j++) dom[i][j] = true;
	}
	int maxCol = -1,
	    uncolouredVertex = -1;
	boolean uncolouredVertices = true;
	solver.getEnvironment().worldPush();
	while (uncolouredVertices){
	    //uncolouredVertex = selectFirstUncolouredVertex();
	    uncolouredVertex = selectMaxSaturatedUncolouredVertex();
	    if (uncolouredVertex > -1) maxCol = Math.max(maxCol,colourVertex(uncolouredVertex));
	    P.remove(uncolouredVertex);
	    uncolouredVertices = uncolouredVertex > -1;
	}
	solver.getEnvironment().worldPop();
	return maxCol + 1; // because 0 is a valid colour.
    }

    private void reject(int i) throws ContradictionException { // delete and reject vertex i
	//System.out.println("reject("+ i +") "+ vars[i] +" candidate = "+ candidate[i].get());
	if (candidate[i].get() == 0) return;
	if (!vars[i].isInstantiated()) vars[i].setVal(0);
	deg[i].set(0);
	P.remove(i);
	candidate[i].set(0);
	for (int k=0;k<adj[i].size();k++){
	    int j = adj[i].get(k); // j is an adjacent candidate vertex
	    deg[j].add(-1);
	    adj[j].remove(i);
	}
	removeColouredVertex(i);
    }
    

    private void select(int i) throws ContradictionException { // delete selected vertex i
	//System.out.println("select("+ i +") "+ vars[i] +" candidate = "+ candidate[i].get());
	if (candidate[i].get() == 0) return;
	if (!vars[i].isInstantiated()) vars[i].setVal(1);
	deg[i].set(0);
	P.remove(i);
	K.add(1); 
	candidate[i].set(0);
	if (K.get() > maxK){maxK = Math.max(maxK,K.get()); saveSolution();}
	Stack<Integer> S = new Stack<Integer>();
	for (int k=0;k<P.size();k++) S.push(P.get(k));
	while (!S.empty()){
	    int j = S.pop();
	    if (A[i][j] == 0) 
		reject(j);
	    else {
		deg[j].add(-1);
		adj[j].remove(i);
	    }
	}
	removeColouredVertex(i);
    }
    
    public void awakeOnInst(int i) throws ContradictionException {
	//System.out.println("awakeOnInst("+ vars[i] +") candidate = "+ candidate[i].get());
	//if (K.get() >= cliqueSize) return;
	if (candidate[i].get() == 1){
	    if (monitor != null) monitor.monitor();
	    if (vars[i].getVal() == 1) 
		select(i);
	    else
		reject(i);
	    boolean change = true;
	    Stack<Integer> S = new Stack<Integer>();
	    if (model > 1)
		while (change){
		    change = false;
		    for (int k=0;k<P.size();k++) S.push(P.get(k));
		    while (!S.empty()){
			int j = S.pop();
			if (deg[j].get() == P.size()-1 && !vars[j].isInstantiated()){
			    change = true;
			    select(j);
			}
			else if (deg[j].get() + K.get() < maxK){
			    change = true;
			    reject(j);
			}
		    }
		}
	    if (P.size() + K.get() <= maxK) fail();
	    if (model == 3){
		//int chromaticNumber = brelaz();
		int chromaticNumber = getMaxSatur();
		if (K.get() + chromaticNumber <= maxK) fail();
		for (int k=0;k<P.size();k++){
		    int j = P.get(k);
		    if (K.get() + saturation[j] + 1 < maxK) 
			vars[j].setVal(0);
		}
	    }
	}
    }
}