code: package com.naveensundarg.shadow.prover.constraints;
  
  import com.naveensundarg.shadow.prover.representations.formula.Formula;
  import com.naveensundarg.shadow.prover.representations.formula.Predicate;
  import com.naveensundarg.shadow.prover.representations.value.Variable;
  import com.naveensundarg.shadow.prover.utils.CollectionUtils;
  import com.naveensundarg.shadow.prover.utils.Sets;
  import us.bpsm.edn.parser.Parseable;
  import us.bpsm.edn.parser.Parser;
  import us.bpsm.edn.parser.Parsers;
  
  import java.io.InputStream;
  import java.io.InputStreamReader;
  import java.util.List;
  import java.util.Map;
  import java.util.Set;
  import java.util.concurrent.atomic.AtomicBoolean;
  import java.util.stream.Collectors;
  
  import static us.bpsm.edn.parser.Parsers.defaultConfiguration;
  
  /**
   * Created by naveensundarg on 9/9/17.
   */
  public class Signature implements Constraint {
  
      private final Map<String, Set<Integer>> arities;
  
      public Signature(Map<String, Set<Integer>> arities) {
  
          this.arities = arities;
      }
  
      public Signature(InputStream is) {
  
          try {
  
              Parseable pbr = Parsers.newParseable(new InputStreamReader(is));
              Parser p = Parsers.newParser(defaultConfiguration());
  
              Map<?, ?> map = (Map<?, ?>) p.nextValue(pbr);
  
              Map<String, Set<Integer>> arities = CollectionUtils.newMap();
              AtomicBoolean errorOccured = new AtomicBoolean(false);
              map.entrySet().forEach(entry -> {
  
                  String name = entry.getKey().toString();
  
                  List<?> vals = (List<?>) entry.getValue();
  
  
                  Set<Integer> numbers = Sets.newSet();
  
                  vals.forEach(x-> numbers.add(Integer.parseInt(x.toString())));
  
                  arities.put(name, numbers);
  
              });
  
  
              if (errorOccured.get()) {
  
                  throw new AssertionError("Could not read axiom set from file.");
              } else {
  
                  this.arities = arities;
              }
  
  
          } catch (Exception e) {
              e.printStackTrace();
              throw new AssertionError("Could not read axiom set from file.");
          }
  
      }
  
  
      private Set<String> predicatesThatAreInCorrect(Formula formula) {
  
          return formula.subFormulae().stream().filter(sub -> sub instanceof Predicate).map(x -> (Predicate) x).filter(x -> {
  
              String name = x.getName();
              int arity = x.getArguments().length;
  
              return !(arities.containsKey(name) && arities.get(name).contains(arity));
  
          }).map(Predicate::toString).collect(Collectors.toSet());
      }
  
      private Set<String> functionsThatAreInCorrect(Formula formula) {
  
          return formula.valuesPresent().stream().filter(v -> !(v instanceof Variable)).filter(x -> {
  
  
              String name = x.getName();
              int arity = x.getArguments().length;
  
              return !(arities.containsKey(name) && arities.get(name).contains(arity));
  
          }).map(Object::toString).collect(Collectors.toSet());
      }
  
      @Override
      public boolean satisfies(Set<Formula> formulae) {
  
  
          Set<String> violations = formulae.stream().
                  map(x->Sets.union(predicatesThatAreInCorrect(x),functionsThatAreInCorrect(x))).reduce(Sets.newSet(), Sets::union);
  
          if (!violations.isEmpty()) {
  
              throw new AssertionError(this.getClass() + " violated by: " + violations);
          }
  
          return true;
  
      }
  
      public static  void main(String[] args){
  
      }
  }
  