/*
 * AbstractReductionRuleApplication.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.sequents.reductionrules;

import edu.clemson.cs.rsrg.absyn.expressions.Exp;
import edu.clemson.cs.rsrg.statushandling.exception.SourceErrorException;
import edu.clemson.cs.rsrg.vcgeneration.sequents.Sequent;
import java.util.ArrayList;
import java.util.List;

/**
 * <p>This is the abstract base class for all the {@code Sequent Reduction Rules}.</p>
 *
 * @author Yu-Shan Sun
 * @version 1.0
 */
public abstract class AbstractReductionRuleApplication
        implements
            ReductionRuleApplication {

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

    /**
     * <p>An impacting reduction means that either {@code myOriginalExp}
     * is a negation {@code exp} or {@code myOriginalExp} created a new
     * associated {@link Sequent}.</p>
     */
    protected boolean myIsImpactingReductionFlag;

    /** <p>The original expression to be reduced</p> */
    protected final Exp myOriginalExp;

    /** <p>The original sequent that contains {@code myOriginalExp}.</p> */
    protected final Sequent myOriginalSequent;

    /** <p>The resulting {@code sequents}.</p> */
    protected final List<Sequent> myResultingSequents;

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

    /**
     * <p>An helper constructor that stores the {@code originalSequent}
     * and the {@code originalExp} we are trying to reduce as well as
     * creating the list to store the resulting {@link Sequent Sequents}.</p>
     *
     * @param originalSequent The original {@link Sequent} that contains
     *                        the expression to be reduced.
     * @param originalExp The {@link Exp} to be reduced.
     */
    protected AbstractReductionRuleApplication(Sequent originalSequent, Exp originalExp) {
        myIsImpactingReductionFlag = false;
        myOriginalExp = originalExp;
        myOriginalSequent = originalSequent;
        myResultingSequents = new ArrayList<>();
    }

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

    /**
     * <p>This method indicates whether or not this {@link ReductionRuleApplication}
     * encountered a {@code not(<exp>)} or if it created a new associated
     * {@link Sequent}.</p>
     *
     * @return {@code true} if we have applied some kind of impacting
     * logical reduction to the original {@link Sequent}, {@code false} otherwise.
     */
    @Override
    public final boolean isIsImpactingReductionFlag() {
        return myIsImpactingReductionFlag;
    }

    // ===========================================================
    // Protected Methods
    // ===========================================================

    /**
     * <p>An helper method that deep copies a list of {@link Exp Exps}.</p>
     *
     * @param originalExpList A list of {@link Exp Exps}.
     *
     * @return A deep copy of {@code originalExpList}.
     */
    protected final List<Exp> copyExpList(List<Exp> originalExpList) {
        List<Exp> copyExpList = new ArrayList<>(originalExpList.size());

        for (Exp exp : originalExpList) {
            copyExpList.add(exp.clone());
        }

        return copyExpList;
    }

    /**
     * <p>An helper method that throws an unexpected expression
     * error message.</p>
     */
    protected final void unexpectedExp() {
        throw new SourceErrorException("[VCGenerator] Found: " + myOriginalExp
                + " of type: " + myOriginalExp.getClass().getSimpleName()
                + " while applying " + getRuleDescription(), myOriginalExp
                .getLocation());
    }

}
@@ -487,16 +487,77 @@
 ns.Exp;%0A
+import edu.clemson.cs.rsrg.parsing.data.LocationDetailModel;%0A
 import e
@@ -3526,16 +3526,94 @@
  Exps%7D.%0A
+     * @param parentLocationDetail Location detail for the parent expression.%0A
      *%0A 
@@ -3733,32 +3733,74 @@
  originalExpList
+, LocationDetailModel parentLocationDetail
 ) %7B%0A        List
@@ -3919,35 +3919,737 @@
     
-copyExpList.add(exp.clone()
+Exp expCopy = exp.clone();%0A%0A            // Check to see if we have a location detail model%0A            // If we have one, the clone method must have made a%0A            // a copy already.%0A            if (exp.getLocationDetailModel() == null) %7B%0A                // Attempt to copy our parent's model.%0A                // YS: At this point, someone should have%0A                //     some sort of location detail model.%0A                //     If not, the VC generator didn't generate%0A                //     the expression properly.%0A                if (parentLocationDetail != null) %7B%0A                    expCopy.setLocationDetailModel(parentLocationDetail.clone());%0A                %7D%0A            %7D%0A%0A            copyExpList.add(expCopy
 );%0A 

Change the helper method to take in a parent location detail model