public interface SMTSettings
Modifier and Type | Method and Description |
---|---|
boolean |
checkForSupport()
Returns true if and only if the version should be checked each time a solver is started.
|
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() |
long |
getObjectBound()
Returns the bit size used for modelling objects when looking for
bounded counter examples.
|
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.
|
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 |
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. |
long getTimeout()
java.lang.String getSMTTemporaryFolder()
int getMaxConcurrentProcesses()
boolean useExplicitTypeHierarchy()
true
If the transitive relations in the sort hierarchy
should be explicitly modeled by formulas.boolean instantiateNullAssumption()
true
If a concrete null
object should be used.boolean makesUseOfTaclets()
true
if taclets should be used as assumptions.int getMaxNumberOfGenerics()
java.util.Collection<Taclet> getTaclets()
boolean useBuiltInUniqueness()
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.boolean useUninterpretedMultiplicationIfNecessary()
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.boolean useAssumptionsForBigSmallIntegers()
true
if for too big respective too small integers (integers that
are not supported) a constant should be introduced.java.lang.String getLogic()
long getMaximumInteger()
long getMinimumInteger()
long getIntBound()
long getHeapBound()
long getSeqBound()
long getObjectBound()
long getLocSetBound()
boolean checkForSupport()
boolean invarianForall()