de.uka.ilkd.key.rule

Class QueryExpand

java.lang.Object

de.uka.ilkd.key.rule.QueryExpand

All Implemented Interfaces:

BuiltInRule, Rule

public class QueryExpand
extends java.lang.Object
implements BuiltInRule

The QueryExpand rule allows to apply contracts or to symbolically execute a query expression in the logic. It replaces the query expression by a new constant and constructs a box formula in the antecedent 'defining' the constant as the result of a method call. The method call is encoded directly as a method call in the box modality. The query is invoked in a context equal to the container type of the query method.

Author:

Richard Bubel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	QueryExpand.QueryEvalPos Query evaluation position.

Field Summary

Fields

Modifier and Type	Field and Description
private static int	DEFAULT_MAP_SIZE
static QueryExpand	INSTANCE
private static Name	QUERY_DEF_NAME
private java.util.WeakHashMap<Term,java.lang.Long>	timeOfTerm Stores a number that indicates the time when term occurred for the first time where this rule was applicable.

Constructor Summary

Constructors

Constructor and Description
QueryExpand()

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) the rule is applied on the given goal using the information of rule application.
private java.util.Vector<Term>	collectQueries(Term t)
private void	collectQueriesRecursively(Term t, java.util.Vector<Term> result) Utility method called by collectQueriesRecursively
DefaultBuiltInRuleApp	createApp(PosInOccurrence pos, TermServices services)
java.lang.String	displayName() returns the display name of the rule
Term	evaluateQueries(Services services, Term term, boolean positiveContext, boolean allowExpandBelowInstQuantifier) Apply "evaluate query" to the queries that occur in term.
private void	findQueriesAndEvaluationPositions(Term t, int level, java.util.Vector<java.lang.Integer> pathInTerm, ImmutableList<QuantifiableVariable> instVars, boolean curPosIsPositive, int qepLevel, boolean qepIsPositive, java.util.List<QueryExpand.QueryEvalPos> qeps) Find queries in t and suitable positions where to insert their evaluations in t.
private ImmutableArray<ProgramVariable>	getRegisteredArgumentVariables(ImmutableArray<ParameterDeclaration> paramDecls, TermServices services)
java.lang.Long	getTimeOfQuery(Term t)
boolean	isApplicable(Goal goal, PosInOccurrence pio) returns true iff a rule is applicable at the given position.
boolean	isApplicableOnSubTerms()
Name	name() the name of the rule
Pair<Term,Term>	queryEvalTerm(Services services, Term query, LogicVariable[] instVars) Creates an invocation of a query in a modal operator and stores the value in a new symbol.
private void	removeRedundant(java.util.List<QueryExpand.QueryEvalPos> qeps) Tries to remove redundant query evaluations/expansions.
protected Term	replace(Term term, Term with, java.util.Iterator<java.lang.Integer> it, TermServices services) Replaces in a term.
private void	storeTimeOfQuery(Term query, Goal goal)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final QueryExpand INSTANCE

DEFAULT_MAP_SIZE

private static final int DEFAULT_MAP_SIZE

See Also:

Constant Field Values

QUERY_DEF_NAME

private static Name QUERY_DEF_NAME

timeOfTerm

private java.util.WeakHashMap<Term,java.lang.Long> timeOfTerm

Stores a number that indicates the time when term occurred for the first time where this rule was applicable. The time is the number of rules applied on this branch.

Constructor Detail

QueryExpand

public QueryExpand()

Method Detail

apply

public ImmutableList<Goal> apply(Goal goal,
                                 Services services,
                                 RuleApp ruleApp)

Description copied from interface: Rule

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface Rule

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

queryEvalTerm

public Pair<Term,Term> queryEvalTerm(Services services,
                                     Term query,
                                     LogicVariable[] instVars)

Creates an invocation of a query in a modal operator and stores the value in a new symbol. This is a utility method, that may also be used by other classes.

Parameters:

services -

query - The query on which the query expand rule is applied

instVars - If null, then the result of the query can be stored in a constant (e.g. res=query(a)). Otherwise it is a list of logical variables that can be instantiated (using the rules allLeft, exRight) and therefore the result of the query must be stored by function that depends on instVars (e.g. forall i; res(i)=query(i)). The list may be empty even if it not null.

Returns:

The formula (!{U}result=res_query) & query()=res_query

getRegisteredArgumentVariables

private ImmutableArray<ProgramVariable> getRegisteredArgumentVariables(ImmutableArray<ParameterDeclaration> paramDecls,
                                                                       TermServices services)

evaluateQueries

public Term evaluateQueries(Services services,
                            Term term,
                            boolean positiveContext,
                            boolean allowExpandBelowInstQuantifier)

Apply "evaluate query" to the queries that occur in term. The query evaluations/expansions are inserted into a copy of term that is returned.

Parameters:

services -

term - A formula that potentially contains queries that should be evaluated/expanded.

positiveContext - Set false iff the term is in a logically negated context wrt. to the succedent.

allowExpandBelowInstQuantifier - TODO

Returns:

A modified version of the term with inserted "query evalutions".

findQueriesAndEvaluationPositions

private void findQueriesAndEvaluationPositions(Term t,
                                               int level,
                                               java.util.Vector<java.lang.Integer> pathInTerm,
                                               ImmutableList<QuantifiableVariable> instVars,
                                               boolean curPosIsPositive,
                                               int qepLevel,
                                               boolean qepIsPositive,
                                               java.util.List<QueryExpand.QueryEvalPos> qeps)

Find queries in t and suitable positions where to insert their evaluations in t. This method is called by the method evaluateQueries<\code>.

Parameters:

t - The term where to search for queries and query evaluation positions.

level - The current recursion level of this method call.

pathInTerm - Vector of integers describing the current path in the syntax tree (of the term at level 0).

instVars - If null, then query evaluation below instantiable quantifiers (i.e. non-Skolemizable quantifiers) is suppressed. If not null, then this list collects the logical variables of instantiable quantifers that the query evaluation depends on. This is to needed to create e.g. (forall i; query(i)=res(i)) instead of (forall i;query(i)=res); the latter is unsound.

curPosIsPositive - True iff the current position in the formula we are in is a logically positive context (when considering polarity wrt. logical negation).

qepLevel - The top-most level on the current path where the query evaluation could be inserted. Its either top-level (0) or below a quantifier.

qepIsPositive - True iff the logical context at position qepLevel is positive (i.e., not negated, or negations have cancelled out).

qeps - The resulting collection of query evaluation positions.

collectQueries

private java.util.Vector<Term> collectQueries(Term t)

collectQueriesRecursively

private void collectQueriesRecursively(Term t,
                                       java.util.Vector<Term> result)

Utility method called by collectQueriesRecursively

removeRedundant

private void removeRedundant(java.util.List<QueryExpand.QueryEvalPos> qeps)

Tries to remove redundant query evaluations/expansions.

replace

protected Term replace(Term term,
                       Term with,
                       java.util.Iterator<java.lang.Integer> it,
                       TermServices services)

Replaces in a term.

Parameters:

term -

with -

it - iterator with argument positions. This is the path in the syntax tree of term.

services - TODO

Returns:

Resulting term after replacement.

name

public Name name()

Description copied from interface: Rule

the name of the rule

Specified by:

name in interface Rule

displayName

public java.lang.String displayName()

Description copied from interface: Rule

returns the display name of the rule

Specified by:

displayName in interface Rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence pio)

Description copied from interface: BuiltInRule

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

Specified by:

isApplicable in interface BuiltInRule

storeTimeOfQuery

private void storeTimeOfQuery(Term query,
                              Goal goal)

getTimeOfQuery

public java.lang.Long getTimeOfQuery(Term t)

createApp

public DefaultBuiltInRuleApp createApp(PosInOccurrence pos,
                                       TermServices services)

Specified by:

createApp in interface BuiltInRule

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule