Java 1.6 version of LogicNG 1.3

pom.xml

@@ -25,12 +25,12 @@
          xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
-  <artifactId>logicng</artifactId>
+  <artifactId>logicng-j6</artifactId>
   <version>1.3</version>
   <packaging>jar</packaging>
 
   <name>LogicNG</name>
-  <description>The Next Generation Logic Library</description>
+  <description>The Next Generation Logic Library (for Java 6)</description>
   <url>http://www.logicng.org</url>
 
   <licenses>
@@ -62,8 +62,8 @@
   <properties>
     <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
 
-    <maven.compiler.source>1.7</maven.compiler.source>
-    <maven.compiler.target>1.7</maven.compiler.target>
+    <maven.compiler.source>1.6</maven.compiler.source>
+    <maven.compiler.target>1.6</maven.compiler.target>
 
     <sonar.language>java</sonar.language>
     <sonar.exclusions>**/LogicNGPropositional*.java,**/LogicNGPseudoBoolean*.java</sonar.exclusions>

src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java

@@ -76,8 +76,8 @@ final class CCAMOBimander implements CCAtMostOne {
    */
   CCAMOBimander(int m) {
     this.m = m;
-    this.groups = new LNGVector<>();
-    this.bits = new LNGVector<>();
+    this.groups = new LNGVector<LNGVector<Literal>>();
+    this.bits = new LNGVector<Literal>();
   }
 
   @Override

src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java

@@ -75,9 +75,9 @@ final class CCAMOCommander implements CCAtMostOne {
    */
   CCAMOCommander(int k) {
     this.k = k;
-    this.literals = new LNGVector<>();
-    this.nextLiterals = new LNGVector<>();
-    this.currentLiterals = new LNGVector<>();
+    this.literals = new LNGVector<Literal>();
+    this.nextLiterals = new LNGVector<Literal>();
+    this.currentLiterals = new LNGVector<Literal>();
   }
 
   @Override

src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java

@@ -91,8 +91,8 @@ private void encodeIntern(final LNGVector<Literal> vars) {
         for (int j = i + 1; j < vars.size(); j++)
           this.result.addClause(vars.get(i).negate(), vars.get(j).negate());
     else {
-      final LNGVector<Literal> l1 = new LNGVector<>(vars.size() / 2);
-      final LNGVector<Literal> l2 = new LNGVector<>(vars.size() / 2);
+      final LNGVector<Literal> l1 = new LNGVector<Literal>(vars.size() / 2);
+      final LNGVector<Literal> l2 = new LNGVector<Literal>(vars.size() / 2);
       int i = 0;
       for (; i < vars.size() / 2; i++)
         l1.push(vars.get(i));

src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java

@@ -79,8 +79,8 @@ final class CCCardinalityNetworks {
 
   void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
-    final LNGVector<Literal> input = new LNGVector<>();
-    final LNGVector<Literal> output = new LNGVector<>();
+    final LNGVector<Literal> input = new LNGVector<Literal>();
+    final LNGVector<Literal> output = new LNGVector<Literal>();
     if (rhs > vars.length / 2) {
       int geq = vars.length - rhs;
       for (final Variable v : vars)
@@ -98,8 +98,8 @@ void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
   }
 
   void buildAMKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
-    final LNGVector<Literal> input = new LNGVector<>();
-    final LNGVector<Literal> output = new LNGVector<>();
+    final LNGVector<Literal> input = new LNGVector<Literal>();
+    final LNGVector<Literal> output = new LNGVector<Literal>();
     for (final Variable var : vars)
       input.push(var);
     this.sorting.sort(rhs + 1, input, result, output, INPUT_TO_OUTPUT);
@@ -110,8 +110,8 @@ void buildAMKForIncremental(final EncodingResult result, final Variable[] vars,
 
   void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
-    final LNGVector<Literal> input = new LNGVector<>();
-    final LNGVector<Literal> output = new LNGVector<>();
+    final LNGVector<Literal> input = new LNGVector<Literal>();
+    final LNGVector<Literal> output = new LNGVector<Literal>();
     final int newRHS = vars.length - rhs;
     if (newRHS > vars.length / 2) {
       int geq = vars.length - newRHS;
@@ -130,8 +130,8 @@ void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
   }
 
   void buildALKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
-    final LNGVector<Literal> input = new LNGVector<>();
-    final LNGVector<Literal> output = new LNGVector<>();
+    final LNGVector<Literal> input = new LNGVector<Literal>();
+    final LNGVector<Literal> output = new LNGVector<Literal>();
     for (final Variable var : vars)
       input.push(var.negate());
     final int newRHS = vars.length - rhs;
@@ -143,8 +143,8 @@ void buildALKForIncremental(final EncodingResult result, final Variable[] vars,
 
   void buildEXK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
-    final LNGVector<Literal> input = new LNGVector<>();
-    final LNGVector<Literal> output = new LNGVector<>();
+    final LNGVector<Literal> input = new LNGVector<Literal>();
+    final LNGVector<Literal> output = new LNGVector<Literal>();
     for (final Variable var : vars)
       input.push(var);
     this.sorting.sort(rhs + 1, input, result, output, BOTH);

src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java

@@ -140,7 +140,7 @@ public void encode(final PBConstraint cc, final EncodingResult result) {
   public Pair<ImmutableFormulaList, CCIncrementalData> encodeIncremental(final PBConstraint cc) {
     final EncodingResult result = EncodingResult.resultForFormula(f);
     final CCIncrementalData incData = this.encodeIncremental(cc, result);
-    return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
+    return new Pair<ImmutableFormulaList, CCIncrementalData>(new ImmutableFormulaList(FType.AND, result.result()), incData);
   }
 
   /**

src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java

@@ -81,7 +81,7 @@ final class CCModularTotalizer {
     this.varError = f.variable("RESERVED@VAR_ERROR");
     this.h0 = this.varUndef;
     this.currentCardinalityRhs = -1;
-    this.inlits = new LNGVector<>();
+    this.inlits = new LNGVector<Literal>();
   }
 
   /**
@@ -132,16 +132,16 @@ CCIncrementalData incrementalData() {
   private int initialize(final EncodingResult result, int rhs, int n) {
     result.reset();
     this.result = result;
-    this.cardinalityUpOutvars = new LNGVector<>();
-    this.cardinalityLwOutvars = new LNGVector<>();
+    this.cardinalityUpOutvars = new LNGVector<Literal>();
+    this.cardinalityLwOutvars = new LNGVector<Literal>();
     int mod = (int) Math.ceil(Math.sqrt(rhs + 1.0));
-    this.cardinalityUpOutvars = new LNGVector<>(n / mod);
+    this.cardinalityUpOutvars = new LNGVector<Literal>(n / mod);
     for (int i = 0; i < n / mod; i++)
       this.cardinalityUpOutvars.push(this.result.newVariable());
-    this.cardinalityLwOutvars = new LNGVector<>(mod - 1);
+    this.cardinalityLwOutvars = new LNGVector<Literal>(mod - 1);
     for (int i = 0; i < mod - 1; i++)
       this.cardinalityLwOutvars.push(this.result.newVariable());
-    this.inlits = new LNGVector<>(n);
+    this.inlits = new LNGVector<Literal>(n);
     this.currentCardinalityRhs = rhs + 1;
     if (this.cardinalityUpOutvars.size() == 0)
       this.cardinalityUpOutvars.push(this.h0);
@@ -170,10 +170,10 @@ private void encodeOutput(int rhs, int mod) {
   }
 
   private void toCNF(int mod, final LNGVector<Literal> ubvars, final LNGVector<Literal> lwvars, int rhs) {
-    LNGVector<Literal> lupper = new LNGVector<>();
-    LNGVector<Literal> llower = new LNGVector<>();
-    LNGVector<Literal> rupper = new LNGVector<>();
-    LNGVector<Literal> rlower = new LNGVector<>();
+    LNGVector<Literal> lupper = new LNGVector<Literal>();
+    LNGVector<Literal> llower = new LNGVector<Literal>();
+    LNGVector<Literal> rupper = new LNGVector<Literal>();
+    LNGVector<Literal> rlower = new LNGVector<Literal>();
     assert rhs > 1;
     int split = rhs / 2;
     int left = 1;
@@ -288,7 +288,7 @@ private void finalAdder(int mod, final LNGVector<Literal> upper, final LNGVector
         if (i + j < upper.size())
           d = upper.get(i + j);
         if (c != this.varUndef && c != this.varError) {
-          final LNGVector<Literal> clause = new LNGVector<>();
+          final LNGVector<Literal> clause = new LNGVector<Literal>();
           if (a != this.varUndef && a != this.varError)
             clause.push(a.negate());
           if (b != this.varUndef && b != this.varError)
@@ -297,7 +297,7 @@ private void finalAdder(int mod, final LNGVector<Literal> upper, final LNGVector
           if (clause.size() > 1)
             this.result.addClause(clause);
         }
-        final LNGVector<Literal> clause = new LNGVector<>();
+        final LNGVector<Literal> clause = new LNGVector<Literal>();
         clause.push(carry.negate());
         if (a != this.varUndef && a != this.varError)
           clause.push(a.negate());

src/main/java/org/logicng/cardinalityconstraints/CCSorting.java

@@ -80,7 +80,7 @@ public enum ImplicationDirection {
    * Constructs a new sorting network.
    */
   public CCSorting() {
-    this.auxVars = new LNGVector<>();
+    this.auxVars = new LNGVector<LNGVector<Literal>>();
   }
 
   private static int counterSorterValue(int m, int n) {
@@ -182,10 +182,10 @@ private void recursiveSorter(int m, int l, final LNGVector<Literal> input, final
     assert output.size() == 0;
     assert n > 1;
     assert m <= n;
-    final LNGVector<Literal> tmpLitsA = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsB = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsO1 = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsO2 = new LNGVector<>();
+    final LNGVector<Literal> tmpLitsA = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsB = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsO1 = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsO2 = new LNGVector<Literal>();
 
     for (int i = 0; i < l; i++)
       tmpLitsA.push(input.get(i));
@@ -250,7 +250,7 @@ private void directSorter(int m, final LNGVector<Literal> input, final EncodingR
     int n = input.size();
     assert n < 20;
     int bitmask = 1;
-    final LNGVector<Literal> clause = new LNGVector<>();
+    final LNGVector<Literal> clause = new LNGVector<Literal>();
     output.clear();
     for (int i = 0; i < m; i++)
       output.push(formula.newVariable());
@@ -337,12 +337,12 @@ private void recursiveMerger(int c, final LNGVector<Literal> inputA, int a, fina
       output.push(y2);
       return;
     }
-    final LNGVector<Literal> oddMerge = new LNGVector<>();
-    final LNGVector<Literal> evenMerge = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsOddA = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsOddB = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsEvenA = new LNGVector<>();
-    final LNGVector<Literal> tmpLitsEvenB = new LNGVector<>();
+    final LNGVector<Literal> oddMerge = new LNGVector<Literal>();
+    final LNGVector<Literal> evenMerge = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsOddA = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsOddB = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsEvenA = new LNGVector<Literal>();
+    final LNGVector<Literal> tmpLitsEvenB = new LNGVector<Literal>();
 
     for (int i = 0; i < a2; i = i + 2)
       tmpLitsOddA.push(inputA.get(i));

src/main/java/org/logicng/cardinalityconstraints/CCTotalizer.java

@@ -129,8 +129,8 @@ void buildEXK(final EncodingResult result, final Variable[] vars, int rhs) {
   private LNGVector<Variable> initializeConstraint(final EncodingResult result, final Variable[] vars) {
     result.reset();
     this.result = result;
-    this.cardinalityInvars = new LNGVector<>(vars.length);
-    final LNGVector<Variable> cardinalityOutvars = new LNGVector<>(vars.length);
+    this.cardinalityInvars = new LNGVector<Variable>(vars.length);
+    final LNGVector<Variable> cardinalityOutvars = new LNGVector<Variable>(vars.length);
     for (final Variable var : vars) {
       this.cardinalityInvars.push(var);
       cardinalityOutvars.push(this.result.newVariable());
@@ -147,8 +147,8 @@ CCIncrementalData incrementalData() {
   }
 
   private void toCNF(final LNGVector<Variable> vars, int rhs, final Bound bound) {
-    final LNGVector<Variable> left = new LNGVector<>();
-    final LNGVector<Variable> right = new LNGVector<>();
+    final LNGVector<Variable> left = new LNGVector<Variable>();
+    final LNGVector<Variable> right = new LNGVector<Variable>();
     assert vars.size() > 1;
     int split = vars.size() / 2;
     for (int i = 0; i < vars.size(); i++) {

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

@@ -43,7 +43,6 @@
 import java.util.List;
 import java.util.Map;
 import java.util.NoSuchElementException;
-import java.util.Objects;
 import java.util.SortedMap;
 import java.util.SortedSet;
 import java.util.TreeMap;
@@ -211,7 +210,7 @@ public boolean containsFormula(final Formula formula) {
    */
   public SortedSet<Variable> variables() {
     if (this.variables == null) {
-      this.variables = new TreeSet<>();
+      this.variables = new TreeSet<Variable>();
       for (final Formula f : this.formulas)
         this.variables.addAll(f.variables());
     }
@@ -223,7 +222,7 @@ public SortedSet<Variable> variables() {
    * @return all literals occurring in this formula list
    */
   public SortedSet<Literal> literals() {
-    final SortedSet<Literal> literals = new TreeSet<>();
+    final SortedSet<Literal> literals = new TreeSet<Literal>();
     for (final Formula f : this.formulas)
       literals.addAll(f.literals());
     return literals;
@@ -235,7 +234,7 @@ public SortedSet<Literal> literals() {
    */
   public SortedMap<Variable, Integer> varProfile() {
     final VariableProfileFunction variableProfileFunction = new VariableProfileFunction();
-    final SortedMap<Variable, Integer> profile = new TreeMap<>();
+    final SortedMap<Variable, Integer> profile = new TreeMap<Variable, Integer>();
     for (final Formula f : this.formulas)
       for (final Map.Entry<Variable, Integer> entry : f.apply(variableProfileFunction).entrySet()) {
         final Integer currentCount = profile.get(entry.getKey());
@@ -253,7 +252,7 @@ public SortedMap<Variable, Integer> varProfile() {
    */
   public SortedMap<Literal, Integer> litProfile() {
     final LiteralProfileFunction literalProfileFunction = new LiteralProfileFunction();
-    final SortedMap<Literal, Integer> profile = new TreeMap<>();
+    final SortedMap<Literal, Integer> profile = new TreeMap<Literal, Integer>();
     for (final Formula f : this.formulas)
       for (final Map.Entry<Literal, Integer> entry : f.apply(literalProfileFunction).entrySet()) {
         final Integer currentCount = profile.get(entry.getKey());
@@ -295,9 +294,12 @@ public List<Formula> toList() {
 
   @Override
   public int hashCode() {
-    return Objects.hash(this.operator, Arrays.hashCode(this.formulas));
+    int result = operator != null ? operator.hashCode() : 0;
+    result = 31 * result + Arrays.hashCode(formulas);
+    return result;
   }
 
+
   @Override
   public boolean equals(final Object other) {
     return this == other || (other instanceof ImmutableFormulaList) && this.operator == ((ImmutableFormulaList) other).operator