public class AutoMacro extends StrategyProofMacro
AutoMacro
is a customizable ProofMacro
for use in
proof scripts. It is possible to
FinishSymbolicExecutionMacro
. The parameters mentioned above have to
be prefixed with "arg_" in proof scripts. From proof scripts, it is also
possible (for all macros, and so also for this one) to start the macro on one
particular formula (via parameter "occ") and thus to realize focussed
applications.Modifier and Type | Class and Description |
---|---|
private static class |
AutoMacro.AutoMacroFilterStrategy
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 java.lang.String |
ALLOW_SPLITS_PARAM_NAME
argument name
|
private boolean |
allowSplits
True iff splits allowed.
|
private java.util.Optional<java.lang.String> |
breakpoint
The breakpoint parameter: String repr. of the statements
|
private static java.lang.String |
BREAKPOINT_PARAM_NAME
argument name
|
private static java.lang.String |
ONLY_HUMAN_PARAM_NAME
argument name
|
private boolean |
onlyHumanReadable
Set to true to suppress all rules tagged as "non-human readable"
|
private static java.lang.String[] |
PARAMS
All names of currently implemented parameters belong here.
|
private static java.lang.String |
SYMBEX_ONLY_PARAM_NAME
argument name
|
private boolean |
symbexOnly
Set to true to suppress all non-symbex rules
|
private java.util.List<java.lang.String> |
whitelist
Rules which never should be suppressed
|
private static java.lang.String |
WHITELIST_PARAM_NAME
argument name
|
Constructor and Description |
---|
AutoMacro() |
Modifier and Type | Method and Description |
---|---|
private boolean |
checkBoolean(java.lang.String paramName,
java.lang.String paramValue) |
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.
|
boolean |
hasParameter(java.lang.String paramName)
Checks whether this
ProofMacro has a parameter named
paramName . |
private static boolean |
isSplittingTaclet(Rule taclet) |
void |
resetParams()
Resets the macro parameters to their defaults.
|
void |
setParameter(java.lang.String paramName,
java.lang.String paramValue)
Sets the parameter named
paramName to the given String
representation in paramValue . |
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps
private static final java.lang.String BREAKPOINT_PARAM_NAME
private static final java.lang.String ALLOW_SPLITS_PARAM_NAME
private static final java.lang.String WHITELIST_PARAM_NAME
private static final java.lang.String SYMBEX_ONLY_PARAM_NAME
private static final java.lang.String ONLY_HUMAN_PARAM_NAME
private static final java.lang.String[] PARAMS
private java.util.Optional<java.lang.String> breakpoint
private boolean allowSplits
private java.util.List<java.lang.String> whitelist
private boolean symbexOnly
private boolean onlyHumanReadable
public java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getName()
ProofMacro
null
constant stringpublic 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 stringpublic void resetParams()
ProofMacro
resetParams
in interface ProofMacro
resetParams
in class AbstractProofMacro
public boolean hasParameter(java.lang.String paramName)
ProofMacro
ProofMacro
has a parameter named
paramName
. For use in proof scripts.hasParameter
in interface ProofMacro
hasParameter
in class AbstractProofMacro
paramName
- The name to check.ProofMacro
has a parameter named
paramName
.public void setParameter(java.lang.String paramName, java.lang.String paramValue) throws java.lang.IllegalArgumentException
ProofMacro
paramName
to the given String
representation in paramValue
. For use in proof scripts.setParameter
in interface ProofMacro
setParameter
in class AbstractProofMacro
paramName
- The name of the parameter.paramValue
- The value of the parameter.java.lang.IllegalArgumentException
- if there is no parameter of that name or the value is
incorrectly formatted (e.g., cannot be converted to a
number).private boolean checkBoolean(java.lang.String paramName, java.lang.String paramValue)
protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
private static boolean isSplittingTaclet(Rule taclet)