de.uka.ilkd.key.settings

Class SMTSettings

java.lang.Object

de.uka.ilkd.key.settings.SMTSettings

All Implemented Interfaces:

SMTSettings

public class SMTSettings
extends java.lang.Object
implements SMTSettings

Field Summary

Fields

Modifier and Type	Field and Description
private ProofDependentSMTSettings	pdSettings
private ProofIndependentSMTSettings	piSettings
private Proof	proof
private java.util.LinkedList<Taclet>	taclets

Constructor Summary

Constructors

Constructor and Description
SMTSettings(ProofDependentSMTSettings pdSettings, ProofIndependentSMTSettings piSettings, Proof proof)

Method Summary

Modifier and Type	Method and Description
void	addListener(SettingsListener listener)
boolean	checkForSupport() Returns true if and only if the version should be checked each time a solver is started.
void	copy(SMTSettings settings)
void	fireSettingsChanged()
long	getHeapBound() Returns the bit size used for modelling heaps when looking for bounded counter examples.
long	getIntBound() Returns the bit size used for modelling integers when looking for bounded counter examples.
long	getLocSetBound() Returns the bit size used for modelling location sets when looking for bounded counter examples.
java.lang.String	getLogic()
int	getMaxConcurrentProcesses() Returns the maximum number of processes that are allowed to run concurrently.
long	getMaximumInteger()
int	getMaxNumberOfGenerics()
long	getMinimumInteger()
int	getModeOfProgressDialog()
long	getObjectBound() Returns the bit size used for modelling objects when looking for bounded counter examples.
java.lang.String	getPathForSMTTranslation()
java.lang.String	getPathForTacletTranslation()
ProofDependentSMTSettings	getPdSettings()
ProofIndependentSMTSettings	getPiSettings()
Proof	getProof()
long	getSeqBound() Returns the bit size used for modelling sequences when looking for bounded counter examples.
java.lang.String	getSMTTemporaryFolder() The path of the folder, where the smt files are stored temporarily.
SupportedTaclets	getSupportedTaclets()
java.util.Collection<Taclet>	getTaclets() The set of taclets that should be used.
long	getTimeout() Returns the timeout that should be used for a single solver (in milliseconds).
boolean	instantiateNullAssumption() true If a concrete null object should be used.
boolean	invarianForall()
boolean	makesUseOfTaclets()
boolean	storeSMTTranslationToFile()
boolean	storeTacletTranslationToFile()
boolean	useAssumptionsForBigSmallIntegers() Returns true if for too big respective too small integers (integers that are not supported) a constant should be introduced.
boolean	useBuiltInUniqueness() Returns true if the uniqueness property should be translated by using the built-in mechanism of the solver.
boolean	useExplicitTypeHierarchy() true If the transitive relations in the sort hierarchy should be explicitly modeled by formulas.
boolean	useUninterpretedMultiplicationIfNecessary() Returns true if a uninterpreted function should be used if the normal normal multiplication is not supported.

Methods inherited from class java.lang.Object

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

Field Detail

pdSettings

private final ProofDependentSMTSettings pdSettings

piSettings

private final ProofIndependentSMTSettings piSettings

proof

private final Proof proof

taclets

private java.util.LinkedList<Taclet> taclets

Constructor Detail

SMTSettings

public SMTSettings(ProofDependentSMTSettings pdSettings,
                   ProofIndependentSMTSettings piSettings,
                   Proof proof)

Method Detail

copy

public void copy(SMTSettings settings)

getPdSettings

public ProofDependentSMTSettings getPdSettings()

getPiSettings

public ProofIndependentSMTSettings getPiSettings()

getProof

public Proof getProof()

getMaxConcurrentProcesses

public int getMaxConcurrentProcesses()

Description copied from interface: SMTSettings

Returns the maximum number of processes that are allowed to run concurrently.

Specified by:

getMaxConcurrentProcesses in interface SMTSettings

getMaxNumberOfGenerics

public int getMaxNumberOfGenerics()

Specified by:

getMaxNumberOfGenerics in interface SMTSettings

Returns:

the maximum number of different generic sorts that is allowed within the taclets that are used.

getSMTTemporaryFolder

public java.lang.String getSMTTemporaryFolder()

Description copied from interface: SMTSettings

The path of the folder, where the smt files are stored temporarily.

Specified by:

getSMTTemporaryFolder in interface SMTSettings

getTaclets

public java.util.Collection<Taclet> getTaclets()

Description copied from interface: SMTSettings

The set of taclets that should be used. Only supported taclets are used by the translation. In case that a taclet is not supported, it is ignored.

Specified by:

getTaclets in interface SMTSettings

getTimeout

public long getTimeout()

Description copied from interface: SMTSettings

Returns the timeout that should be used for a single solver (in milliseconds).

Specified by:

getTimeout in interface SMTSettings

instantiateNullAssumption

public boolean instantiateNullAssumption()

Description copied from interface: SMTSettings

true If a concrete null object should be used.

Specified by:

instantiateNullAssumption in interface SMTSettings

makesUseOfTaclets

public boolean makesUseOfTaclets()

Specified by:

makesUseOfTaclets in interface SMTSettings

Returns:

true if taclets should be used as assumptions.

useAssumptionsForBigSmallIntegers

public boolean useAssumptionsForBigSmallIntegers()

Description copied from interface: SMTSettings

Returns true if for too big respective too small integers (integers that are not supported) a constant should be introduced.

Specified by:

useAssumptionsForBigSmallIntegers in interface SMTSettings

useBuiltInUniqueness

public boolean useBuiltInUniqueness()

Description copied from interface: SMTSettings

Returns true if the uniqueness property should be translated by using the built-in mechanism of the solver. Has only some effect if the solver supports a built in feature for uniqueness.

Specified by:

useBuiltInUniqueness in interface SMTSettings

useExplicitTypeHierarchy

public boolean useExplicitTypeHierarchy()

Description copied from interface: SMTSettings

true If the transitive relations in the sort hierarchy should be explicitly modeled by formulas.

Specified by:

useExplicitTypeHierarchy in interface SMTSettings

useUninterpretedMultiplicationIfNecessary

public boolean useUninterpretedMultiplicationIfNecessary()

Description copied from interface: SMTSettings

Returns true if a uninterpreted function should be used if the normal normal multiplication is not supported. In case that such a function should not be used an exception is thrown when a not supported multiplication occurs.

Specified by:

useUninterpretedMultiplicationIfNecessary in interface SMTSettings

getSupportedTaclets

public SupportedTaclets getSupportedTaclets()

getModeOfProgressDialog

public int getModeOfProgressDialog()

storeSMTTranslationToFile

public boolean storeSMTTranslationToFile()

storeTacletTranslationToFile

public boolean storeTacletTranslationToFile()

getPathForTacletTranslation

public java.lang.String getPathForTacletTranslation()

getPathForSMTTranslation

public java.lang.String getPathForSMTTranslation()

fireSettingsChanged

public void fireSettingsChanged()

addListener

public void addListener(SettingsListener listener)

getMaximumInteger

public long getMaximumInteger()

Specified by:

getMaximumInteger in interface SMTSettings

getMinimumInteger

public long getMinimumInteger()

Specified by:

getMinimumInteger in interface SMTSettings

getLogic

public java.lang.String getLogic()

Specified by:

getLogic in interface SMTSettings

Returns:

Returns the logic used by solvers using SMT-Lib-Format

checkForSupport

public boolean checkForSupport()

Description copied from interface: SMTSettings

Returns true if and only if the version should be checked each time a solver is started.

Specified by:

checkForSupport in interface SMTSettings

getIntBound

public long getIntBound()

Description copied from interface: SMTSettings

Returns the bit size used for modelling integers when looking for bounded counter examples.

Specified by:

getIntBound in interface SMTSettings

Returns:

a positive integer indicating the bit-size

getHeapBound

public long getHeapBound()

Description copied from interface: SMTSettings

Returns the bit size used for modelling heaps when looking for bounded counter examples.

Specified by:

getHeapBound in interface SMTSettings

Returns:

a positive integer indicating the bit-size

getSeqBound

public long getSeqBound()

Description copied from interface: SMTSettings

Returns the bit size used for modelling sequences when looking for bounded counter examples.

Specified by:

getSeqBound in interface SMTSettings

Returns:

a positive integer indicating the bit-size

getObjectBound

public long getObjectBound()

Description copied from interface: SMTSettings

Returns the bit size used for modelling objects when looking for bounded counter examples.

Specified by:

getObjectBound in interface SMTSettings

Returns:

a positive integer indicating the bit-size

getLocSetBound

public long getLocSetBound()

Description copied from interface: SMTSettings

Returns the bit size used for modelling location sets when looking for bounded counter examples.

Specified by:

getLocSetBound in interface SMTSettings

Returns:

a positive integer indicating the bit-size

invarianForall

public boolean invarianForall()

Specified by:

invarianForall in interface SMTSettings