352 add model evaluation on FloatingPointFormula

src/org/sosy_lab/java_smt/api/Evaluator.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -106,6 +106,13 @@ public interface Evaluator extends AutoCloseable {
    */
   @Nullable String evaluate(EnumerationFormula formula);
 
+  /**
+   * Type-safe evaluation for floating-point formulas.
+   *
+   * <p>The formula does not need to be a variable, we also allow complex expression.
+   */
+  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
+
   /**
    * Free resources associated with this evaluator (existing {@link Formula} instances stay valid,
    * but {@link #evaluate(Formula)} etc. must not be called again).

src/org/sosy_lab/java_smt/api/FloatingPointNumber.java

@@ -0,0 +1,130 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.api;
+
+import com.google.auto.value.AutoValue;
+import com.google.common.base.Preconditions;
+import com.google.errorprone.annotations.Immutable;
+import java.math.BigInteger;
+import java.util.BitSet;
+
+/**
+ * Represents a floating-point number with customizable precision, consisting of sign, exponent, and
+ * mantissa components.
+ */
+@Immutable
+@AutoValue
+public abstract class FloatingPointNumber {
+
+  public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8;
+  public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23;
+  public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
+  public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52;
+
+  /** Whether the number is positive (TRUE) or negative (FALSE). */
+  public abstract boolean getSign();
+
+  /** The exponent of the floating-point number, given as numeric value. */
+  public abstract BigInteger getExponent();
+
+  /** The mantissa (aka significand) of the floating-point number, given as numeric value. */
+  public abstract BigInteger getMantissa();
+
+  public abstract int getExponentSize();
+
+  public abstract int getMantissaSize();
+
+  public static FloatingPointNumber of(
+      boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) {
+    Preconditions.checkArgument(exponent.bitLength() <= exponentSize);
+    Preconditions.checkArgument(mantissa.bitLength() <= mantissaSize);
+    Preconditions.checkArgument(exponent.compareTo(BigInteger.ZERO) >= 0);
+    Preconditions.checkArgument(mantissa.compareTo(BigInteger.ZERO) >= 0);
+    return new AutoValue_FloatingPointNumber(sign, exponent, mantissa, exponentSize, mantissaSize);
+  }
+
+  public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) {
+    Preconditions.checkArgument(0 < exponentSize);
+    Preconditions.checkArgument(0 < mantissaSize);
+    Preconditions.checkArgument(bits.length() == 1 + exponentSize + mantissaSize);
+    Preconditions.checkArgument(bits.chars().allMatch(c -> c == '0' || c == '1'));
+    boolean sign = bits.charAt(0) == '1';
+    BigInteger exponent = new BigInteger(bits.substring(1, 1 + exponentSize), 2);
+    BigInteger mantissa =
+        new BigInteger(bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSize), 2);
+    return of(sign, exponent, mantissa, exponentSize, mantissaSize);
+  }
+
+  private boolean isSinglePrecision() {
+    return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
+        && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE;
+  }
+
+  private boolean isDoublePrecision() {
+    return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
+        && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
+  }
+
+  /** compute a representation as Java-based float value, if possible. */
+  public float floatValue() {
+    Preconditions.checkArgument(
+        isSinglePrecision(),
+        "Can not represent floating point number %s as Java-based float value.",
+        this);
+    var bits = getBits();
+    return Float.intBitsToFloat(bits.length() == 0 ? 0 : (int) bits.toLongArray()[0]);
+  }
+
+  /** compute a representation as Java-based double value, if possible. */
+  public double doubleValue() {
+    Preconditions.checkArgument(
+        isSinglePrecision() || isDoublePrecision(),
+        "Can not represent floating point number %s as Java-based double value.",
+        this);
+    if (isSinglePrecision()) {
+      // lets be nice to the user and automatically convert from single to double precision
+      return floatValue();
+    }
+    var bits = getBits();
+    return Double.longBitsToDouble(bits.length() == 0 ? 0 : getBits().toLongArray()[0]);
+  }
+
+  private BitSet getBits() {
+    var mantissaSize = getMantissaSize();
+    var exponentSize = getExponentSize();
+    var mantissa = getMantissa();
+    var exponent = getExponent();
+    var bits = new BitSet(1 + exponentSize + mantissaSize);
+    if (getSign()) {
+      bits.set(exponentSize + mantissaSize);
+    }
+    for (int i = 0; i < exponentSize; i++) {
+      bits.set(mantissaSize + i, exponent.testBit(i));
+    }
+    for (int i = 0; i < mantissaSize; i++) {
+      bits.set(i, mantissa.testBit(i));
+    }
+    return bits;
+  }
+
+  /**
+   * Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their
+   * bit-representations in this exact ordering.
+   */
+  @Override
+  public final String toString() {
+    var length = 1 + getExponentSize() + getMantissaSize();
+    var str = new StringBuilder(length);
+    var bits = getBits();
+    for (int i = 0; i < length; i++) {
+      str.append(bits.get(i) ? '1' : '0');
+    }
+    return str.reverse().toString();
+  }
+}

src/org/sosy_lab/java_smt/api/FormulaType.java

@@ -8,6 +8,11 @@
 
 package org.sosy_lab.java_smt.api;
 
+import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE;
+import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE;
+import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE;
+import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE;
+
 import com.google.common.base.Joiner;
 import com.google.common.base.Preconditions;
 import com.google.common.base.Splitter;
@@ -213,8 +218,10 @@ public static FloatingPointType getDoublePrecisionFloatingPointType() {
   @Immutable
   public static final class FloatingPointType extends FormulaType<FloatingPointFormula> {
 
-    private static final FloatingPointType SINGLE_PRECISION_FP_TYPE = new FloatingPointType(8, 23);
-    private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE = new FloatingPointType(11, 52);
+    private static final FloatingPointType SINGLE_PRECISION_FP_TYPE =
+        new FloatingPointType(SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE);
+    private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE =
+        new FloatingPointType(DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE);
 
     private final int exponentSize;
     private final int mantissaSize;

src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -17,6 +17,8 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
@@ -31,8 +33,8 @@ public abstract class AbstractEvaluator<TFormulaInfo, TType, TEnv> implements Ev
 
   protected AbstractEvaluator(
       AbstractProver<?> pProver, FormulaCreator<TFormulaInfo, TType, TEnv, ?> creator) {
-    this.prover = pProver;
-    this.creator = creator;
+    this.prover = Preconditions.checkNotNull(pProver);
+    this.creator = Preconditions.checkNotNull(creator);
   }
 
   @SuppressWarnings("unchecked")
@@ -84,6 +86,12 @@ public final String evaluate(EnumerationFormula f) {
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
+  @Override
+  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) {
+    Preconditions.checkState(!isClosed());
+    return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f));
+  }
+
   @Nullable
   @Override
   public final BigInteger evaluate(BitvectorFormula f) {
@@ -126,9 +134,7 @@ protected boolean isClosed() {
 
   @Override
   public void close() {
-    if (prover != null) { // can be NULL for testing
-      prover.unregisterEvaluator(this);
-    }
+    prover.unregisterEvaluator(this);
     closed = true;
   }
 }

src/org/sosy_lab/java_smt/basicimpl/CachingModel.java

@@ -16,6 +16,8 @@
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -85,6 +87,11 @@ public void close() {
     return delegate.evaluate(formula);
   }
 
+  @Override
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) {
+    return delegate.evaluate(formula);
+  }
+
   @Override
   public String toString() {
     return delegate.toString();

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java

@@ -17,6 +17,8 @@
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -81,6 +83,12 @@ class StatisticsModel implements Model {
     return delegate.evaluate(pF);
   }
 
+  @Override
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) {
+    stats.modelEvaluations.getAndIncrement();
+    return delegate.evaluate(pF);
+  }
+
   @Override
   public ImmutableList<ValueAssignment> asList() {
     stats.modelListings.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java

@@ -17,6 +17,8 @@
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -90,6 +92,13 @@ class SynchronizedModel implements Model {
     }
   }
 
+  @Override
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) {
+    synchronized (sync) {
+      return delegate.evaluate(pF);
+    }
+  }
+
   @Override
   public ImmutableList<ValueAssignment> asList() {
     synchronized (sync) {

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java

@@ -17,6 +17,8 @@
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.Model;
@@ -87,6 +89,11 @@ class SynchronizedModelWithContext implements Model {
     throw new UnsupportedOperationException(UNSUPPORTED_OPERATION);
   }
 
+  @Override
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) {
+    throw new UnsupportedOperationException(UNSUPPORTED_OPERATION);
+  }
+
   @Override
   public ImmutableList<ValueAssignment> asList() {
     throw new UnsupportedOperationException(UNSUPPORTED_OPERATION);