public static class RuleAppSMT.SMTRule extends java.lang.Object implements BuiltInRule
Constructor and Description |
---|
SMTRule() |
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() |
public static final Name name
public RuleAppSMT createApp(PosInOccurrence pos)
public RuleAppSMT createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
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 boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
public java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object