de.uka.ilkd.key.smt

Class AbstractSolverType

java.lang.Object

de.uka.ilkd.key.smt.AbstractSolverType

All Implemented Interfaces:

SolverType

abstract class AbstractSolverType
extends java.lang.Object
implements SolverType

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	installWasChecked
private boolean	isInstalled
private boolean	isSupportedVersion
private java.lang.String	solverCommand
private java.lang.String	solverParameters
private java.lang.String	solverVersion
private boolean	supportHasBeenChecked

Fields inherited from interface de.uka.ilkd.key.smt.SolverType

ALL_SOLVERS, CVC3_SOLVER, CVC4_SOLVER, SIMPLIFY_SOLVER, YICES_SOLVER, Z3_CE_SOLVER, Z3_SOLVER

Constructor Summary

Constructors

Constructor and Description
AbstractSolverType()

Method Summary

Modifier and Type	Method and Description
private static boolean	checkEnvVariable(java.lang.String cmd)
boolean	checkForSupport() Checks for support and returns the result.
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	getVersion() Returns the current version that is installed, if it has already been checked, otherwise null.
boolean	isInstalled(boolean recheck) check, if this solver is installed and can be used.
static boolean	isInstalled(java.lang.String cmd)
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.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.smt.SolverType

createSolver, createTranslator, getDefaultSolverCommand, getDefaultSolverParameters, getDelimiters, getInfo, getName, getSupportedVersions, getVersionParameter, supportsIfThenElse

Field Detail

installWasChecked

private boolean installWasChecked

isInstalled

private boolean isInstalled

solverParameters

private java.lang.String solverParameters

solverCommand

private java.lang.String solverCommand

solverVersion

private java.lang.String solverVersion

isSupportedVersion

private boolean isSupportedVersion

supportHasBeenChecked

private boolean supportHasBeenChecked

Constructor Detail

AbstractSolverType

AbstractSolverType()

Method Detail

isInstalled

public static boolean isInstalled(java.lang.String cmd)

isInstalled

public boolean isInstalled(boolean recheck)

check, if this solver is installed and can be used.

Specified by:

isInstalled in interface SolverType

Parameters:

recheck - if false, the solver is not checked again, if a cached value for this exists.

Returns:

true, if it is installed.

checkEnvVariable

private static boolean checkEnvVariable(java.lang.String cmd)

checkForSupport

public boolean checkForSupport()

Description copied from interface: SolverType

Checks for support and returns the result.

Specified by:

checkForSupport in interface SolverType

supportHasBeenChecked

public boolean supportHasBeenChecked()

Description copied from interface: SolverType

returns true if and only if the support has been checked for the currently installed solver.

Specified by:

supportHasBeenChecked in interface SolverType

isSupportedVersion

public boolean isSupportedVersion()

Description copied from interface: SolverType

Returns whether the currently installed version is supported.

Specified by:

isSupportedVersion in interface SolverType

getSolverParameters

public java.lang.String getSolverParameters()

Description copied from interface: SolverType

The currently used parameters for the solver.

Specified by:

getSolverParameters in interface SolverType

setSolverParameters

public void setSolverParameters(java.lang.String s)

Specified by:

setSolverParameters in interface SolverType

setSolverCommand

public void setSolverCommand(java.lang.String s)

Specified by:

setSolverCommand in interface SolverType

getSolverCommand

public final java.lang.String getSolverCommand()

Description copied from interface: SolverType

the command for starting the solver. For example "z3" if it is registered in the PATH variable, otherwise "ABSOLUTE_PATH/z3"

Specified by:

getSolverCommand in interface SolverType

getVersion

public java.lang.String getVersion()

Description copied from interface: SolverType

Returns the current version that is installed, if it has already been checked, otherwise null.

Specified by:

getVersion in interface SolverType

getRawVersion

public java.lang.String getRawVersion()

Description copied from interface: SolverType

Retrieve the version string without check for support. Returns null if the solver is not installed.

Specified by:

getRawVersion in interface SolverType

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

modifyProblem

public java.lang.String modifyProblem(java.lang.String problem)

Description copied from interface: SolverType

Directly before the problem description is sent to the solver one can modify the problem string by using this method.

Specified by:

modifyProblem in interface SolverType