de.uka.ilkd.key.strategy.quantifierHeuristics

Class EqualityConstraint

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint

All Implemented Interfaces:

Constraint

Deprecated.

@Deprecated
public class EqualityConstraint
extends java.lang.Object
implements Constraint

This class implements a persistent constraint. The constraint contains pairs of Metavariables X and Terms t meaning X=t. It offers services like joining two Constraint objects, adding new constraints to this one by unfying two terms and creating all necessary Metavariable - Term pairs. There are no public constructors to build up a new Constraint use the BOTTOM constraint of the Constraint interface (static final class variable) and add the needed constraints. If a constraint would not be satisfiable (cycles, unification failed) the Constraint TOP of interface Constraint is returned.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	EqualityConstraint.ECPair Deprecated.

Nested classes/interfaces inherited from interface de.uka.ilkd.key.strategy.quantifierHeuristics.Constraint

Constraint.Top

Field Summary

Fields

Modifier and Type	Field and Description
private static BooleanContainer	CONSTRAINTBOOLEANCONTAINER Deprecated. contains a boolean value
private static EqualityConstraint.ECPair	ecPair0 Deprecated.
private static NameAbstractionTable	FAILED Deprecated. used to encode that handleJava results in an unsatisfiable constraint (faster than using exceptions)
private java.lang.Integer	hashCode Deprecated.
private java.util.HashMap<Metavariable,Term>	instantiationCache Deprecated. cache for return values of getInstantiation
private static java.util.Map<EqualityConstraint.ECPair,Constraint>	joinCache Deprecated.
private static java.lang.Object	joinCacheMonitor Deprecated.
private static java.util.Map<EqualityConstraint.ECPair,Constraint>	joinCacheOld Deprecated.
private java.util.HashMap<Metavariable,Term>	map Deprecated. stores constraint content as a mapping from Metavariable to Term
private static java.util.WeakHashMap<Term,ImmutableSet<Metavariable>>	mvCache Deprecated.

Fields inherited from interface de.uka.ilkd.key.strategy.quantifierHeuristics.Constraint

BOTTOM, TOP

Constructor Summary

Constructors

Modifier	Constructor and Description
	EqualityConstraint() Deprecated. Don't use this constructor, use Constraint.BOTTOM instead
private	EqualityConstraint(java.util.HashMap<Metavariable,Term> map) Deprecated.

Method Summary

Modifier and Type	Method and Description
private static NameAbstractionTable	checkNat(NameAbstractionTable nat) Deprecated.
protected java.lang.Object	clone() Deprecated.
private static boolean	compareBoundVariables(QuantifiableVariable ownVar, QuantifiableVariable cmpVar, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars) Deprecated. compare two quantifiable variables if they are equal modulo renaming
private Constraint	descendRecursively(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat, boolean modifyThis, TermServices services) Deprecated.
boolean	equals(java.lang.Object obj) Deprecated. checks equality of constraints by subsuming relation (only equal if no new sorts need to be introduced for subsumption)
Term	getDirectInstantiation(Metavariable p_mv) Deprecated.
Term	getInstantiation(Metavariable p_mv, Services services) Deprecated. Find a term the given metavariable can be instantiated with which is consistent with every instantiation that satisfies this constraint (that means, the term such an instantiation substitutes the metavariable with can always be unified with the returned term).
private Term	getInstantiationIfExisting(Metavariable p_mv) Deprecated.
private EqualityConstraint	getMutableConstraint(boolean modifyThis) Deprecated.
private static NameAbstractionTable	handleJava(Term t0, Term t1, NameAbstractionTable nat) Deprecated.
private Constraint	handleQuantifiableVariable(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars) Deprecated.
private Constraint	handleTwoMetavariables(Term t0, Term t1, boolean modifyThis, TermServices services) Deprecated.
private boolean	hasCycle(Metavariable mv, Term term) Deprecated. checks if there is a cycle if the metavariable mv and Term term would be added to this constraint e.g.
private boolean	hasCycleByInst(Metavariable mv, Term term) Deprecated.
int	hashCode() Deprecated.
private static int	indexOf(QuantifiableVariable var, ImmutableList<QuantifiableVariable> list) Deprecated.
private Term	instantiate(Term p, Services services) Deprecated. instantiates term p according to the instantiations of the metavariables described by this constraint.
private Constraint	introduceNewMV(Term t0, Term t1, boolean modifyThis, TermServices services) Deprecated. Resolve an equation X=Y (concerning two metavariables) by introducing a third variable Z whose sort is the intersection of the sorts of X,Y and adding equations X=Z,Y=Z.
boolean	isAsStrongAs(Constraint co) Deprecated.
boolean	isAsWeakAs(Constraint co) Deprecated.
boolean	isBottom() Deprecated. returns true if Bottom
(package private) boolean	isDefined(Metavariable mv) Deprecated. ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY
boolean	isSatisfiable() Deprecated. a constraint being instance of this class is satisfiable.
Constraint	join(Constraint co, TermServices services) Deprecated. joins the given constraint with this constraint and returns the joint new constraint.
Constraint	join(Constraint co, TermServices services, BooleanContainer unchanged) Deprecated. joins constraint co with this constraint and returns the joint new constraint.
private Constraint	joinHelp(EqualityConstraint co, TermServices services) Deprecated.
static ImmutableSet<Metavariable>	metaVars(Term t) Deprecated.
private Constraint	normalize(Metavariable mv, Term t, boolean modifyThis, TermServices services) Deprecated. checks for cycles and adds additional constraints if necessary PRECONDITION: the sorts of mv and t match; if t is also a metavariable with same sort as mv, the order of mv and t is correct (using Metavariable.compareTo)
java.util.Iterator<Metavariable>	restrictedMetavariables() Deprecated.
java.lang.String	toString() Deprecated.
Constraint	unify(Term t1, Term t2, TermServices services) Deprecated. unifies terms t1 and t2
Constraint	unify(Term t1, Term t2, TermServices services, BooleanContainer unchanged) Deprecated. executes unification for terms t1 and t2.
private Constraint	unifyHelp(Term t1, Term t2, boolean modifyThis, TermServices services) Deprecated. Unify t1 and t2
private Constraint	unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat, boolean modifyThis, TermServices services) Deprecated. Compares two terms modulo bound renaming and return a (possibly new) constraint object that holds the instantiations necessary to make the two terms equal.
(package private) Term	valueOf(Metavariable mv) Deprecated. ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY

Methods inherited from class java.lang.Object

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

Field Detail

CONSTRAINTBOOLEANCONTAINER

private static final BooleanContainer CONSTRAINTBOOLEANCONTAINER

Deprecated.

contains a boolean value

map

private java.util.HashMap<Metavariable,Term> map

Deprecated.

stores constraint content as a mapping from Metavariable to Term

instantiationCache

private java.util.HashMap<Metavariable,Term> instantiationCache

Deprecated.

cache for return values of getInstantiation

hashCode

private java.lang.Integer hashCode

Deprecated.

mvCache

private static java.util.WeakHashMap<Term,ImmutableSet<Metavariable>> mvCache

Deprecated.

FAILED

private static NameAbstractionTable FAILED

Deprecated.

used to encode that handleJava results in an unsatisfiable constraint (faster than using exceptions)

joinCacheMonitor

private static final java.lang.Object joinCacheMonitor

Deprecated.

joinCache

private static java.util.Map<EqualityConstraint.ECPair,Constraint> joinCache

Deprecated.

joinCacheOld

private static java.util.Map<EqualityConstraint.ECPair,Constraint> joinCacheOld

Deprecated.

ecPair0

private static final EqualityConstraint.ECPair ecPair0

Deprecated.

Constructor Detail

EqualityConstraint

public EqualityConstraint()

Deprecated.

Don't use this constructor, use Constraint.BOTTOM instead

EqualityConstraint

private EqualityConstraint(java.util.HashMap<Metavariable,Term> map)

Deprecated.

Method Detail

metaVars

public static ImmutableSet<Metavariable> metaVars(Term t)

Deprecated.

clone

protected java.lang.Object clone()

Deprecated.

Overrides:

clone in class java.lang.Object

isBottom

public final boolean isBottom()

Deprecated.

returns true if Bottom

Specified by:

isBottom in interface Constraint

Returns:

true if Bottom

isSatisfiable

public final boolean isSatisfiable()

Deprecated.

a constraint being instance of this class is satisfiable. If a method realizes that an unsatisfiable Constraint would be built because of failed unification, cycle or s.th. similar it returns the singleton TOP being instance of the subclass Top

Specified by:

isSatisfiable in interface Constraint

Returns:

true always

restrictedMetavariables

public java.util.Iterator<Metavariable> restrictedMetavariables()

Deprecated.

Returns:

list of metavariables, instantiations of which may restricted by this constraint

getDirectInstantiation

public Term getDirectInstantiation(Metavariable p_mv)

Deprecated.

Returns:

The most general known term that is more defining than p_mv itself by which p_mv can be replaced if the constraint is valid (or null if the constraint allows arbitrary instantiations of p_mv). This is just the entry of map.

getInstantiation

public Term getInstantiation(Metavariable p_mv,
                             Services services)

Deprecated.

Find a term the given metavariable can be instantiated with which is consistent with every instantiation that satisfies this constraint (that means, the term such an instantiation substitutes the metavariable with can always be unified with the returned term).

Specified by:

getInstantiation in interface Constraint

Parameters:

p_mv - the Metavariable

services - the Services

Returns:

a term the given metavariable can be instantiated with

getInstantiationIfExisting

private Term getInstantiationIfExisting(Metavariable p_mv)

Deprecated.

instantiate

private Term instantiate(Term p,
                         Services services)

Deprecated.

instantiates term p according to the instantiations of the metavariables described by this constraint.

Parameters:

p - the Term p to be instantiated

Returns:

the instantiated term

unify

public Constraint unify(Term t1,
                        Term t2,
                        TermServices services)

Deprecated.

unifies terms t1 and t2

Specified by:

unify in interface Constraint

Parameters:

t1 - Term to be unified

t2 - term to be unified

services - the Services providing access to the type model (e.g. necessary when introducing intersection sorts)

Returns:

TOP if not possible, else a new constraint with after unification of t1 and t2

unify

public Constraint unify(Term t1,
                        Term t2,
                        TermServices services,
                        BooleanContainer unchanged)

Deprecated.

executes unification for terms t1 and t2.

Specified by:

unify in interface Constraint

Parameters:

t1 - Term to be unfied

t2 - Term to be unfied

services - the Services providing access to the type model (e.g. necessary when introducing intersection sorts)

unchanged - true iff the new constraint equals this one

Returns:

TOP if not possible, else a new constraint unifying t1 and t2 ( == this iff this subsumes the unification )

compareBoundVariables

private static boolean compareBoundVariables(QuantifiableVariable ownVar,
                                             QuantifiableVariable cmpVar,
                                             ImmutableList<QuantifiableVariable> ownBoundVars,
                                             ImmutableList<QuantifiableVariable> cmpBoundVars)

Deprecated.

compare two quantifiable variables if they are equal modulo renaming

Parameters:

ownVar - first QuantifiableVariable to be compared

cmpVar - second QuantifiableVariable to be compared

ownBoundVars - variables bound above the current position

cmpBoundVars - variables bound above the current position

indexOf

private static int indexOf(QuantifiableVariable var,
                           ImmutableList<QuantifiableVariable> list)

Deprecated.

Returns:

the index of the first occurrence of var in list, or -1 if the variable is not an element of the list

unifyHelp

private Constraint unifyHelp(Term t0,
                             Term t1,
                             ImmutableList<QuantifiableVariable> ownBoundVars,
                             ImmutableList<QuantifiableVariable> cmpBoundVars,
                             NameAbstractionTable nat,
                             boolean modifyThis,
                             TermServices services)

Deprecated.

Compares two terms modulo bound renaming and return a (possibly new) constraint object that holds the instantiations necessary to make the two terms equal.

Parameters:

t0 - the first term

t1 - the second term

ownBoundVars - variables bound above the current position

cmpBoundVars - variables bound above the current position

modifyThis - this is an object that has just been created during this unification process

services - the Services providing access to the type model (e.g. necessary when introducing intersection sorts). Value null is allowed, but unification fails (i.e. @link Constraint#TOP is returned), if e.g. intersection sorts are required.

Returns:

a constraint under which t0, t1 are equal modulo bound renaming. this is returned iff the terms are equal modulo bound renaming under this, or modifyThis==true and the terms are unifiable. For !modifyThis a new object is created, and this is never modified. Constraint.TOP is always returned for ununifiable terms

introduceNewMV

private Constraint introduceNewMV(Term t0,
                                  Term t1,
                                  boolean modifyThis,
                                  TermServices services)

Deprecated.

Resolve an equation X=Y (concerning two metavariables) by introducing a third variable Z whose sort is the intersection of the sorts of X,Y and adding equations X=Z,Y=Z. NB: This method must only be called if none of the sorts of t0,t1 is subsort of the other one. Otherwise the resulting equation might get commuted, Z might occur on the left side of the new equations and horrible things will happen.

Parameters:

t0 -

t1 -

services -

Returns:

the constraint

handleJava

private static NameAbstractionTable handleJava(Term t0,
                                               Term t1,
                                               NameAbstractionTable nat)

Deprecated.

descendRecursively

private Constraint descendRecursively(Term t0,
                                      Term t1,
                                      ImmutableList<QuantifiableVariable> ownBoundVars,
                                      ImmutableList<QuantifiableVariable> cmpBoundVars,
                                      NameAbstractionTable nat,
                                      boolean modifyThis,
                                      TermServices services)

Deprecated.

checkNat

private static NameAbstractionTable checkNat(NameAbstractionTable nat)

Deprecated.

handleTwoMetavariables

private Constraint handleTwoMetavariables(Term t0,
                                          Term t1,
                                          boolean modifyThis,
                                          TermServices services)

Deprecated.

handleQuantifiableVariable

private Constraint handleQuantifiableVariable(Term t0,
                                              Term t1,
                                              ImmutableList<QuantifiableVariable> ownBoundVars,
                                              ImmutableList<QuantifiableVariable> cmpBoundVars)

Deprecated.

unifyHelp

private Constraint unifyHelp(Term t1,
                             Term t2,
                             boolean modifyThis,
                             TermServices services)

Deprecated.

Unify t1 and t2

Parameters:

modifyThis - this is an object that has just been created during this unification process

services - the Services providing access to the type model

Returns:

a constraint under which t0, t1 are equal modulo bound renaming. this is returned iff the terms are equal modulo bound renaming under this, or modifyThis==true and the terms are unifiable. For !modifyThis a new object is created, and this is never modified. Constraint.TOP is always returned for ununifiable terms

normalize

private Constraint normalize(Metavariable mv,
                             Term t,
                             boolean modifyThis,
                             TermServices services)

Deprecated.

checks for cycles and adds additional constraints if necessary PRECONDITION: the sorts of mv and t match; if t is also a metavariable with same sort as mv, the order of mv and t is correct (using Metavariable.compareTo)

Parameters:

mv - Metavariable asked to be mapped to the term t

t - the Term the metavariable should be mapped to (if there are no cycles )

services - the Services providing access to the type model

Returns:

the resulting Constraint ( == this iff this subsumes the new constraint )

getMutableConstraint

private EqualityConstraint getMutableConstraint(boolean modifyThis)

Deprecated.

equals

public boolean equals(java.lang.Object obj)

Deprecated.

checks equality of constraints by subsuming relation (only equal if no new sorts need to be introduced for subsumption)

Specified by:

equals in interface Constraint

Overrides:

equals in class java.lang.Object

isAsStrongAs

public boolean isAsStrongAs(Constraint co)

Deprecated.

Specified by:

isAsStrongAs in interface Constraint

Returns:

true iff this constraint is as strong as "co", i.e. every instantiation satisfying "this" also satisfies "co".

isAsWeakAs

public boolean isAsWeakAs(Constraint co)

Deprecated.

Specified by:

isAsWeakAs in interface Constraint

Returns:

true iff this constraint is as weak as "co", i.e. every instantiation satisfying "co" also satisfies "this".

join

public Constraint join(Constraint co,
                       TermServices services)

Deprecated.

joins the given constraint with this constraint and returns the joint new constraint.

Specified by:

join in interface Constraint

Parameters:

co - Constraint to be joined with this one

services - the Services providing access to the type model

Returns:

the joined constraint

join

public Constraint join(Constraint co,
                       TermServices services,
                       BooleanContainer unchanged)

Deprecated.

joins constraint co with this constraint and returns the joint new constraint. The BooleanContainer is used to wrap a second return value and indicates a subsumption of co by this constraint.

Specified by:

join in interface Constraint

Parameters:

co - Constraint to be joined with this one

services - the Services providing access to the type model

unchanged - the BooleanContainers value set true, if this constraint is as strong as co

Returns:

the joined constraint

joinHelp

private Constraint joinHelp(EqualityConstraint co,
                            TermServices services)

Deprecated.

hasCycle

private boolean hasCycle(Metavariable mv,
                         Term term)

Deprecated.

checks if there is a cycle if the metavariable mv and Term term would be added to this constraint e.g. X=g(Y), Y=f(X)

Parameters:

mv - the Metavariable

term - The Term

Returns:

a boolean that is true iff. adding a mapping (mv,term) would cause a cycle

hasCycleByInst

private boolean hasCycleByInst(Metavariable mv,
                               Term term)

Deprecated.

isDefined

boolean isDefined(Metavariable mv)

Deprecated.

ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY

Returns:

true if metavar is contained as key

valueOf

Term valueOf(Metavariable mv)

Deprecated.

ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY

Returns:

mapping to mv

toString

public java.lang.String toString()

Deprecated.

Specified by:

toString in interface Constraint

Overrides:

toString in class java.lang.Object

Returns:

String representation of the constraint

hashCode

public int hashCode()

Deprecated.

Specified by:

hashCode in interface Constraint

Overrides:

hashCode in class java.lang.Object