new concept for computation handlers

src/main/java/com/booleworks/logicng/backbones/BackboneGeneration.java

@@ -7,7 +7,8 @@
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Variable;
-import com.booleworks.logicng.handlers.SATHandler;
+import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.NopHandler;
 import com.booleworks.logicng.solvers.SATSolver;
 import com.booleworks.logicng.solvers.functions.BackboneFunction;
 import com.booleworks.logicng.solvers.sat.SATSolverConfig;
@@ -41,14 +42,13 @@ private BackboneGeneration() {
      * @param variables the given collection of relevant variables for the
      *                  backbone computation
      * @param type      the type of backbone variables that should be computed
-     * @param handler   an optional handler for the backbone computation's SAT
-     *                  solver
+     * @param handler   a handler
      * @return the backbone or {@code null} if the computation was aborted by
      *         the handler
      */
     public static Backbone compute(final FormulaFactory f, final Collection<Formula> formulas,
                                    final Collection<Variable> variables, final BackboneType type,
-                                   final SATHandler handler) {
+                                   final ComputationHandler handler) {
         if (formulas == null || formulas.isEmpty()) {
             throw new IllegalArgumentException("Provide at least one formula for backbone computation");
         }
@@ -70,7 +70,7 @@ public static Backbone compute(final FormulaFactory f, final Collection<Formula>
      */
     public static Backbone compute(final FormulaFactory f, final Collection<Formula> formulas,
                                    final Collection<Variable> variables, final BackboneType type) {
-        return compute(f, formulas, variables, type, null);
+        return compute(f, formulas, variables, type, NopHandler.get());
     }
 
     /**

src/main/java/com/booleworks/logicng/explanations/mus/DeletionBasedMUS.java

@@ -4,10 +4,12 @@
 
 package com.booleworks.logicng.explanations.mus;
 
+import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.MUS_COMPUTATION_STARTED;
+import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT;
+
 import com.booleworks.logicng.datastructures.Tristate;
 import com.booleworks.logicng.explanations.UNSATCore;
 import com.booleworks.logicng.formulas.FormulaFactory;
-import com.booleworks.logicng.handlers.Handler;
 import com.booleworks.logicng.propositions.Proposition;
 import com.booleworks.logicng.solvers.SATSolver;
 import com.booleworks.logicng.solvers.SolverState;
@@ -25,7 +27,7 @@ public final class DeletionBasedMUS extends MUSAlgorithm {
     @Override
     public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
                                                            final MUSConfig config) {
-        Handler.start(config.handler);
+        config.handler.shouldResume(MUS_COMPUTATION_STARTED);
         final List<T> mus = new ArrayList<>(propositions.size());
         final List<SolverState> solverStates = new ArrayList<>(propositions.size());
         final SATSolver solver = SATSolver.newSolver(f);
@@ -34,7 +36,7 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
             solver.add(proposition);
         }
         boolean sat = solver.satCall().handler(config.handler).sat() == Tristate.TRUE;
-        if (Handler.aborted(config.handler)) {
+        if (!config.handler.shouldResume(NO_EVENT)) {
             return null;
         }
         if (sat) {
@@ -46,7 +48,7 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
                 solver.add(prop);
             }
             sat = solver.satCall().handler(config.handler).sat() == Tristate.TRUE;
-            if (Handler.aborted(config.handler)) {
+            if (!config.handler.shouldResume(NO_EVENT)) {
                 return null;
             }
             if (sat) {

src/main/java/com/booleworks/logicng/explanations/mus/MUSConfig.java

@@ -6,7 +6,8 @@
 
 import com.booleworks.logicng.configurations.Configuration;
 import com.booleworks.logicng.configurations.ConfigurationType;
-import com.booleworks.logicng.handlers.SATHandler;
+import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.NopHandler;
 
 /**
  * The configuration object for the MUS generation.
@@ -24,7 +25,7 @@ public enum Algorithm {
     }
 
     final Algorithm algorithm;
-    final SATHandler handler;
+    final ComputationHandler handler;
 
     /**
      * Constructs a new configuration with a given type.
@@ -58,7 +59,7 @@ public String toString() {
     public static class Builder {
 
         private Algorithm algorithm = Algorithm.DELETION;
-        private SATHandler handler = null;
+        private ComputationHandler handler = NopHandler.get();
 
         private Builder() {
             // Initialize only via factory
@@ -80,7 +81,7 @@ public Builder algorithm(final Algorithm algorithm) {
          * @param handler the SAT handler
          * @return the current builder
          */
-        public Builder handler(final SATHandler handler) {
+        public Builder handler(final ComputationHandler handler) {
             this.handler = handler;
             return this;
         }

src/main/java/com/booleworks/logicng/explanations/mus/PlainInsertionBasedMUS.java

@@ -4,11 +4,13 @@
 
 package com.booleworks.logicng.explanations.mus;
 
+import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.MUS_COMPUTATION_STARTED;
+import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT;
+
 import com.booleworks.logicng.datastructures.Tristate;
 import com.booleworks.logicng.explanations.UNSATCore;
 import com.booleworks.logicng.formulas.FormulaFactory;
-import com.booleworks.logicng.handlers.Handler;
-import com.booleworks.logicng.handlers.SATHandler;
+import com.booleworks.logicng.handlers.ComputationHandler;
 import com.booleworks.logicng.propositions.Proposition;
 import com.booleworks.logicng.solvers.SATSolver;
 
@@ -25,7 +27,7 @@ public class PlainInsertionBasedMUS extends MUSAlgorithm {
     @Override
     public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
                                                            final MUSConfig config) {
-        Handler.start(config.handler);
+        config.handler.shouldResume(MUS_COMPUTATION_STARTED);
         final List<T> currentFormula = new ArrayList<>(propositions.size());
         currentFormula.addAll(propositions);
         final List<T> mus = new ArrayList<>(propositions.size());
@@ -46,7 +48,7 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
                 transitionProposition = removeProposition;
                 solver.add(removeProposition);
             }
-            if (Handler.aborted(config.handler)) {
+            if (!config.handler.shouldResume(NO_EVENT)) {
                 return null;
             }
             currentFormula.clear();
@@ -59,8 +61,8 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
         return new UNSATCore<>(mus, true);
     }
 
-    private static boolean shouldProceed(final SATSolver solver, final SATHandler handler) {
+    private static boolean shouldProceed(final SATSolver solver, final ComputationHandler handler) {
         final boolean sat = solver.satCall().handler(handler).sat() == Tristate.TRUE;
-        return sat && !Handler.aborted(handler);
+        return sat && handler.shouldResume(NO_EVENT);
     }
 }

src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java

@@ -4,13 +4,16 @@
 
 package com.booleworks.logicng.explanations.smus;
 
+import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT;
+
 import com.booleworks.logicng.datastructures.Assignment;
 import com.booleworks.logicng.datastructures.Tristate;
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Variable;
-import com.booleworks.logicng.handlers.Handler;
-import com.booleworks.logicng.handlers.OptimizationHandler;
+import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.NopHandler;
+import com.booleworks.logicng.handlers.events.ComputationStartedEvent;
 import com.booleworks.logicng.propositions.Proposition;
 import com.booleworks.logicng.propositions.StandardProposition;
 import com.booleworks.logicng.solvers.SATSolver;
@@ -58,14 +61,14 @@ private SmusComputation() {
      */
     public static <P extends Proposition> List<P> computeSmus(final FormulaFactory f, final List<P> propositions,
                                                               final List<Formula> additionalConstraints) {
-        return computeSmus(f, propositions, additionalConstraints, null);
+        return computeSmus(f, propositions, additionalConstraints, NopHandler.get());
     }
 
     /**
      * Computes the SMUS for the given list of propositions modulo some
      * additional constraint.
      * <p>
-     * The SMUS computation can be called with an {@link OptimizationHandler}.
+     * The SMUS computation can be called with an {@link ComputationHandler}.
      * The given handler instance will be used for every subsequent *
      * {@link OptimizationFunction} call and the handler's SAT handler is used
      * for every subsequent SAT call.
@@ -79,8 +82,8 @@ public static <P extends Proposition> List<P> computeSmus(final FormulaFactory f
      */
     public static <P extends Proposition> List<P> computeSmus(final FormulaFactory f, final List<P> propositions,
                                                               final List<Formula> additionalConstraints,
-                                                              final OptimizationHandler handler) {
-        Handler.start(handler);
+                                                              final ComputationHandler handler) {
+        handler.shouldResume(ComputationStartedEvent.SMUS_COMPUTATION_STARTED);
         final SATSolver growSolver = SATSolver.newSolver(f);
         growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : additionalConstraints);
         final Map<Variable, P> propositionMapping = new TreeMap<>();
@@ -89,19 +92,18 @@ public static <P extends Proposition> List<P> computeSmus(final FormulaFactory f
             propositionMapping.put(selector, proposition);
             growSolver.add(f.equivalence(selector, proposition.formula()));
         }
-        final boolean sat = growSolver.satCall().handler(OptimizationHandler.satHandler(handler))
-                .addFormulas(propositionMapping.keySet()).sat() == Tristate.TRUE;
-        if (sat || Handler.aborted(handler)) {
+        final boolean sat = growSolver.satCall().handler(handler).addFormulas(propositionMapping.keySet()).sat() == Tristate.TRUE;
+        if (sat || !handler.shouldResume(NO_EVENT)) {
             return null;
         }
         final SATSolver hSolver = SATSolver.newSolver(f);
         while (true) {
             final SortedSet<Variable> h = minimumHs(hSolver, propositionMapping.keySet(), handler);
-            if (h == null || Handler.aborted(handler)) {
+            if (h == null || !handler.shouldResume(NO_EVENT)) {
                 return null;
             }
             final SortedSet<Variable> c = grow(growSolver, h, propositionMapping.keySet(), handler);
-            if (Handler.aborted(handler)) {
+            if (!handler.shouldResume(NO_EVENT)) {
                 return null;
             }
             if (c == null) {
@@ -122,7 +124,7 @@ public static <P extends Proposition> List<P> computeSmus(final FormulaFactory f
      */
     public static List<Formula> computeSmusForFormulas(final FormulaFactory f, final List<Formula> formulas,
                                                        final List<Formula> additionalConstraints) {
-        return computeSmusForFormulas(f, formulas, additionalConstraints, null);
+        return computeSmusForFormulas(f, formulas, additionalConstraints, NopHandler.get());
     }
 
     /**
@@ -137,30 +139,30 @@ public static List<Formula> computeSmusForFormulas(final FormulaFactory f, final
      */
     public static List<Formula> computeSmusForFormulas(final FormulaFactory f, final List<Formula> formulas,
                                                        final List<Formula> additionalConstraints,
-                                                       final OptimizationHandler handler) {
+                                                       final ComputationHandler handler) {
         final List<Proposition> props = formulas.stream().map(StandardProposition::new).collect(Collectors.toList());
         final List<Proposition> smus = computeSmus(f, props, additionalConstraints, handler);
         return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList());
     }
 
     private static SortedSet<Variable> minimumHs(final SATSolver hSolver, final Set<Variable> variables,
-                                                 final OptimizationHandler handler) {
+                                                 final ComputationHandler handler) {
         final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder()
                 .handler(handler)
                 .literals(variables)
                 .minimize().build());
-        return Handler.aborted(handler) ? null : new TreeSet<>(minimumHsModel.positiveVariables());
+        return !handler.shouldResume(NO_EVENT) ? null : new TreeSet<>(minimumHsModel.positiveVariables());
     }
 
     private static SortedSet<Variable> grow(final SATSolver growSolver, final SortedSet<Variable> h,
-                                            final Set<Variable> variables, final OptimizationHandler handler) {
+                                            final Set<Variable> variables, final ComputationHandler handler) {
         final SolverState solverState = growSolver.saveState();
         growSolver.add(h);
         final Assignment maxModel = growSolver.execute(OptimizationFunction.builder()
                 .handler(handler)
                 .literals(variables)
                 .maximize().build());
-        if (maxModel == null || Handler.aborted(handler)) {
+        if (maxModel == null || !handler.shouldResume(NO_EVENT)) {
             return null;
         } else {
             final SortedSet<Variable> maximumSatisfiableSet = maxModel.positiveVariables();

src/main/java/com/booleworks/logicng/formulas/Formula.java

@@ -10,6 +10,7 @@
 import com.booleworks.logicng.functions.NumberOfAtomsFunction;
 import com.booleworks.logicng.functions.NumberOfNodesFunction;
 import com.booleworks.logicng.functions.VariablesFunction;
+import com.booleworks.logicng.handlers.NopHandler;
 import com.booleworks.logicng.knowledgecompilation.bdds.BDD;
 import com.booleworks.logicng.knowledgecompilation.bdds.BDDFactory;
 import com.booleworks.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel;
@@ -356,7 +357,7 @@ default BDD bdd(final FormulaFactory f, final VariableOrderingProvider provider)
         } else {
             kernel = new BDDKernel(f, provider.getOrder(f, formula), varNum * 30, varNum * 20);
         }
-        return BDDFactory.build(f, formula, kernel, null);
+        return BDDFactory.build(f, formula, kernel, NopHandler.get());
     }
 
     /**

src/main/java/com/booleworks/logicng/handlers/ComputationHandler.java

@@ -1,25 +1,24 @@
-// SPDX-License-Identifier: Apache-2.0 and MIT
-// Copyright 2015-2023 Christoph Zengler
-// Copyright 2023-20xx BooleWorks GmbH
-
 package com.booleworks.logicng.handlers;
 
+import com.booleworks.logicng.handlers.events.LogicNGEvent;
+
 /**
- * A computation handler.
- * @version 1.6.2
- * @since 1.6.2
+ * Interface for a computation handler.
+ * @since 3.0.0
+ * @version 3.0.0
  */
-public abstract class ComputationHandler implements Handler {
-
-    protected boolean aborted;
-
-    @Override
-    public boolean aborted() {
-        return aborted;
-    }
+public interface ComputationHandler {
+    /**
+     * Processes the given event and returns {@code true} if the computation
+     * should be resumed and {@code false} if it should be aborted.
+     * @param event the event to handle, must not be {@code null}
+     * @return whether the computation should be resumed or not
+     */
+    boolean shouldResume(LogicNGEvent event);
 
-    @Override
-    public void started() {
-        aborted = false;
-    }
+    /**
+     * @deprecated should be removed
+     */
+    @Deprecated
+    boolean isAborted();
 }