de.uka.ilkd.key.smt

Class RuleAppSMT.SMTRule

java.lang.Object

de.uka.ilkd.key.smt.RuleAppSMT.SMTRule

All Implemented Interfaces:

BuiltInRule, Rule

Enclosing class:

RuleAppSMT

public static class RuleAppSMT.SMTRule
extends java.lang.Object
implements BuiltInRule

Field Summary

Fields

Modifier and Type	Field and Description
static Name	name

Constructor Summary

Constructors

Constructor and Description
SMTRule()

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.
RuleAppSMT	createApp(PosInOccurrence pos)
RuleAppSMT	createApp(PosInOccurrence pos, TermServices services)
java.lang.String	displayName() returns the display name of the rule
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
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

name

public static final Name name

Constructor Detail

SMTRule

public SMTRule()

Method Detail

createApp

public RuleAppSMT createApp(PosInOccurrence pos)

createApp

public RuleAppSMT createApp(PosInOccurrence pos,
                            TermServices services)

Specified by:

createApp in interface BuiltInRule

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

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

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule

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

name

public Name name()

Description copied from interface: Rule

the name of the rule

Specified by:

name in interface Rule