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

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

import java.util.List;
import java.util.Arrays;
import java.util.ArrayList;
import de.uni_freiburg.informatik.ultimate.model.acsl.ACSLNode;
/**
 * Contract (for Function and Statement)
 * if Contract is for Function or for Statement depends of its position in the code.
 */
public class Contract extends ACSLNode {
    private static final java.util.function.Predicate<ACSLNode> VALIDATOR = 
			ACSLNode.VALIDATORS.get(Contract.class);
    /**
     * The contract stmt of this contract.
     */
    ContractStatement[] contractStmt;

    /**
     * The behaviors of this contract.
     */
    Behavior[] behaviors;

    /**
     * The completeness of this contract.
     */
    Completeness completeness;

    /**
     * The constructor taking initial values.
     * @param contractStmt the contract stmt of this contract.
     */
    public Contract(ContractStatement[] contractStmt) {
        super();
        this.contractStmt = contractStmt;
        assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid Contract: " + this;
    }

    /**
     * The constructor taking initial values.
     * @param contractStmt the contract stmt of this contract.
     * @param behaviors the behaviors of this contract.
     * @param completeness the completeness of this contract.
     */
    public Contract(ContractStatement[] contractStmt, Behavior[] behaviors, Completeness completeness) {
        super();
        this.contractStmt = contractStmt;
        this.behaviors = behaviors;
        this.completeness = completeness;
        assert VALIDATOR == null || VALIDATOR.test(this) : "Invalid Contract: " + this;
    }

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

    /**
     * Gets the contract stmt of this contract.
     * @return the contract stmt of this contract.
     */
    public ContractStatement[] getContractStmt() {
        return contractStmt;
    }

    /**
     * Gets the behaviors of this contract.
     * @return the behaviors of this contract.
     */
    public Behavior[] getBehaviors() {
        return behaviors;
    }

    /**
     * Sets the behaviors of this contract.
     * @param behaviors the behaviors of this contract.
     */
    public void setBehaviors(Behavior[] behaviors) {
        this.behaviors = behaviors;
    }

    /**
     * Gets the completeness of this contract.
     * @return the completeness of this contract.
     */
    public Completeness getCompleteness() {
        return completeness;
    }

    /**
     * Sets the completeness of this contract.
     * @param completeness the completeness of this contract.
     */
    public void setCompleteness(Completeness completeness) {
        this.completeness = completeness;
    }

    public List<ACSLNode> getOutgoingNodes() {
        List<ACSLNode> children = super.getOutgoingNodes();
        if(contractStmt!=null){
            children.addAll(Arrays.asList(contractStmt));
        }
        if(behaviors!=null){
            children.addAll(Arrays.asList(behaviors));
        }
        children.add(completeness);
        return children;
    }

    public void accept(ACSLVisitor visitor) {
        if (visitor.visit(this)) {
            if(contractStmt!=null){
                for (ContractStatement elem : contractStmt) {
                    elem.accept(visitor);
                }
            }
            if(behaviors!=null){
                for (Behavior elem : behaviors) {
                    elem.accept(visitor);
                }
            }
            if(completeness!=null){
                completeness.accept(visitor);
            }
        }
    }

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

        boolean isChanged=false;
            ArrayList<ContractStatement> tmpListnewcontractStmt = new ArrayList<>();
        if(contractStmt != null){
            for(ContractStatement elem : contractStmt){
                ContractStatement newcontractStmt = (ContractStatement)elem.accept(visitor);
                isChanged = isChanged || newcontractStmt != elem;
                tmpListnewcontractStmt.add(newcontractStmt);
            }
        }
            ArrayList<Behavior> tmpListnewbehaviors = new ArrayList<>();
        if(behaviors != null){
            for(Behavior elem : behaviors){
                Behavior newbehaviors = (Behavior)elem.accept(visitor);
                isChanged = isChanged || newbehaviors != elem;
                tmpListnewbehaviors.add(newbehaviors);
            }
        }
            Completeness newcompleteness = null;
        if(completeness != null){
            newcompleteness = (Completeness)completeness.accept(visitor);
        }
        if(isChanged || completeness != newcompleteness){
            return new Contract(tmpListnewcontractStmt.toArray(new ContractStatement[0]), tmpListnewbehaviors.toArray(new Behavior[0]), newcompleteness);
        }
        return this;
    }
}