<commit_before>/*
 * AbstractRegisterSequent.java
 * ---------------------------------
 * Copyright (c) 2022
 * 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.nProver.utilities.treewakers;

import edu.clemson.rsrg.absyn.expressions.Exp;
import edu.clemson.rsrg.absyn.expressions.mathexpr.*;
import edu.clemson.rsrg.nProver.GeneralPurposeProver;
import edu.clemson.rsrg.nProver.registry.CongruenceClassRegistry;
import edu.clemson.rsrg.treewalk.TreeWalker;
import edu.clemson.rsrg.treewalk.TreeWalkerStackVisitor;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * <p>
 * This abstract class labels all the {@link Exp} with a number to be used by the {@link GeneralPurposeProver}. The
 * concrete logic of registering each expression is left to its child class. This visitor logic is implemented as a
 * {@link TreeWalkerStackVisitor}.
 * </p>
 *
 * @author <NAME>
 * @author <NAME>.
 *
 * @version 1.0
 */
public abstract class AbstractRegisterSequent extends TreeWalkerStackVisitor {

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

    /**
     * <p>
     * This map contains the mapping between the argument expressions for the most immediate operator to be registered.
     * </p>
     */
    protected final Map<Exp, Integer> myArgumentsCache;

    /**
     * <p>
     * This map contains the mapping between expressions and its associated integer number.
     * </p>
     */
    protected final Map<String, Integer> myExpLabels;

    /**
     * <p>
     * A counter for the next expression
     * </p>
     */
    protected int myNextLabel;

    /**
     * <p>
     * This registry contains the target sequent VC to be proved.
     * </p>
     */
    protected final CongruenceClassRegistry<Integer, String, String, String> myRegistry;

    // ===========================================================
    // Global Operator Labels
    // ===========================================================

    /**
     * <p>
     * A constant representing the {@code =} operator.
     * </p>
     */
    public static final int OP_EQUALS = 2;

    /**
     * <p>
     * A constant representing the {@code <=} operator.
     * </p>
     */
    public static final int OP_LESS_THAN_OR_EQUALS = 1;

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

    /**
     * <p>
     * This helper constructor stores all relevant classes for the child classes to use.
     * </p>
     *
     * @param registry
     *            The registry that will contain the target sequent VC to be proved.
     * @param expLabels
     *            A mapping between expressions and its associated integer number.
     * @param nextLabel
     *            The number to be assigned initially as a label.
     */
    protected AbstractRegisterSequent(CongruenceClassRegistry<Integer, String, String, String> registry,
            Map<String, Integer> expLabels, int nextLabel) {
        myArgumentsCache = new LinkedHashMap<>();
        myRegistry = registry;
        myExpLabels = expLabels;
        myNextLabel = nextLabel;
    }

    // ===========================================================
    // Visitor Methods
    // ===========================================================

    // -----------------------------------------------------------
    // Math Expression-Related
    // -----------------------------------------------------------

    /**
     * <p>
     * Code that gets executed after visiting a {@link InfixExp}.
     * </p>
     *
     * @param exp
     *            An infix expression.
     */
    @Override
    public void postInfixExp(InfixExp exp) {
        // If this is not an infix operator we have seen, then add it to our map
        if (!myExpLabels.containsKey(exp.getOperatorAsString())) {
            myExpLabels.put(exp.getOperatorAsString(), myNextLabel);
            myNextLabel++;
        }
    }

    /**
     * <p>
     * Code that gets executed after visiting a {@link FunctionExp}.
     * </p>
     *
     * @param exp
     *            A function expression.
     */
    @Override
    public void postFunctionExp(FunctionExp exp) {
        // If this is not a function name we have seen, then add it to our map
        if (!myExpLabels.containsKey(exp.getOperatorAsString())) {
            myExpLabels.put(exp.getOperatorAsString(), myNextLabel);
            myNextLabel++;
        }
    }

    /**
     * <p>
     * This method redefines how a {@link FunctionExp} should be walked.<commit_msg>Redefined the walk for DotExp so we can handle those kinds of expressions<commit_after>/*
 * AbstractRegisterSequent.java
 * ---------------------------------
 * Copyright (c) 2022
 * 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.nProver.utilities.treewakers;

import edu.clemson.rsrg.absyn.expressions.Exp;
import edu.clemson.rsrg.absyn.expressions.mathexpr.*;
import edu.clemson.rsrg.nProver.GeneralPurposeProver;
import edu.clemson.rsrg.nProver.registry.CongruenceClassRegistry;
import edu.clemson.rsrg.statushandling.exception.SourceErrorException;
import edu.clemson.rsrg.treewalk.TreeWalker;
import edu.clemson.rsrg.treewalk.TreeWalkerStackVisitor;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * <p>
 * This abstract class labels all the {@link Exp} with a number to be used by the {@link GeneralPurposeProver}. The
 * concrete logic of registering each expression is left to its child class. This visitor logic is implemented as a
 * {@link TreeWalkerStackVisitor}.
 * </p>
 *
 * @author <NAME>
 * @author <NAME>.
 *
 * @version 1.0
 */
public abstract class AbstractRegisterSequent extends TreeWalkerStackVisitor {

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

    /**
     * <p>
     * This map contains the mapping between the argument expressions for the most immediate operator to be registered.
     * </p>
     */
    protected final Map<Exp, Integer> myArgumentsCache;

    /**
     * <p>
     * This map contains the mapping between expressions and its associated integer number.
     * </p>
     */
    protected final Map<String, Integer> myExpLabels;

    /**
     * <p>
     * A counter for the next expression
     * </p>
     */
    protected int myNextLabel;

    /**
     * <p>
     * This registry contains the target sequent VC to be proved.
     * </p>
     */
    protected final CongruenceClassRegistry<Integer, String, String, String> myRegistry;

    // ===========================================================
    // Global Operator Labels
    // ===========================================================

    /**
     * <p>
     * A constant representing the {@code =} operator.
     * </p>
     */
    public static final int OP_EQUALS = 2;

    /**
     * <p>
     * A constant representing the {@code <=} operator.
     * </p>
     */
    public static final int OP_LESS_THAN_OR_EQUALS = 1;

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

    /**
     * <p>
     * This helper constructor stores all relevant classes for the child classes to use.
     * </p>
     *
     * @param registry
     *            The registry that will contain the target sequent VC to be proved.
     * @param expLabels
     *            A mapping between expressions and its associated integer number.
     * @param nextLabel
     *            The number to be assigned initially as a label.
     */
    protected AbstractRegisterSequent(CongruenceClassRegistry<Integer, String, String, String> registry,
            Map<String, Integer> expLabels, int nextLabel) {
        myArgumentsCache = new LinkedHashMap<>();
        myRegistry = registry;
        myExpLabels = expLabels;
        myNextLabel = nextLabel;
    }

    // ===========================================================
    // Visitor Methods
    // ===========================================================

    // -----------------------------------------------------------
    // Math Expression-Related
    // -----------------------------------------------------------

    /**
     * <p>
     * Code that gets executed after visiting a {@link InfixExp}.
     * </p>
     *
     * @param exp
     *            An infix expression.
     */
    @Override
    public void postInfixExp(InfixExp exp) {
        // If this is not an infix operator we have seen, then add it to our map
        if (!myExpLabels.containsKey(exp.getOperatorAsString())) {
            myExpLabels.put(exp.getOperatorAsString(), myNextLabel);
            myNextLabel++;
        }
    }

    /**
     * <p>
     * This method redefines how a {@link DotExp} should be walked.
     * </p>
     *
     * @param exp
     *            A dotted expression.
     *
     * @return {@code true}
     */
    @Override
    public final boolean walkDotExp(DotExp exp) {
        preAny(exp);
        preExp(exp);
        preMathExp(exp);
        preDotExp(exp);

        // YS: We will need to special handle DotExp since it is
        // really one named expression separated by dots.
        List<Exp> segments = exp.getSegments();
        for (Exp e : segments) {
            if (e instanceof FunctionExp) {
                // YS: For right now we can handle everything,
                // but FunctionExp (i.e., Stack.Val_in(...))
                // since we don't know how to do deal with them yet.
                throw new SourceErrorException("[nProver] Cannot handle function " + ((FunctionExp) e).getName()
                        + " in the dot expression " + exp, e.getLocation());
            }
        }

        // YS: If we got here, we didn't have any FunctionExps inside our DotExp
        // Logic for handling dot expressions
        storeInArgumentCache(exp);

        postDotExp(exp);
        postMathExp(exp);
        postExp(exp);
        postAny(exp);

        return true;
    }

    /**
     * <p>
     * Code that gets executed after visiting a {@link FunctionExp}.
     * </p>
     *
     * @param exp
     *            A function expression.
     */
    @Override
    public void postFunctionExp(FunctionExp exp) {
        // If this is not a function name we have seen, then add it to our map
        if (!myExpLabels.containsKey(exp.getOperatorAsString())) {
            myExpLabels.put(exp.getOperatorAsString(), myNextLabel);
            myNextLabel++;
        }
    }

    /**
     * <p>
     * This method redefines how a {@link FunctionExp} should be walked.
{'fraction_non_alphanumeric': 0.20448921880523152, 'fraction_numerical': 0.0014139271827500884, 'mean_word_length': 2.225135366201197, 'pattern_counts': {'":': 0, '<': 66, '<?xml version=': 0, '>': 64, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3024564', 'n_tokens_mistral': 3022, 'n_tokens_neox': 2889, 'n_words': 917}