| java.lang.Object
 de.uka.ilkd.key.logic.IntersectionConstraint
| IntersectionConstraint | | public class IntersectionConstraint implements Constraint(Code) | | Class representing the intersection of a set of constraints
(i.e. of arbitrary objects implementing the
"Constraint"-interface). Intersection means the constraint allowing
an instantiation of metavariables iff there exists a constraint
within the set allowing this instantiation.
|
| Method Summary | |
| public boolean | equals(Object obj)
| | public Term | getInstantiation(Metavariable p_mv)
| | public int | hashCode()
| | public static Constraint | intersect(Constraint p_c0, Constraint p_c1, ConstraintContainer p_diff)
Intersects p_c0 with p_c1, returning a constraint weaker or as
strong as both p_c0 and p_c1. | | public static Constraint | intersect(Constraint p_c0, Constraint p_c1)
| | protected Constraint | intersectHelp(Constraint p_co, ConstraintContainer p_diff)
Intersects this constraint with p_co. | | protected IntersectionConstraint | intersectHelp2(Constraint p_co, BooleanContainer p_stronger)
Removes all elements from "this.subConstraints" that are
stronger than "p_co". | | protected Constraint | intersectSimplify()
| | 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. | | protected boolean | isAsWeakAsInteger(Constraint co)
| | public boolean | isBottom()
| | 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 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 String | toString()
| | public Constraint | unify(Term t1, Term t2, Services services)
executes unification for terms t1 and t2
Parameters:
t1 - Term to be unified
Parameters:
t2 - term to be unified
Parameters:
services - a Namespace where new sorts that may be created when unifying are added. | | public Constraint | unify(Term t1, Term t2, Services services, BooleanContainer unchanged)
executes unification for terms t1 and t2. |
| IntersectionConstraint | | protected IntersectionConstraint()(Code) | | Use the static attributes of "Constraint" for new constraints
|
| equals | | public boolean equals(Object obj)(Code) | | checks equality of constraints by subsuming relation
|
| getInstantiation | | public Term getInstantiation(Metavariable p_mv)(Code) | | Currently not needed, should return something more specific
|
| hashCode | | public int hashCode()(Code) | | |
| intersect | | public static Constraint intersect(Constraint p_c0, Constraint p_c1, ConstraintContainer p_diff)(Code) | | Intersects p_c0 with p_c1, returning a constraint weaker or as
strong as both p_c0 and p_c1.
Parameters:
p_diff - a constraint which is as strong (-> simple) as possiblesatisfyingintersect ( p_c0, p_diff.val () ) == intersect ( p_c0, p_c1 ) |
| intersectHelp | | protected Constraint intersectHelp(Constraint p_co, ConstraintContainer p_diff)(Code) | | Intersects this constraint with p_co.
Parameters:
p_diff - a constraint which is as strong as possiblesatisfying this.intersectHelp ( p_diff.val () ) == this.intersectHelp ( p_co ) A constraint representing the intersection of this andp_co |
| intersectHelp2 | | protected IntersectionConstraint intersectHelp2(Constraint p_co, BooleanContainer p_stronger)(Code) | | Removes all elements from "this.subConstraints" that are
stronger than "p_co". Iff "p_co" is stronger than any element
of "this.subConstraints", "p_stronger" is set to true (and
"this" is returned). The return value may in fact be a not
well-formed object of this class ("subConstraints" may be empty
or contain only one element), that can be made correct by
calling "intersectSimplify".
|
| intersectSimplify | | protected Constraint intersectSimplify()(Code) | | Make an "IntersectionConstraint" well-formed
|
| 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". |
| isAsWeakAsInteger | | protected boolean isAsWeakAsInteger(Constraint co)(Code) | | Same as "isAsWeakAs" for "co" not an IntersectionConstraint
|
| isBottom | | public boolean isBottom()(Code) | | returns true if Bottom
true if Bottom |
| isSatisfiable | | 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. Every implementing class should
handle the cases co == TOP and ( co instanceof EqualityConstraint ).
Parameters:
co - Constraint to be joined with this one sort_ns a Namespace where new sorts that may be created when unifying are added. If the value is null unifying and therewith joining will fail if new sorts are required the joined constraint |
| join | | public 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 - a Namespace where new sorts that may be created when unifying are added. If the value is null unifying will fail if new sorts are required for a succesfull unification
Parameters:
unchanged - the BooleanContainers value set true, if thisconstraint is stronger than co (false may stand for "don'tknow") 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) |
| toString | | public String toString()(Code) | | String representation of the constraint |
| unify | | public Constraint unify(Term t1, Term t2, Services services)(Code) | | executes unification for terms t1 and t2
Parameters:
t1 - Term to be unified
Parameters:
t2 - term to be unified
Parameters:
services - a Namespace where new sorts that may be created when unifying are added. If the value is null unifying will fail if new sorts are required for a succesfull unification 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 - a Namespace where new sorts that may be created when unifying are added. If the value is null unifying will fail if new sorts are required for a succesfull unification
Parameters:
unchanged - true iff the new constraint is subsumed bythis one TOP if not possible, else a new constraint with afterunification of t1 and t2 |
|
|