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

import edu.kit.iti.formal.pse.worthwhile.model.ast.Assertion;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assignment;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assumption;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Axiom;
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.FunctionDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Invariant;
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.ReturnStatement;
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.visitor.ASTNodeVisitor;

/**
 * Applies the Weakest Precondition calculus to a {@link Program}.
 */
class WPStrategy extends ASTNodeVisitor implements FormulaGenerator {
    /**
     * The weakest precondition that implies the correctness of the remainder {@link Program}.
     */
    private Expression weakestPrecondition;

    /**
     * @return the weakestPrecondition
     */
    public Expression getWeakestPrecondition() {
	// begin-user-code
	return this.weakestPrecondition;
	// end-user-code
    }

    /**
     * @param program
     *            the {@link Program} to calculate the weakest precondition for
     * @return the weakest precondition that implies the correctness of <code>program</code>
     * @see FormulaGenerator#transformProgram(Program program)
     */
    public Expression transformProgram(Program program) {
	// begin-user-code
	// TODO Auto-generated method stub
	return null;
	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Assertion assertion)
     */
    public void visit(Assertion assertion) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Assignment assignment)
     */
    public void visit(Assignment assignment) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Assumption assumption)
     */
    public void visit(Assumption assumption) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Axiom axiom)
     */
    public void visit(Axiom axiom) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Block block)
     */
    public void visit(Block block) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Conditional conditional)
     */
    public void visit(Conditional conditional) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(FunctionDeclaration functionDeclaration)
     */
    public void visit(FunctionDeclaration functionDeclaration) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Invariant invariant)
     */
    public void visit(Invariant invariant) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Loop loop)
     */
    public void visit(Loop loop) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Postcondition postcondition)
     */
    public void visit(Postcondition postcondition) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Precondition precondition)
     */
    public void visit(Precondition precondition) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(Program program)
     */
    public void visit(Program program) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(ReturnStatement returnStatement)
     */
    public void visit(ReturnStatement returnStatement) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(VariableDeclaration variableDeclaration)
     */
    public void visit(VariableDeclaration variableDeclaration) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }

    /**
     * @see ASTNodeVisitor#visit(VariableReference variableReference)
     */
    public void visit(VariableReference variableReference) {
	// begin-user-code
	// TODO Auto-generated method stub

	// end-user-code
    }
}
@@ -1001,78 +1001,8 @@
 on;%0A
-import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;%0A
 impo
@@ -4809,237 +4809,8 @@
 ub%0A%0A
-%09// end-user-code%0A    %7D%0A%0A    /**%0A     * @see ASTNodeVisitor#visit(VariableReference variableReference)%0A     */%0A    public void visit(VariableReference variableReference) %7B%0A%09// begin-user-code%0A%09// TODO Auto-generated method stub%0A%0A
 %09// 

Remove leftover visit from WPStrategy.java