Merge branch 'development' into feature/ubtree-empty-set

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.4.2-SNAPSHOT</version>
+  <version>2.5.0-SNAPSHOT</version>
   <packaging>bundle</packaging>
 
   <name>LogicNG</name>

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

@@ -88,6 +88,11 @@ public LNGBooleanVector(final boolean... elems) {
         this.size = elems.length;
     }
 
+    LNGBooleanVector(final boolean[] elements, final int size) {
+        this.elements = elements;
+        this.size = size;
+    }
+
     /**
      * Returns whether the vector is empty or not.
      * @return {@code true} if the vector is empty, {@code false} otherwise

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

@@ -88,6 +88,11 @@ public LNGIntVector(final int... elems) {
         this.size = elems.length;
     }
 
+    LNGIntVector(final int[] elements, final int size) {
+        this.elements = elements;
+        this.size = size;
+    }
+
     /**
      * Returns whether the vector is empty or not.
      * @return {@code true} if the vector is empty, {@code false} otherwise

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

@@ -88,6 +88,11 @@ public LNGLongVector(final long... elems) {
         this.size = elems.length;
     }
 
+    LNGLongVector(final long[] elements, final int size) {
+        this.elements = elements;
+        this.size = size;
+    }
+
     /**
      * Returns whether the vector is empty or not.
      * @return {@code true} if the vector is empty, {@code false} otherwise

src/main/java/org/logicng/solvers/MiniSat.java

@@ -75,10 +75,10 @@ public class MiniSat extends SATSolver {
     public enum SolverStyle {MINISAT, GLUCOSE, MINICARD}
 
     protected final MiniSatConfig config;
-    protected final MiniSatStyleSolver solver;
-    protected final CCEncoder ccEncoder;
-    protected final SolverStyle style;
-    protected final LNGIntVector validStates;
+    protected MiniSatStyleSolver solver;
+    protected CCEncoder ccEncoder;
+    protected SolverStyle style;
+    protected LNGIntVector validStates;
     protected final boolean initialPhase;
     protected final boolean incremental;
     protected int nextStateId;
@@ -122,6 +122,36 @@ protected MiniSat(final FormulaFactory f, final SolverStyle solverStyle, final M
         this.fullPgTransformation = new PlaistedGreenbaumTransformationSolver(false, this.underlyingSolver(), this.initialPhase);
     }
 
+    /**
+     * Constructs a new MiniSat solver with a given underlying solver core. This
+     * method is primarily used for serialization purposes and should not be
+     * required in any other application use case.
+     * @param f                the formula factory
+     * @param underlyingSolver the underlying solver core
+     */
+    public MiniSat(final FormulaFactory f, final MiniSatStyleSolver underlyingSolver) {
+        super(f);
+        this.config = underlyingSolver.getConfig();
+        if (underlyingSolver instanceof MiniSat2Solver) {
+            this.style = SolverStyle.MINISAT;
+        } else if (underlyingSolver instanceof MiniCard) {
+            this.style = SolverStyle.MINICARD;
+        } else if (underlyingSolver instanceof GlucoseSyrup) {
+            this.style = SolverStyle.GLUCOSE;
+        } else {
+            throw new IllegalArgumentException("Unknown solver type: " + underlyingSolver.getClass());
+        }
+        this.initialPhase = underlyingSolver.getConfig().initialPhase();
+        this.solver = underlyingSolver;
+        this.result = UNDEF;
+        this.incremental = underlyingSolver.getConfig().incremental();
+        this.validStates = new LNGIntVector();
+        this.nextStateId = 0;
+        this.ccEncoder = new CCEncoder(f);
+        this.pgTransformation = new PlaistedGreenbaumTransformationSolver(true, underlyingSolver, this.initialPhase);
+        this.fullPgTransformation = new PlaistedGreenbaumTransformationSolver(false, underlyingSolver, this.initialPhase);
+    }
+
     /**
      * Returns a new MiniSat solver with the MiniSat configuration from the formula factory.
      * @param f the formula factory

src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java

@@ -104,6 +104,16 @@ public LNGBoundedIntQueue() {
         this.queueSize = 0;
     }
 
+    LNGBoundedIntQueue(final LNGIntVector elems, final int first, final int last, final long sumOfQueue,
+                       final int maxSize, final int queueSize) {
+        this.elems = elems;
+        this.first = first;
+        this.last = last;
+        this.sumOfQueue = sumOfQueue;
+        this.maxSize = maxSize;
+        this.queueSize = queueSize;
+    }
+
     /**
      * Initializes the size of this queue.
      * @param size the size
@@ -154,6 +164,30 @@ private void growTo(final int size) {
         this.last = 0;
     }
 
+    LNGIntVector getElems() {
+        return this.elems;
+    }
+
+    int getFirst() {
+        return this.first;
+    }
+
+    int getLast() {
+        return this.last;
+    }
+
+    long getSumOfQueue() {
+        return this.sumOfQueue;
+    }
+
+    int getMaxSize() {
+        return this.maxSize;
+    }
+
+    int getQueueSize() {
+        return this.queueSize;
+    }
+
     @Override
     public String toString() {
         return String.format("LNGBoundedIntQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}",

src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java

@@ -104,6 +104,16 @@ public LNGBoundedLongQueue() {
         this.queueSize = 0;
     }
 
+    LNGBoundedLongQueue(final LNGLongVector elems, final int first, final int last, final long sumOfQueue,
+                        final int maxSize, final int queueSize) {
+        this.elems = elems;
+        this.first = first;
+        this.last = last;
+        this.sumOfQueue = sumOfQueue;
+        this.maxSize = maxSize;
+        this.queueSize = queueSize;
+    }
+
     /**
      * Initializes the size of this queue.
      * @param size the size
@@ -172,6 +182,30 @@ public void fastClear() {
         this.sumOfQueue = 0;
     }
 
+    LNGLongVector getElems() {
+        return this.elems;
+    }
+
+    int getFirst() {
+        return this.first;
+    }
+
+    int getLast() {
+        return this.last;
+    }
+
+    long getSumOfQueue() {
+        return this.sumOfQueue;
+    }
+
+    int getMaxSize() {
+        return this.maxSize;
+    }
+
+    int getQueueSize() {
+        return this.queueSize;
+    }
+
     @Override
     public String toString() {
         return String.format("LNGBoundedLongQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}",

src/main/java/org/logicng/solvers/datastructures/LNGHeap.java

@@ -69,6 +69,12 @@ public LNGHeap(final MiniSatStyleSolver solver) {
         this.indices = new LNGIntVector(1000);
     }
 
+    LNGHeap(final MiniSatStyleSolver s, final LNGIntVector heap, final LNGIntVector indices) {
+        this.s = s;
+        this.heap = heap;
+        this.indices = indices;
+    }
+
     /**
      * Returns the left position on the heap for a given position.
      * @param pos the position
@@ -252,6 +258,14 @@ private void percolateDown(final int pos) {
         this.indices.set(y, p);
     }
 
+    LNGIntVector getHeap() {
+        return this.heap;
+    }
+
+    LNGIntVector getIndices() {
+        return this.indices;
+    }
+
     @Override
     public String toString() {
         final StringBuilder sb = new StringBuilder("LNGHeap{");

src/main/java/org/logicng/solvers/datastructures/MSClause.java

@@ -123,6 +123,21 @@ public MSClause(final LNGIntVector ps, final boolean learnt, final boolean isAtM
         this.atMostWatchers = -1;
     }
 
+    MSClause(final LNGIntVector data, final boolean learnt, final boolean isAtMost, final double activity,
+             final int szWithoutSelectors, final boolean seen, final long lbd, final boolean canBeDel,
+             final boolean oneWatched, final int atMostWatchers) {
+        this.data = data;
+        this.learnt = learnt;
+        this.isAtMost = isAtMost;
+        this.activity = activity;
+        this.szWithoutSelectors = szWithoutSelectors;
+        this.seen = seen;
+        this.lbd = lbd;
+        this.canBeDel = canBeDel;
+        this.oneWatched = oneWatched;
+        this.atMostWatchers = atMostWatchers;
+    }
+
     /**
      * Returns the size (number of literals) of this clause.
      * @return the size
@@ -301,6 +316,10 @@ public int cardinality() {
         return this.data.size() - this.atMostWatchers + 1;
     }
 
+    LNGIntVector getData() {
+        return this.data;
+    }
+
     @Override
     public int hashCode() {
         return this.data.hashCode();

src/main/java/org/logicng/solvers/datastructures/MSVariable.java

@@ -74,6 +74,16 @@ public MSVariable(final boolean polarity) {
         this.decision = false;
     }
 
+    MSVariable(final Tristate assignment, final int level, final MSClause reason, final double activity,
+               final boolean polarity, final boolean decision) {
+        this.assignment = assignment;
+        this.level = level;
+        this.reason = reason;
+        this.activity = activity;
+        this.polarity = polarity;
+        this.decision = decision;
+    }
+
     /**
      * Sets the decision level of this variable.
      * @param level the decision level

src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java

@@ -516,14 +516,14 @@ protected MSClause propagate() {
     }
 
     @Override
-    protected boolean litRedundant(final int p, final int abstractLevels) {
-        this.analyzeStack.clear();
-        this.analyzeStack.push(p);
-        final int top = this.analyzeToClear.size();
-        while (this.analyzeStack.size() > 0) {
-            assert v(this.analyzeStack.back()).reason() != null;
-            final MSClause c = v(this.analyzeStack.back()).reason();
-            this.analyzeStack.pop();
+    protected boolean litRedundant(final int p, final int abstractLevels, final LNGIntVector analyzeToClear) {
+        final LNGIntVector analyzeStack = new LNGIntVector();
+        analyzeStack.push(p);
+        final int top = analyzeToClear.size();
+        while (analyzeStack.size() > 0) {
+            assert v(analyzeStack.back()).reason() != null;
+            final MSClause c = v(analyzeStack.back()).reason();
+            analyzeStack.pop();
             if (c.size() == 2 && value(c.get(0)) == Tristate.FALSE) {
                 assert value(c.get(1)) == Tristate.TRUE;
                 final int tmp = c.get(0);
@@ -535,13 +535,13 @@ protected boolean litRedundant(final int p, final int abstractLevels) {
                 if (!this.seen.get(var(q)) && v(q).level() > 0) {
                     if (v(q).reason() != null && (abstractLevel(var(q)) & abstractLevels) != 0) {
                         this.seen.set(var(q), true);
-                        this.analyzeStack.push(q);
-                        this.analyzeToClear.push(q);
+                        analyzeStack.push(q);
+                        analyzeToClear.push(q);
                     } else {
-                        for (int j = top; j < this.analyzeToClear.size(); j++) {
-                            this.seen.set(var(this.analyzeToClear.get(j)), false);
+                        for (int j = top; j < analyzeToClear.size(); j++) {
+                            this.seen.set(var(analyzeToClear.get(j)), false);
                         }
-                        this.analyzeToClear.removeElements(this.analyzeToClear.size() - top);
+                        analyzeToClear.removeElements(analyzeToClear.size() - top);
                         return false;
                     }
                 }
@@ -985,14 +985,14 @@ protected void simplifyClause(final LNGIntVector outLearnt, final LNGIntVector s
         for (i = 0; i < selectors.size(); i++) {
             outLearnt.push(selectors.get(i));
         }
-        this.analyzeToClear = new LNGIntVector(outLearnt);
+        final LNGIntVector analyzeToClear = new LNGIntVector(outLearnt);
         if (this.ccminMode == MiniSatConfig.ClauseMinimization.DEEP) {
             int abstractLevel = 0;
             for (i = 1; i < outLearnt.size(); i++) {
                 abstractLevel |= abstractLevel(var(outLearnt.get(i)));
             }
             for (i = j = 1; i < outLearnt.size(); i++) {
-                if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel)) {
+                if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel, analyzeToClear)) {
                     outLearnt.set(j++, outLearnt.get(i));
                 }
             }
@@ -1052,8 +1052,8 @@ protected void simplifyClause(final LNGIntVector outLearnt, final LNGIntVector s
             }
             this.lastDecisionLevel.clear();
         }
-        for (int m = 0; m < this.analyzeToClear.size(); m++) {
-            this.seen.set(var(this.analyzeToClear.get(m)), false);
+        for (int m = 0; m < analyzeToClear.size(); m++) {
+            this.seen.set(var(analyzeToClear.get(m)), false);
         }
         for (int m = 0; m < selectors.size(); m++) {
             this.seen.set(var(selectors.get(m)), false);
@@ -1073,4 +1073,3 @@ protected boolean isRotatable(final int lit) {
         return true;
     }
 }
-