de.uka.ilkd.key.macros.scripts

Class SMTCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<SMTCommand.SMTCommandArguments>

de.uka.ilkd.key.macros.scripts.SMTCommand

All Implemented Interfaces:

ProofScriptCommand<SMTCommand.SMTCommandArguments>

public class SMTCommand
extends AbstractCommand<SMTCommand.SMTCommandArguments>

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	SMTCommand.SMTCommandArguments

Field Summary

Fields

Modifier and Type	Field and Description
private static java.util.Map<java.lang.String,SolverType>	SOLVER_MAP

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
SMTCommand()

Method Summary

Modifier and Type	Method and Description
private static java.util.Map<java.lang.String,SolverType>	computeSolverMap()
private SolverTypeCollection	computeSolvers(java.lang.String value)
SMTCommand.SMTCommandArguments	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(SMTCommand.SMTCommandArguments args)
java.lang.String	getName() Returns the name of this proof command.

Methods inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

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

Field Detail

SOLVER_MAP

private static final java.util.Map<java.lang.String,SolverType> SOLVER_MAP

Constructor Detail

SMTCommand

public SMTCommand()

Method Detail

computeSolverMap

private static java.util.Map<java.lang.String,SolverType> computeSolverMap()

evaluateArguments

public SMTCommand.SMTCommandArguments evaluateArguments(EngineState state,
                                                        java.util.Map<java.lang.String,java.lang.String> arguments)
                                                 throws java.lang.Exception

Specified by:

evaluateArguments in interface ProofScriptCommand<SMTCommand.SMTCommandArguments>

Overrides:

evaluateArguments in class AbstractCommand<SMTCommand.SMTCommandArguments>

Returns:

Throws:

java.lang.Exception

getName

public java.lang.String getName()

Description copied from interface: ProofScriptCommand

Returns the name of this proof command. The name should be constant and not be clash with the name of other commands. The name is essential for finding this command within an hashmap.

Returns:

a non-null, non-empty string

See Also:

ProofScriptEngine

execute

public void execute(SMTCommand.SMTCommandArguments args)
             throws ScriptException,
                    java.lang.InterruptedException

Overrides:

execute in class AbstractCommand<SMTCommand.SMTCommandArguments>

Throws:

ScriptException

java.lang.InterruptedException

computeSolvers

private SolverTypeCollection computeSolvers(java.lang.String value)