code: package com.naveensundarg.shadow.prover.core.rules;
  
  import com.naveensundarg.shadow.prover.core.proof.Unifier;
  import com.naveensundarg.shadow.prover.representations.cnf.Clause;
  import com.naveensundarg.shadow.prover.representations.cnf.Literal;
  import com.naveensundarg.shadow.prover.representations.formula.Predicate;
  import com.naveensundarg.shadow.prover.representations.value.Value;
  import com.naveensundarg.shadow.prover.representations.value.Variable;
  import com.naveensundarg.shadow.prover.utils.Sets;
  
  import java.util.Arrays;
  import java.util.Map;
  import java.util.Objects;
  import java.util.Set;
  import java.util.stream.Collectors;
  
  import static com.naveensundarg.shadow.prover.utils.Sets.newSet;
  
  /**
   * Created by naveensundarg on 4/15/16.
   */
  public enum DemodulationImplementation implements ForwardClauseRule {
  
      INSTANCE;
  
  
      private boolean isEquals(Clause clause){
  
          return clause.getLiterals().size()==1 &&
                  clause.getLiterals().stream().allMatch(x->x.getPredicate().getName().equals("="));
  
      }
  
      private Value getLeft(Clause clause){
  
          assert isEquals(clause);
          return clause.getLiterals().stream().map(Literal::getPredicate).map(x->x.getArguments()[0]).findAny().get();
      }
  
      private Value getRight(Clause clause){
  
          assert isEquals(clause);
          return clause.getLiterals().stream().map(Literal::getPredicate).map(x->x.getArguments()[1]).findAny().get();
      }
  
      @Override
      public Set<Clause> apply(Clause clause1, Clause clause2) {
  
          return Sets.union(applyInner(clause1, clause2), applyInner(clause2, clause1));
  
      }
      public Set<Clause> applyInner(Clause clause1, Clause clause2) {
  
  
          if(isEquals(clause1)){
              Value x = getLeft(clause1);
              Value y = getRight(clause1);
  
              Set<Map<Variable, Value>> subUnifications =
  
                      clause2.getLiterals().stream().
                              map(Literal::getPredicate).
                              map(Predicate::getArguments).
                              flatMap(Arrays::stream).
                              map(Z-> Unifier.subUnify(x, Z)).
                              filter(Objects::nonNull).
                              reduce(newSet(), Sets::union);
  
  
              return subUnifications.stream().map(theta-> clause2.replace(x.apply(theta), y.apply(theta))).collect(Collectors.toSet());
  
          } else {
  
              return newSet();
          }
  
  
  
      }
  
  
  }
  