de.uka.ilkd.key.rule.conditions

Class MetaDisjointCondition

java.lang.Object

de.uka.ilkd.key.rule.VariableConditionAdapter

de.uka.ilkd.key.rule.conditions.MetaDisjointCondition

All Implemented Interfaces:

VariableCondition

public final class MetaDisjointCondition
extends VariableConditionAdapter

Field Summary

Fields

Modifier and Type	Field and Description
private TermSV	var1
private TermSV	var2

Constructor Summary

Constructors

Constructor and Description
MetaDisjointCondition(TermSV s1, TermSV s2)

Method Summary

Modifier and Type	Method and Description
boolean	check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, Services services) checks if the condition for a correct instantiation is fulfilled
private static boolean	clearlyDisjoint(Term t1, Term t2, Services services)
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.rule.VariableConditionAdapter

check

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

var1

private final TermSV var1

var2

private final TermSV var2

Constructor Detail

MetaDisjointCondition

public MetaDisjointCondition(TermSV s1,
                             TermSV s2)

Method Detail

clearlyDisjoint

private static boolean clearlyDisjoint(Term t1,
                                       Term t2,
                                       Services services)

check

public boolean check(SchemaVariable var,
                     SVSubstitute subst,
                     SVInstantiations svInst,
                     Services services)

Description copied from class: VariableConditionAdapter

checks if the condition for a correct instantiation is fulfilled

Specified by:

check in class VariableConditionAdapter

Parameters:

var - the template Variable to be instantiated

svInst - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed

services - the program information object

Returns:

true iff condition is fulfilled

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object