<commit_before>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.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;

/**
 * Substitute {@link VariableReference}s in an {@link Expression} with another {@link Expression}.
 * 
 * @see VariableReferenceSubstitution#substitute(VariableDeclaration, Expression)
 * @author fabian
 * 
 */
class VariableReferenceSubstitution extends SubstitutionVisitor<Expression> {
	/**
	 * Substitutes occurrences of a {@link VariableDeclaration} in an {@link Expression} with another
	 * <code>Expression</code>.
	 * 
	 * A clone of the <code>substitute</code> is used for substitution.
	 * 
	 * @param expression
	 *                the <code>Expression</code> to search for occurrences of <code>variable</code>
	 * @param variable
	 *                the <code>VariableDeclaration</code> the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the <code>Expression</code> occurrences of <code>variable</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 occurrence of <code>variable</code>
	 */
	public static Expression substitute(final Expression expression, final VariableDeclaration variable,
	                final Expression substitute) {
		final VariableReferenceSubstitution substitutor = new VariableReferenceSubstitution(variable,
		                substitute);
		expression.accept(substitutor);
		if (substitutor.getFound()) {
			substitutor.setFound(false);
			return substitutor.getSubstitute();
		}
		return expression;
	}

	/**
	 * The {@link VariableDeclaration} the substituted {@link VariableReference}s have to be occurrences of.
	 */
	private VariableDeclaration variable;

	/**
	 * 
	 * @param variable
	 *                the {@link VariableDeclaration} the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the {@link Expression} occurrences of {@link VariableReferenceSubstitution#variable} are
	 *                substituted with
	 */
	VariableReferenceSubstitution(final VariableDeclaration variable, final Expression substitute) {
		super(substitute);
		this.variable = variable;
	}

	@Override
	public void visit(final VariableReference variableReference) {
		if (variableReference.getVariable() == this.variable) {
			this.setFound(true);
		}
	}<commit_msg>[prover] Fix VariableReferenceSubstitution ignores index access<commit_after>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.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCreatorHelper;

/**
 * Substitute {@link VariableReference}s in an {@link Expression} with another {@link Expression}.
 * 
 * @see VariableReferenceSubstitution#substitute(VariableDeclaration, Expression)
 * @author fabian
 * 
 */
class VariableReferenceSubstitution extends SubstitutionVisitor<Expression> {
	/**
	 * Substitutes occurrences of a {@link VariableDeclaration} in an {@link Expression} with another
	 * <code>Expression</code>.
	 * 
	 * A clone of the <code>substitute</code> is used for substitution.
	 * 
	 * @param expression
	 *                the <code>Expression</code> to search for occurrences of <code>variable</code>
	 * @param variable
	 *                the <code>VariableDeclaration</code> the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the <code>Expression</code> occurrences of <code>variable</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 occurrence of <code>variable</code>
	 */
	public static Expression substitute(final Expression expression, final VariableDeclaration variable,
	                final Expression substitute) {
		final VariableReferenceSubstitution substitutor = new VariableReferenceSubstitution(variable,
		                substitute);
		expression.accept(substitutor);
		if (substitutor.getFound()) {
			substitutor.setFound(false);
			return substitutor.getSubstitute();
		}
		return expression;
	}

	/**
	 * The {@link VariableDeclaration} the substituted {@link VariableReference}s have to be occurrences of.
	 */
	private VariableDeclaration variable;

	/**
	 * The {@link Expression} occurrences of {@link VariableReferenceSubstitution#variable} are substituted with.
	 */
	private Expression substitute;

	/**
	 * 
	 * @param variable
	 *                the {@link VariableDeclaration} the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the {@link Expression} occurrences of {@link VariableReferenceSubstitution#variable} are
	 *                substituted with
	 */
	VariableReferenceSubstitution(final VariableDeclaration variable, final Expression substitute) {
		super(null);
		this.variable = variable;
		this.substitute = substitute;
	}

	@Override
	public void visit(final VariableReference variableReference) {
		final VariableDeclaration referencedVariable = variableReference.getVariable();

		if (referencedVariable == this.variable) {
			final Expression index = variableReference.getIndex();
			if (index != null) {
				this.setSubstitute(AstNodeCreatorHelper.createArrayFunctionAccess(index,
				                this.substitute));
			} else {
				this.setSubstitute(this.substitute);
			}
			this.setFound(true);
		}
	}
{'fraction_non_alphanumeric': 0.09657373194491098, 'fraction_numerical': 0.0, 'mean_word_length': 3.7716346153846154, 'pattern_counts': {'":': 0, '<': 49, '<?xml version=': 0, '>': 49, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7595951', 'n_tokens_mistral': 1730, 'n_tokens_neox': 1456, 'n_words': 413}