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;

public class FreshVariableSetVisitor extends HierarchialASTNodeVisitor {

	private Map<VariableDeclaration, VariableDeclaration> variableMap = new LinkedHashMap<VariableDeclaration, VariableDeclaration>();

	private Stack<Expression> substituteExpressionStack = new Stack<Expression>();

	public Map<VariableDeclaration, VariableDeclaration> getVariableMap() {
		return this.variableMap;
	}

	@Override
	public 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 void visit(final Literal a) {
		this.substituteExpressionStack.push(a);
	}

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

	@Override
	public 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);
	}
}

@@ -692,81 +692,415 @@
 r;%0A%0A
-public class FreshVariableSetVisitor extends HierarchialASTNodeVisitor %7B%0A
+/**%0A * A visitor to replace all %7B@link VariableDeclaration%7D with new instances with the same name and type.%0A * %0A * @author Leon Handreke%0A */%0Apublic class FreshVariableSetVisitor extends HierarchialASTNodeVisitor %7B%0A%0A%09/**%0A%09 * Map old variables to the new, fresh variables.%0A%09 * %0A%09 * Use a LinkedHashMap here because the ordering of the keys is stable, which is needed to make the results%0A%09 * deterministic%0A%09 */
 %0A%09pr
@@ -1229,16 +1229,90 @@
 on%3E();%0A%0A
+%09/**%0A%09 * Stack to hand expressions back up the calling visit method.%0A%09 */%0A
 %09private
@@ -1385,22 +1385,176 @@
 n%3E();%0A%0A%09
-public
+/**%0A%09 * A mapping from the substituted to the substitute %7B@link VariableDeclaration%7Ds.%0A%09 * %0A%09 * @return the mapping from old to new variables%0A%09 */%0A%09public final
  Map%3CVar
@@ -1653,32 +1653,38 @@
 verride%0A%09public 
+final 
 void visit(final
@@ -1923,32 +1923,38 @@
 verride%0A%09public 
+final 
 void visit(final
@@ -2024,32 +2024,38 @@
 verride%0A%09public 
+final 
 void visit(final
@@ -2226,16 +2226,22 @@
 %09public 
+final 
 void vis
@@ -2276,16 +2276,17 @@
 ) %7B%0A%09%09if
+ 
 (!this.v

Comment and clean up FreshVariableSetVisitor