package edu.kit.iti.formal.pse.worthwhile.prover;

import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Stack;

import edu.kit.iti.formal.pse.worthwhile.model.ast.BinaryExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Literal;
import edu.kit.iti.formal.pse.worthwhile.model.ast.UnaryExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCloneHelper;
import edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor;

/**
 * A visitor to replace all {@link VariableDeclaration} with new instances with the same name and type.
 * 
 * @author Leon Handreke
 */
public class FreshVariableSetVisitor extends HierarchialASTNodeVisitor {

	/**
	 * Map old variables to the new, fresh variables.
	 * 
	 * Use a LinkedHashMap here because the ordering of the keys is stable, which is needed to make the results
	 * deterministic
	 */
	private Map<VariableDeclaration, VariableDeclaration> variableMap = new LinkedHashMap<VariableDeclaration, VariableDeclaration>();

	/**
	 * Stack to hand expressions back up the calling visit method.
	 */
	private Stack<Expression> substituteExpressionStack = new Stack<Expression>();

	/**
	 * A mapping from the substituted to the substitute {@link VariableDeclaration}s.
	 * 
	 * @return the mapping from old to new variables
	 */
	public final Map<VariableDeclaration, VariableDeclaration> getVariableMap() {
		return this.variableMap;
	}

	@Override
	public final void visit(final BinaryExpression b) {
		b.getLeft().accept(this);
		b.setLeft(this.substituteExpressionStack.pop());
		b.getRight().accept(this);
		b.setRight(this.substituteExpressionStack.pop());
		this.substituteExpressionStack.push(b);
	}

	@Override
	public final void visit(final Literal a) {
		this.substituteExpressionStack.push(a);
	}

	@Override
	public final void visit(final UnaryExpression u) {
		u.getOperand().accept(this);
		u.setOperand(this.substituteExpressionStack.pop());
		this.substituteExpressionStack.push(u);
	}

	@Override
	public final void visit(final VariableReference v) {
		if (!this.variableMap.containsKey(v.getVariable())) {
			// if the VariableDeclaration was first seen, create a new one with the same name
			VariableDeclaration newVariable = AstNodeCloneHelper.clone(v.getVariable());
			newVariable.setInitialValue(null);
			this.variableMap.put(v.getVariable(), newVariable);
		}
		// substitute the old VariableDeclaration with a fresh one
		v.setVariable(this.variableMap.get(v.getVariable()));

		this.substituteExpressionStack.push(v);
	}
}

@@ -101,32 +101,8 @@
 Map;
-%0Aimport java.util.Stack;
 %0A%0Aim
@@ -172,71 +172,8 @@
 on;%0A
-import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;%0A
 impo
@@ -1146,163 +1146,8 @@
 );%0A%0A
-%09/**%0A%09 * Stack to hand expressions back up the calling visit method.%0A%09 */%0A%09private Stack%3CExpression%3E substituteExpressionStack = new Stack%3CExpression%3E();%0A%0A
 %09/**
@@ -1446,330 +1446,178 @@
 nal 
-BinaryExpression b) %7B%0A%09%09b.getLeft().accept(this);%0A%09%09b.setLeft(this.substituteExpressionStack.pop());%0A%09%09b.getRight().accept(this);%0A%09%09b.setRight(this.substituteExpressionStack.pop());%0A%09%09this.substituteExpressionStack.push(b);%0A%09%7D%0A%0A%09@Override%0A%09public final void visit(final Literal a) %7B%0A%09%09this.substituteExpressionStack.push(a
+Literal literal) %7B%0A%09%09// do nothing for Literals%0A%09%7D%0A%0A%09@Override%0A%09public final void visit(final BinaryExpression b) %7B%0A%09%09b.getLeft().accept(this);%0A%09%09b.getRight().accept(this
 );%0A%09
@@ -1717,104 +1717,8 @@
 s);%0A
-%09%09u.setOperand(this.substituteExpressionStack.pop());%0A%09%09this.substituteExpressionStack.push(u);%0A
 %09%7D%0A%0A
@@ -2220,51 +2220,8 @@
 )));
-%0A%0A%09%09this.substituteExpressionStack.push(v);
 %0A%09%7D%0A

Simplify FreshVariableSetVisitor