replace Assignment with Model in several places

src/main/java/com/booleworks/logicng/datastructures/Assignment.java

@@ -9,10 +9,8 @@
 import com.booleworks.logicng.formulas.Literal;
 import com.booleworks.logicng.formulas.Variable;
 
-import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
-import java.util.List;
 import java.util.Objects;
 import java.util.SortedSet;
 import java.util.TreeSet;
@@ -31,7 +29,6 @@
  * @version 3.0.0
  * @since 1.0
  */
-
 public final class Assignment {
 
     private final SortedSet<Variable> pos = new TreeSet<>();
@@ -187,47 +184,6 @@ public Model model() {
         return new Model(this);
     }
 
-    /**
-     * Creates the blocking clause for this assignment.
-     * @param f the formula factory
-     * @return the blocking clause for this assignment
-     */
-    public Formula blockingClause(final FormulaFactory f) {
-        final List<Literal> ops = new ArrayList<>();
-        for (final Literal lit : pos) {
-            ops.add(lit.negate(f));
-        }
-        for (final Literal lit : neg) {
-            ops.add(lit.negate(f));
-        }
-        return f.or(ops);
-    }
-
-    /**
-     * Creates the blocking clause for this assignment wrt. a given set of
-     * literals. If the set is {@code null}, all literals are considered
-     * relevant.
-     * @param f        the formula factory
-     * @param literals the set of literals
-     * @return the blocking clause for this assignment
-     */
-    public Formula blockingClause(final FormulaFactory f, final Collection<? extends Literal> literals) {
-        if (literals == null) {
-            return blockingClause(f);
-        }
-        final List<Literal> ops = new ArrayList<>();
-        for (final Literal lit : literals) {
-            final Variable var = lit.variable();
-            final Literal negatedVar = var.negate(f);
-            if (pos.contains(var)) {
-                ops.add(negatedVar);
-            } else if (neg.contains(negatedVar)) {
-                ops.add(var);
-            }
-        }
-        return f.or(ops);
-    }
-
     @Override
     public int hashCode() {
         return Objects.hash(pos, neg);

src/main/java/com/booleworks/logicng/datastructures/Model.java

@@ -11,9 +11,12 @@
 
 import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.Collection;
 import java.util.Collections;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Objects;
+import java.util.Set;
 import java.util.SortedSet;
 import java.util.TreeSet;
 
@@ -136,6 +139,43 @@ public SortedSet<Variable> negativeVariables() {
         return set;
     }
 
+    /**
+     * Creates the blocking clause for this model.
+     * @param f the formula factory
+     * @return the blocking clause for this model
+     */
+    public Formula blockingClause(final FormulaFactory f) {
+        final List<Literal> ops = new ArrayList<>();
+        for (final Literal lit : literals) {
+            ops.add(lit.negate(f));
+        }
+        return f.or(ops);
+    }
+
+    /**
+     * Creates the blocking clause for this model wrt. a given set of
+     * literals. If the set is {@code null}, all literals are considered
+     * relevant.
+     * @param f        the formula factory
+     * @param literals the set of literals
+     * @return the blocking clause for this model
+     */
+    public Formula blockingClause(final FormulaFactory f, final Collection<? extends Literal> literals) {
+        if (literals == null) {
+            return blockingClause(f);
+        }
+        final Set<Literal> myLiterals = new HashSet<>(this.literals);
+        final List<Literal> ops = new ArrayList<>();
+        for (final Literal lit : literals) {
+            if (myLiterals.contains(lit)) {
+                ops.add(lit.negate(f));
+            } else if (myLiterals.contains(lit.negate(f))) {
+                ops.add(lit);
+            }
+        }
+        return f.or(ops);
+    }
+
     @Override
     public boolean equals(final Object o) {
         if (this == o) {

src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java

@@ -6,7 +6,7 @@
 
 import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.SMUS_COMPUTATION_STARTED;
 
-import com.booleworks.logicng.datastructures.Assignment;
+import com.booleworks.logicng.datastructures.Model;
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Variable;
@@ -158,7 +158,7 @@ public static LNGResult<List<Formula>> computeSmusForFormulas(
     private static LNGResult<SortedSet<Variable>> minimumHs(final SATSolver hSolver,
                                                             final Set<Variable> variables,
                                                             final ComputationHandler handler) {
-        final LNGResult<Assignment> minimumHsModel = hSolver.execute(OptimizationFunction.builder()
+        final LNGResult<Model> minimumHsModel = hSolver.execute(OptimizationFunction.builder()
                 .literals(variables)
                 .minimize().build(), handler);
         if (!minimumHsModel.isSuccess()) {
@@ -176,7 +176,7 @@ private static LNGResult<SortedSet<Variable>> grow(final SATSolver growSolver, f
         if (!growSolver.sat()) {
             return null;
         }
-        final LNGResult<Assignment> maxModel = growSolver.execute(OptimizationFunction.builder()
+        final LNGResult<Model> maxModel = growSolver.execute(OptimizationFunction.builder()
                 .literals(variables)
                 .maximize().build(), handler);
         if (!maxModel.isSuccess()) {

src/main/java/com/booleworks/logicng/functions/MinimumPrimeImplicantFunction.java

@@ -4,7 +4,7 @@
 
 package com.booleworks.logicng.functions;
 
-import com.booleworks.logicng.datastructures.Assignment;
+import com.booleworks.logicng.datastructures.Model;
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.FormulaFunction;
@@ -62,7 +62,7 @@ public LNGResult<SortedSet<Literal>> apply(final Formula formula, final Computat
             throw new IllegalArgumentException("The given formula must be satisfiable");
         }
 
-        final LNGResult<Assignment> minimumModel =
+        final LNGResult<Model> minimumModel =
                 solver.execute(OptimizationFunction.minimize(newVar2oldLit.keySet()), handler);
         if (!minimumModel.isSuccess()) {
             return LNGResult.canceled(minimumModel.getCancelCause());

src/main/java/com/booleworks/logicng/handlers/events/OptimizationFoundBetterBoundEvent.java

@@ -1,6 +1,6 @@
 package com.booleworks.logicng.handlers.events;
 
-import com.booleworks.logicng.datastructures.Assignment;
+import com.booleworks.logicng.datastructures.Model;
 import com.booleworks.logicng.solvers.functions.OptimizationFunction;
 
 import java.util.function.Supplier;
@@ -13,21 +13,21 @@
  */
 public class OptimizationFoundBetterBoundEvent implements LNGEvent {
 
-    private final Supplier<Assignment> model;
+    private final Supplier<Model> model;
 
     /**
      * Creates a new event including a supplier to get the latest model.
      * @param model the latest model
      */
-    public OptimizationFoundBetterBoundEvent(final Supplier<Assignment> model) {
+    public OptimizationFoundBetterBoundEvent(final Supplier<Model> model) {
         this.model = model;
     }
 
     /**
      * Returns the supplier for the latest model.
      * @return the supplier for the latest model
      */
-    public Supplier<Assignment> getModel() {
+    public Supplier<Model> getModel() {
         return model;
     }
 

src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDD.java

@@ -4,7 +4,6 @@
 
 package com.booleworks.logicng.knowledgecompilation.bdds;
 
-import com.booleworks.logicng.datastructures.Assignment;
 import com.booleworks.logicng.datastructures.Model;
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
@@ -114,7 +113,7 @@ public Formula toFormula(final FormulaFactory f) {
      * formula. If {@code followPathsToTrue} is deactivated, the paths leading
      * to the {@code false} terminal are followed to generate the formula and
      * the resulting formula is negated. Depending on the formula and the number
-     * of satisfying assignments, the generated formula can be more compact
+     * of satisfying models, the generated formula can be more compact
      * using the {@code true} paths or {@code false} paths, respectively.
      * @param followPathsToTrue the extraction style
      * @return the formula for this BDD
@@ -130,7 +129,7 @@ public Formula toFormula(final boolean followPathsToTrue) {
      * formula. If {@code followPathsToTrue} is deactivated, the paths leading
      * to the {@code false} terminal are followed to generate the formula and
      * the resulting formula is negated. Depending on the formula and the number
-     * of satisfying assignments, the generated formula can be more compact
+     * of satisfying models, the generated formula can be more compact
      * using the {@code true} paths or {@code false} paths, respectively.
      * @param f                 the formula factory to generate new formulas
      * @param followPathsToTrue the extraction style
@@ -407,17 +406,17 @@ public BDD forall(final Variable... variables) {
      * Returns an arbitrary model of this BDD or {@code null} if there is none.
      * @return an arbitrary model of this BDD
      */
-    public Assignment model() {
-        return createAssignment(kernel.factory(), operations.satOne(index));
+    public Model model() {
+        return createModel(kernel.factory(), operations.satOne(index));
     }
 
     /**
      * Returns an arbitrary model of this BDD or {@code null} if there is none.
      * @param f the formula factory to generate new formulas
      * @return an arbitrary model of this BDD
      */
-    public Assignment model(final FormulaFactory f) {
-        return createAssignment(f, operations.satOne(index));
+    public Model model(final FormulaFactory f) {
+        return createModel(f, operations.satOne(index));
     }
 
     /**
@@ -429,7 +428,7 @@ public Assignment model(final FormulaFactory f) {
      *                     model
      * @return an arbitrary model of this BDD
      */
-    public Assignment model(final boolean defaultValue, final Collection<Variable> variables) {
+    public Model model(final boolean defaultValue, final Collection<Variable> variables) {
         return model(kernel.factory(), defaultValue, variables);
     }
 
@@ -443,11 +442,11 @@ public Assignment model(final boolean defaultValue, final Collection<Variable> v
      *                     model
      * @return an arbitrary model of this BDD
      */
-    public Assignment model(final FormulaFactory f, final boolean defaultValue, final Collection<Variable> variables) {
+    public Model model(final FormulaFactory f, final boolean defaultValue, final Collection<Variable> variables) {
         final int varBDD = BDDFactory.build(variables, kernel).index;
         final int pol = defaultValue ? BDDKernel.BDD_TRUE : BDDKernel.BDD_FALSE;
         final int modelBDD = operations.satOneSet(index, varBDD, pol);
-        return createAssignment(f, modelBDD);
+        return createModel(f, modelBDD);
     }
 
     /**
@@ -459,7 +458,7 @@ public Assignment model(final FormulaFactory f, final boolean defaultValue, fina
      *                     model
      * @return an arbitrary model of this BDD
      */
-    public Assignment model(final boolean defaultValue, final Variable... variables) {
+    public Model model(final boolean defaultValue, final Variable... variables) {
         return model(kernel.factory(), defaultValue, Arrays.asList(variables));
     }
 
@@ -473,15 +472,15 @@ public Assignment model(final boolean defaultValue, final Variable... variables)
      *                     model
      * @return an arbitrary model of this BDD
      */
-    public Assignment model(final FormulaFactory f, final boolean defaultValue, final Variable... variables) {
+    public Model model(final FormulaFactory f, final boolean defaultValue, final Variable... variables) {
         return model(f, defaultValue, Arrays.asList(variables));
     }
 
     /**
      * Returns a full model of this BDD or {@code null} if there is none.
      * @return a full model of this BDD
      */
-    public Assignment fullModel() {
+    public Model fullModel() {
         return fullModel(kernel.factory());
     }
 
@@ -490,8 +489,8 @@ public Assignment fullModel() {
      * @param f the formula factory to generate new formulas
      * @return a full model of this BDD
      */
-    public Assignment fullModel(final FormulaFactory f) {
-        return createAssignment(f, operations.fullSatOne(index));
+    public Model fullModel(final FormulaFactory f) {
+        return createModel(f, operations.fullSatOne(index));
     }
 
     /**
@@ -517,9 +516,9 @@ public BigInteger pathCountZero() {
     public SortedSet<Variable> support() {
         final int supportBDD = operations.support(index);
         // only variables, cannot create new literals
-        final Assignment assignment = createAssignment(kernel.factory(), supportBDD);
-        assert assignment == null || assignment.negativeLiterals().isEmpty();
-        return assignment == null ? Collections.emptySortedSet() : new TreeSet<>(assignment.positiveVariables());
+        final Model model = createModel(kernel.factory(), supportBDD);
+        assert model == null || model.negativeLiterals().isEmpty();
+        return model == null ? Collections.emptySortedSet() : new TreeSet<>(model.positiveVariables());
     }
 
     /**
@@ -590,33 +589,33 @@ public BDDNode toLngBdd() {
     }
 
     /**
-     * Creates an assignment from a BDD.
+     * Creates an model from a BDD.
      * @param f        the formula factory to generate new formulas
      * @param modelBDD the BDD
-     * @return the assignment
+     * @return the model
      * @throws IllegalStateException if the BDD does not represent a unique
      *                               model
      */
-    private Assignment createAssignment(final FormulaFactory f, final int modelBDD) {
+    private Model createModel(final FormulaFactory f, final int modelBDD) {
         if (modelBDD == BDDKernel.BDD_FALSE) {
             return null;
         }
         if (modelBDD == BDDKernel.BDD_TRUE) {
-            return new Assignment();
+            return new Model();
         }
         final List<int[]> nodes = operations.allNodes(modelBDD);
-        final Assignment assignment = new Assignment();
+        final List<Literal> model = new ArrayList<>();
         for (final int[] node : nodes) {
             final Variable variable = kernel.getVariableForIndex(node[1]);
             if (node[2] == BDDKernel.BDD_FALSE) {
-                assignment.addLiteral(variable);
+                model.add(variable);
             } else if (node[3] == BDDKernel.BDD_FALSE) {
-                assignment.addLiteral(variable.negate(f));
+                model.add(variable.negate(f));
             } else {
                 throw new IllegalStateException("Expected that the model BDD has one unique path through the BDD.");
             }
         }
-        return assignment;
+        return new Model(model);
     }
 
     @Override

src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java

@@ -16,6 +16,7 @@
 import com.booleworks.logicng.util.FormulaHelper;
 
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.List;
 import java.util.SortedSet;
 import java.util.TreeSet;
@@ -67,7 +68,7 @@ public SortedSet<Literal> reduceImplicant(final SortedSet<Literal> implicant) {
      * @return a prime implicant or null if the computation was canceled by the
      *         handler
      */
-    public LNGResult<SortedSet<Literal>> reduceImplicant(final SortedSet<Literal> implicant,
+    public LNGResult<SortedSet<Literal>> reduceImplicant(final Collection<Literal> implicant,
                                                          final ComputationHandler handler) {
         handler.shouldResume(ComputationStartedEvent.IMPLICATE_REDUCTION_STARTED);
         final SortedSet<Literal> primeImplicant = new TreeSet<>(implicant);