public static class AbstractSMTTranslator.Configuration
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private boolean |
hasNumberLimit |
private boolean |
mentionLogic
Used for SMT2 format: if true the (set-logic AUFLIA) command is used otherwise
the logic is not set.
|
private boolean |
supportsOnlySimpleMultiplication
Some solvers (e.q Yices) support only multiplications where
one operand is a simple integer (even a constant symbol is
not allowed.).
|
Constructor and Description |
---|
Configuration(boolean supportsOnlySimpleMultiplication,
boolean mentionLogic) |
Configuration(boolean supportsOnlySimpleMultiplication,
boolean hasNumberLimit,
boolean mentionLogic) |
Modifier and Type | Method and Description |
---|---|
boolean |
hasNumberLimit() |
boolean |
mentionLogic() |
private final boolean supportsOnlySimpleMultiplication
private final boolean hasNumberLimit
private final boolean mentionLogic