public class RuleAppSMT extends AbstractBuiltInRuleApp
Modifier and Type | Class and Description |
---|---|
static class |
RuleAppSMT.SMTRule |
Modifier and Type | Field and Description |
---|---|
static RuleAppSMT.SMTRule |
rule |
private java.lang.String |
title |
builtInRule, ifInsts, pio
Modifier | Constructor and Description |
---|---|
(package private) |
RuleAppSMT(RuleAppSMT.SMTRule rule,
PosInOccurrence pio) |
private |
RuleAppSMT(RuleAppSMT.SMTRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
java.lang.String title) |
private |
RuleAppSMT(RuleAppSMT.SMTRule rule,
java.lang.String title) |
Modifier and Type | Method and Description |
---|---|
boolean |
complete()
returns true if all variables are instantiated
|
java.lang.String |
getTitle() |
PosInOccurrence |
posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula) of this rule application
|
RuleAppSMT |
replacePos(PosInOccurrence newPos) |
BuiltInRule |
rule()
returns the rule of this rule application
|
RuleAppSMT |
setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
RuleAppSMT |
setTitle(java.lang.String title) |
RuleAppSMT |
tryToInstantiate(Goal goal)
Tries to complete the rule application from the available information.
|
execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, setMutable, toString
public static final RuleAppSMT.SMTRule rule
private final java.lang.String title
RuleAppSMT(RuleAppSMT.SMTRule rule, PosInOccurrence pio)
private RuleAppSMT(RuleAppSMT.SMTRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, java.lang.String title)
private RuleAppSMT(RuleAppSMT.SMTRule rule, java.lang.String title)
public RuleAppSMT replacePos(PosInOccurrence newPos)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractBuiltInRuleApp
public java.lang.String getTitle()
public PosInOccurrence posInOccurrence()
AbstractBuiltInRuleApp
posInOccurrence
in interface RuleApp
posInOccurrence
in class AbstractBuiltInRuleApp
public BuiltInRule rule()
AbstractBuiltInRuleApp
rule
in interface IBuiltInRuleApp
rule
in interface RuleApp
rule
in class AbstractBuiltInRuleApp
public RuleAppSMT setTitle(java.lang.String title)
public RuleAppSMT setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp
public RuleAppSMT tryToInstantiate(Goal goal)
IBuiltInRuleApp
UserInterfaceControl
to complete a built-in rule.
Returns a complete app only if there is exactly one contract.
If you want a complete app for combined contracts, use forceInstantiate
instead.
For an example implementation see e.g. UseOperationContractRule
or UseDependencyContractRule
.tryToInstantiate
in interface IBuiltInRuleApp
tryToInstantiate
in class AbstractBuiltInRuleApp