public class SMTSettings extends java.lang.Object implements SMTSettings
Modifier and Type | Field and Description |
---|---|
private ProofDependentSMTSettings |
pdSettings |
private ProofIndependentSMTSettings |
piSettings |
private Proof |
proof |
private java.util.LinkedList<Taclet> |
taclets |
Constructor and Description |
---|
SMTSettings(ProofDependentSMTSettings pdSettings,
ProofIndependentSMTSettings piSettings,
Proof proof) |
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. |
private final ProofDependentSMTSettings pdSettings
private final ProofIndependentSMTSettings piSettings
private final Proof proof
private java.util.LinkedList<Taclet> taclets
public SMTSettings(ProofDependentSMTSettings pdSettings, ProofIndependentSMTSettings piSettings, Proof proof)
public void copy(SMTSettings settings)
public ProofDependentSMTSettings getPdSettings()
public ProofIndependentSMTSettings getPiSettings()
public Proof getProof()
public int getMaxConcurrentProcesses()
SMTSettings
getMaxConcurrentProcesses
in interface SMTSettings
public int getMaxNumberOfGenerics()
getMaxNumberOfGenerics
in interface SMTSettings
public java.lang.String getSMTTemporaryFolder()
SMTSettings
getSMTTemporaryFolder
in interface SMTSettings
public java.util.Collection<Taclet> getTaclets()
SMTSettings
getTaclets
in interface SMTSettings
public long getTimeout()
SMTSettings
getTimeout
in interface SMTSettings
public boolean instantiateNullAssumption()
SMTSettings
true
If a concrete null
object should be used.instantiateNullAssumption
in interface SMTSettings
public boolean makesUseOfTaclets()
makesUseOfTaclets
in interface SMTSettings
true
if taclets should be used as assumptions.public boolean useAssumptionsForBigSmallIntegers()
SMTSettings
true
if for too big respective too small integers (integers that
are not supported) a constant should be introduced.useAssumptionsForBigSmallIntegers
in interface SMTSettings
public boolean useBuiltInUniqueness()
SMTSettings
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.useBuiltInUniqueness
in interface SMTSettings
public boolean useExplicitTypeHierarchy()
SMTSettings
true
If the transitive relations in the sort hierarchy
should be explicitly modeled by formulas.useExplicitTypeHierarchy
in interface SMTSettings
public boolean useUninterpretedMultiplicationIfNecessary()
SMTSettings
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.useUninterpretedMultiplicationIfNecessary
in interface SMTSettings
public SupportedTaclets getSupportedTaclets()
public int getModeOfProgressDialog()
public boolean storeSMTTranslationToFile()
public boolean storeTacletTranslationToFile()
public java.lang.String getPathForTacletTranslation()
public java.lang.String getPathForSMTTranslation()
public void fireSettingsChanged()
public void addListener(SettingsListener listener)
public long getMaximumInteger()
getMaximumInteger
in interface SMTSettings
public long getMinimumInteger()
getMinimumInteger
in interface SMTSettings
public java.lang.String getLogic()
getLogic
in interface SMTSettings
public boolean checkForSupport()
SMTSettings
checkForSupport
in interface SMTSettings
public long getIntBound()
SMTSettings
getIntBound
in interface SMTSettings
public long getHeapBound()
SMTSettings
getHeapBound
in interface SMTSettings
public long getSeqBound()
SMTSettings
getSeqBound
in interface SMTSettings
public long getObjectBound()
SMTSettings
getObjectBound
in interface SMTSettings
public long getLocSetBound()
SMTSettings
getLocSetBound
in interface SMTSettings
public boolean invarianForall()
invarianForall
in interface SMTSettings