de.uka.ilkd.key.smt

Class AbstractSMTTranslator.Configuration

java.lang.Object

de.uka.ilkd.key.smt.AbstractSMTTranslator.Configuration

Enclosing class:

AbstractSMTTranslator

public static class AbstractSMTTranslator.Configuration
extends java.lang.Object

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
Configuration(boolean supportsOnlySimpleMultiplication, boolean mentionLogic)
Configuration(boolean supportsOnlySimpleMultiplication, boolean hasNumberLimit, boolean mentionLogic)

Method Summary

Modifier and Type	Method and Description
boolean	hasNumberLimit()
boolean	mentionLogic()

Methods inherited from class java.lang.Object

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

Field Detail

supportsOnlySimpleMultiplication

private final boolean supportsOnlySimpleMultiplication

Some solvers (e.q Yices) support only multiplications where one operand is a simple integer (even a constant symbol is not allowed.). In this case the multiplication is translated into a uninterpreted function with some assumptions.

hasNumberLimit

private final boolean hasNumberLimit

mentionLogic

private final boolean mentionLogic

Used for SMT2 format: if true the (set-logic AUFLIA) command is used otherwise the logic is not set. For instance Z3 then uses automatically the appropriate logic.

Constructor Detail

Configuration

public Configuration(boolean supportsOnlySimpleMultiplication,
                     boolean mentionLogic)

Configuration

public Configuration(boolean supportsOnlySimpleMultiplication,
                     boolean hasNumberLimit,
                     boolean mentionLogic)

Method Detail

hasNumberLimit

public boolean hasNumberLimit()

mentionLogic

public boolean mentionLogic()