de.uka.ilkd.key.smt

Class RuleAppSMT

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.smt.RuleAppSMT

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class RuleAppSMT
extends AbstractBuiltInRuleApp

The rule application that is used when a goal is closed by means of an external solver. So far it stores the rule that that has been used and a title containing some information for the user.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	RuleAppSMT.SMTRule

Field Summary

Fields

Modifier and Type	Field and Description
static RuleAppSMT.SMTRule	rule
private java.lang.String	title

Fields inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

builtInRule, ifInsts, pio

Constructor Summary

Constructors

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)

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, setMutable, toString

Methods inherited from class java.lang.Object

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

Field Detail

rule

public static final RuleAppSMT.SMTRule rule

title

private final java.lang.String title

Constructor Detail

RuleAppSMT

RuleAppSMT(RuleAppSMT.SMTRule rule,
           PosInOccurrence pio)

RuleAppSMT

private RuleAppSMT(RuleAppSMT.SMTRule rule,
                   PosInOccurrence pio,
                   ImmutableList<PosInOccurrence> ifInsts,
                   java.lang.String title)

RuleAppSMT

private RuleAppSMT(RuleAppSMT.SMTRule rule,
                   java.lang.String title)

Method Detail

replacePos

public RuleAppSMT replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

complete

public boolean complete()

Description copied from class: AbstractBuiltInRuleApp

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Overrides:

complete in class AbstractBuiltInRuleApp

Returns:

true if all variables are instantiated

getTitle

public java.lang.String getTitle()

posInOccurrence

public PosInOccurrence posInOccurrence()

Description copied from class: AbstractBuiltInRuleApp

returns the PositionInOccurrence (representing a SequentFormula and a position in the corresponding formula) of this rule application

Specified by:

posInOccurrence in interface RuleApp

Overrides:

posInOccurrence in class AbstractBuiltInRuleApp

rule

public BuiltInRule rule()

Description copied from class: AbstractBuiltInRuleApp

returns the rule of this rule application

Specified by:

rule in interface IBuiltInRuleApp

Specified by:

rule in interface RuleApp

Overrides:

rule in class AbstractBuiltInRuleApp

setTitle

public RuleAppSMT setTitle(java.lang.String title)

setIfInsts

public RuleAppSMT setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

tryToInstantiate

public RuleAppSMT tryToInstantiate(Goal goal)

Description copied from interface: IBuiltInRuleApp

Tries to complete the rule application from the available information. Attention: Do neither add GUI code to the rules nor use this method directly Instead ask the implementation of the 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.

Specified by:

tryToInstantiate in interface IBuiltInRuleApp

Specified by:

tryToInstantiate in class AbstractBuiltInRuleApp