content: package at.ac.tuwien.kr.alpha.core.grounder.structure;
  
  import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
  
  import java.util.Collections;
  import java.util.HashSet;
  import java.util.LinkedHashSet;
  import java.util.Set;
  
  import at.ac.tuwien.kr.alpha.api.programs.VariableNormalizableAtom;
  import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
  import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier;
  import at.ac.tuwien.kr.alpha.core.grounder.Unification;
  
  /**
   * Copyright (c) 2018, the Alpha Team.
   */
  public class LitSet {
  	private final Atom atom;
  	private final Set<Unifier> complementSubstitutions;
  	private final int hashCode;
  	private final Atom normalizedLiteral;
  	private final Set<Unifier> normalizedSubstitutions;
  	private static int litSetCounter = 1;
  
  	LitSet(Atom atom, Set<Unifier> complementSubstitutions) {
  		this.atom = atom.renameVariables("_AS" + litSetCounter++);
  		this.complementSubstitutions = new HashSet<>();
  		for (Unifier complementSubstitution : complementSubstitutions) {
  			if (complementSubstitution == null) {
  				throw oops("Unifier is null.");
  			}
  			Unifier unifyRightAtom = normalizeSubstitution(atom, complementSubstitution, this.atom);
  			if (unifyRightAtom == null) {
  				throw oops("Unification result is null.");
  			}
  			this.complementSubstitutions.add(unifyRightAtom);
  		}
  		this.normalizedLiteral = computeNormalized(this.atom, "_N");
  		this.normalizedSubstitutions = computeNormalizedSubstitutions();
  		this.hashCode = computeHashCode();
  	}
  
  	/**
  	 * Normalizes a substitution over the originalAtom into a substitution over the normalizedAtom.
  	 * @param originalAtom
  	 * @param substitution
  	 * @param normalizedAtom
  	 * @return
  	 */
  	private Unifier normalizeSubstitution(Atom originalAtom, Unifier substitution, Atom normalizedAtom) {
  		Atom substitutedLiteral = originalAtom.substitute(substitution);
  		return Unification.instantiate(normalizedAtom, substitutedLiteral);
  	}
  
  	/**
  	 * Checks if the complementSubstitutions exclude everything.
  	 * @return true if this LitSet represents the empty set (i.e., everything excluded).
  	 */
  	public boolean coversNothing() {
  		for (Unifier substitution : complementSubstitutions) {
  			if (Unification.instantiate(atom.substitute(substitution), atom) != null) {
  				return true;
  			}
  		}
  		return false;
  	}
  
  	public Atom getAtom() {
  		return atom;
  	}
  
  	Set<Unifier> getComplementSubstitutions() {
  		return Collections.unmodifiableSet(complementSubstitutions);
  	}
  
  	@Override
  	public String toString() {
  		StringBuilder sb = new StringBuilder("(" + atom + ",{");
  		for (Unifier complementSubstitution : complementSubstitutions) {
  			sb.append(atom.substitute(complementSubstitution));
  			sb.append(", ");
  		}
  		sb.append("})");
  		return sb.toString();
  	}
  
  	@Override
  	public boolean equals(Object o) {
  		if (this == o) {
  			return true;
  		}
  		if (o == null || getClass() != o.getClass()) {
  			return false;
  		}
  
  		LitSet litSet = (LitSet) o;
  
  		if (hashCode() != o.hashCode()) {
  			return false;
  		}
  
  		if (!normalizedLiteral.equals(litSet.normalizedLiteral)) {
  			return false;
  		}
  
  		return normalizedSubstitutions.equals(litSet.normalizedSubstitutions);
  	}
  
  	@Override
  	public int hashCode() {
  		return hashCode;
  	}
  
  	private int computeHashCode() {
  		int result = normalizedLiteral.hashCode();
  		result = 31 * result + normalizedSubstitutions.hashCode();
  		return result;
  	}
  
  	private Atom computeNormalized(Atom atom, String prefix) {
  		if (atom instanceof VariableNormalizableAtom) {
  			return ((VariableNormalizableAtom) atom).normalizeVariables(prefix, 0);
  		} else {
  			throw oops("Atom to normalize is of unknown type: " + atom);
  		}
  	}
  
  	private Set<Unifier> computeNormalizedSubstitutions() {
  		Set<Unifier> ret = new LinkedHashSet<>();
  		for (Unifier substitution : complementSubstitutions) {
  			Unifier preNormalizedSubstitution = normalizeSubstitution(atom, substitution, normalizedLiteral);
  			// Unifier may still contain variables in the right-hand side, those have to be normalized, too.
  			Atom appliedSub = normalizedLiteral.substitute(preNormalizedSubstitution);
  			// Apply substitution and normalize all remaining variables, i.e., those appearing at the right-hand side of the substitution.
  			Atom normalized = computeNormalized(appliedSub, "_X");
  			// Compute final substitution from normalized atom to the one where also variables are normalized.
  			Unifier normalizedSubstitution = new Unifier(Unification.instantiate(normalizedLiteral, normalized));
  			ret.add(normalizedSubstitution);
  		}
  		return ret;
  	}
  }
  