Skip to content

Revert: API change: convert the abstract class "FormulaType" to interface. #615 #617

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kfriedberger merged 2 commits into from
Apr 2, 2026
Merged

Revert: API change: convert the abstract class "FormulaType" to interface. #615 #617

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d4c53fb
Revert "simplify FloatingPointRoundingModeType."
kfriedberger Mar 17, 2026
98b4355
Revert "convert the abstract class "FormulaType" to interface."
kfriedberger Mar 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
120 changes: 59 additions & 61 deletions src/org/sosy_lab/java_smt/api/FormulaType.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

Expand All @@ -25,77 +25,72 @@
import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;

/**
* Subclasses of this interface represent the different types of formulas supported by SMT solvers,
* typically including boolean, integer, bitvector, and more. Each type corresponds to a specific
* class of formulas that can be created and manipulated using the SMT solver's API.
*
* <p>Subclasses of this interface must be immutable, as they are used as keys in maps and sets, and
* their immutability ensures that they can be safely shared and used without unintended side
* effects.
* Type of a formula.
*
* @param <T> Formula class corresponding to the given formula type.
*/
@SuppressWarnings("checkstyle:constantname")
@Immutable
public interface FormulaType<T extends Formula> {
public abstract class FormulaType<T extends Formula> {

private FormulaType() {}

default boolean isArrayType() {
public boolean isArrayType() {
return false;
}

default boolean isBitvectorType() {
public boolean isBitvectorType() {
return false;
}

default boolean isBooleanType() {
public boolean isBooleanType() {
return false;
}

default boolean isFloatingPointType() {
public boolean isFloatingPointType() {
return false;
}

default boolean isFloatingPointRoundingModeType() {
public boolean isFloatingPointRoundingModeType() {
return false;
}

default boolean isNumeralType() {
public boolean isNumeralType() {
return false;
}

default boolean isRationalType() {
public boolean isRationalType() {
return false;
}

default boolean isIntegerType() {
public boolean isIntegerType() {
return false;
}

default boolean isSLType() {
public boolean isSLType() {
return false;
}

default boolean isStringType() {
public boolean isStringType() {
return false;
}

default boolean isRegexType() {
public boolean isRegexType() {
return false;
}

default boolean isEnumerationType() {
public boolean isEnumerationType() {
return false;
}

/** returns a human-readable representation of the formula type. */
@Override
String toString();
public abstract String toString();

/** returns a correctly formatted string that can be used in SMTLIB2 declarations. */
String toSMTLIBString();
/** return the correctly formatted SMTLIB2 type declaration. */
public abstract String toSMTLIBString();

@Immutable
abstract class NumeralType<T extends NumeralFormula> implements FormulaType<T> {
public abstract static class NumeralType<T extends NumeralFormula> extends FormulaType<T> {

@Override
public final boolean isNumeralType() {
Expand All @@ -104,7 +99,7 @@ public final boolean isNumeralType() {
}

@SuppressWarnings("ClassInitializationDeadlock")
FormulaType<RationalFormula> RationalType =
public static final FormulaType<RationalFormula> RationalType =
new NumeralType<>() {

@Override
Expand All @@ -124,7 +119,7 @@ public String toSMTLIBString() {
};

@SuppressWarnings("ClassInitializationDeadlock")
FormulaType<IntegerFormula> IntegerType =
public static final FormulaType<IntegerFormula> IntegerType =
new NumeralType<>() {

@Override
Expand All @@ -143,7 +138,7 @@ public String toSMTLIBString() {
}
};

FormulaType<BooleanFormula> BooleanType =
public static final FormulaType<BooleanFormula> BooleanType =
new FormulaType<>() {

@Override
Expand All @@ -162,12 +157,12 @@ public String toSMTLIBString() {
}
};

static BitvectorType getBitvectorTypeWithSize(int size) {
public static BitvectorType getBitvectorTypeWithSize(int size) {
return new BitvectorType(size);
}

@Immutable
final class BitvectorType implements FormulaType<BitvectorFormula> {
public static final class BitvectorType extends FormulaType<BitvectorFormula> {
private final int size;

private BitvectorType(int size) {
Expand Down Expand Up @@ -229,7 +224,7 @@ public String toSMTLIBString() {
*/
@Deprecated(since = "6.0", forRemoval = true)
@SuppressWarnings("InlineMeSuggester")
static FloatingPointType getFloatingPointType(
public static FloatingPointType getFloatingPointType(
int exponentSize, int mantissaSizeWithoutHiddenBit) {
return getFloatingPointTypeFromSizesWithoutHiddenBit(
exponentSize, mantissaSizeWithoutHiddenBit);
Expand All @@ -252,7 +247,7 @@ static FloatingPointType getFloatingPointType(
* significand), excluding the hidden bit.
* @return the newly constructed {@link FloatingPointType}.
*/
static FloatingPointType getFloatingPointTypeFromSizesWithoutHiddenBit(
public static FloatingPointType getFloatingPointTypeFromSizesWithoutHiddenBit(
int exponentSize, int mantissaSizeWithoutHiddenBit) {
checkArgument(exponentSize > 1, "Exponent size must be greater than 1");
checkArgument(
Expand All @@ -278,7 +273,7 @@ static FloatingPointType getFloatingPointTypeFromSizesWithoutHiddenBit(
* significand), including the hidden bit.
* @return the newly constructed {@link FloatingPointType}.
*/
static FloatingPointType getFloatingPointTypeFromSizesWithHiddenBit(
public static FloatingPointType getFloatingPointTypeFromSizesWithHiddenBit(
int exponentSize, int mantissaSizeWithHiddenBit) {
checkArgument(
mantissaSizeWithHiddenBit > 1,
Expand All @@ -292,7 +287,7 @@ static FloatingPointType getFloatingPointTypeFromSizesWithHiddenBit(
* of the sign bit, an exponent sized 8 bits, and a mantissa sized 23 bits (excluding the
* hidden bit).
*/
static FloatingPointType getSinglePrecisionFloatingPointType() {
public static FloatingPointType getSinglePrecisionFloatingPointType() {
return FloatingPointType.SINGLE_PRECISION_FP_TYPE;
}

Expand All @@ -301,12 +296,12 @@ static FloatingPointType getSinglePrecisionFloatingPointType() {
* of the sign bit, an exponent sized 11 bits, and a mantissa sized 52 bits (excluding the
* hidden bit).
*/
static FloatingPointType getDoublePrecisionFloatingPointType() {
public static FloatingPointType getDoublePrecisionFloatingPointType() {
return FloatingPointType.DOUBLE_PRECISION_FP_TYPE;
}

@Immutable
final class FloatingPointType implements FormulaType<FloatingPointFormula> {
public static final class FloatingPointType extends FormulaType<FloatingPointFormula> {

@SuppressWarnings("removal")
private static final FloatingPointType SINGLE_PRECISION_FP_TYPE =
Expand Down Expand Up @@ -412,35 +407,38 @@ public String toSMTLIBString() {
}
}

FormulaType<FloatingPointRoundingModeFormula> FloatingPointRoundingModeType =
new FormulaType<>() {
public static final FormulaType<FloatingPointRoundingModeFormula> FloatingPointRoundingModeType =
new FloatingPointRoundingModeType();

@Override
public boolean isFloatingPointRoundingModeType() {
return true;
}
private static final class FloatingPointRoundingModeType
extends FormulaType<FloatingPointRoundingModeFormula> {

@Override
public String toString() {
return "FloatingPointRoundingMode";
}
@Override
public boolean isFloatingPointRoundingModeType() {
return true;
}

@Override
public String toSMTLIBString() {
throw new UnsupportedOperationException(
"rounding mode is not expected in symbol declarations");
}
};
@Override
public String toString() {
return "FloatingPointRoundingMode";
}

@Override
public String toSMTLIBString() {
throw new UnsupportedOperationException(
"rounding mode is not expected in symbol declarations");
}
}

@SuppressWarnings("MethodTypeParameterName")
static <TD extends Formula, TR extends Formula> ArrayFormulaType<TD, TR> getArrayType(
public static <TD extends Formula, TR extends Formula> ArrayFormulaType<TD, TR> getArrayType(
FormulaType<TD> pDomainSort, FormulaType<TR> pRangeSort) {
return new ArrayFormulaType<>(pDomainSort, pRangeSort);
}

@SuppressWarnings("ClassTypeParameterName")
final class ArrayFormulaType<TI extends Formula, TE extends Formula>
implements FormulaType<ArrayFormula<TI, TE>> {
public static final class ArrayFormulaType<TI extends Formula, TE extends Formula>
extends FormulaType<ArrayFormula<TI, TE>> {

private final FormulaType<TE> elementType;
private final FormulaType<TI> indexType;
Expand Down Expand Up @@ -491,11 +489,11 @@ public String toSMTLIBString() {
}
}

static EnumerationFormulaType getEnumerationType(String pName, Set<String> pElements) {
public static EnumerationFormulaType getEnumerationType(String pName, Set<String> pElements) {
return new EnumerationFormulaType(pName, pElements);
}

final class EnumerationFormulaType implements FormulaType<EnumerationFormula> {
public static final class EnumerationFormulaType extends FormulaType<EnumerationFormula> {

private final String name;
private final ImmutableSet<String> elements;
Expand Down Expand Up @@ -550,7 +548,7 @@ public String toSMTLIBString() {
}
}

FormulaType<StringFormula> StringType =
public static final FormulaType<StringFormula> StringType =
new FormulaType<>() {

@Override
Expand All @@ -569,7 +567,7 @@ public String toSMTLIBString() {
}
};

FormulaType<RegexFormula> RegexType =
public static final FormulaType<RegexFormula> RegexType =
new FormulaType<>() {

@Override
Expand All @@ -592,7 +590,7 @@ public String toSMTLIBString() {
* Parse a string and return the corresponding type. This method is the counterpart of {@link
* #toString()}.
*/
static FormulaType<?> fromString(String t) {
public static FormulaType<?> fromString(String t) {
if (BooleanType.toString().equals(t)) {
return BooleanType;
} else if (IntegerType.toString().equals(t)) {
Expand Down
Loading