code: package com.naveensundarg.shadow.prover.representations.formula;
  
  import com.naveensundarg.shadow.prover.representations.value.Value;
  import com.naveensundarg.shadow.prover.representations.value.Variable;
  import com.naveensundarg.shadow.prover.utils.CollectionUtils;
  import com.naveensundarg.shadow.prover.utils.CommonUtils;
  import com.naveensundarg.shadow.prover.utils.Sets;
  
  import java.util.Map;
  import java.util.Set;
  import java.util.function.UnaryOperator;
  
  /**
   * Created by naveensundarg on 5/4/16.
   */
  public class Communicates extends BaseFormula{
  
      private final Value agent1;
      private final Value agent2;
      private final Value time;
      private final Formula formula;
      private final Set<Formula> subFormulae;
  
      private Set<Variable> variables;
      private Set<Value> values;
  
      private final Set<Variable> boundVariables;
  
      private final Set<Value> allValues;
  
      private final int weight;
  
      public Communicates(Value agent1,Value agent2, Value time, Formula formula) {
  
  
          this.agent1 = agent1;
          this.agent2 = agent2;
          this.time = time;
          this.formula = formula;
          this.subFormulae = CollectionUtils.setFrom(formula.subFormulae());
          this.subFormulae.add(this);
  
          this.allValues = Sets.newSet();
          this.allValues.add(agent1);
          this.allValues.add(agent2);
  
          this.allValues.add(time);
  
          this.variables = CollectionUtils.setFrom(formula.variablesPresent());
          this.values = CollectionUtils.setFrom(formula.valuesPresent());
  
          this.boundVariables = CollectionUtils.setFrom(formula.boundVariablesPresent());
  
          if (agent1 instanceof Variable) {
              variables.add((Variable) agent1);
          }
  
          if (agent2 instanceof Variable) {
              variables.add((Variable) agent2);
          }
          if (time instanceof Variable) {
              variables.add((Variable) time);
  
          }
  
          this.weight = 1 + agent1.getWeight()  + agent2.getWeight() + time.getWeight()  + formula.getWeight();
      }
  
      public Formula getFormula(){
          return formula;
      }
  
  
      public Value getOrigin() {
          return agent1;
      }
  
      public Value getDestination() {
          return agent1;
      }
  
      public Value getTime() {
          return time;
      }
  
      public Set<Formula> getSubFormulae() {
          return subFormulae;
      }
  
      public Set<Variable> getVariables() {
          return variables;
      }
  
      @Override
      public Set<Formula> subFormulae() {
          return subFormulae;
      }
  
      @Override
      public Set<Variable> variablesPresent() {
          return variables;
      }
  
      @Override
      public Formula apply(Map<Variable, Value> substitution) {
          return null;
      }
  
      @Override
      public Formula shadow(int level) {
          return new Atom("|"+ CommonUtils.sanitizeShadowedString(toString())+"|");
      }
  
      @Override
      public Formula applyOperation(UnaryOperator<Formula> operator) {
          return null;
      }
  
      @Override
      public int getLevel() {
          return 2;
      }
  
      @Override
      public int getWeight() {
          return weight;
      }
  
  
      @Override
      public String toString() {
          return "(Communicates! "
                  + agent1 + " "
                  + agent2 + " "
  
                  + time + " "+
                  formula + ")";
      }
  
      @Override
      public String toSnarkString() {
          return "(Communicates! "
                  + agent1.toSnarkString() + " "
                  + agent2.toSnarkString() + " "
  
                  + time.toSnarkString() + " "+
                  formula.toSnarkString() + ")";
      }
  
      @Override
      public boolean equals(Object o) {
          if (this == o) return true;
          if (o == null || getClass() != o.getClass()) return false;
  
          Communicates that = (Communicates) o;
  
          if (!agent1.equals(that.agent1)) return false;
          if (!agent2.equals(that.agent2)) return false;
          if (!time.equals(that.time)) return false;
          return formula.equals(that.formula);
      }
  
      @Override
      public int hashCode() {
          int result = safeHashCode(agent1);
          result = 31 * result + safeHashCode(agent2);
          result = 31 * result + safeHashCode(time);
          result = 31 * result + safeHashCode(formula);
          return result;
      }
  
      @Override
      public Set<Value> allValues() {
          return allValues;
      }
  
      @Override
      public String getName() {
          return "Communicates";
      }
  
  
      @Override
      public Formula replaceSubFormula(Formula oldFormula, Formula newFormula) {
          if(oldFormula.equals(this)){
  
              return newFormula;
          }
  
          if(!subFormulae().contains(oldFormula)){
  
              return this;
          }
  
  
          return new Communicates(agent1, agent2, time, formula.replaceSubFormula(oldFormula, newFormula));
      }
  
      @Override
      public Set<Variable> boundVariablesPresent() {
          return boundVariables;
      }
  
      @Override
      public Set<Value> valuesPresent() {
          return values;
      }
  }
  