Add user propagator feature

build/gitlab-ci.yml

@@ -40,6 +40,7 @@ build-dependencies:
   artifacts:
     paths:
       - "lib/java/"
+    expire_in: 1 day # sufficient for building later stages and near-time debugging
 
 
 # Build binaries and provide them to later stages
@@ -51,6 +52,8 @@ build-dependencies:
     paths:
       - "bin/"
       - "*.jar"
+      - "hs_err_pid*.log"
+      - "core.*"
 
 build:jdk-11:
   <<: *build

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

@@ -189,4 +189,17 @@ interface AllSatCallback<R> {
     /** Returning the result generated after all the {@link #apply} calls went through. */
     R getResult() throws InterruptedException;
   }
+
+  /**
+   * Registers a {@link UserPropagator} for this prover environment. Only a single user propagator
+   * can be registered at a time, and each user propagator shall only be registered once in its
+   * lifetime (see also {@link UserPropagator#initializeWithBackend}).
+   *
+   * @param propagator The (fresh) user propagator to register.
+   * @return {@code true}, if the user propagator was successfully registered. Most SMT solvers do
+   *     not support user propagators and hence return {@code false}.
+   */
+  default boolean registerUserPropagator(UserPropagator propagator) {
+    return false;
+  }
 }

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/api/PropagatorBackend.java

@@ -0,0 +1,95 @@
+// 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 java.util.Optional;
+
+/**
+ * The PropagatorBackend class is used by {@link UserPropagator} to implement custom user
+ * propagators. It contains functions to interact with the SAT/SMT core during solving, for example,
+ * it provides the ability to propagate conflicts and to influence the decision-making.
+ */
+public interface PropagatorBackend {
+
+  /**
+   * Registers an expression to be observed by a {@link UserPropagator}. See {@link
+   * UserPropagator#onKnownValue} and {@link UserPropagator#onDecision} for more information.
+   *
+   * @param theoryExpr The expression to observe.
+   */
+  void registerExpression(BooleanFormula theoryExpr);
+
+  /**
+   * Raises a conflict caused by a set of conflicting assignments. Shall only be called from within
+   * a callback by {@link UserPropagator} such as {@link UserPropagator#onKnownValue} and {@link
+   * UserPropagator#onFinalCheck()}.
+   *
+   * <p>Effectively causes the solver to learn the implication "{@code conflictExpressions} =&gt;
+   * false"
+   *
+   * @param conflictExpressions A set of inconsistent assignments.
+   */
+  void propagateConflict(BooleanFormula[] conflictExpressions);
+
+  /**
+   * Propagates a consequence implied by a set of assigned expressions. Shall only be called from
+   * within a callback by {@link UserPropagator} such as {@link UserPropagator#onKnownValue} and
+   * {@link UserPropagator#onFinalCheck()}.
+   *
+   * <p>Effectively causes the solver to learn the implication "/\ {@code assignedExpressions} =&gt;
+   * {@code consequence}" It is possible to have an empty set of {@code assignedExpressions} to
+   * generate a theory lemma.
+   *
+   * @param assignedExpressions A set of assigned expressions.
+   * @param consequence The consequence implied by the assigned expressions.
+   */
+  void propagateConsequence(BooleanFormula[] assignedExpressions, BooleanFormula consequence);
+
+  /**
+   * Propagates a decision to be made by the solver. If called during {@link
+   * UserPropagator#onKnownValue}, will set the next decision to be made. If called during {@link
+   * UserPropagator#onDecision}, will overwrite the current decision to be made.
+   *
+   * @param expr The expression to assign to next.
+   * @param value The value to be assigned. If not given, the solver will decide.
+   * @return False, if the value of {@code expr} is already assigned. True, otherwise. Note that the
+   *     value of {@code expr} may already be decided before being reported via {@link
+   *     UserPropagator#onKnownValue}.
+   */
+  boolean propagateNextDecision(BooleanFormula expr, Optional<Boolean> value);
+
+  /**
+   * Enables tracking of expression values for the associated {@link UserPropagator} via {@link
+   * UserPropagator#onKnownValue}.
+   *
+   * <p>This function is typically called from {@link UserPropagator#initializeWithBackend} if the
+   * theory solver needs to listen to the value of expressions registered by {@link
+   * #registerExpression}.
+   */
+  void notifyOnKnownValue();
+
+  /**
+   * Enables tracking of decisions made for the associated {@link UserPropagator} via {@link
+   * UserPropagator#onDecision(BooleanFormula, boolean)}.
+   *
+   * <p>This function is typically called from {@link UserPropagator#initializeWithBackend} if the
+   * theory solver needs to listen to and/or modify the decisions made by the solver on expressions
+   * registered by {@link #registerExpression}.
+   */
+  void notifyOnDecision();
+
+  /**
+   * Enables the final callback {@link UserPropagator#onFinalCheck()} that is invoked when the
+   * solver finds a full satisfying assignment.
+   *
+   * <p>This function is typically called from {@link UserPropagator#initializeWithBackend} if the
+   * theory solver needs to perform final consistency checks.
+   */
+  void notifyOnFinalCheck();
+}