<commit_before>package edu.kit.iti.formal.pse.worthwhile.prover;

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.FunctionCall;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Literal;
import edu.kit.iti.formal.pse.worthwhile.model.ast.QuantifiedExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.UnaryExpression;
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;

/**
 * Substitutes a child reference with some {@link Expression} in the parent {@link ASTNode} when indicated so by the
 * child.
 * 
 * Implements {@link HierarchialASTNodeVisitor#visit(FunctionCall}, {@link
 * HierarchialASTNodeVisitor#visit(QuantifiedExpression}, {@link HierarchialASTNodeVisitor#visit(BinaryExpression)} and
 * {@link HierarchialASTNodeVisitor#visit(UnaryExpression)} to traverse {@link Expression}s and substitute the
 * respective child references when the visited children called {@link SubstitutionVisitor#setFound(Boolean)}.
 * {@link HierarchialASTNodeVisitor#visit(Expression)} is implemented with an empty body so that the default visit
 * operation is ignored and subclasses just have to override the visit methods in which they want to actually call
 * {@link SubstitutionVisitor#setFound(Boolean)}.
 * 
 * @author fabian
 * 
 */
class SubstitutionVisitor extends HierarchialASTNodeVisitor {
	/**
	 * The {@link Expression} children are substituted with when {@link SubstitutionVisitor#found} was set.
	 */
	private Expression substitute;

	/**
	 * Indicates whether a matching child has been found and has to be substituted in the parent {@link ASTNode}.
	 */
	private Boolean found = false;

	/**
	 * 
	 * @param substitute
	 *                the {@link Expression} found child {@link ASTNode}s are substituted with
	 */
	SubstitutionVisitor(final Expression substitute) {
		this.substitute = substitute;
	}

	/**
	 * @return the found
	 */
	final Boolean getFound() {
		return this.found;
	}

	/**
	 * @param found
	 *                the found to set
	 */
	final void setFound(final Boolean found) {
		this.found = found;
	}

	/**
	 * @return a clone of the {@link SubstitutionVisitor#substitute}
	 */
	final Expression getSubstitute() {
		return AstNodeCloneHelper.clone(this.substitute);
	}

	/**
	 * 
	 * @param substitute
	 *                the {@link Expression} found child {@link ASTNode}s are substituted with
	 */
	final void setSubstitute(final Expression substitute) {
		this.substitute = substitute;
	}

	@Override
	public void visit(final QuantifiedExpression quantifiedExpression) {
		final Expression condition = quantifiedExpression.getCondition();
		if (condition != null) {
			condition.accept(this);

			if (found) {
				quantifiedExpression.setCondition(this.getSubstitute());
				found = false;
			}
		}

		quantifiedExpression.getExpression().accept(this);
		if (found) {<commit_msg>[prover] Recurse from Program into Expressions in SubstitutionVisitor<commit_after>package edu.kit.iti.formal.pse.worthwhile.prover;

import edu.kit.iti.formal.pse.worthwhile.model.ast.Annotation;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assignment;
import edu.kit.iti.formal.pse.worthwhile.model.ast.BinaryExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Block;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Conditional;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionCall;
import edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Invariant;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Literal;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Loop;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Postcondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Precondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;
import edu.kit.iti.formal.pse.worthwhile.model.ast.QuantifiedExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnStatement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Statement;
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;

/**
 * Substitutes a child reference with some {@link Expression} in the parent {@link ASTNode} when indicated so by the
 * child.
 * 
 * Implements all {@link Statement} visit methods, {@link HierarchialASTNodeVisitor#visit(FunctionCall}, {@link
 * HierarchialASTNodeVisitor#visit(QuantifiedExpression}, {@link HierarchialASTNodeVisitor#visit(BinaryExpression)} and
 * {@link HierarchialASTNodeVisitor#visit(UnaryExpression)} to traverse {@link Expression}s and substitute the
 * respective child references when the visited children called {@link SubstitutionVisitor#setFound(Boolean)}.
 * {@link HierarchialASTNodeVisitor#visit(Expression)} is implemented with an empty body so that the default visit
 * operation is ignored and subclasses just have to override the visit methods in which they want to actually call
 * {@link SubstitutionVisitor#setFound(Boolean)}.
 * 
 * @author fabian
 * 
 */
class SubstitutionVisitor extends HierarchialASTNodeVisitor {
	/**
	 * The {@link Expression} children are substituted with when {@link SubstitutionVisitor#found} was set.
	 */
	private Expression substitute;

	/**
	 * Indicates whether a matching child has been found and has to be substituted in the parent {@link ASTNode}.
	 */
	private Boolean found = false;

	/**
	 * 
	 * @param substitute
	 *                the {@link Expression} found child {@link ASTNode}s are substituted with
	 */
	SubstitutionVisitor(final Expression substitute) {
		this.substitute = substitute;
	}

	/**
	 * @return the found
	 */
	final Boolean getFound() {
		return this.found;
	}

	/**
	 * @param found
	 *                the found to set
	 */
	final void setFound(final Boolean found) {
		this.found = found;
	}

	/**
	 * @return a clone of the {@link SubstitutionVisitor#substitute}
	 */
	final Expression getSubstitute() {
		return AstNodeCloneHelper.clone(this.substitute);
	}

	/**
	 * 
	 * @param substitute
	 *                the {@link Expression} found child {@link ASTNode}s are substituted with
	 */
	final void setSubstitute(final Expression substitute) {
		this.substitute = substitute;
	}

	@Override
	public void visit(final Program program) {
		for (final FunctionDeclaration f : program.getFunctionDeclarations()) {
			f.accept(this);
		}

		program.getMainBlock().accept(this);
	}

	@Override
	public void visit(final FunctionDeclaration functionDeclaration) {
		for (final Precondition p : functionDeclaration.getPreconditions()) {
			p.accept(this);
		}
		for (final Postcondition p : functionDeclaration.getPostconditions()) {
			p.accept(this);
		}
		functionDeclaration.getBody().accept(this);
	}

	@Override
	public void visit(final Annotation annotation) {
		annotation.getExpression().accept(this);
	}

	@Override
	public void visit(final Assignment assignment) {
		assignment.getValue().accept(this);
	}

	@Override
	public void visit(final Block block) {
		for (final Statement s : block.getStatements()) {
			s.accept(this);
		}
	}

	@Override
	public void visit(final Conditional conditional) {
		conditional.getCondition().accept(this);
	}

	@Override
	public void visit(final Loop loop) {
		loop.getCondition().accept(this);
		for (final Invariant i : loop.getInvariants()) {
			i.accept(this);
		}
		loop.getBody().accept(this);
	}

	@Override
	public void visit(final ReturnStatement returnStatement) {
		returnStatement.getReturnValue().accept(this);
	}

	@Override
	public void visit(final VariableDeclaration variableDeclaration) {
		variableDeclaration.getInitialValue().accept(this);
	}

	@Override
	public void visit(final QuantifiedExpression quantifiedExpression) {
		final Expression condition = quantifiedExpression.getCondition();
		if (condition != null) {
			condition.accept(this);

			if (found) {
				quantifiedExpression.setCondition(this.getSubstitute());
				found = false;
			}
		}

		quantifiedExpression.getExpression().accept(this);
		if (found) {
{'fraction_non_alphanumeric': 0.10983530503363488, 'fraction_numerical': 0.0, 'mean_word_length': 4.559638942617666, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, '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': '382539', 'n_tokens_mistral': 2712, 'n_tokens_neox': 2501, 'n_words': 599}