/* QuantifierExpression -- Automatically generated by TreeBuilder (2024-10-27T16:47Z) */

package de.uni_freiburg.informatik.ultimate.model.acsl.ast;

import java.util.List;
import de.uni_freiburg.informatik.ultimate.model.acsl.ACSLNode;
/**
 * Represents a quantifier expression which is a special form of a expression.
 */
public class QuantifierExpression extends Expression {
    private static final java.util.function.Predicate<ACSLNode> VALIDATOR = 
			ACSLNode.VALIDATORS.get(QuantifierExpression.class);
    /**
     * This is true for universal and false for existential quantifier.
     */
    boolean isUniversal;

    /**
     * The type params of this quantifier expression.
     */
    String[] typeParams;

    /**
     * The subformula of this quantifier expression.
     */
    Expression subformula;

    /**
     * The parameters of this quantifier expression.
     */
    String[] parameters;

    /**
     * The attributes of this quantifier expression.
     */
    String[] attributes;

    /**
     * The constructor taking initial values.
     * @param isUniversal this is true for universal and false for existential quantifier.
     * @param typeParams the type params of this quantifier expression.
     * @param subformula the subformula of this quantifier expression.
     * @param parameters the parameters of this quantifier expression.
     * @param attributes the attributes of this quantifier expression.
     */
    public QuantifierExpression(boolean isUniversal, String[] typeParams, Expression subformula, String[] parameters, String[] attributes) {
        super();
        this.isUniversal = isUniversal;
        this.typeParams = typeParams;
        this.subformula = subformula;
        this.parameters = parameters;
        this.attributes = attributes;
        assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid QuantifierExpression: " + this;
    }

    /**
     * The constructor taking initial values.
     * @param type the type of this expression.
     * @param isUniversal this is true for universal and false for existential quantifier.
     * @param typeParams the type params of this quantifier expression.
     * @param subformula the subformula of this quantifier expression.
     * @param parameters the parameters of this quantifier expression.
     * @param attributes the attributes of this quantifier expression.
     */
    public QuantifierExpression(ACSLType type, boolean isUniversal, String[] typeParams, Expression subformula, String[] parameters, String[] attributes) {
        super(type);
        this.isUniversal = isUniversal;
        this.typeParams = typeParams;
        this.subformula = subformula;
        this.parameters = parameters;
        this.attributes = attributes;
        assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid QuantifierExpression: " + this;
    }

    /**
     * Returns a textual description of this object.
     */
    public String toString() {
        StringBuffer sb = new StringBuffer();
        sb.append("QuantifierExpression").append('[');
        sb.append(isUniversal);
        sb.append(',');
        if (typeParams == null) {
            sb.append("null");
        } else {
            sb.append('[');
            for(int i1 = 0; i1 < typeParams.length; i1++) {
                if (i1 > 0) sb.append(',');
                    sb.append(typeParams[i1]);
            }
            sb.append(']');
        }
        sb.append(',').append(subformula);
        sb.append(',');
        if (parameters == null) {
            sb.append("null");
        } else {
            sb.append('[');
            for(int i1 = 0; i1 < parameters.length; i1++) {
                if (i1 > 0) sb.append(',');
                    sb.append(parameters[i1]);
            }
            sb.append(']');
        }
        sb.append(',');
        if (attributes == null) {
            sb.append("null");
        } else {
            sb.append('[');
            for(int i1 = 0; i1 < attributes.length; i1++) {
                if (i1 > 0) sb.append(',');
                    sb.append(attributes[i1]);
            }
            sb.append(']');
        }
        return sb.append(']').toString();
    }

    /**
     * Checks this is true for universal and false for existential quantifier.
     * @return this is true for universal and false for existential quantifier.
     */
    public boolean isUniversal() {
        return isUniversal;
    }

    /**
     * Gets the type params of this quantifier expression.
     * @return the type params of this quantifier expression.
     */
    public String[] getTypeParams() {
        return typeParams;
    }

    /**
     * Gets the subformula of this quantifier expression.
     * @return the subformula of this quantifier expression.
     */
    public Expression getSubformula() {
        return subformula;
    }

    /**
     * Gets the parameters of this quantifier expression.
     * @return the parameters of this quantifier expression.
     */
    public String[] getParameters() {
        return parameters;
    }

    /**
     * Gets the attributes of this quantifier expression.
     * @return the attributes of this quantifier expression.
     */
    public String[] getAttributes() {
        return attributes;
    }

    public List<ACSLNode> getOutgoingNodes() {
        List<ACSLNode> children = super.getOutgoingNodes();
        children.add(subformula);
        return children;
    }

    public void accept(ACSLVisitor visitor) {
        if (visitor.visit((Expression)this)) {
            //visit parent types higher up if necessary
        } else {
            return;
        }
        if (visitor.visit(this)) {
            if(subformula!=null){
                subformula.accept(visitor);
            }
            if(type!=null){
                type.accept(visitor);
            }
        }
    }

    public Expression accept(ACSLTransformer visitor) {
        Expression node = visitor.transform(this);
        if(node != this){
            return node;
        }

            Expression newsubformula = null;
        if(subformula != null){
            newsubformula = (Expression)subformula.accept(visitor);
        }
            ACSLType newtype = null;
        if(type != null){
            newtype = (ACSLType)type.accept(visitor);
        }
        if(subformula != newsubformula || type != newtype){
            return new QuantifierExpression(newtype, isUniversal, typeParams, newsubformula, parameters, attributes);
        }
        return this;
    }
}