Merge branch 'development'

Author: czengler

README.md

@@ -1,4 +1,4 @@
-[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.6.1-ff69b4.svg)
+[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.6.2-ff69b4.svg)
 
 <img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300">
 
@@ -19,7 +19,7 @@ LogicNG is released in the Maven Central Repository.  To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>1.6.1</version>
+  <version>1.6.2</version>
 </dependency>
 ```
 to your Maven POM.
@@ -62,6 +62,11 @@ We recently started a Wiki section for a [FAQ](https://github.com/logic-ng/Logic
 The library is released under the Apache License and therefore is free to use in any private, educational, or commercial projects.  Commercial support is available through the German company [BooleWorks GmbH](http://www.booleworks.com) - the company behind LogicNG.  Please contact Christoph Zengler at christoph@logicng.org for further details.
 
 ## Changelog
+
+### Version 1.6.2 (Release January 2020)
+* Some improvements to handlers for computations
+* New BDD handlers
+
 ### Version 1.6.1 (Release September 2019)
 * A new method for solving a formula with a given literal ordering.
 * Minor refactoring of the Formatter super class (no effects on callers).

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>1.6.1</version>
+  <version>1.6.2</version>
   <packaging>jar</packaging>
 
   <name>LogicNG</name>

src/main/java/org/logicng/bdds/BDDFactory.java

@@ -57,8 +57,6 @@
 
 package org.logicng.bdds;
 
-import static org.logicng.formulas.FType.AND;
-
 import org.logicng.bdds.datastructures.BDD;
 import org.logicng.bdds.datastructures.BDDConstant;
 import org.logicng.bdds.datastructures.BDDInnerNode;
@@ -67,12 +65,15 @@
 import org.logicng.collections.LNGVector;
 import org.logicng.datastructures.Assignment;
 import org.logicng.formulas.Equivalence;
+import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Implication;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Not;
 import org.logicng.formulas.Variable;
+import org.logicng.handlers.BDDHandler;
+import org.logicng.handlers.TimeoutHandler;
 
 import java.math.BigDecimal;
 import java.util.ArrayList;
@@ -91,7 +92,7 @@
 
 /**
  * The factory for the jBuddy implementation.
- * @version 1.4.0
+ * @version 1.6.2
  * @since 1.4.0
  */
 public class BDDFactory {
@@ -135,15 +136,41 @@ protected BDDFactory(final BDDKernel kernel, final FormulaFactory f) {
    * @return the top node of the BDD
    */
   public BDD build(final Formula formula) {
-    return new BDD(buildRec(formula), this);
+    return build(formula, null);
+  }
+
+  /**
+   * Builds a BDD for a given formula.  BDDs support all Boolean formula types but not pseudo-Boolean constraints.
+   * The reason is that before converting a formula to a BDD one must specify the number of variables.  In case of
+   * pseudo-Boolean constraints this number depends on the translation of the constraint.  Therefore the caller first
+   * has to transform any pseudo-Boolean constraints in their respective CNF representation before converting them
+   * to a BDD.
+   *
+   * If a BDD handler is given and the BDD generation is aborted due to the handler, the method will return
+   * {@link BDDKernel#BDD_ABORT} as result. If {@code null} is passed as handler, the generation will continue without
+   * interruption.
+   * @param formula the formula
+   * @param handler the BDD handler
+   * @return the top node of the BDD or {@link BDDKernel#BDD_ABORT} if the computation was aborted
+   */
+  public BDD build(final Formula formula, final BDDHandler handler) {
+    if (handler != null) {
+      handler.started();
+    }
+    return new BDD(buildRec(formula, handler), this);
   }
 
   /**
    * Recursive build procedure for the BDD.
+   *
+   * If a BDD handler is given and the BDD generation is aborted due to the handler, the method will return
+   * {@link BDDKernel#BDD_ABORT} as result. If {@code null} is passed as handler, the generation will continue without
+   * interruption.
    * @param formula the formula
-   * @return the BDD index
+   * @param handler the BDD handler
+   * @return the BDD index or {@link BDDKernel#BDD_ABORT} if the computation was aborted
    */
-  private int buildRec(final Formula formula) {
+  private int buildRec(final Formula formula, final BDDHandler handler) {
     switch (formula.type()) {
       case FALSE:
         return BDDKernel.BDD_FALSE;
@@ -158,26 +185,59 @@ private int buildRec(final Formula formula) {
           this.idx2var.put(idx, lit.variable());
         }
         return lit.phase() ? this.kernel.ithVar(idx) : this.kernel.nithVar(idx);
-      case NOT:
+      case NOT: {
         final Not not = (Not) formula;
-        return this.kernel.addRef(this.kernel.not(buildRec(not.operand())));
-      case IMPL:
+        final int operand = buildRec(not.operand(), handler);
+        if (operand == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        } else {
+          return this.kernel.addRef(this.kernel.not(operand), handler);
+        }
+      }
+      case IMPL: {
         final Implication impl = (Implication) formula;
-        return this.kernel.addRef(this.kernel.implication(buildRec(impl.left()), buildRec(impl.right())));
-      case EQUIV:
+        final int left = buildRec(impl.left(), handler);
+        if (left == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        }
+        final int right = buildRec(impl.right(), handler);
+        if (right == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        }
+        return this.kernel.addRef(this.kernel.implication(left, right), handler);
+      }
+      case EQUIV: {
         final Equivalence equiv = (Equivalence) formula;
-        return this.kernel.addRef(this.kernel.equivalence(buildRec(equiv.left()), buildRec(equiv.right())));
+        final int left = buildRec(equiv.left(), handler);
+        if (left == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        }
+        final int right = buildRec(equiv.right(), handler);
+        if (right == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        }
+        return this.kernel.addRef(this.kernel.equivalence(left, right), handler);
+      }
       case AND:
-      case OR:
+      case OR: {
         final Iterator<Formula> it = formula.iterator();
-        int res = buildRec(it.next());
-        while (it.hasNext())
-          res = formula.type() == AND
-                  ? this.kernel.addRef(this.kernel.and(res, buildRec(it.next())))
-                  : this.kernel.addRef(this.kernel.or(res, buildRec(it.next())));
+        int res = buildRec(it.next(), handler);
+        if (res == BDDKernel.BDD_ABORT) {
+          return BDDKernel.BDD_ABORT;
+        }
+        while (it.hasNext()) {
+          final int operand = buildRec(it.next(), handler);
+          if (operand == BDDKernel.BDD_ABORT) {
+            return BDDKernel.BDD_ABORT;
+          }
+          res = formula.type() == FType.AND
+                  ? this.kernel.addRef(this.kernel.and(res, operand), handler)
+                  : this.kernel.addRef(this.kernel.or(res, operand), handler);
+        }
         return res;
+      }
       case PBC:
-        return buildRec(formula.nnf());
+        return buildRec(formula.nnf(), handler);
       default:
         throw new IllegalArgumentException("Unsupported operator for BDD generation: " + formula.type());
     }

src/main/java/org/logicng/bdds/jbuddy/BDDKernel.java

@@ -57,6 +57,8 @@
 
 package org.logicng.bdds.jbuddy;
 
+import org.logicng.handlers.BDDHandler;
+
 import java.math.BigDecimal;
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -65,11 +67,12 @@
 
 /**
  * The jBuddy kernel.
- * @version 1.4.0
+ * @version 1.6.2
  * @since 1.4.0
  */
 public class BDDKernel {
 
+  public static final int BDD_ABORT = -1;
   public static final int BDD_TRUE = 1;
   public static final int BDD_FALSE = 0;
 
@@ -115,7 +118,7 @@ private enum Operand {
   protected int varnum; // Number of defined BDD variables
   private int[] refstack; // Internal node reference stack
   private int refstacktop; // Internal node reference stack top
-  protected  int[] level2var; // Level -> variable table
+  protected int[] level2var; // Level -> variable table
 
   private int[] quantvarset; // Current variable set for quant.
   private int quantvarsetID; // Current id used in quantvarset
@@ -391,12 +394,17 @@ private int notRec(final int r) {
   /**
    * Adds a reference for a given node.  Reference counting is done on externally referenced nodes only and the count for
    * a specific node {@code r} can and must be increased using this function to avoid loosing the node in the next
-   * garbage collection.
-   * @param root the node
+   * garbage collection.  If a BDD handler is given, the handler's {@link BDDHandler#newRefAdded()} method is called.
+   * If the generation gets aborted due to the handler, the method will return {@link BDDKernel#BDD_ABORT} as result. If
+   * {@code null} is passed as handler, the generation will continue without interruption.
+   * @param root    the node
+   * @param handler the BDD handler
    * @return return the node
    * @throws IllegalArgumentException if the root node was invalid
    */
-  public int addRef(final int root) {
+  public int addRef(final int root, final BDDHandler handler) {
+    if (handler != null && !handler.newRefAdded())
+      return BDD_ABORT;
     if (root < 2)
       return root;
     if (root >= this.nodesize)
@@ -1061,7 +1069,7 @@ public int support(final int r) {
 
     for (int n = this.supportMax; n >= supportMin; --n)
       if (this.supportSet[n] == this.supportID) {
-        addRef(res);
+        addRef(res, null);
         final int tmp = makeNode(n, 0, res);
         delRef(res);
         res = tmp;

src/main/java/org/logicng/formulas/printer/FormulaStringRepresentation.java

@@ -92,12 +92,31 @@ protected String toInnerString(Formula formula) {
     }
 
     /**
-     * Returns a bracketed string version of a given formula.
+     * Returns a bracketed string version of a given formula. Exception: If the formula is a trivial pseudo-Boolean
+     * constraint, then the string version of the formula is returned without brackets.
      * @param formula the formula
      * @return {@code "(" + formula.toString() + ")"}
      */
     protected String bracket(final Formula formula) {
-        return String.format("%s%s%s", this.lbr(), this.toInnerString(formula), this.rbr());
+        if (isTrivialCase(formula)) {
+            return this.toInnerString(formula);
+        } else {
+            return String.format("%s%s%s", this.lbr(), this.toInnerString(formula), this.rbr());
+        }
+    }
+
+    /**
+     * Checks if the formula is a pseudo-Boolean constraint that is trivially false or trivially true.
+     * @param formula the formula
+     * @return {@code true} if the formula is a trivial pseudo-Boolean constraint, otherwise {@code false}
+     */
+    protected boolean isTrivialCase(Formula formula) {
+        if (formula.type() == FType.PBC) {
+            PBConstraint pbc = (PBConstraint) formula;
+            return pbc.isTrivialFalse() || pbc.isTrivialTrue();
+        } else {
+            return false;
+        }
     }
 
     /**

src/main/java/org/logicng/handlers/BDDHandler.java

@@ -0,0 +1,43 @@
+///////////////////////////////////////////////////////////////////////////
+//                   __                _      _   ________               //
+//                  / /   ____  ____ _(_)____/ | / / ____/               //
+//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
+//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
+//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
+//                           /____/                                      //
+//                                                                       //
+//               The Next Generation Logic Library                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+//                                                                       //
+//  Copyright 2015-20xx Christoph Zengler                                //
+//                                                                       //
+//  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.logicng.handlers;
+
+/**
+ * Interface for a handler for the BDD factory.
+ * @version 1.6.2
+ * @since 1.6.2
+ */
+public interface BDDHandler extends Handler {
+
+  /**
+   * This method is called every a new reference is added, i.e the method {@link org.logicng.bdds.jbuddy.BDDKernel#addRef(int, BDDHandler)} is called.
+   * @return whether BDD generation should be continued or not
+   */
+  boolean newRefAdded();
+}

src/main/java/org/logicng/handlers/ComputationHandler.java

@@ -0,0 +1,21 @@
+package org.logicng.handlers;
+
+/**
+ * A computation handler.
+ * @version 1.6.2
+ * @since 1.6.2
+ */
+public abstract class ComputationHandler implements Handler {
+
+  protected boolean aborted;
+
+  @Override
+  public boolean aborted() {
+    return this.aborted;
+  }
+
+  @Override
+  public void started() {
+    this.aborted = false;
+  }
+}

src/main/java/org/logicng/handlers/FactorizationHandler.java

@@ -32,10 +32,10 @@
 
 /**
  * A handler for factorization methods (CNF, DNF).
- * @version 1.0
+ * @version 1.6.2
  * @since 1.0
  */
-public interface FactorizationHandler {
+public interface FactorizationHandler extends Handler {
 
   /**
    * This method is called every time a distribution is performed.
@@ -49,5 +49,4 @@ public interface FactorizationHandler {
    * @return whether the factorization should be continued or not
    */
   boolean createdClause(final Formula clause);
-
 }

src/main/java/org/logicng/handlers/Handler.java

@@ -0,0 +1,22 @@
+package org.logicng.handlers;
+
+/**
+ * Interface for a handler.  A handler can be used as callback for different time-intensive computations in order
+ * to abort these computations.  There are same often used default handlers already implemented and users can
+ * implement their own handlers by implementing the respective interfaces.
+ * @version 1.6.2
+ * @since 1.6.2
+ */
+public interface Handler {
+
+  /**
+   * Returns whether the computation was aborted by the handler.
+   * @return {@code true} if the computation was aborted by the handler, otherwise {@code false}
+   */
+  public boolean aborted();
+
+  /**
+   * This method is called when the computation starts.
+   */
+  public void started();
+}