| |
|
| java.lang.Object de.uka.ilkd.key.proof.init.ModStrategy
ModStrategy | public class ModStrategy (Code) | | Describes if the parts of an initial configuration are to be modified
or not when reading input to the prover.
|
MOD_ALL | final public static ModStrategy MOD_ALL(Code) | | A constant strategy modifying always
|
NO_FUNCS | final public static ModStrategy NO_FUNCS(Code) | | A strategy modifying everything except functions
|
NO_GENSORTS | final public static ModStrategy NO_GENSORTS(Code) | | A strategy modifying everything except generic sorts
|
NO_VARS | final public static ModStrategy NO_VARS(Code) | | A strategy modifying everything except variables
|
NO_VARS_FUNCS | final public static ModStrategy NO_VARS_FUNCS(Code) | | A strategy modifying everything except variables and functions
|
NO_VARS_FUNCS_GENSORTS | final public static ModStrategy NO_VARS_FUNCS_GENSORTS(Code) | | A strategy modifying everything except variables, functions and generic sorts
|
NO_VARS_GENSORTS | final public static ModStrategy NO_VARS_GENSORTS(Code) | | A strategy modifying everything except variables and generic sorts
|
modifyChoices | public boolean modifyChoices()(Code) | | returns true iff the choice namespace should be modified
|
modifyFunctions | public boolean modifyFunctions()(Code) | | returns true iff the functions namespace should be modified
|
modifyGenericSorts | public boolean modifyGenericSorts()(Code) | | returns true iff the sorts namespace should be modified concerning
generic sorts
|
modifyHeuristics | public boolean modifyHeuristics()(Code) | | returns true iff the heuristics namespace should be modified
|
modifyJavaInfo | public boolean modifyJavaInfo()(Code) | | returns true iff the java model info should be modified
|
modifyProgramVariables | public boolean modifyProgramVariables()(Code) | | returns true iff the variable namespace should be modified
|
modifySorts | public boolean modifySorts()(Code) | | returns true iff the sorts namespace should be modified concerning
concrete sorts
|
modifyVariables | public boolean modifyVariables()(Code) | | returns true iff the variable namespace should be modified
|
|
|
|