// ** This file was generated with DemFGen (vers:4/15/2011)

package csp;

import edu.neu.ccs.demeterf.lib.*;
import edu.neu.ccs.demeterf.lib.*;
import scg.*;
import java.util.Iterator;





/** Representation of CSPInstance */
public class CSPInstance implements InstanceI{
    protected List<Var> vars;
    protected Cons<Clause> clauses;

    /** Construct a(n) CSPInstance Instance */
    public CSPInstance(List<Var> vars, Cons<Clause> clauses){
        this.vars = vars;
        this.clauses = clauses;
    }
    /** Is the given object Equal to this CSPInstance? */
    public boolean equals(Object o){
        if(!(o instanceof CSPInstance))return false;
        if(o == this)return true;
        CSPInstance oo = (CSPInstance)o;
        return (((Object)vars).equals(oo.vars))&&(((Object)clauses).equals(oo.clauses));
    }
    /** Parse an instance of CSPInstance from the given String */
    public static CSPInstance parse(String inpt) throws csp.ParseException{
        return new csp.TheParser(new java.io.StringReader(inpt)).parse_CSPInstance();
    }
    /** Parse an instance of CSPInstance from the given Stream */
    public static CSPInstance parse(java.io.InputStream inpt) throws csp.ParseException{
        return new csp.TheParser(inpt).parse_CSPInstance();
    }
    /** Parse an instance of CSPInstance from the given Reader */
    public static CSPInstance parse(java.io.Reader inpt) throws csp.ParseException{
        return new csp.TheParser(inpt).parse_CSPInstance();
    }

    /** Field Class for CSPInstance.vars */
    public static class vars extends edu.neu.ccs.demeterf.Fields.any{}
    /** Field Class for CSPInstance.clauses */
    public static class clauses extends edu.neu.ccs.demeterf.Fields.any{}
 
	public double valid(SolutionI solution, Config config){
		CSPSolution cspSolution = (CSPSolution) solution;
		if(cspSolution.getAssign().size() != getVars().length())
			return 0;
		boolean isValid = true;
		for(Iterator<Var> vars = getVars().iterator(); vars.hasNext();){
			isValid &= cspSolution.getAssign().containsKey(vars.next());
		}
		if(isValid)
			return 1;
		else 
			return 0;
	}
	public double quality(SolutionI solution){
		CSPSolution cspSolution = (CSPSolution) solution;
		List<Entry<Var, Boolean>> s = cspSolution.getAssign().toList();
		List<Clause> list = getClauses();
		List<Clause> reduced = s.fold(new List.Fold<Entry<Var,Boolean>,List<Clause>>(){
            public List<Clause> fold(Entry<Var,Boolean> a, List<Clause> p){
                return reduce(p, a.getKey(), a.getVal());
            }
        },list);
        return satisfiedRatio(reduced);
	}
	
	/** Reduce a given Problem based on a single Literal assignment */
    public static List<Clause> reduce(List<Clause> clauses, final Var var, final boolean val){
    	return clauses.map(new List.Map<Clause, Clause>() {
    		public Clause map(Clause c){
    			int i = c.getVars().index(var);
                if(i < 0 || (c.getRelnum() == 255))return c;
                return new Clause(new Relation(3, c.getRelnum())
                                     .reduce(i, val?1:0),1, c.getVars());
    		}
		});
        
    }

    /** Calculate the satifaction ratio of a (reduced) Problem */
    public static double satisfiedRatio(List<Clause> clauses){
        return clauses.fold(new List.Fold<Clause,R>(){
            public R fold(Clause c, R r)
            { return r.add((c.getRelnum() == 255)?c.getWeight():0, c.getWeight()); }
        }, new R(0,0)).result();
    }
    
    /** Accumulation for the satisfaction ratio */
    static class R{
        double top, bot;
        R(double t, double b){ top = t; bot = b; }
        R add(int t, int b){ return new R(top+t, bot+b); }
        double result(){ return bot==0.0?1.0:top/(double)bot; }
    }
	

    /** DGP method from Class Display */
    public String display(){ return csp.Display.DisplayM(this); }
    /** DGP method from Class Print */
    public String print(){ return csp.Print.PrintM(this); }
    /** DGP method from Class ToStr */
    public String toStr(){ return csp.ToStr.ToStrM(this); }
    /** DGP method from Class PrintToString */
    public String toString(){ return csp.PrintToString.PrintToStringM(this); }
    /** DGP method from Class HashCode */
    public int hashCode(){ return csp.HashCode.HashCodeM(this); }
    /** Setter for field CSPInstance.vars */
    public void setVars(List<Var> _vars){ vars = _vars; }
    /** Setter for field CSPInstance.clauses */
    public void setClauses(Cons<Clause> _clauses){ clauses = _clauses; }
    /** Getter for field CSPInstance.vars */
    public List<Var> getVars(){ return vars; }
    /** Getter for field CSPInstance.clauses */
    public Cons<Clause> getClauses(){ return clauses; }

}