public class FinishSymbolicExecutionMacro extends StrategyProofMacro
Strategy
which assigns to
any rule application infinite costs if there is no modality on the sequent.Modifier and Type | Class and Description |
---|---|
private static class |
FinishSymbolicExecutionMacro.FilterSymbexStrategy
The Class FilterAppManager is a special strategy assigning to any rule
infinite costs if the goal has no modality
|
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private static Name |
NON_HUMAN_INTERACTION_RULESET |
Constructor and Description |
---|
FinishSymbolicExecutionMacro() |
Modifier and Type | Method and Description |
---|---|
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
java.lang.String |
getScriptCommandName()
Gets a unique short name for this macro that can be used in proof
scripts.
|
(package private) static boolean |
hasModality(Node node)
find a modality term in a node
|
private static boolean |
hasModality(Term term) |
private static boolean |
isInRuleSet(Rule rule,
Name ruleSetName) |
(package private) static boolean |
isNonHumanInteractionTagged(Rule rule)
Checks if a rule is marked as not suited for interaction.
|
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter
private static final Name NON_HUMAN_INTERACTION_RULESET
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getScriptCommandName()
AbstractProofMacro
null
is returned, the macro cannot be addressed from
within scripts.
By default, proof macros do not support scripts, thus null
is returned.getScriptCommandName
in interface ProofMacro
getScriptCommandName
in class AbstractProofMacro
null
if not supported, or a non-null
constant string as the short namepublic java.lang.String getDescription()
ProofMacro
null
constant stringstatic boolean hasModality(Node node)
node
- TODOprivate static boolean hasModality(Term term)
static boolean isNonHumanInteractionTagged(Rule rule)
rule
- TODOprotected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro