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

import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnValueReference;

/**
 * Substitute {@link ReturnValueReference}s in an {@link Expression} with another {@link Expression}.
 * 
 * @see ReturnValueReferenceSubstitution#substitute(VariableDeclaration, Expression)
 * @author fabian
 * 
 */
class ReturnValueReferenceSubstitution extends SubstitutionVisitor<Expression> {
	/**
	 * Substitutes {@link ReturnValueReference}s with the given {@link Expression}.
	 * 
	 * A clone of the <code>substitute</code> is used for substitution.
	 * 
	 * @param expression
	 *                the <code>Expression</code> to search for <code>ReturnValueReferences</code>
	 * @param substitute
	 *                the <code>Expression</code> <code>ReturnValueReferences</code> are substituted with
	 * @return the substituted <code>expression</code>, which differs from the passed <code>expression</code> when
	 *         the <code>expression</code> itself was an <code>ReturnValueReference</code>
	 */
	public static Expression substitute(final Expression expression, final Expression substitute) {
		final ReturnValueReferenceSubstitution substitutor = new ReturnValueReferenceSubstitution(substitute);
		expression.accept(substitutor);
		if (substitutor.getFound()) {
			substitutor.setFound(false);
			return substitutor.getSubstitute();
		}
		return expression;
	}

	/**
	 * 
	 * @param substitute
	 *                the {@link Expression} {@link ReturnValueReference}s are substituted with
	 */
	ReturnValueReferenceSubstitution(final Expression substitute) {
		super(substitute);
	}

	@Override
	public void visit(final ReturnValueReference returnValueReference) {
		this.setFound(true);
	}
}

@@ -99,91 +99,539 @@
 ast.
-Expression;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnValueReference
+ArrayFunction;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.ArrayFunctionAccess;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnValueReference;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCloneHelper;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCreatorHelper;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor
 ;%0A%0A/
@@ -931,16 +931,154 @@
 sion%3E %7B%0A
+%09/**%0A%09 * The %3Ccode%3EExpression%3C/code%3E %3Ccode%3EReturnValueReferences%3C/code%3E are substituted with.%0A%09 */%0A%09private final Expression substitute;%0A%0A
 %09/**%0A%09 *
@@ -2253,16 +2253,43 @@
 %09%09super(
+null);%0A%09%09this.substitute = 
 substitu
@@ -2290,17 +2290,16 @@
 bstitute
-)
 ;%0A%09%7D%0A%0A%09@
@@ -2377,16 +2377,833 @@
 ence) %7B%0A
+%09%09final Expression index = returnValueReference.getIndex();%0A%09%09if (index != null) %7B%0A%09%09%09this.substitute.accept(new HierarchialASTNodeVisitor() %7B%0A%09%09%09%09@Override%0A%09%09%09%09public void visit(final ArrayFunction arrayFunction) %7B%0A%09%09%09%09%09final ArrayFunctionAccess substitute = AstNodeCreatorHelper%0A%09%09%09%09%09                .createArrayFunctionAccess(index, arrayFunction);%0A%09%09%09%09%09ReturnValueReferenceSubstitution.this.setSubstitute(substitute);%0A%09%09%09%09%7D%0A%0A%09%09%09%09@Override%0A%09%09%09%09public void visit(final VariableReference variableReference) %7B%0A%09%09%09%09%09final VariableReference substitute = AstNodeCloneHelper%0A%09%09%09%09%09                .clone(variableReference);%0A%09%09%09%09%09substitute.setIndex(returnValueReference.getIndex());%0A%09%09%09%09%09ReturnValueReferenceSubstitution.this.setSubstitute(substitute);%0A%09%09%09%09%7D%0A%09%09%09%7D);%0A%09%09%7D else %7B%0A%09%09%09this.setSubstitute(this.substitute);%0A%09%09%7D%0A%0A
 %09%09this.s

Fix ReturnValueReferenceSubstitution ignores index access