formula helper for variables() and literals() of multiple formuals

logic-ng · Apr 11, 2019 · 9bc4a74 · 9bc4a74
1 parent 284b3aa
commit 9bc4a74
Show file tree

Hide file tree

Showing 6 changed files with 65 additions and 44 deletions.
diff --git a/src/main/java/org/logicng/backbones/BackboneGeneration.java b/src/main/java/org/logicng/backbones/BackboneGeneration.java
@@ -30,6 +30,7 @@
 
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.Variable;
+import org.logicng.util.FormulaHelper;
 
 import java.util.Collection;
 import java.util.Collections;
@@ -57,14 +58,6 @@ private BackboneGeneration() {
         // Intentionally left empty.
     }
 
-    private static SortedSet<Variable> allVariablesInFormulas(final Collection<Formula> formulas) {
-        final SortedSet<Variable> variables = new TreeSet<>();
-        for (final Formula formula : formulas) {
-            variables.addAll(formula.variables());
-        }
-        return variables;
-    }
-
     /**
      * Sets a new backbone configuration.
      * @param config the new backbone configuration
@@ -103,7 +96,7 @@ public static Backbone compute(final Collection<Formula> formulas, final Collect
      * @return the backbone or {@code null} if the formula is UNSAT
      */
     public static Backbone compute(final Collection<Formula> formulas, final BackboneType type) {
-        return compute(formulas, allVariablesInFormulas(formulas), type);
+        return compute(formulas, FormulaHelper.variables(formulas), type);
     }
 
     /**
@@ -112,7 +105,7 @@ public static Backbone compute(final Collection<Formula> formulas, final Backbon
      * @return the backbone or {@code null} if the formula is UNSAT
      */
     public static Backbone compute(final Collection<Formula> formulas) {
-        return compute(formulas, allVariablesInFormulas(formulas), BackboneType.POSITIVE_AND_NEGATIVE);
+        return compute(formulas, FormulaHelper.variables(formulas), BackboneType.POSITIVE_AND_NEGATIVE);
     }
 
     /**
@@ -171,7 +164,7 @@ public static Backbone computePositive(final Collection<Formula> formulas, final
      * @return the positive backbone or {@code null} if the formula is UNSAT
      */
     public static Backbone computePositive(final Collection<Formula> formulas) {
-        return compute(formulas, allVariablesInFormulas(formulas), BackboneType.ONLY_POSITIVE);
+        return compute(formulas, FormulaHelper.variables(formulas), BackboneType.ONLY_POSITIVE);
     }
 
     /**
@@ -209,7 +202,7 @@ public static Backbone computeNegative(final Collection<Formula> formulas, final
      * @return the negative backbone or {@code null} if the formula is UNSAT
      */
     public static Backbone computeNegative(final Collection<Formula> formulas) {
-        return compute(formulas, allVariablesInFormulas(formulas), BackboneType.ONLY_NEGATIVE);
+        return compute(formulas, FormulaHelper.variables(formulas), BackboneType.ONLY_NEGATIVE);
     }
 
     /**

diff --git a/src/main/java/org/logicng/collections/ImmutableFormulaList.java b/src/main/java/org/logicng/collections/ImmutableFormulaList.java
@@ -36,6 +36,7 @@
 import org.logicng.formulas.Variable;
 import org.logicng.functions.LiteralProfileFunction;
 import org.logicng.functions.VariableProfileFunction;
+import org.logicng.util.FormulaHelper;
 
 import java.util.Arrays;
 import java.util.Collection;
@@ -211,9 +212,7 @@ public boolean containsFormula(final Formula formula) {
    */
   public SortedSet<Variable> variables() {
     if (this.variables == null) {
-      this.variables = new TreeSet<>();
-      for (final Formula f : this.formulas)
-        this.variables.addAll(f.variables());
+      this.variables = FormulaHelper.variables(formulas);
     }
     return this.variables;
   }
@@ -223,10 +222,7 @@ public SortedSet<Variable> variables() {
    * @return all literals occurring in this formula list
    */
   public SortedSet<Literal> literals() {
-    final SortedSet<Literal> literals = new TreeSet<>();
-    for (final Formula f : this.formulas)
-      literals.addAll(f.literals());
-    return literals;
+    return FormulaHelper.literals(formulas);
   }
 
   /**

diff --git a/src/main/java/org/logicng/formulas/BinaryOperator.java b/src/main/java/org/logicng/formulas/BinaryOperator.java
@@ -29,6 +29,7 @@
 package org.logicng.formulas;
 
 import org.logicng.datastructures.Substitution;
+import org.logicng.util.FormulaHelper;
 
 import java.util.Collections;
 import java.util.Iterator;
@@ -113,20 +114,14 @@ public boolean isAtomicFormula() {
   @Override
   public SortedSet<Variable> variables() {
     if (this.variables == null) {
-      final SortedSet<Variable> set = new TreeSet<>();
-      set.addAll(this.left.variables());
-      set.addAll(this.right.variables());
-      this.variables = Collections.unmodifiableSortedSet(set);
+      this.variables = Collections.unmodifiableSortedSet(FormulaHelper.variables(left, right));
     }
     return this.variables;
   }
 
   @Override
   public SortedSet<Literal> literals() {
-    final SortedSet<Literal> set = new TreeSet<>();
-    set.addAll(this.left.literals());
-    set.addAll(this.right.literals());
-    return Collections.unmodifiableSortedSet(set);
+    return Collections.unmodifiableSortedSet(FormulaHelper.literals(left, right));
   }
 
   @Override

diff --git a/src/main/java/org/logicng/formulas/NAryOperator.java b/src/main/java/org/logicng/formulas/NAryOperator.java
@@ -30,6 +30,7 @@
 
 import org.logicng.datastructures.Assignment;
 import org.logicng.datastructures.Substitution;
+import org.logicng.util.FormulaHelper;
 
 import java.util.ArrayList;
 import java.util.Collection;
@@ -107,22 +108,14 @@ public boolean isAtomicFormula() {
   @Override
   public SortedSet<Variable> variables() {
     if (this.variables == null) {
-      final SortedSet<Variable> set = new TreeSet<>();
-      for (final Formula op : this.operands) {
-        set.addAll(op.variables());
-      }
-      this.variables = Collections.unmodifiableSortedSet(set);
+      this.variables = Collections.unmodifiableSortedSet(FormulaHelper.variables(operands));
     }
     return this.variables;
   }
 
   @Override
   public SortedSet<Literal> literals() {
-    final SortedSet<Literal> set = new TreeSet<>();
-    for (final Formula op : this.operands) {
-      set.addAll(op.literals());
-    }
-    return Collections.unmodifiableSortedSet(set);
+    return Collections.unmodifiableSortedSet(FormulaHelper.literals(operands));
   }
 
   @Override

diff --git a/src/main/java/org/logicng/formulas/PBConstraint.java b/src/main/java/org/logicng/formulas/PBConstraint.java
@@ -34,6 +34,7 @@
 import org.logicng.datastructures.Assignment;
 import org.logicng.datastructures.Substitution;
 import org.logicng.datastructures.Tristate;
+import org.logicng.util.FormulaHelper;
 import org.logicng.util.Pair;
 
 import java.util.Arrays;
@@ -418,19 +419,14 @@ public boolean isAtomicFormula() {
   @Override
   public SortedSet<Variable> variables() {
     if (this.variables == null) {
-      this.variables = new TreeSet<>();
-      for (final Literal lit : this.literals)
-        this.variables.add(lit.variable());
-      this.variables = Collections.unmodifiableSortedSet(this.variables);
+      this.variables = Collections.unmodifiableSortedSet(FormulaHelper.variables(literals));
     }
     return this.variables;
   }
 
   @Override
   public SortedSet<Literal> literals() {
-    final SortedSet<Literal> lits = new TreeSet<>();
-    Collections.addAll(lits, this.literals);
-    return Collections.unmodifiableSortedSet(lits);
+    return Collections.unmodifiableSortedSet(FormulaHelper.literals(literals));
   }
 
   @Override

diff --git a/src/main/java/org/logicng/util/FormulaHelper.java b/src/main/java/org/logicng/util/FormulaHelper.java
@@ -0,0 +1,48 @@
+package org.logicng.util;
+
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Literal;
+import org.logicng.formulas.Variable;
+
+import java.util.Collection;
+import java.util.SortedSet;
+import java.util.TreeSet;
+
+public class FormulaHelper {
+
+    private FormulaHelper() {
+        // Intentionally left empty
+    }
+
+    public static SortedSet<Variable> variables(Formula... formulas) {
+        SortedSet<Variable> variables = new TreeSet<>();
+        for (Formula f : formulas) {
+            variables.addAll(f.variables());
+        }
+        return variables;
+    }
+
+    public static SortedSet<Variable> variables(Collection<? extends Formula> formulas) {
+        SortedSet<Variable> variables = new TreeSet<>();
+        for (Formula f : formulas) {
+            variables.addAll(f.variables());
+        }
+        return variables;
+    }
+
+    public static SortedSet<Literal> literals(Formula... formulas) {
+        SortedSet<Literal> literals = new TreeSet<>();
+        for (Formula f : formulas) {
+            literals.addAll(f.literals());
+        }
+        return literals;
+    }
+
+    public static SortedSet<Literal> literals(Collection<? extends Formula> formulas) {
+        SortedSet<Literal> literals = new TreeSet<>();
+        for (Formula f : formulas) {
+            literals.addAll(f.literals());
+        }
+        return literals;
+    }
+}