import java.util.HashMap;
import java.util.Iterator;
import java.util.Vector;

class Check{
	/**
	 * Checks if all constraints have been satisfied
	 * 
	 * @param csp
	 * 			the CSP instance to check
	 * 
	 * @return truth value of check
	 */
	public static boolean checkSAT(CSP csp){
		for (int i=0;i<csp.num_rel;i++){
			Rel3 rel = (Rel3)csp.relations.get(i);
			int relationNumber=rel.number;
			if (csp.assignment.get(new Integer(rel.x))!=null)
				relationNumber=Relation1.reduce(rel.number,2,((Integer)csp.assignment.get(new Integer(rel.x))).intValue());
			if (csp.assignment.get(new Integer(rel.y))!=null)
				relationNumber=Relation1.reduce(relationNumber,1,((Integer)csp.assignment.get(new Integer(rel.y))).intValue());
			if (csp.assignment.get(new Integer(rel.z))!=null)
				relationNumber=Relation1.reduce(relationNumber, 0, ((Integer)csp.assignment.get(new Integer(rel.z))).intValue());
			
			if (relationNumber!=255) return false;
		}
		
		return true;
	}
	
	/**
	 * returns the number of constraints satisfied at the current time
	 * 
	 * @param assignment
	 * 			the current partial assignment
	 * 
	 * @param csp
	 * 			the CSP instance to check
	 * 
	 * @return number of SAT constr
	 */
	
	public static int checkMAXSAT(HashMap assignment, CSP csp){
		
		int sat=0;
		
		for (int i=0;i<csp.num_rel;i++){
			Rel3 rel = (Rel3)csp.relations.get(i);
			int relationNumber=rel.number;
			if (assignment.get(new Integer(rel.x))!=null)
				relationNumber=Relation1.reduce(rel.number,2,((Integer)assignment.get(new Integer(rel.x))).intValue());
			if (assignment.get(new Integer(rel.y))!=null)
				relationNumber=Relation1.reduce(relationNumber,1,((Integer)assignment.get(new Integer(rel.y))).intValue());
			if (assignment.get(new Integer(rel.z))!=null)
				relationNumber=Relation1.reduce(relationNumber, 0, ((Integer)assignment.get(new Integer(rel.z))).intValue());
			
			if (relationNumber==255) sat+=rel.weight; 
		}
		
		return sat;
	}
	
	/**
	 * Returns nr constraints unsatisfied at the current time
	 * 
	 * @param partialAssignment
	 * 			the partial assignment to check for UNSAT constr
	 * 
	 * @param csp
	 * 			the CSP instance to check
	 */
	
	public static int checkUnsat(HashMap partialAssignment, CSP csp){
		int unsat=0;

		for (int i=0;i<csp.num_rel;i++){
			Rel3 rel = (Rel3)csp.relations.get(i);
			int relationNumber=rel.number;
			if (partialAssignment.get(new Integer(rel.x))!=null){
				relationNumber=Relation1.reduce(relationNumber,2,((Integer)partialAssignment.get(new Integer(rel.x))).intValue());
			}
			if (partialAssignment.get(new Integer(rel.y))!=null){
				relationNumber=Relation1.reduce(relationNumber,1,((Integer)partialAssignment.get(new Integer(rel.y))).intValue());
			}
			if (partialAssignment.get(new Integer(rel.z))!=null){
				relationNumber=Relation1.reduce(relationNumber, 0, ((Integer)partialAssignment.get(new Integer(rel.z))).intValue());
			}
			if (relationNumber==0) unsat+=rel.weight; 
			
			
		}
		
		return unsat;
	}
	
	/**
	 * compute subtracted added pairs
	 * 
	 * @param initial
	 * 			is it the first pair computation or not
	 * 
	 * @param csp
	 * 			the CSP instance for which to compute (relation, fraction) pair
	 * 
	 */
	
	public static void computePairs(boolean initial, CSP csp){
		
		HashMap pairsaux=new HashMap();
		
		
		for (int i=0;i<csp.num_rel;i++){
			//System.out.println(i+" "+test.num_rel);
			Rel3 rel = (Rel3)csp.relations.get(i);
			int relationNumber=rel.number;
			if (csp.assignment.get(new Integer(rel.x))!=null)
				relationNumber=Relation1.reduce(relationNumber,2,((Integer)csp.assignment.get(new Integer(rel.x))).intValue());
			if (csp.assignment.get(new Integer(rel.y))!=null)
				relationNumber=Relation1.reduce(relationNumber,1,((Integer)csp.assignment.get(new Integer(rel.y))).intValue());
			if (csp.assignment.get(new Integer(rel.z))!=null)
				relationNumber=Relation1.reduce(relationNumber, 0, ((Integer)csp.assignment.get(new Integer(rel.z))).intValue());
			
			if (pairsaux.containsKey(new Integer(relationNumber))){
				int k=((Integer)pairsaux.get(new Integer(relationNumber))).intValue();
				pairsaux.put(new Integer(relationNumber),new Integer(k+rel.weight));
			}
			else{
				pairsaux.put(new Integer(relationNumber),new Integer(rel.weight));
			}
			
		}
		if (initial){
			csp.pairs=new Vector();
			Iterator it=pairsaux.keySet().iterator();
			
			while (it.hasNext()){
				Integer relnum=(Integer)it.next();
				Integer fraction=(Integer)pairsaux.get(relnum);
			
				csp.pairs.add(new Pair(relnum.intValue(), fraction.intValue()*1.0/csp.total_nr));
			}
		}
		else{
			csp.subtractedPairs=csp.getPairs();
			csp.addedPairs.clear();
			
			Iterator it=pairsaux.keySet().iterator();
			
			while (it.hasNext()){
				Integer relnum=(Integer)it.next();
				Integer fraction=(Integer)pairsaux.get(relnum);
			
				csp.addedPairs.add(new Pair(relnum.intValue(), fraction.intValue()*1.0/csp.total_nr));
			}
			
		}
		
	}
	
	/**
	 * 
	 * @param currentAssignment
	 * 			the current variable partial assignment
	 * 
	 * @param decides
	 * 			an array representing an or between variables
	 * 
	 * @return true if the current partial assignment makes the array unsatisfied
	 * 
	 */
	
	public static boolean unsatisfies(HashMap currentAssignment,Vector decides){
		int unsatisf=0;
		
		for (int p=0;p<decides.size();p++){
			VarAssign var_assign=(VarAssign)decides.get(p);
			
			if (currentAssignment.get(var_assign.getVar())!=null){
				if (((Integer)currentAssignment.get(var_assign.getVar())).equals((Integer)var_assign.getAssign())) return false;
				else unsatisf++;
			}
			else{
				return false;
			}
		}
		
		if (unsatisf==decides.size() && decides.size()>0) return true;
		return false;
	}
	
	/**
	 * 
	 * @param v_a
	 * 			a <variable,assignment> object
	 * 
	 * @param csp
	 * 			the current CSP instance
	 * 
	 * @return true if we can perform a decide with the specified VarAssign
	 */

	public static boolean canDecide(VarAssign v_a,CSP csp){
		HashMap currentAssignment=new HashMap(csp.assignment);
		currentAssignment.put(v_a.getVar(), v_a.getAssign());
		for (int i=0;i<csp.superresolution.size();i++){
			Vector decide=(Vector)csp.superresolution.get(i);
			if (unsatisfies(currentAssignment,decide)){
				System.out.println("Unsatisfied");
				return false;
			}
			else{
			}
		}
		return true;
	}
}