public interface SolverType
Modifier and Type | Field and Description |
---|---|
static java.util.List<SolverType> |
ALL_SOLVERS |
static SolverType |
CVC3_SOLVER
Class for the CVC3 solver.
|
static SolverType |
CVC4_SOLVER
CVC4 is the successor to CVC3.
|
static SolverType |
SIMPLIFY_SOLVER
Class for the Simplify solver.
|
static SolverType |
YICES_SOLVER
Class for the Yices solver.
|
static SolverType |
Z3_CE_SOLVER
Class for the Z3 solver.
|
static SolverType |
Z3_SOLVER
Class for the Z3 solver.
|
Modifier and Type | Method and Description |
---|---|
boolean |
checkForSupport()
Checks for support and returns the result.
|
SMTSolver |
createSolver(SMTProblem problem,
SolverListener listener,
Services services)
Creates an instance of SMTSolver representing a concrete instance of that solver.
|
SMTTranslator |
createTranslator(Services services)
The translator to be used.
|
java.lang.String |
getDefaultSolverCommand() |
java.lang.String |
getDefaultSolverParameters()
The default parameters which should be used for starting a solver
|
java.lang.String[] |
getDelimiters()
The delimiters of the messages that are sent from the solver to KeY.
|
java.lang.String |
getInfo()
Some specific information about the solver which can be presented.
|
java.lang.String |
getName()
Returns the name of the solver.
|
java.lang.String |
getRawVersion()
Retrieve the version string without check for support.
|
java.lang.String |
getSolverCommand()
the command for starting the solver.
|
java.lang.String |
getSolverParameters()
The currently used parameters for the solver.
|
java.lang.String[] |
getSupportedVersions()
Returns an array of all versions that are supported by KeY.
|
java.lang.String |
getVersion()
Returns the current version that is installed, if it has already been checked, otherwise null.
|
java.lang.String |
getVersionParameter()
Returns the parameter that can be used to gain the version of the solver when
executing it.
|
boolean |
isInstalled(boolean recheck)
Checks whether the solver is installed.
|
boolean |
isSupportedVersion()
Returns whether the currently installed version is supported.
|
java.lang.String |
modifyProblem(java.lang.String problem)
Directly before the problem description is sent to the solver one can modify the problem string by using
this method.
|
void |
setSolverCommand(java.lang.String s) |
void |
setSolverParameters(java.lang.String s) |
boolean |
supportHasBeenChecked()
returns true if and only if the support has been checked for the currently installed solver.
|
boolean |
supportsIfThenElse()
Returns true if and only if the solver supports if-then-else terms.
|
static final SolverType Z3_SOLVER
static final SolverType Z3_CE_SOLVER
static final SolverType CVC3_SOLVER
static final SolverType CVC4_SOLVER
static final SolverType YICES_SOLVER
static final SolverType SIMPLIFY_SOLVER
static final java.util.List<SolverType> ALL_SOLVERS
SMTSolver createSolver(SMTProblem problem, SolverListener listener, Services services)
java.lang.String getName()
boolean isInstalled(boolean recheck)
recheck
is set to true
the method should check for the path variable of the system and for the absolute path,
otherwise it can return the result of the previous call.java.lang.String getInfo()
null
means no information.java.lang.String getSolverParameters()
void setSolverParameters(java.lang.String s)
java.lang.String getDefaultSolverParameters()
java.lang.String getSolverCommand()
void setSolverCommand(java.lang.String s)
java.lang.String getDefaultSolverCommand()
SMTTranslator createTranslator(Services services)
java.lang.String[] getDelimiters()
boolean supportsIfThenElse()
java.lang.String modifyProblem(java.lang.String problem)
java.lang.String getVersionParameter()
java.lang.String[] getSupportedVersions()
java.lang.String getVersion()
java.lang.String getRawVersion()
boolean isSupportedVersion()
boolean checkForSupport()
boolean supportHasBeenChecked()