Package edu.harvard.seas.pl.abcdatalog.util.substitution

Class UnionFindBasedUnifier

java.lang.Object
edu.harvard.seas.pl.abcdatalog.util.substitution.UnionFindBasedUnifier
All Implemented Interfaces:
Substitution, TermUnifier
public class UnionFindBasedUnifier extends Object implements TermUnifier
A mapping from variables to terms. Implemented using a union-find data structure.

  • Constructor Details

    • UnionFindBasedUnifier

      public UnionFindBasedUnifier()
      Constructs an empty substitution.

    • UnionFindBasedUnifier

      public UnionFindBasedUnifier(UnionFindBasedUnifier other)
      Constructs a substitution from another substitution.
      Parameters:
      other - the other substitution

  • Method Details

    • get

      public Term get(Variable x)
      Retrieves the mapping of a variable.
      Specified by:
      get in interface Substitution
      Parameters:
      x - the variable
      Returns:
      the term that the variable is bound to, or null if the variable is not in the substitution

    • apply

      public Term[] apply(Term[] original)
      Description copied from interface: Substitution
      Apply this substitution to a list of terms, creating a new list.
      Specified by:
      apply in interface Substitution
      Parameters:
      original - the original list
      Returns:
      the new list

    • fromTerms

      public static UnionFindBasedUnifier fromTerms(List<Term> xs, List<Term> ys)
      Creates a substitution from unifying two lists of terms.
      Parameters:
      xs - the first list
      ys - the second list
      Returns:
      the substitution, or null if the two lists do not unify

    • fromTerms

      public static Substitution fromTerms(Term[] elts, Term[] elts2)
      Creates a substitution from unifying two arrays of terms.
      Parameters:
      xs - the first array
      ys - the second array
      Returns:
      the substitution, or null if the two lists do not unify

    • put

      public void put(Variable v, Term t)
      Adds a mapping from a variable to a term. Throws an IllegalArgumentException if doing so would result in a variable mapping to multiple constants.
      Parameters:
      v - the variable
      t - the term
      Throws:
      IllegalArgumentException - If the variable is already mapped to a different term

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • unify

      public boolean unify(Variable u, Term v)
      Description copied from interface: TermUnifier
      Attempts to unify a variable with a term. Returns a boolean representing whether the unification was successful. Unification fails if it would lead to a variable being unified with two distinct constants.
      Specified by:
      unify in interface TermUnifier
      Parameters:
      u - the variable
      v - the term
      Returns:
      whether the unification was successful