@Deprecated public class EqualityConstraint extends java.lang.Object implements Constraint
Modifier and Type | Class and Description |
---|---|
private static class |
EqualityConstraint.ECPair
Deprecated.
|
Constraint.Top
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.
|
BOTTOM, TOP
Modifier | Constructor and Description |
---|---|
|
EqualityConstraint()
Deprecated.
Don't use this constructor, use Constraint.BOTTOM instead
|
private |
EqualityConstraint(java.util.HashMap<Metavariable,Term> map)
Deprecated.
|
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
|
private static final BooleanContainer CONSTRAINTBOOLEANCONTAINER
private java.util.HashMap<Metavariable,Term> map
private java.util.HashMap<Metavariable,Term> instantiationCache
private java.lang.Integer hashCode
private static java.util.WeakHashMap<Term,ImmutableSet<Metavariable>> mvCache
private static NameAbstractionTable FAILED
private static final java.lang.Object joinCacheMonitor
private static java.util.Map<EqualityConstraint.ECPair,Constraint> joinCache
private static java.util.Map<EqualityConstraint.ECPair,Constraint> joinCacheOld
private static final EqualityConstraint.ECPair ecPair0
public EqualityConstraint()
private EqualityConstraint(java.util.HashMap<Metavariable,Term> map)
public static ImmutableSet<Metavariable> metaVars(Term t)
protected java.lang.Object clone()
clone
in class java.lang.Object
public final boolean isBottom()
isBottom
in interface Constraint
public final boolean isSatisfiable()
isSatisfiable
in interface Constraint
public java.util.Iterator<Metavariable> restrictedMetavariables()
public Term getDirectInstantiation(Metavariable p_mv)
public Term getInstantiation(Metavariable p_mv, Services services)
getInstantiation
in interface Constraint
p_mv
- the Metavariableservices
- the Servicesprivate Term getInstantiationIfExisting(Metavariable p_mv)
private Term instantiate(Term p, Services services)
p
according to the instantiations
of the metavariables described by this constraint.p
- the Term p to be instantiatedpublic Constraint unify(Term t1, Term t2, TermServices services)
unify
in interface Constraint
t1
- Term to be unifiedt2
- term to be unifiedservices
- the Services providing access to the type model
(e.g. necessary when introducing intersection sorts)public Constraint unify(Term t1, Term t2, TermServices services, BooleanContainer unchanged)
unify
in interface Constraint
t1
- Term to be unfiedt2
- Term to be unfiedservices
- the Services providing access to the type model
(e.g. necessary when introducing intersection sorts)unchanged
- true iff the new constraint equals this oneprivate static boolean compareBoundVariables(QuantifiableVariable ownVar, QuantifiableVariable cmpVar, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars)
ownVar
- first QuantifiableVariable to be comparedcmpVar
- second QuantifiableVariable to be comparedownBoundVars
- variables bound above the current positioncmpBoundVars
- variables bound above the current positionprivate static int indexOf(QuantifiableVariable var, ImmutableList<QuantifiableVariable> list)
var
in
list
, or -1
if the variable is not
an element of the listprivate Constraint unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat, boolean modifyThis, TermServices services)
t0
- the first termt1
- the second termownBoundVars
- variables bound above the current positioncmpBoundVars
- variables bound above the current positionmodifyThis
- this
is an object that has just been created
during this unification processservices
- 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.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
termsprivate Constraint introduceNewMV(Term t0, Term t1, boolean modifyThis, TermServices services)
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.t0
- t1
- services
- private static NameAbstractionTable handleJava(Term t0, Term t1, NameAbstractionTable nat)
private Constraint descendRecursively(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat, boolean modifyThis, TermServices services)
private static NameAbstractionTable checkNat(NameAbstractionTable nat)
private Constraint handleTwoMetavariables(Term t0, Term t1, boolean modifyThis, TermServices services)
private Constraint handleQuantifiableVariable(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars)
private Constraint unifyHelp(Term t1, Term t2, boolean modifyThis, TermServices services)
modifyThis
- this
is an object that has just been created
during this unification processservices
- the Services providing access to the type modelthis
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
termsprivate Constraint normalize(Metavariable mv, Term t, boolean modifyThis, TermServices services)
mv
- Metavariable asked to be mapped to the term tt
- the Term the metavariable should be mapped to (if there
are no cycles )services
- the Services providing access to the type modelprivate EqualityConstraint getMutableConstraint(boolean modifyThis)
public boolean equals(java.lang.Object obj)
equals
in interface Constraint
equals
in class java.lang.Object
public boolean isAsStrongAs(Constraint co)
isAsStrongAs
in interface Constraint
public boolean isAsWeakAs(Constraint co)
isAsWeakAs
in interface Constraint
public Constraint join(Constraint co, TermServices services)
join
in interface Constraint
co
- Constraint to be joined with this oneservices
- the Services providing access to the type modelpublic Constraint join(Constraint co, TermServices services, BooleanContainer unchanged)
join
in interface Constraint
co
- Constraint to be joined with this oneservices
- the Services providing access to the type modelunchanged
- the BooleanContainers value set true, if this
constraint is as strong as coprivate Constraint joinHelp(EqualityConstraint co, TermServices services)
private boolean hasCycle(Metavariable mv, Term term)
mv
- the Metavariableterm
- The Termprivate boolean hasCycleByInst(Metavariable mv, Term term)
boolean isDefined(Metavariable mv)
Term valueOf(Metavariable mv)
public java.lang.String toString()
toString
in interface Constraint
toString
in class java.lang.Object
public int hashCode()
hashCode
in interface Constraint
hashCode
in class java.lang.Object