public class SMTCommand extends AbstractCommand<SMTCommand.SMTCommandArguments>
Modifier and Type | Class and Description |
---|---|
(package private) static class |
SMTCommand.SMTCommandArguments |
Modifier and Type | Field and Description |
---|---|
private static java.util.Map<java.lang.String,SolverType> |
SOLVER_MAP |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
SMTCommand() |
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.
|
execute, getArguments, getDocumentation
private static final java.util.Map<java.lang.String,SolverType> SOLVER_MAP
private static java.util.Map<java.lang.String,SolverType> computeSolverMap()
public SMTCommand.SMTCommandArguments evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
evaluateArguments
in interface ProofScriptCommand<SMTCommand.SMTCommandArguments>
evaluateArguments
in class AbstractCommand<SMTCommand.SMTCommandArguments>
java.lang.Exception
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
public void execute(SMTCommand.SMTCommandArguments args) throws ScriptException, java.lang.InterruptedException
execute
in class AbstractCommand<SMTCommand.SMTCommandArguments>
ScriptException
java.lang.InterruptedException
private SolverTypeCollection computeSolvers(java.lang.String value)