Add user propagator feature

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

@@ -189,4 +189,16 @@ 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.
+   *
+   * @param propagator The user propagator to register.
+   * @return true, if the user propagator was successfully registered. Most SMT solvers
+   * do not support user propagators and hence return "false".
+   */
+  default boolean registerUserPropagator(UserPropagator propagator) {
+    return false;
+  }
 }

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

@@ -0,0 +1,100 @@
+// 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} =>
+   *   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} =>
+   * {@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(BooleanFormula, BooleanFormula)}.
+   *
+   * <p>This function is typically called from {@link UserPropagator#initialize()} 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#initialize()} 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#initialize()} if the
+   * theory solver needs to perform final consistency checks.
+   */
+  void notifyOnFinalCheck();
+}

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

@@ -0,0 +1,114 @@
+// 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;
+
+/**
+ * Allows user-defined propagators (~ theory solvers) to be implemented.
+ * It is advised to inherit from {@link org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator}
+ * rather than implementing this interface directly.
+ *
+ * <p> A user propagator provides various callbacks that are invoked by the solver during the
+ * solving process. Within these callbacks, the user can react to and influence the solver
+ * by calling into the {@link PropagatorBackend}. For example, he can raise conflicts
+ * whenever the solver makes assignments inconsistent to the user-defined theory.
+ */
+public interface UserPropagator {
+
+  /**
+   * This callback is invoked whenever the solver creates a new decision level.
+   * A user propagator should maintain backtracking points on each push to enable later
+   * backtracking.
+   */
+  void onPush();
+
+  /**
+   * This callback is invoked when the solver backtracks. The solver can backtrack multiple
+   * levels simultaneously.
+   * @param numPoppedLevels The number of levels to backtrack (~ number of pushes to backtrack).
+   */
+  void onPop(int numPoppedLevels);
+
+  /**
+   * This callback is invoked when the solver finds a complete satisfying assignment.
+   * The user can check the found model for consistency and potentially raise conflicts via
+   * {@link PropagatorBackend#propagateConflict(BooleanFormula[])}.
+   * <p>
+   * Note: This callback is only invoked if the user propagator enabled it via
+   * {@link PropagatorBackend#notifyOnFinalCheck()}.
+   */
+  void onFinalCheck();
+
+  /**
+   * This callback is invoked if the solver gets to know the value of a registered expression
+   * ({@link #registerExpression}).
+   * Within the callback, the user can raise conflicts via
+   * {@link PropagatorBackend#propagateConflict}, propagate consequences via
+   * {@link PropagatorBackend#propagateConsequence}, or influence the solvers decision heuristics
+   * via {@link PropagatorBackend#propagateNextDecision}.
+   * <p>
+   * The reported value is only known on the current and later push levels,
+   * but will get invalidated when backtracking.
+   * <p>
+   * Note: This callback is only invoked if the user propagator enabled it via
+   * {@link PropagatorBackend#notifyOnKnownValue()}.
+   *
+   * @param expr  The expressions whose value is known.
+   * @param value The value of the expression.
+   */
+  void onKnownValue(BooleanFormula expr, boolean value);
+
+  /**
+   * This callback is invoked if the solver decides to branch on a registered expression.
+   * ({@link #registerExpression}).
+   * Within the callback, the user can change the decision by calling
+   * {@link PropagatorBackend#propagateNextDecision}.
+   * <p>
+   * Note: This callback is only invoked if the user propagator enabled it via
+   * {@link PropagatorBackend#notifyOnDecision()}.
+   * @param expr The expressions whose value gets decided (usually a literal).
+   * @param value The decision value.
+   */
+  void onDecision(BooleanFormula expr, boolean value);
+
+  /**
+   * Connects this user propagator with a {@link PropagatorBackend}. The backend is used
+   * to register expressions, raise conflicts, propagate consequences, etc.
+   * @param backend The propagator backend.
+   */
+  void injectBackend(PropagatorBackend backend);
+
+  /**
+   * This method is similar to a constructor but is guaranteed to get invoked only after
+   * {@link #injectBackend} was successfully called.
+   * The user can enable notifications by accessing the injected {@link PropagatorBackend}.
+   */
+  void initialize();
+
+  /**
+   * Registers an expression to be observed by the {@link UserPropagator}.
+   * Solver actions related to the expression are reported:
+   * <ul>
+   *   <li>
+   *     The callback {@link UserPropagator#onKnownValue} gets invoked if the value of a
+   *     registered expression becomes known (if notification was enabled via
+   *    {@link PropagatorBackend#notifyOnKnownValue}).
+   *   </li>
+   *   <li>
+   *     The callback {@link UserPropagator#onDecision} gets invoked right before the
+   *     solver decides on the value of a registered expression (if notification was enabled via
+   *     {@link PropagatorBackend#notifyOnDecision()}).
+   *   </li>
+   * </ul>
+   *
+   * @param theoryExpr The expression to observe.
+   */
+  void registerExpression(BooleanFormula theoryExpr);
+
+
+}

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

@@ -0,0 +1,59 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2016  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package org.sosy_lab.java_smt.basicimpl;
+
+import com.google.common.base.Preconditions;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.UserPropagator;
+import org.sosy_lab.java_smt.api.PropagatorBackend;
+
+public abstract class AbstractUserPropagator implements UserPropagator  {
+
+  protected @Nullable PropagatorBackend backend;
+
+  @Override
+  public void onFinalCheck() {
+
+  }
+
+  @Override
+  public void onKnownValue(BooleanFormula expr, boolean value) {
+
+  }
+
+  @Override
+  public void onDecision(BooleanFormula expr, boolean value) {
+
+  }
+
+  @Override
+  public final void injectBackend(PropagatorBackend backend) {
+    this.backend = Preconditions.checkNotNull(backend);
+  }
+
+  @Override
+  public void registerExpression(BooleanFormula theoryExpr) {
+    Preconditions.checkState(backend != null);
+    backend.registerExpression(theoryExpr);
+  }
+
+}