Main {
  public static void main(String args[]) throws Exception {{
	ClassGraph cg = new ClassGraph(true,false);
	CSP csp = CSP.parse(System.in);
	
	//Create a copy using DemeterJ generated CopyVisitor
	CSP csp0 = csp.copy();
	
	//get the variable assignment
	Literal l = (Literal)cg.fetch(csp,"from CSP via Preamble to Literal");
	Ident lit = (Ident)cg.fetch(l,"from Literal to edu.neu.ccs.demeter.Ident");
	boolean literalValue = l instanceof Pos; //Bad!! should add method get value to Literal
	ReductionVisitor rv = new ReductionVisitor(lit.toString(),literalValue);
	cg.traverse(csp,"from CSP to *",rv);
	
	//print using DemeterJ generated PrintVisitor
	System.out.println("\nCSP Before reduction:");
	csp0.print();
	System.out.println("\nCSP after reduction:");
	csp.print();
	
  }}
}

CSP{
    traversal toAll(UniversalVisitor) {
	to *;
	}
    
    //Use DemeterJ Generated PrintVisitor
    public void print(){{
	PrintVisitor pv = new PrintVisitor(System.out);
	pv.start();
	toAll(pv);
	pv.finish();
    }}

    //Use DemeterJ Generated CopyVisitor
    CSP copy(){{
	CopyVisitor cv = new CopyVisitor(CSP.class);
	cv.start();
	toAll(cv);
	cv.finish();
	return ((CSP)cv.get_return_val());
    }}
}

ReductionVisitor{
	{{
	String var; //name of the variable to be reduced
	Boolean val; //value of the variable to be reduced
	
	Boolean sat; //is the current constraint sat?
	Boolean neg; //is the current Literal negated?
	Boolean skip; //should we skip the current literal?
	int w; //weight of the current constraint

	Constraint_List constraints; //To hold the updated set of constraints
	Literal_List literals; //To hold the updated set of literals of the current constraints

	//Create a new visitor to reduce the CSP assuming that "var" has the value "val"
	public ReductionVisitor(String var, Boolean val){
		this.var = var;
		this.val = val;
	}

	public void before(CSP host){
		constraints = new Constraint_List();
	}

	public void before(Constraint host){
		literals = new Literal_List();
		sat = false;
	}

	public void before(Satisfied host){
		sat = true;
	}

	public void before(Unsatisfied host){
		sat = false;
	}

	public void before(Neg host){
		neg = true;
	}

	public void before(Pos host){
		neg = false;
	}

	public void before(Weight host){
		w = host.get_v();
	}

	public void before(Variable host){
		if(host.get_v().toString().equals(var)){
			//check if a literal is true
			if(neg!=val){ // !neg&val || neg&!val
				//constraint becomes sat
				sat = true;
			}
			//either literal becomes true or false it won't be copied to output
			skip = true;
		}else{
			//just copy the literal to output
			skip = false;
		}
	}

	public void after(Literal host){
		if(!skip&&!sat){
			literals.addElement(host);		
		}
	}

	public void after(Constraint host){
		if (sat){
			//sat
			constraints.addElement(new Satisfied(new Weight(w)));
		}else if (literals.size()==0){
			//Unsat
			constraints.addElement(new Unsatisfied(new Weight(w)));
		}else{
			//ProperConstraint
			constraints.addElement(new ProperConstraint(new Weight(w),new RelationName(),literals));
		}
	}

	public void after(CSP host){
		host.set_constraints(constraints);
	}

	}}
}