| java.lang.Object de.uka.ilkd.key.logic.Term de.uka.ilkd.key.logic.QuantifierTerm
QuantifierTerm | class QuantifierTerm extends Term (Code) | | |
QuantifierTerm | public QuantifierTerm(Operator op, QuantifiableVariable[] varsBoundHere, Term subTerm)(Code) | | creates a quantifier term
Parameters: op - Operator representing the Quantifier (all, exist) of this term Parameters: varsBoundHere - an array of Variable containing all variablesbound by the quantifier Parameters: sort - the Sort of this Term (is bool) |
QuantifierTerm | public QuantifierTerm(Operator op, ArrayOfQuantifiableVariable varsBoundHere, Term subTerm)(Code) | | creates a quantifier term
Parameters: op - Operator representing the Quantifier (all, exist) of this term Parameters: varsBoundHere - an array of Variable containing all variablesbound by the quantifier Parameters: sort - the Sort of this Term (is bool) |
arity | public int arity()(Code) | | arity of the quantifier term 1 as int |
depth | public int depth()(Code) | | depth of the term |
sub | public Term sub(int n)(Code) | | n-th subterm (always the only one) |
varsBoundHere | public ArrayOfQuantifiableVariable varsBoundHere(int n)(Code) | | the variables the term bound direct if it is a Quantifier(term) |
|
|