let FormulaType have its own SMTLIB2 representation.
@@ -65,6 +65,9 @@ public abstract class FormulaType<T extends Formula> {
@Override
public abstract String toString();
+ /** return the correctly formatted SMTLIB2 type declaration. */
+ public abstract String toSMTLIBString();
+
@Immutable
public abstract static class NumeralType<T extends NumeralFormula> extends FormulaType<T> {
@@ -86,6 +89,11 @@ public abstract class FormulaType<T extends Formula> {
public String toString() {
return "Rational";
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "Real";
+ }
};
public static final FormulaType<IntegerFormula> IntegerType =
@@ -100,6 +108,11 @@ public abstract class FormulaType<T extends Formula> {
public String toString() {
return "Integer";
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "Int";
+ }
};
public static final FormulaType<BooleanFormula> BooleanType =
@@ -114,6 +127,11 @@ public abstract class FormulaType<T extends Formula> {
public String toString() {
return "Boolean";
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "Bool";
+ }
};
public static BitvectorType getBitvectorTypeWithSize(int size) {
@@ -158,6 +176,11 @@ public abstract class FormulaType<T extends Formula> {
public int hashCode() {
return size;
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "(_ BitVec " + size + ")";
+ }
}
public static FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize) {
@@ -225,6 +248,11 @@ public abstract class FormulaType<T extends Formula> {
public String toString() {
return "FloatingPoint<exp=" + exponentSize + ",mant=" + mantissaSize + ">";
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")";
+ }
}
public static final FormulaType<FloatingPointRoundingModeFormula> FloatingPointRoundingModeType =
@@ -242,6 +270,12 @@ public abstract class FormulaType<T extends Formula> {
public String toString() {
return "FloatingPointRoundingMode";
}
+
+ @Override
+ public String toSMTLIBString() {
+ throw new UnsupportedOperationException(
+ "rounding mode is not expected in symbol declarations");
+ }
}
@SuppressWarnings("MethodTypeParameterName")
@@ -303,6 +337,11 @@ public abstract class FormulaType<T extends Formula> {
return elementType.equals(other.elementType) && indexType.equals(other.indexType);
}
+
+ @Override
+ public String toSMTLIBString() {
+ return "(Array " + indexType.toSMTLIBString() + " " + elementType.toSMTLIBString() + ")";
+ }
}
/**
