Merge branch 'development'

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.0-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.1-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.0</version>
+  <version>1.6.1</version>
 </dependency>
 ```
 to your Maven POM.
@@ -62,6 +62,10 @@ 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 [email protected] for further details.
 
 ## Changelog
+### 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).
+* Fixed the behaviour of model enumeration with additional variables.
 
 ### Version 1.6.0 (Release September 2019)
 * A new method for generating CNFs directly on the solver instead of using the formula factory.

pom.xml

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

src/main/java/org/logicng/explanations/unsatcores/algorithms/PlainInsertionBasedMUS.java

@@ -59,7 +59,7 @@ public <T extends Proposition> UNSATCore<T> computeMUS(List<T> propositions, For
         solver.add(p);
       int count = currentFormula.size();
       while (solver.sat() == Tristate.TRUE) {
-        if (count < 0)
+        if (count == 0)
           throw new IllegalArgumentException("Cannot compute a MUS for a satisfiable formula set.");
         final T removeProposition = currentFormula.get(--count);
         currentSubset.add(removeProposition);

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

@@ -32,19 +32,31 @@
 
 /**
  * Super class for a formula string representation.
- *
  * @version 1.3
  * @since 1.0
  */
 public abstract class FormulaStringRepresentation {
 
     /**
      * Returns the string representation of the given formula.
-     *
+     * <p>
+     * In order to add a prefix/suffix or do one-time calculations on the formula it is recommended to overwrite this
+     * method in sub-classes.
      * @param formula the formula
      * @return the string representation of the formula
      */
     public String toString(final Formula formula) {
+        return toInnerString(formula);
+    }
+
+    /**
+     * Returns the string representation of the given formula.
+     * <p>
+     * This method is used for recursive calls in order to format the sub-formulas.
+     * @param formula the formula
+     * @return the string representation of the formula
+     */
+    protected String toInnerString(Formula formula) {
         switch (formula.type()) {
             case FALSE:
                 return this.falsum();
@@ -68,10 +80,11 @@ public String toString(final Formula formula) {
                 return this.naryOperator(nary, String.format("%s", op));
             case PBC:
                 final PBConstraint pbc = (PBConstraint) formula;
-                if (pbc.isTrivialFalse())
+                if (pbc.isTrivialFalse()) {
                     return this.falsum();
-                else if (pbc.isTrivialTrue())
+                } else if (pbc.isTrivialTrue()) {
                     return this.verum();
+                }
                 return String.format("%s%s%d", this.pbLhs(pbc.operands(), pbc.coefficients()), this.pbComparator(pbc.comparator()), pbc.rhs());
             default:
                 throw new IllegalArgumentException("Cannot print the unknown formula type " + formula.type());
@@ -80,32 +93,29 @@ else if (pbc.isTrivialTrue())
 
     /**
      * Returns a bracketed string version of a given formula.
-     *
      * @param formula the formula
      * @return {@code "(" + formula.toString() + ")"}
      */
     protected String bracket(final Formula formula) {
-        return String.format("%s%s%s", this.lbr(), this.toString(formula), this.rbr());
+        return String.format("%s%s%s", this.lbr(), this.toInnerString(formula), this.rbr());
     }
 
     /**
      * Returns the string representation of a binary operator.
-     *
      * @param operator the binary operator
      * @param opString the operator string
      * @return the string representation
      */
     protected String binaryOperator(final BinaryOperator operator, final String opString) {
         final String leftString = operator.type().precedence() < operator.left().type().precedence()
-                ? this.toString(operator.left()) : this.bracket(operator.left());
+                ? this.toInnerString(operator.left()) : this.bracket(operator.left());
         final String rightString = operator.type().precedence() < operator.right().type().precedence()
-                ? this.toString(operator.right()) : this.bracket(operator.right());
+                ? this.toInnerString(operator.right()) : this.bracket(operator.right());
         return String.format("%s%s%s", leftString, opString, rightString);
     }
 
     /**
      * Returns the string representation of an n-ary operator.
-     *
      * @param operator the n-ary operator
      * @param opString the operator string
      * @return the string representation
@@ -119,19 +129,18 @@ protected String naryOperator(final NAryOperator operator, final String opString
             if (++count == size) {
                 last = op;
             } else {
-                sb.append(operator.type().precedence() < op.type().precedence() ? this.toString(op) : this.bracket(op));
+                sb.append(operator.type().precedence() < op.type().precedence() ? this.toInnerString(op) : this.bracket(op));
                 sb.append(opString);
             }
         }
         if (last != null) {
-            sb.append(operator.type().precedence() < last.type().precedence() ? this.toString(last) : this.bracket(last));
+            sb.append(operator.type().precedence() < last.type().precedence() ? this.toInnerString(last) : this.bracket(last));
         }
         return sb.toString();
     }
 
     /**
      * Returns the string representation of the left-hand side of a pseudo-Boolean constraint.
-     *
      * @param operands     the literals of the constraint
      * @param coefficients the coefficients of the constraint
      * @return the string representation
@@ -160,85 +169,73 @@ protected String pbLhs(final Literal[] operands, final int[] coefficients) {
 
     /**
      * Returns the string representation of false.
-     *
      * @return the string representation of false
      */
     protected abstract String falsum();
 
     /**
      * Returns the string representation of true.
-     *
      * @return the string representation of true
      */
     protected abstract String verum();
 
     /**
      * Returns the string representation of not.
-     *
      * @return the string representation of not
      */
     protected abstract String negation();
 
     /**
      * Returns the string representation of an implication.
-     *
      * @return the string representation of an implication
      */
     protected abstract String implication();
 
     /**
      * Returns the string representation of an equivalence.
-     *
      * @return the string representation of an equivalence
      */
     protected abstract String equivalence();
 
     /**
      * Returns the string representation of and.
-     *
      * @return the string representation of and
      */
     protected abstract String and();
 
     /**
      * Returns the string representation of or.
-     *
      * @return the string representation of or
      */
     protected abstract String or();
 
     /**
      * Returns the string representation of a pseudo-Boolean comparator.
-     *
      * @param comparator the pseudo-Boolean comparator
      * @return the string representation of a pseudo-Boolean comparator
      */
     protected abstract String pbComparator(final CType comparator);
 
     /**
      * Returns the string representation of a pseudo-Boolean multiplication.
-     *
      * @return the string representation of a pseudo-Boolean multiplication
      */
     protected abstract String pbMul();
 
     /**
      * Returns the string representation of a pseudo-Boolean addition.
-     *
      * @return the string representation of a pseudo-Boolean addition
      */
     protected abstract String pbAdd();
 
     /**
      * Returns the string representation of a left bracket.
-     *
      * @return the string representation of a left bracket
      */
     protected abstract String lbr();
 
     /**
      * Returns the string representation of right bracket.
-     *
      * @return the string representation of right bracket
      */
     protected abstract String rbr();

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

@@ -59,13 +59,13 @@ private static String latexName(final String name) {
   }
 
   @Override
-  public String toString(final Formula formula) {
+  public String toInnerString(final Formula formula) {
     switch (formula.type()) {
       case LITERAL:
         final Literal lit = (Literal) formula;
         return lit.phase() ? latexName(lit.name()) : this.negation() + " " + latexName(lit.name());
       default:
-        return super.toString(formula);
+        return super.toInnerString(formula);
     }
   }
 

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

@@ -99,7 +99,7 @@ public SortedStringRepresentation(final List<Variable> varOrder) {
      * @return the sorted string representation of the formula with regard to the variable ordering
      */
     @Override
-    public String toString(final Formula formula) {
+    public String toInnerString(final Formula formula) {
         switch (formula.type()) {
             case FALSE:
                 return falsum();
@@ -154,12 +154,12 @@ protected String naryOperator(final NAryOperator operator, final String opString
             if (++count == size) {
                 last = op;
             } else {
-                sb.append(operator.type().precedence() < op.type().precedence() ? toString(op) : bracket(op));
+                sb.append(operator.type().precedence() < op.type().precedence() ? toInnerString(op) : bracket(op));
                 sb.append(opString);
             }
         }
         if (last != null) {
-            sb.append(operator.type().precedence() < last.type().precedence() ? toString(last) : bracket(last));
+            sb.append(operator.type().precedence() < last.type().precedence() ? toInnerString(last) : bracket(last));
         }
         return sb.toString();
     }
@@ -226,8 +226,8 @@ private String sortedEquivalence(final Equivalence equivalence) {
             right = equivalence.left();
             left = equivalence.right();
         }
-        final String leftString = FType.EQUIV.precedence() < left.type().precedence() ? toString(left) : bracket(left);
-        final String rightString = FType.EQUIV.precedence() < right.type().precedence() ? toString(right) : bracket(right);
+        final String leftString = FType.EQUIV.precedence() < left.type().precedence() ? toInnerString(left) : bracket(left);
+        final String rightString = FType.EQUIV.precedence() < right.type().precedence() ? toInnerString(right) : bracket(right);
         return String.format("%s%s%s", leftString, equivalence(), rightString);
     }
 

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

@@ -99,13 +99,13 @@ private static String getSubscript(final String number) {
   }
 
   @Override
-  public String toString(final Formula formula) {
+  protected String toInnerString(final Formula formula) {
     switch (formula.type()) {
       case LITERAL:
         final Literal lit = (Literal) formula;
         return lit.phase() ? utf8Name(lit.name()) : this.negation() + utf8Name(lit.name());
       default:
-        return super.toString(formula);
+        return super.toInnerString(formula);
     }
   }
 

src/main/java/org/logicng/solvers/CleaneLing.java

@@ -426,4 +426,14 @@ public SortedSet<Literal> upZeroLiterals() {
     public Set<Formula> formulaOnSolver() {
         throw new UnsupportedOperationException("The CleaneLing solver does not support returning the formula on the solver");
     }
+
+    @Override
+    public void setSelectionOrder(List<? extends Literal> selectionOrder) {
+        throw new UnsupportedOperationException("The CleaneLing solver does not support a custom selection order");
+    }
+
+    @Override
+    public void resetSelectionOrder() {
+        throw new UnsupportedOperationException("The CleaneLing solver does not support a custom selection order");
+    }
 }

src/main/java/org/logicng/solvers/MiniSat.java

@@ -78,10 +78,6 @@
 import java.util.SortedSet;
 import java.util.TreeSet;
 
-import static org.logicng.datastructures.Tristate.FALSE;
-import static org.logicng.datastructures.Tristate.TRUE;
-import static org.logicng.datastructures.Tristate.UNDEF;
-
 /**
  * Wrapper for the MiniSAT-style SAT solvers.
  * @version 1.6.0
@@ -378,15 +374,19 @@ public List<Assignment> enumerateAllModels(final Collection<Variable> variables,
       }
     }
     LNGIntVector relevantAllIndices = null;
+    final TreeSet<Variable> uniqueAdditionalVariables = new TreeSet<>(additionalVariables);
+    if (variables != null) {
+      uniqueAdditionalVariables.removeAll(variables);
+    }
     if (relevantIndices != null) {
-      if (additionalVariables.isEmpty()) {
+      if (uniqueAdditionalVariables.isEmpty()) {
         relevantAllIndices = relevantIndices;
       } else {
-        relevantAllIndices = new LNGIntVector(relevantIndices.size() + additionalVariables.size());
+        relevantAllIndices = new LNGIntVector(relevantIndices.size() + uniqueAdditionalVariables.size());
         for (int i = 0; i < relevantIndices.size(); ++i) {
           relevantAllIndices.push(relevantIndices.get(i));
         }
-        for (final Variable var : additionalVariables) {
+        for (final Variable var : uniqueAdditionalVariables) {
           relevantAllIndices.push(this.solver.idxForName(var.name()));
         }
       }
@@ -709,4 +709,14 @@ public Set<Formula> formulaOnSolver() {
     }
     return formulas;
   }
+
+  @Override
+  public void setSelectionOrder(final List<? extends Literal> selectionOrder) {
+    this.solver.setSelectionOrder(selectionOrder);
+  }
+
+  @Override
+  public void resetSelectionOrder() {
+    this.solver.resetSelectionOrder();
+  }
 }