de.uka.ilkd.key.rule.metaconstruct

Class ExpandQueriesMetaConstruct

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.AbstractTermTransformer

de.uka.ilkd.key.rule.metaconstruct.ExpandQueriesMetaConstruct

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, TermTransformer, Sorted

public class ExpandQueriesMetaConstruct
extends AbstractTermTransformer

Uses the class QueryExpand in order to insert query expansions in the term that the meta construct is applied on.

Author:

gladisch

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	name

Fields inherited from class de.uka.ilkd.key.logic.op.AbstractTermTransformer

ADD_CAST, ARRAY_BASE_INSTANCE_OF, CONSTANT_VALUE, DIVIDE_LCR_MONOMIALS, DIVIDE_MONOMIALS, ENUM_CONSTANT_VALUE, EXPAND_QUERIES, INTRODUCE_ATPRE_DEFINITIONS, MEMBER_PV_TO_FIELD, META_ADD, META_AND, META_DIV, META_EQ, META_GEQ, META_GREATER, META_LEQ, META_LESS, META_MUL, META_OR, META_POW, META_SHIFTLEFT, META_SHIFTRIGHT, META_SUB, META_XOR, METASORT

Constructor Summary

Constructors

Constructor and Description
ExpandQueriesMetaConstruct()

Method Summary

Modifier and Type	Method and Description
Term	transform(Term term, SVInstantiations svInst, Services services) term.sub(0) is the term that possibly contains queries.

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractTermTransformer

convertToDecimalString, name2metaop

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Field Detail

name

public static final java.lang.String name

See Also:

Constant Field Values

Constructor Detail

ExpandQueriesMetaConstruct

public ExpandQueriesMetaConstruct()

Method Detail

transform

public Term transform(Term term,
                      SVInstantiations svInst,
                      Services services)

term.sub(0) is the term that possibly contains queries. term.sub(1) is expected to be true or false. True indicates that the meta construct appears in a positive context wrt. to logical negation, (e.g. in the succedent or negated in the antecedent) False implies means that the meta construct appears in a negative context. (e.g. in the antecedent or negated in the succedent)