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.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(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;
	}

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

			if (found) {
				quantifiedExpression.setCondition(AstNodeCloneHelper.clone(substitute));
				found = false;
			}
		}

		quantifiedExpression.getExpression().accept(this);
		if (found) {
			quantifiedExpression.setExpression(AstNodeCloneHelper.clone(substitute));
			found = false;
		}
	}

	@Override
	public void visit(final BinaryExpression binaryExpression) {
		binaryExpression.getLeft().accept(this);
		if (found) {
			binaryExpression.setLeft(AstNodeCloneHelper.clone(substitute));
			found = false;
		}

		binaryExpression.getRight().accept(this);
		if (found) {
			binaryExpression.setRight(AstNodeCloneHelper.clone(substitute));
			found = false;
		}
	}

	@Override
	public void visit(final UnaryExpression unaryExpression) {
		unaryExpression.getOperand().accept(this);
		if (found) {
			unaryExpression.setOperand(AstNodeCloneHelper.clone(substitute));
			found = false;
		}
	}

	@Override
	public void visit(final Literal literal) {
		// we reached an Expression leaf, ignore default operation
	}

	@Override
	public void visit(final VariableReference variableReference) {
		// we reached an Expression leaf, ignore default operation
	}
}
@@ -2213,24 +2213,349 @@
  found;%0A%09%7D%0A%0A
+%09/**%0A%09 * @return the substitute%0A%09 */%0A%09final Expression getSubstitute() %7B%0A%09%09return this.substitute;%0A%09%7D%0A%0A%09/**%0A%09 * %0A%09 * @param substitute%0A%09 *                the %7B@link Expression%7D found child %7B@link ASTNode%7Ds are substituted with%0A%09 */%0A%09final void setSubstitute(final Expression substitute) %7B%0A%09%09this.substitute = substitute;%0A%09%7D%0A%0A
 %09@Override%0A%09

Add substitute setter/getter to SubstitutionVisitor