public class SaveInstCommand extends AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>
SchemaVariable
by the last
TacletApp
into an abbreviation for later use. A nice use case is a
manual loop invariant rule application, where the newly introduced
anonymizing Skolem constants can be saved for later interactive
instantiations. As for the LetCommand
, it is not allowed to call this
command multiple times with the same name argument (all names used for
remembering instantiations are "final").documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
SaveInstCommand() |
Modifier and Type | Method and Description |
---|---|
java.util.Map<java.lang.String,java.lang.String> |
evaluateArguments(EngineState state,
java.util.Map<java.lang.String,java.lang.String> arguments) |
void |
execute(AbstractUserInterfaceControl uiControl,
java.util.Map<java.lang.String,java.lang.String> args,
EngineState stateMap) |
java.lang.String |
getName()
Returns the name of this proof command.
|
execute, getArguments, getDocumentation
public java.util.Map<java.lang.String,java.lang.String> evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
evaluateArguments
in interface ProofScriptCommand<java.util.Map<java.lang.String,java.lang.String>>
evaluateArguments
in class AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>
public void execute(AbstractUserInterfaceControl uiControl, java.util.Map<java.lang.String,java.lang.String> args, EngineState stateMap) throws ScriptException, java.lang.InterruptedException
execute
in interface ProofScriptCommand<java.util.Map<java.lang.String,java.lang.String>>
execute
in class AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>
uiControl
- the current ui controllerargs
- the script argumentsstateMap
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happenspublic java.lang.String getName()
ProofScriptCommand
ProofScriptEngine