| java.lang.Object
 de.uka.ilkd.key.logic.EqualityConstraint
| EqualityConstraint | | public class EqualityConstraint implements Constraint(Code) | | 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.
|
| Method Summary | |
| protected synchronized Object | clone()
| | public boolean | equals(Object obj)
| | public Term | getDirectInstantiation(Metavariable p_mv)
The most general known term that is more defining thanp_mv itself by which p_mv can be replaced if the constraint isvalid (or null if the constraint allows arbitraryinstantiations of p_mv). | | public synchronized Term | getInstantiation(Metavariable p_mv)
| | public int | hashCode()
| | public boolean | isAsStrongAs(Constraint co)
true iff this constraint is as strong as "co",i.e. | | public boolean | isAsWeakAs(Constraint co)
true iff this constraint is as weak as "co",i.e. | | final public boolean | isBottom()
| | boolean | isDefined(Metavariable mv)
| | final public boolean | isSatisfiable()
a constraint being instance of this class is satisfiable. | | public Constraint | join(Constraint co, Services services)
joins the given constraint with this constraint
and returns the joint new constraint. | | public synchronized Constraint | join(Constraint co, Services services, BooleanContainer unchanged)
joins constraint co with this constraint
and returns the joint new constraint. | | public Constraint | removeVariables(SetOfMetavariable mvs)
| | public IteratorOfMetavariable | restrictedMetavariables()
| | public String | toString()
| | public Constraint | unify(Term t1, Term t2, Services services)
unifies terms t1 and t2
Parameters:
t1 - Term to be unified
Parameters:
t2 - term to be unified
Parameters:
services - the Services providing access to the type model(e.g. | | public Constraint | unify(Term t1, Term t2, Services services, BooleanContainer unchanged)
executes unification for terms t1 and t2. | | Term | valueOf(Metavariable mv)
|
| EqualityConstraint | | public EqualityConstraint()(Code) | | Don't use this constructor, use Constraint.BOTTOM instead
|
| equals | | public boolean equals(Object obj)(Code) | | checks equality of constraints by subsuming relation (only equal if no
new sorts need to be introduced for subsumption)
|
| getDirectInstantiation | | public Term getDirectInstantiation(Metavariable p_mv)(Code) | | The most general known term that is more defining thanp_mv itself by which p_mv can be replaced if the constraint isvalid (or null if the constraint allows arbitraryinstantiations of p_mv). This is just the entry of map. |
| getInstantiation | | public synchronized Term getInstantiation(Metavariable p_mv)(Code) | | the term by which p_mv is instantiated by the mostgeneral substitution satisfying the constraint |
| hashCode | | public int hashCode()(Code) | | |
| isAsStrongAs | | public boolean isAsStrongAs(Constraint co)(Code) | | true iff this constraint is as strong as "co",i.e. every instantiation satisfying "this" also satisfies "co". |
| isAsWeakAs | | public boolean isAsWeakAs(Constraint co)(Code) | | true iff this constraint is as weak as "co",i.e. every instantiation satisfying "co" also satisfies "this". |
| isBottom | | final public boolean isBottom()(Code) | | returns true if Bottom
true if Bottom |
| isDefined | | boolean isDefined(Metavariable mv)(Code) | | ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY
true if metavar is contained as key |
| isSatisfiable | | final public boolean isSatisfiable()(Code) | | 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
true always |
| join | | public Constraint join(Constraint co, Services services)(Code) | | joins the given constraint with this constraint
and returns the joint new constraint.
Parameters:
co - Constraint to be joined with this one the joined constraint |
| join | | public synchronized Constraint join(Constraint co, Services services, BooleanContainer unchanged)(Code) | | 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.
Parameters:
co - Constraint to be joined with this one
Parameters:
services - the Services providing access to the type model
Parameters:
unchanged - the BooleanContainers value set true, if thisconstraint is as strong as co the joined constraint |
| removeVariables | | public Constraint removeVariables(SetOfMetavariable mvs)(Code) | | a constraint derived from this one by removing allconstraints on the given variable, which may therefore have anyvalue according to the new constraint (the possible values ofother variables are not modified) |
| restrictedMetavariables | | public IteratorOfMetavariable restrictedMetavariables()(Code) | | list of metavariables, instantiations of which mayrestricted by this constraint |
| toString | | public String toString()(Code) | | String representation of the constraint |
| unify | | public Constraint unify(Term t1, Term t2, Services services)(Code) | | unifies terms t1 and t2
Parameters:
t1 - Term to be unified
Parameters:
t2 - term to be unified
Parameters:
services - the Services providing access to the type model(e.g. necessary when introducing intersection sorts) TOP if not possible, else a new constraint with afterunification of t1 and t2 |
| unify | | public Constraint unify(Term t1, Term t2, Services services, BooleanContainer unchanged)(Code) | | executes unification for terms t1 and t2.
Parameters:
t1 - Term to be unfied
Parameters:
t2 - Term to be unfied
Parameters:
services - the Services providing access to the type model(e.g. necessary when introducing intersection sorts)
Parameters:
unchanged - true iff the new constraint equals this one TOP if not possible, else a new constraint unifying t1and t2 ( == this iff this subsumes the unification ) |
|
|