| de.uka.ilkd.key.logic.Constraint
All known Subclasses: de.uka.ilkd.key.logic.EqualityConstraint, de.uka.ilkd.key.logic.IntersectionConstraint,
| Constraint | | public interface Constraint (Code) | | Abstract constraint interface for constraints offering unification
of terms and joins. There are no public constructors to build up a
new Constraint use the BOTTOM constraint (static final class
variable) and add the needed constraints if a constraint would not
be satisfiable (cycles, unification failed) the Constraint TOP is
returned. TOP is as well as BOTTOM a static final class variable
(means usage of singleton pattern for Constraints BOTTOM and TOP).
Unsatisfiable constrains should only be representated by the TOP
element.
|
| Method Summary | |
| boolean | equals(Object obj)
| | Term | getInstantiation(Metavariable p_mv)
| | boolean | isAsStrongAs(Constraint co)
true iff this constraint is as strong as "co",i.e. | | boolean | isAsWeakAs(Constraint co)
true iff this constraint is as weak as "co",i.e. | | boolean | isBottom()
| | boolean | isSatisfiable()
a constraint being instance of this class is satisfiable. | | Constraint | join(Constraint co, Services services)
joins the given constraint with this constraint and returns
the joint new constraint. | | Constraint | join(Constraint co, Services services, BooleanContainer unchanged)
joins constraint co with this constraint and returns the joint
new constraint. | | Constraint | removeVariables(SetOfMetavariable mvs)
| | String | toString()
| | Constraint | unify(Term t1, Term t2, Services services)
tries to unify the 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 modelthe parameter may be null but then the unification fails (i.e. | | Constraint | unify(Term t1, Term t2, Services services, BooleanContainer unchanged)
tries to unify terms t1 and t2. |
| BOTTOM | | Constraint BOTTOM(Code) | | standard constraint class implementing the offered functionality
|
| equals | | boolean equals(Object obj)(Code) | | checks equality of constraints
|
| getInstantiation | | Term getInstantiation(Metavariable p_mv)(Code) | | Find a term the given metavariable can be instantiatedwith which is consistent with every instantiation thatsatisfies this constraint (that means, the term such aninstantiation substitutes the metavariable with can always beunified with the returned term). |
| isAsStrongAs | | boolean isAsStrongAs(Constraint co)(Code) | | true iff this constraint is as strong as "co",i.e. every instantiation satisfying "this" also satisfies "co". |
| isAsWeakAs | | boolean isAsWeakAs(Constraint co)(Code) | | true iff this constraint is as weak as "co",i.e. every instantiation satisfying "co" also satisfies "this". |
| isBottom | | boolean isBottom()(Code) | | returns true if Bottom
true if Bottom |
| isSatisfiable | | 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 | | Constraint join(Constraint co, Services services)(Code) | | joins the given constraint with this constraint and returns
the joint new constraint. Every implementing class should
handle the cases co == TOP and ( co instanceof EqualityConstraint ).
Parameters:
co - Constraint to be joined with this one
Parameters:
services - the Services providing access to the type model the joined constraint |
| join | | 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. Every implementing class should handle the cases co
== TOP and ( co instanceof EqualityConstraint ).
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 | | 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) |
| toString | | String toString()(Code) | | String representation of the constraint |
| unify | | Constraint unify(Term t1, Term t2, Services services)(Code) | | tries to unify the 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 modelthe parameter may be null but then the unification fails (i.e. @link Constraint#TOP is returned) when accessingthe type model (e.g. for introducing intersection sorts) would be necessary). TOP if not possible, else a new constraint with afterunification of t1 and t2 |
| unify | | Constraint unify(Term t1, Term t2, Services services, BooleanContainer unchanged)(Code) | | tries to unify 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
Parameters:
unchanged - true iff the new constraint equals this one TOP if not possible, else a new constraint with afterunification of t1 and t2 |
|
|