Merge branch 'development' into feature/backbones

.gitignore

@@ -14,9 +14,9 @@ target/
 .sonar/
 
 # test logs
-tests/maxsat/log.txt
-tests/partialmaxsat/log.txt
-tests/partialweightedmaxsat/log.txt
+src/test/resources/maxsat/log.txt
+src/test/resources/partialmaxsat/log.txt
+src/test/resources/partialweightedmaxsat/log.txt
 
 # test temporary files
-tests/writers/temp/*.dot
+src/test/resources/writers/temp/*.dot

pom.xml

@@ -72,7 +72,7 @@
 
     <!-- Dependency Versions -->
     <version.antlr>4.7.1</version.antlr>
-    <version.jacoco>0.8.0</version.jacoco>
+    <version.jacoco>0.8.3</version.jacoco>
     <version.coveralls>4.3.0</version.coveralls>
     <version.junit>4.12</version.junit>
     <version.assertj>2.8.0</version.assertj>
@@ -155,7 +155,7 @@
       <plugin>
         <groupId>org.apache.maven.plugins</groupId>
         <artifactId>maven-surefire-plugin</artifactId>
-        <version>2.22.0</version>
+        <version>3.0.0-M3</version>
         <configuration>
           <useSystemClassLoader>false</useSystemClassLoader>
         </configuration>
@@ -253,7 +253,7 @@
           <plugin>
             <groupId>org.apache.maven.plugins</groupId>
             <artifactId>maven-javadoc-plugin</artifactId>
-            <version>2.10.4</version>
+            <version>3.0.1</version>
             <executions>
               <execution>
                 <id>attach-javadocs</id>

src/main/java/org/logicng/collections/LNGVector.java

@@ -124,7 +124,6 @@ public T back() {
    * Pushes an element at the end of the vector.
    * @param element the element
    */
-  @SuppressWarnings("unchecked")
   public void push(final T element) {
     int newSize = this.size + 1;
     this.ensure(newSize);

src/main/java/org/logicng/datastructures/Assignment.java

@@ -98,13 +98,9 @@ public Assignment(final Collection<? extends Literal> lits) {
    */
   public Assignment(final Literal... lits) {
     this(false);
-    for (Literal lit : lits)
-      if (lit.phase())
-        this.pos.add((Variable) lit);
-      else {
-        this.neg.add(lit);
-        this.negVars.add((Variable) lit.negate());
-      }
+    for (Literal lit : lits) {
+      addLiteral(lit);
+    }
   }
 
   /**
@@ -116,13 +112,9 @@ public Assignment(final Literal... lits) {
    */
   public Assignment(final Collection<? extends Literal> lits, final boolean fastEvaluable) {
     this(fastEvaluable);
-    for (Literal lit : lits)
-      if (lit.phase())
-        this.pos.add((Variable) lit);
-      else {
-        this.neg.add(lit);
-        this.negVars.add((Variable) lit.negate());
-      }
+    for (Literal lit : lits) {
+      addLiteral(lit);
+    }
   }
 
   /**
@@ -142,12 +134,7 @@ public Assignment(final Literal lit) {
    */
   public Assignment(final Literal lit, final boolean fastEvaluable) {
     this(fastEvaluable);
-    if (lit.phase())
-      this.pos.add((Variable) lit);
-    else {
-      this.neg.add(lit);
-      this.negVars.add((Variable) lit.negate());
-    }
+    addLiteral(lit);
   }
 
   /**
@@ -224,21 +211,22 @@ public SortedSet<Literal> literals() {
    */
   public void addLiteral(final Literal lit) {
     if (lit.phase())
-      this.pos.add((Variable) lit);
+      this.pos.add(lit.variable());
     else {
       this.neg.add(lit);
-      this.negVars.add((Variable) lit.negate());
+      this.negVars.add(lit.variable());
     }
   }
 
   /**
-   * Evaluates a given literal.  Will be {@code false} if the literal is unknown.
+   * Evaluates a given literal.  A literal not covered by the assignment evaluates
+   * to {@code false} if it is positive, otherwise it evaluates to {@code true}.
    * @param lit the literal
-   * @return the evaluation of the literal or {@code false} if unknown
+   * @return the evaluation of the literal
    */
   public boolean evaluateLit(final Literal lit) {
     if (lit.phase())
-      return this.pos.contains(lit);
+      return this.pos.contains(lit.variable());
     else
       return this.neg.contains(lit) || !this.pos.contains(lit.variable());
   }

src/main/java/org/logicng/datastructures/ubtrees/UBNode.java

@@ -0,0 +1,94 @@
+package org.logicng.datastructures.ubtrees;
+
+import java.util.Objects;
+import java.util.SortedMap;
+import java.util.SortedSet;
+import java.util.TreeMap;
+
+/**
+ * A node in a UBTree, holding a comparable element.
+ * @param <T> The element type of the node, must be comparable
+ * @version 1.5.0
+ * @since 1.5.0
+ */
+public class UBNode<T extends Comparable<T>> {
+
+    private final T element;
+    private final SortedMap<T, UBNode<T>> children;
+    private SortedSet<T> set;
+
+    /**
+     * Constructs a new UB Tree node with the given element.
+     * @param element the node's element
+     */
+    UBNode(T element) {
+        this.element = element;
+        this.children = new TreeMap<>();
+    }
+
+    /**
+     * Returns the element of this node.
+     * @return the element of this node.
+     */
+    T element() {
+        return this.element;
+    }
+
+    /**
+     * Returns the set of this node.  If this node is a terminal node, it holds a set
+     * of the UB Tree.  In this case this methods returns this set, otherwise it returns
+     * {@code null}.
+     * @return the set of this node if it is a terminal node, {@code null} otherwise
+     */
+    SortedSet<T> set() {
+        return this.set;
+    }
+
+    /**
+     * Returns all children of this node.
+     * @return a mapping from element to its node - all of which are children of the current node
+     */
+    SortedMap<T, UBNode<T>> children() {
+        return this.children;
+    }
+
+    /**
+     * Returns whether this node is a terminal node or not.
+     * @return {@code true} if this is a terminal node, {@code false} otherwise
+     */
+    boolean isEndOfPath() {
+        return this.set != null;
+    }
+
+    /**
+     * Sets a set for this node and therefore this node is a terminal node.
+     * @param set the set for this node
+     */
+    void setEndSet(final SortedSet<T> set) {
+        this.set = set;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) { return true; }
+        if (o == null || getClass() != o.getClass()) { return false; }
+        UBNode<?> ubNode = (UBNode<?>) o;
+        return Objects.equals(element, ubNode.element) &&
+                Objects.equals(children, ubNode.children) &&
+                Objects.equals(set, ubNode.set);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(element, children, set);
+    }
+
+    @Override
+    public String toString() {
+        return "UBNode{" +
+                "element=" + element +
+                ", children=" + children +
+                ", set=" + set +
+                '}';
+    }
+}