de.uka.ilkd.key.strategy.quantifierHeuristics

Class Constraint.Top

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.Constraint.Top

All Implemented Interfaces:

Constraint

Enclosing interface:

Constraint

Deprecated.

@Deprecated
public static class Constraint.Top
extends java.lang.Object
implements Constraint

Constraint class for representating the TOP (unsatisfiable) constraint.

Nested Class Summary

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

Constraint.Top

Field Summary

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

BOTTOM, TOP

Constructor Summary

Constructors

Constructor and Description
Top() Deprecated. creation of TOP

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object obj) Deprecated. checks equality of constraints
Term	getInstantiation(Metavariable p_mv, Services services) Deprecated. as this constraint is unsatisfiable it just returns the metavariable given as argument
int	hashCode() Deprecated.
boolean	isAsStrongAs(Constraint co) Deprecated.
boolean	isAsWeakAs(Constraint co) Deprecated.
boolean	isBottom() Deprecated. returns true if Bottom
boolean	isSatisfiable() Deprecated. is an unsatisfiable Constraint satisfiable?
Constraint	join(Constraint co, TermServices services) Deprecated. joint of Top and co is Top
Constraint	join(Constraint co, TermServices services, BooleanContainer c) Deprecated. joint of Top and co is Top and Top subsumes every constraint
java.lang.String	toString() Deprecated.
Constraint	unify(Term t1, Term t2, TermServices services) Deprecated. adding new constraints to an unsatisfiable constraint results in an unsatisfiable constraint so this one is returned
Constraint	unify(Term t1, Term t2, TermServices services, BooleanContainer unchanged) Deprecated. tries to unify terms t1 and t2.

Methods inherited from class java.lang.Object

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

Constructor Detail

Top

public Top()

Deprecated.

creation of TOP

Method Detail

isSatisfiable

public boolean isSatisfiable()

Deprecated.

is an unsatisfiable Constraint satisfiable? NO.

Specified by:

isSatisfiable in interface Constraint

Returns:

always false

getInstantiation

public Term getInstantiation(Metavariable p_mv,
                             Services services)

Deprecated.

as this constraint is unsatisfiable it just returns the metavariable given as argument

Specified by:

getInstantiation in interface Constraint

Parameters:

p_mv - the Metavariable

services - the Services

Returns:

the instantiation of the metavariable

unify

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

Deprecated.

adding new constraints to an unsatisfiable constraint results in an unsatisfiable constraint so this one is returned

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 the parameter may be null but then the unification fails (i.e. @link Constraint#TOP is returned) when accessing the type model (e.g. for introducing intersection sorts) would be necessary).

Returns:

always this

unify

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

Deprecated.

Description copied from interface: Constraint

tries to unify 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

unchanged - true iff the new constraint equals this one

Returns:

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

equals

public boolean equals(java.lang.Object obj)

Deprecated.

Description copied from interface: Constraint

checks equality of constraints

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.

joint of Top and co is Top

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:

this

join

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

Deprecated.

joint of Top and co is Top and Top subsumes every 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

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

Returns:

this

isBottom

public boolean isBottom()

Deprecated.

returns true if Bottom

Specified by:

isBottom in interface Constraint

Returns:

true if Bottom

toString

public java.lang.String toString()

Deprecated.

Specified by:

toString in interface Constraint

Overrides:

toString in class java.lang.Object

Returns:

String representing the TOP constraint

hashCode

public int hashCode()

Deprecated.

Specified by:

hashCode in interface Constraint

Overrides:

hashCode in class java.lang.Object