public class QueryExpand extends java.lang.Object implements BuiltInRule
Modifier and Type | Field and Description |
---|---|
static QueryExpand |
INSTANCE |
Constructor and Description |
---|
QueryExpand() |
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.
|
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 . |
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.
|
protected Term |
replace(Term term,
Term with,
java.util.Iterator<java.lang.Integer> it,
TermServices services)
Replaces in a term.
|
java.lang.String |
toString() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final QueryExpand INSTANCE
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedpublic Pair<Term,Term> queryEvalTerm(Services services, Term query, LogicVariable[] instVars)
services
- query
- The query on which the query expand rule is appliedinstVars
- 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.public Term evaluateQueries(Services services, Term term, boolean positiveContext, boolean allowExpandBelowInstQuantifier)
term
. The query evaluations/expansions are inserted
into a copy of term
that is returned.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
- TODOterm
with inserted "query evalutions".protected Term replace(Term term, Term with, java.util.Iterator<java.lang.Integer> it, TermServices services)
term
- with
- it
- iterator with argument positions. This is the path in the syntax tree of term.services
- TODOpublic java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public java.lang.Long getTimeOfQuery(Term t)
public DefaultBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
Copyright © 2003-2019 The KeY-Project.