/*
 * PresumeStmtRule.java
 * ---------------------------------
 * Copyright (c) 2017
 * RESOLVE Software Research Group
 * School of Computing
 * Clemson University
 * All rights reserved.
 * ---------------------------------
 * This file is subject to the terms and conditions defined in
 * file 'LICENSE.txt', which is part of this source code package.
 */
package edu.clemson.cs.rsrg.vcgeneration.proofrules.statement;

import edu.clemson.cs.rsrg.absyn.statements.AssumeStmt;
import edu.clemson.cs.rsrg.absyn.statements.ConfirmStmt;
import edu.clemson.cs.rsrg.absyn.statements.PresumeStmt;
import edu.clemson.cs.rsrg.vcgeneration.proofrules.AbstractProofRuleApplication;
import edu.clemson.cs.rsrg.vcgeneration.proofrules.ProofRuleApplication;
import edu.clemson.cs.rsrg.vcgeneration.utilities.AssertiveCodeBlock;
import org.stringtemplate.v4.ST;
import org.stringtemplate.v4.STGroup;

/**
 * <p>This class contains the logic for applying the {@code presume}
 * rule.</p>
 *
 * @author Yu-Shan Sun
 * @version 1.0
 */
public class PresumeStmtRule extends AbstractProofRuleApplication
        implements
            ProofRuleApplication {

    // ===========================================================
    // Member Fields
    // ===========================================================

    /** <p>The {@link PresumeStmt} we are applying the rule to.</p> */
    private final PresumeStmt myPresumeStmt;

    // ===========================================================
    // Constructors
    // ===========================================================

    /**
     * <p>This creates a new application of the {@code presume}
     * rule.</p>
     *
     * @param presumeStmt The {@link PresumeStmt} we are applying
     *                 the rule to.
     * @param block The assertive code block that the subclasses are
     *              applying the rule to.
     * @param stGroup The string template group we will be using.
     * @param blockModel The model associated with {@code block}.
     */
    public PresumeStmtRule(PresumeStmt presumeStmt, AssertiveCodeBlock block,
            STGroup stGroup, ST blockModel) {
        super(block, stGroup, blockModel);
        myPresumeStmt = presumeStmt;
    }

    // ===========================================================
    // Public Methods
    // ===========================================================

    /**
     * <p>This method applies the {@code Proof Rule}.</p>
     */
    @Override
    public final void applyRule() {
        // Add a new confirm statement followed by a stipulate assume statement
        // generated the presume statement to to the assertive code block.
        // YS: We clone the location and expression to avoid aliasing.
        myCurrentAssertiveCodeBlock.addStatement(new ConfirmStmt(myPresumeStmt
                .getLocation().clone(), myPresumeStmt.getAssertion().clone(),
                false));
        myCurrentAssertiveCodeBlock.addStatement(new AssumeStmt(myPresumeStmt
                .getLocation().clone(), myPresumeStmt.getAssertion().clone(),
                true));

        // Add the different details to the various different output models
        ST stepModel = mySTGroup.getInstanceOf("outputVCGenStep");
        stepModel.add("proofRuleName", getRuleDescription()).add(
                "currentStateOfBlock", myCurrentAssertiveCodeBlock);
        myBlockModel.add("vcGenSteps", stepModel.render());
    }

    /**
     * <p>This method returns a description associated with
     * the {@code Proof Rule}.</p>
     *
     * @return A string.
     */
    @Override
    public final String getRuleDescription() {
        return "Presume Rule";
    }

}
@@ -2561,18 +2561,9 @@
 by a
- stipulate
+n
  ass
@@ -3076,19 +3076,20 @@
         
-tru
+fals
 e));%0A%0A  

Make presume generate assume not stipulate