Package org.sosy_lab.java_smt.api
Class FormulaType<T extends Formula>
- java.lang.Object
-
- org.sosy_lab.java_smt.api.FormulaType<T>
-
- Type Parameters:
T
- Formula class corresponding to the given formula type.
- Direct Known Subclasses:
FormulaType.ArrayFormulaType
,FormulaType.BitvectorType
,FormulaType.EnumerationFormulaType
,FormulaType.FloatingPointType
,FormulaType.NumeralType
@Immutable public abstract class FormulaType<T extends Formula> extends Object
Type of a formula.
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static class
FormulaType.ArrayFormulaType<TI extends Formula,TE extends Formula>
static class
FormulaType.BitvectorType
static class
FormulaType.EnumerationFormulaType
static class
FormulaType.FloatingPointType
static class
FormulaType.NumeralType<T extends NumeralFormula>
-
Field Summary
Fields Modifier and Type Field Description static FormulaType<BooleanFormula>
BooleanType
static FormulaType<FloatingPointRoundingModeFormula>
FloatingPointRoundingModeType
static FormulaType<NumeralFormula.IntegerFormula>
IntegerType
static FormulaType<NumeralFormula.RationalFormula>
RationalType
static FormulaType<RegexFormula>
RegexType
static FormulaType<StringFormula>
StringType
-
Method Summary
-
-
-
Field Detail
-
RationalType
public static final FormulaType<NumeralFormula.RationalFormula> RationalType
-
IntegerType
public static final FormulaType<NumeralFormula.IntegerFormula> IntegerType
-
BooleanType
public static final FormulaType<BooleanFormula> BooleanType
-
FloatingPointRoundingModeType
public static final FormulaType<FloatingPointRoundingModeFormula> FloatingPointRoundingModeType
-
StringType
public static final FormulaType<StringFormula> StringType
-
RegexType
public static final FormulaType<RegexFormula> RegexType
-
-
Method Detail
-
isArrayType
public boolean isArrayType()
-
isBitvectorType
public boolean isBitvectorType()
-
isBooleanType
public boolean isBooleanType()
-
isFloatingPointType
public boolean isFloatingPointType()
-
isFloatingPointRoundingModeType
public boolean isFloatingPointRoundingModeType()
-
isNumeralType
public boolean isNumeralType()
-
isRationalType
public boolean isRationalType()
-
isIntegerType
public boolean isIntegerType()
-
isSLType
public boolean isSLType()
-
isStringType
public boolean isStringType()
-
isRegexType
public boolean isRegexType()
-
isEnumerationType
public boolean isEnumerationType()
-
toSMTLIBString
public abstract String toSMTLIBString()
return the correctly formatted SMTLIB2 type declaration.
-
getBitvectorTypeWithSize
public static FormulaType.BitvectorType getBitvectorTypeWithSize(int size)
-
getFloatingPointType
public static FormulaType.FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize)
-
getSinglePrecisionFloatingPointType
public static FormulaType.FloatingPointType getSinglePrecisionFloatingPointType()
-
getDoublePrecisionFloatingPointType
public static FormulaType.FloatingPointType getDoublePrecisionFloatingPointType()
-
getArrayType
public static <TD extends Formula,TR extends Formula> FormulaType.ArrayFormulaType<TD,TR> getArrayType(FormulaType<TD> pDomainSort, FormulaType<TR> pRangeSort)
-
getEnumerationType
public static FormulaType.EnumerationFormulaType getEnumerationType(String pName, Set<String> pElements)
-
fromString
public static FormulaType<?> fromString(String t)
Parse a string and return the corresponding type. This method is the counterpart oftoString()
.
-
-