/*
 * VCGenPipeline.java
 * ---------------------------------
 * Copyright (c) 2021
 * 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.rsrg.init.pipeline;

import edu.clemson.rsrg.absyn.declarations.moduledecl.ModuleDec;
import edu.clemson.rsrg.init.CompileEnvironment;
import edu.clemson.rsrg.init.ResolveCompiler;
import edu.clemson.rsrg.init.output.OutputListener;
import edu.clemson.rsrg.statushandling.StatusHandler;
import edu.clemson.rsrg.treewalk.TreeWalker;
import edu.clemson.rsrg.typeandpopulate.symboltables.MathSymbolTableBuilder;
import edu.clemson.rsrg.typeandpopulate.utilities.ModuleIdentifier;
import edu.clemson.rsrg.vcgeneration.VCGenerator;

/**
 * <p>
 * This is pipeline that generates verification conditions (VCs) using the RESOLVE AST and symbol table.
 * </p>
 *
 * @author Yu-Shan Sun
 *
 * @version 1.0
 */
public class VCGenPipeline extends AbstractPipeline {

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

    /**
     * <p>
     * This generates a pipeline to generate VCs.
     * </p>
     *
     * @param ce
     *            The current compilation environment.
     * @param symbolTable
     *            The symbol table.
     */
    public VCGenPipeline(CompileEnvironment ce, MathSymbolTableBuilder symbolTable) {
        super(ce, symbolTable);
    }

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

    /**
     * {@inheritDoc}
     */
    @Override
    public final void process(ModuleIdentifier currentTarget) {
        ModuleDec moduleDec = myCompileEnvironment.getModuleAST(currentTarget);
        StatusHandler statusHandler = myCompileEnvironment.getStatusHandler();
        VCGenerator vcGenerator = new VCGenerator(mySymbolTable, myCompileEnvironment);
        if (myCompileEnvironment.flags.isFlagSet(ResolveCompiler.FLAG_DEBUG)) {
            StringBuffer sb = new StringBuffer();
            sb.append("\n---------------Generating VCs---------------\n\n");
            sb.append("Generating VCs for: ");
            sb.append(moduleDec.getName());

            statusHandler.info(null, sb.toString());
        }

        // Walk the AST and generate VCs
        TreeWalker.visit(vcGenerator, moduleDec);

        // Output the contents to listener objects
        for (OutputListener listener : myCompileEnvironment.getOutputListeners()) {
            listener.vcGeneratorResult(myCompileEnvironment.getFile(currentTarget).toString(),
                    moduleDec.getName().getName(), vcGenerator.getFinalAssertiveCodeBlocks(),
                    vcGenerator.getVerboseModeOutput());
        }

        if (myCompileEnvironment.flags.isFlagSet(ResolveCompiler.FLAG_DEBUG)) {
            StringBuffer sb = new StringBuffer();
            sb.append("\n---------------End Generating VCs---------------\n");

            statusHandler.info(null, sb.toString());
        }
    }

}

@@ -897,16 +897,205 @@
 nerator;
+%0Aimport edu.clemson.rsrg.vcgeneration.utilities.AssertiveCodeBlock;%0Aimport edu.clemson.rsrg.vcgeneration.utilities.VerificationCondition;%0Aimport java.util.LinkedList;%0Aimport java.util.List;
 %0A%0A/**%0A *
@@ -1316,16 +1316,343 @@
 line %7B%0A%0A
+    // ===========================================================%0A    // Member Fields%0A    // ===========================================================%0A%0A    /**%0A     * %3Cp%3E%0A     * The module's final list of verification conditions.%0A     * %3C/p%3E%0A     */%0A    private final List%3CVerificationCondition%3E myVerificationConditions;%0A%0A
     // =
@@ -2146,16 +2146,71 @@
 Table);%0A
+        myVerificationConditions = new LinkedList%3C%3E();%0A
     %7D%0A%0A 
@@ -2357,32 +2357,339 @@
 ==============%0A%0A
+    /**%0A     * %3Cp%3E%0A     * This method returns the verification conditions generated by this module.%0A     * %3C/p%3E%0A     *%0A     * @return A list of %7B@link VerificationCondition%7Ds.%0A     */%0A    public final List%3CVerificationCondition%3E getVerificationConditions() %7B%0A        return myVerificationConditions;%0A    %7D%0A%0A
     /**%0A     * %7B
@@ -3809,24 +3809,24 @@
 deBlocks(),%0A
-
             
@@ -3873,32 +3873,311 @@
 ());%0A        %7D%0A%0A
+        // Store all the verification conditions from each assertive code block%0A        myVerificationConditions.clear();%0A        for (AssertiveCodeBlock block : vcGenerator.getFinalAssertiveCodeBlocks()) %7B%0A            myVerificationConditions.addAll(block.getVCs());%0A        %7D%0A%0A
         if (myCo

Store the verification conditions in the pipeline for the prover