de.uka.ilkd.key.rule

Class QueryExpand.QueryEvalPos

java.lang.Object

de.uka.ilkd.key.rule.QueryExpand.QueryEvalPos

All Implemented Interfaces:

java.lang.Comparable<QueryExpand.QueryEvalPos>

Enclosing class:

QueryExpand

private class QueryExpand.QueryEvalPos
extends java.lang.Object
implements java.lang.Comparable<QueryExpand.QueryEvalPos>

Query evaluation position. Describes where to insert a query evaluation/expansion (see QueryExpand) in a formula.

Author:

gladisch

Field Summary

Fields

Modifier and Type	Field and Description
LogicVariable[]	instVars
java.util.Vector<java.lang.Integer>	pathInTerm Path in the syntax tree of the term where the query evaluation/expansion should be inserted.
boolean	positivePosition Positive or negative position wrt. logical negation.
Term	query The query that is subject to query evaluation/expansion.

Constructor Summary

Constructors

Constructor and Description
QueryEvalPos(Term query, java.util.Vector<java.lang.Integer> path, int level, ImmutableList<QuantifiableVariable> iVars, boolean isPositive)

Method Summary

Modifier and Type	Method and Description
int	compareTo(QueryExpand.QueryEvalPos other) For sorting.
Term	getTermOnPath(Term root)
boolean	subsumes(QueryExpand.QueryEvalPos other)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

query

public final Term query

The query that is subject to query evaluation/expansion. The query itself is not modified but a formula is added at a position described by the other fields.

positivePosition

public final boolean positivePosition

Positive or negative position wrt. logical negation.

pathInTerm

public final java.util.Vector<java.lang.Integer> pathInTerm

Path in the syntax tree of the term where the query evaluation/expansion should be inserted. The first element has no meaning and should be null. The path starts with the second element.

instVars

public final LogicVariable[] instVars

Constructor Detail

QueryEvalPos

public QueryEvalPos(Term query,
                    java.util.Vector<java.lang.Integer> path,
                    int level,
                    ImmutableList<QuantifiableVariable> iVars,
                    boolean isPositive)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getTermOnPath

public Term getTermOnPath(Term root)

subsumes

public boolean subsumes(QueryExpand.QueryEvalPos other)

compareTo

public int compareTo(QueryExpand.QueryEvalPos other)

For sorting. Longer paths come first in order to apply modifications to the target term in a depth-first order.

Specified by:

compareTo in interface java.lang.Comparable<QueryExpand.QueryEvalPos>