blog
Class Substitution

java.lang.Object
  blog.Substitution

public class Substitution
extends java.lang.Object

A mapping from logical variables to terms.

Field Summary

protected java.util.Map<LogicalVar,Term>

map

Constructor Summary

Substitution()
Creates a new "empty" substitution that does not change anything.

Substitution(java.util.List<LogicalVar> vars, java.util.List<? extends Term> terms)
Creates a new substitution that maps the given list of logical variables respectively to the given list of terms.

Method Summary

void	add(LogicalVar var, Term replacement) Adds the given mapping to this substitution, replacing any existing mapping for var.
boolean	equals(java.lang.Object o)
java.util.Set<LogicalVar>	getPreimage(Term t, boolean allowSelf) Returns the set of logical variables that map to the given term.
Term	getReplacement(LogicalVar var) Returns the replacement for the given logical variable, or the logical variable itself if no replacement has been specified.
java.util.Set<LogicalVar>	getVars()
boolean	hasConstant()
int	hashCode()
boolean	isOneToOneOn(java.util.Collection<LogicalVar> vars) Returns true if this substitution, restricted to the given variables, is one-to-one.
boolean	makeEqual(Term t1, Term t2) Adds the given mapping to this substitution, and keeps the substitution in normal form (so that the rewrites can be applied in any order).
void	remove(LogicalVar var) Removes the mapping (if any) for the given logical variable.
int	size()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

map

protected java.util.Map<LogicalVar,Term> map

Constructor Detail

Substitution

public Substitution()

Creates a new "empty" substitution that does not change anything.

Substitution

public Substitution(java.util.List<LogicalVar> vars,
                    java.util.List<? extends Term> terms)

Creates a new substitution that maps the given list of logical variables respectively to the given list of terms.

Throws:

java.lang.IllegalArgumentException - if the two given lists have different lengths

Method Detail

add

public void add(LogicalVar var,
                Term replacement)

Adds the given mapping to this substitution, replacing any existing mapping for var.

remove

public void remove(LogicalVar var)

Removes the mapping (if any) for the given logical variable.

makeEqual

public boolean makeEqual(Term t1,
                         Term t2)

Adds the given mapping to this substitution, and keeps the substitution in normal form (so that the rewrites can be applied in any order). Returns false if the substitution can't be converted to normal form. This function is doing a simple case of unification.

getReplacement

public Term getReplacement(LogicalVar var)

Returns the replacement for the given logical variable, or the logical variable itself if no replacement has been specified.

getPreimage

public java.util.Set<LogicalVar> getPreimage(Term t,
                                             boolean allowSelf)

Returns the set of logical variables that map to the given term.

Parameters:

allowSelf - if true, the set returned may include t itself; otherwise t is excluded

isOneToOneOn

public boolean isOneToOneOn(java.util.Collection<LogicalVar> vars)

Returns true if this substitution, restricted to the given variables, is one-to-one.

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

size

public int size()

hasConstant

public boolean hasConstant()

getVars

public java.util.Set<LogicalVar> getVars()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object