Refactored formulas package

logic-ng · Jan 19, 2020 · df6efc8 · df6efc8
1 parent b98bf36
commit df6efc8
Show file tree

Hide file tree

Showing 11 changed files with 34 additions and 71 deletions.
diff --git a/src/main/java/org/logicng/formulas/And.java b/src/main/java/org/logicng/formulas/And.java
@@ -33,6 +33,7 @@
 
 import org.logicng.datastructures.Assignment;
 
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.LinkedHashSet;
 
@@ -44,7 +45,7 @@
  * - does not contain duplicates
  * - does not contain complementary literals
  * - does not contain constants
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
 public final class And extends NAryOperator {
@@ -55,7 +56,7 @@ public final class And extends NAryOperator {
      * @param f        the factory which created this instance
      * @param isCNF    is {@code true} if the formula is in CNF, {@code false} otherwise
      */
-    And(final LinkedHashSet<? extends Formula> operands, final FormulaFactory f, boolean isCNF) {
+    And(final LinkedHashSet<? extends Formula> operands, final FormulaFactory f, final boolean isCNF) {
         super(FType.AND, operands, f);
         if (isCNF) {
             this.setPredicateCacheEntry(IS_CNF, true);
@@ -67,12 +68,7 @@ public final class And extends NAryOperator {
 
     @Override
     public boolean evaluate(final Assignment assignment) {
-        for (Formula op : operands) {
-            if (!op.evaluate(assignment)) {
-                return false;
-            }
-        }
-        return true;
+        return Arrays.stream(this.operands).allMatch(op -> op.evaluate(assignment));
     }
 
     @Override

diff --git a/src/main/java/org/logicng/formulas/BinaryOperator.java b/src/main/java/org/logicng/formulas/BinaryOperator.java
@@ -37,7 +37,7 @@
 
 /**
  * Super class for Boolean binary operators.
- * @version 1.5.1
+ * @version 2.0.0
  * @since 1.0
  */
 public abstract class BinaryOperator extends Formula {

diff --git a/src/main/java/org/logicng/formulas/CFalse.java b/src/main/java/org/logicng/formulas/CFalse.java
@@ -52,7 +52,7 @@ public boolean evaluate(final Assignment assignment) {
 
     @Override
     public Constant negate() {
-        return f.verum();
+        return this.f.verum();
     }
 
     @Override

diff --git a/src/main/java/org/logicng/formulas/CTrue.java b/src/main/java/org/logicng/formulas/CTrue.java
@@ -52,7 +52,7 @@ public boolean evaluate(final Assignment assignment) {
 
     @Override
     public Constant negate() {
-        return f.falsum();
+        return this.f.falsum();
     }
 
     @Override

diff --git a/src/main/java/org/logicng/formulas/Constant.java b/src/main/java/org/logicng/formulas/Constant.java
@@ -38,7 +38,7 @@
 
 /**
  * Super class for Boolean constants.
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
 public abstract class Constant extends Formula {

diff --git a/src/main/java/org/logicng/formulas/FormulaFunction.java b/src/main/java/org/logicng/formulas/FormulaFunction.java
@@ -31,9 +31,10 @@
 /**
  * A function on a formula.
  * @param <T> the result type of the function
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
+@FunctionalInterface
 public interface FormulaFunction<T> {
 
     /**

diff --git a/src/main/java/org/logicng/formulas/FormulaPredicate.java b/src/main/java/org/logicng/formulas/FormulaPredicate.java
@@ -30,9 +30,10 @@
 
 /**
  * A predicate on a formula.
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
+@FunctionalInterface
 public interface FormulaPredicate {
 
     /**

diff --git a/src/main/java/org/logicng/formulas/FormulaTransformation.java b/src/main/java/org/logicng/formulas/FormulaTransformation.java
@@ -30,9 +30,10 @@
 
 /**
  * A transformation on a formula.
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
+@FunctionalInterface
 public interface FormulaTransformation {
 
     /**

diff --git a/src/main/java/org/logicng/formulas/NAryOperator.java b/src/main/java/org/logicng/formulas/NAryOperator.java
@@ -34,17 +34,18 @@
 import org.logicng.datastructures.Substitution;
 import org.logicng.util.FormulaHelper;
 
-import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.SortedSet;
+import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
 /**
  * Super class for Boolean n-ary operators.
- * @version 1.5.1
+ * @version 2.0.0
  * @since 1.0
  */
 public abstract class NAryOperator extends Formula {
@@ -69,10 +70,7 @@ public long numberOfAtoms() {
         if (this.numberOfAtoms != -1) {
             return this.numberOfAtoms;
         }
-        this.numberOfAtoms = 0;
-        for (final Formula f : this.operands) {
-            this.numberOfAtoms += f.numberOfAtoms();
-        }
+        this.numberOfAtoms = Arrays.stream(this.operands).mapToLong(Formula::numberOfAtoms).sum();
         return this.numberOfAtoms;
     }
 
@@ -81,10 +79,7 @@ public long numberOfNodes() {
         if (this.numberOfNodes != -1) {
             return this.numberOfNodes;
         }
-        this.numberOfNodes = 1;
-        for (final Formula f : this.operands) {
-            this.numberOfNodes += f.numberOfNodes();
-        }
+        this.numberOfNodes = 1 + Arrays.stream(this.operands).mapToLong(Formula::numberOfNodes).sum();
         return this.numberOfNodes;
     }
 
@@ -118,20 +113,12 @@ public SortedSet<Literal> literals() {
 
     @Override
     public boolean containsVariable(final Variable variable) {
-        for (final Formula op : this.operands) {
-            if (op.containsVariable(variable)) {
-                return true;
-            }
-        }
-        return false;
+        return Arrays.stream(this.operands).anyMatch(op -> op.containsVariable(variable));
     }
 
     @Override
     public Formula restrict(final Assignment assignment) {
-        final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-        for (final Formula op : this.operands) {
-            nops.add(op.restrict(assignment));
-        }
+        final LinkedHashSet<Formula> nops = Arrays.stream(this.operands).map(op -> op.restrict(assignment)).collect(Collectors.toCollection(LinkedHashSet::new));
         return this.f.naryOperator(this.type, nops);
     }
 
@@ -141,17 +128,9 @@ public boolean containsNode(final Formula formula) {
             return true;
         }
         if (this.type != formula.type) {
-            for (final Formula op : this.operands) {
-                if (op.containsNode(formula)) {
-                    return true;
-                }
-            }
-            return false;
-        }
-        final List<Formula> fOps = new ArrayList<>(formula.numberOfOperands());
-        for (final Formula op : formula) {
-            fOps.add(op);
+            return Arrays.stream(this.operands).anyMatch(op -> op.containsNode(formula));
         }
+        final List<Formula> fOps = formula.stream().collect(Collectors.toList());
         for (final Formula op : this.operands) {
             fOps.remove(op);
             if (op.containsNode(formula)) {
@@ -163,10 +142,7 @@ public boolean containsNode(final Formula formula) {
 
     @Override
     public Formula substitute(final Substitution substitution) {
-        final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-        for (final Formula op : this.operands) {
-            nops.add(op.substitute(substitution));
-        }
+        final LinkedHashSet<Formula> nops = Arrays.stream(this.operands).map(op -> op.substitute(substitution)).collect(Collectors.toCollection(LinkedHashSet::new));
         return this.f.naryOperator(this.type, nops);
     }
 
@@ -179,10 +155,7 @@ public Formula negate() {
     public Formula nnf() {
         Formula nnf = this.transformationCache.get(NNF);
         if (nnf == null) {
-            final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-            for (final Formula op : this.operands) {
-                nops.add(op.nnf());
-            }
+            final LinkedHashSet<Formula> nops = Arrays.stream(this.operands).map(Formula::nnf).collect(Collectors.toCollection(LinkedHashSet::new));
             nnf = this.f.naryOperator(this.type, nops);
             this.transformationCache.put(NNF, nnf);
         }
@@ -197,9 +170,7 @@ public Formula nnf() {
     protected int hashCode(final int shift) {
         if (this.hashCode == 0) {
             int temp = 1;
-            for (final Formula formula : this.operands) {
-                temp += formula.hashCode();
-            }
+            temp += Arrays.stream(this.operands).mapToInt(Object::hashCode).sum();
             temp *= shift;
             this.hashCode = temp;
         }

diff --git a/src/main/java/org/logicng/formulas/Not.java b/src/main/java/org/logicng/formulas/Not.java
@@ -36,11 +36,12 @@
 import java.util.Collections;
 import java.util.LinkedHashSet;
 import java.util.SortedSet;
+import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
 /**
  * Boolean negation.
- * @version 1.1
+ * @version 2.0.0
  * @since 1.0
  */
 public final class Not extends Formula {
@@ -150,10 +151,7 @@ public Formula nnf() {
             switch (this.operand.type) {
                 case AND:
                 case OR:
-                    final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-                    for (final Formula op : this.operand) {
-                        nops.add(op.negate().nnf());
-                    }
+                    final LinkedHashSet<Formula> nops = this.operand.stream().map(op -> op.negate().nnf()).collect(Collectors.toCollection(LinkedHashSet::new));
                     nnf = this.f.naryOperator(this.operand.type == FType.AND ? FType.OR : FType.AND, nops);
                     break;
                 case IMPL:
@@ -162,8 +160,7 @@ public Formula nnf() {
                     break;
                 case EQUIV:
                     final BinaryOperator equiv = (BinaryOperator) this.operand;
-                    nnf = this.f.and(this.f.or(equiv.left.negate().nnf(), equiv.right.negate().nnf()),
-                            this.f.or(equiv.left.nnf(), equiv.right.nnf()));
+                    nnf = this.f.and(this.f.or(equiv.left.negate().nnf(), equiv.right.negate().nnf()), this.f.or(equiv.left.nnf(), equiv.right.nnf()));
                     break;
                 case PBC:
                     nnf = this.operand.negate().nnf();

diff --git a/src/main/java/org/logicng/formulas/Or.java b/src/main/java/org/logicng/formulas/Or.java
@@ -33,6 +33,7 @@
 
 import org.logicng.datastructures.Assignment;
 
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.LinkedHashSet;
 
@@ -44,7 +45,7 @@
  * - does not contain duplicates
  * - does not contain complementary literals
  * - does not contain constants
- * @version 1.0
+ * @version 2.0.0
  * @since 1.0
  */
 public final class Or extends NAryOperator {
@@ -57,7 +58,7 @@ public final class Or extends NAryOperator {
      * @param f        the factory which created this instance
      * @param isClause is {@code true} if the formula is a clause, {@code false} otherwise
      */
-    Or(final LinkedHashSet<? extends Formula> operands, final FormulaFactory f, boolean isClause) {
+    Or(final LinkedHashSet<? extends Formula> operands, final FormulaFactory f, final boolean isClause) {
         super(FType.OR, operands, f);
         if (isClause) {
             this.setPredicateCacheEntry(IS_CNF, true);
@@ -71,12 +72,7 @@ public final class Or extends NAryOperator {
 
     @Override
     public boolean evaluate(final Assignment assignment) {
-        for (Formula op : operands) {
-            if (op.evaluate(assignment)) {
-                return true;
-            }
-        }
-        return false;
+        return Arrays.stream(this.operands).anyMatch(op -> op.evaluate(assignment));
     }
 
     /**