package JavaAgent.resource.fopl;


import java.util.*;

/** 
** A UnificationException can occur in an attemt to extend a Substitution. 
** When a Substitution is built up, usually during unification, new Variables
** that were not mentioned in the Substitution yet can be added to the 
** Substitution. When two Variables are unified with each other they are part
** of the Substitution, but there is no Term in the Substitution they are 
** being mapped to. Thus, when a Term is instantiated under a Substitution
** a new VarTerm with a new Variable is generated to which the old, unified 
** Variables can be mapped. To avoid unifying this Variable again, a 
** Substitution is blocked once such a new Variable has been generated.
** An attemt to extend a Substitution at this stage will cause a 
** UnificationException.
** @see Variable
** @see Substitution
*/

public class UnificationException extends Exception {

  /**
  ** This constructor takes a String which should be a short message 
  ** indicating why this exception was thrown and the Substitution from
  ** which it was thrown.
  */
  public UnificationException(String str, Substitution subst) {
    super(str);
    theSubst = subst;
  }

  /**
  ** This function returns the Substitution in which the Exception occured.
  ** @return the Substitution in which the Exception occured
  */
  public Substitution getSubstitution() {
    return theSubst;
  }

  private Substitution theSubst;
}


