Preparations for formula and solver serializiation

logic-ng · May 4, 2024 · b6e6975 · b6e6975
1 parent 10ab16e
commit b6e6975
Show file tree

Hide file tree

Showing 10 changed files with 162 additions and 29 deletions.
diff --git a/src/main/java/org/logicng/collections/LNGBooleanVector.java b/src/main/java/org/logicng/collections/LNGBooleanVector.java
@@ -88,7 +88,12 @@ public LNGBooleanVector(final boolean... elems) {
         this.size = elems.length;
     }
 
-    LNGBooleanVector(final boolean[] elements, final int size) {
+    /**
+     * Creates a vector with the given elements and capacity.
+     * @param elements the elements
+     * @param size     the capacity of the vector
+     */
+    public LNGBooleanVector(final boolean[] elements, final int size) {
         this.elements = elements;
         this.size = size;
     }

diff --git a/src/main/java/org/logicng/collections/LNGIntVector.java b/src/main/java/org/logicng/collections/LNGIntVector.java
@@ -88,7 +88,12 @@ public LNGIntVector(final int... elems) {
         this.size = elems.length;
     }
 
-    LNGIntVector(final int[] elements, final int size) {
+    /**
+     * Creates a vector with the given elements and capacity.
+     * @param elements the elements
+     * @param size     the capacity of the vector
+     */
+    public LNGIntVector(final int[] elements, final int size) {
         this.elements = elements;
         this.size = size;
     }

diff --git a/src/main/java/org/logicng/collections/LNGLongVector.java b/src/main/java/org/logicng/collections/LNGLongVector.java
@@ -88,7 +88,12 @@ public LNGLongVector(final long... elems) {
         this.size = elems.length;
     }
 
-    LNGLongVector(final long[] elements, final int size) {
+    /**
+     * Creates a vector with the given elements and capacity.
+     * @param elements the elements
+     * @param size     the capacity of the vector
+     */
+    public LNGLongVector(final long[] elements, final int size) {
         this.elements = elements;
         this.size = size;
     }

diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java
@@ -104,8 +104,8 @@ public LNGBoundedIntQueue() {
         this.queueSize = 0;
     }
 
-    LNGBoundedIntQueue(final LNGIntVector elems, final int first, final int last, final long sumOfQueue,
-                       final int maxSize, final int queueSize) {
+    public 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;
@@ -164,27 +164,27 @@ private void growTo(final int size) {
         this.last = 0;
     }
 
-    LNGIntVector getElems() {
+    public LNGIntVector getElems() {
         return this.elems;
     }
 
-    int getFirst() {
+    public int getFirst() {
         return this.first;
     }
 
-    int getLast() {
+    public int getLast() {
         return this.last;
     }
 
-    long getSumOfQueue() {
+    public long getSumOfQueue() {
         return this.sumOfQueue;
     }
 
-    int getMaxSize() {
+    public int getMaxSize() {
         return this.maxSize;
     }
 
-    int getQueueSize() {
+    public int getQueueSize() {
         return this.queueSize;
     }
 

diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java
@@ -104,8 +104,8 @@ public LNGBoundedLongQueue() {
         this.queueSize = 0;
     }
 
-    LNGBoundedLongQueue(final LNGLongVector elems, final int first, final int last, final long sumOfQueue,
-                        final int maxSize, final int queueSize) {
+    public 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;
@@ -182,27 +182,27 @@ public void fastClear() {
         this.sumOfQueue = 0;
     }
 
-    LNGLongVector getElems() {
+    public LNGLongVector getElems() {
         return this.elems;
     }
 
-    int getFirst() {
+    public int getFirst() {
         return this.first;
     }
 
-    int getLast() {
+    public int getLast() {
         return this.last;
     }
 
-    long getSumOfQueue() {
+    public long getSumOfQueue() {
         return this.sumOfQueue;
     }
 
-    int getMaxSize() {
+    public int getMaxSize() {
         return this.maxSize;
     }
 
-    int getQueueSize() {
+    public int getQueueSize() {
         return this.queueSize;
     }
 

diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java
@@ -69,8 +69,14 @@ public LNGHeap(final MiniSatStyleSolver solver) {
         this.indices = new LNGIntVector(1000);
     }
 
-    LNGHeap(final MiniSatStyleSolver s, final LNGIntVector heap, final LNGIntVector indices) {
-        this.s = s;
+    /**
+     * Constructs a new heap for a given solver and content.
+     * @param solver  the solver
+     * @param heap    the heap content
+     * @param indices the indices content
+     */
+    public LNGHeap(final MiniSatStyleSolver solver, final LNGIntVector heap, final LNGIntVector indices) {
+        this.s = solver;
         this.heap = heap;
         this.indices = indices;
     }
@@ -258,11 +264,11 @@ private void percolateDown(final int pos) {
         this.indices.set(y, p);
     }
 
-    LNGIntVector getHeap() {
+    public LNGIntVector getHeap() {
         return this.heap;
     }
 
-    LNGIntVector getIndices() {
+    public LNGIntVector getIndices() {
         return this.indices;
     }
 

diff --git a/src/main/java/org/logicng/solvers/datastructures/MSClause.java b/src/main/java/org/logicng/solvers/datastructures/MSClause.java
@@ -123,9 +123,9 @@ 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) {
+    public 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;
@@ -316,7 +316,7 @@ public int cardinality() {
         return this.data.size() - this.atMostWatchers + 1;
     }
 
-    LNGIntVector getData() {
+    public LNGIntVector getData() {
         return this.data;
     }
 

diff --git a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java
@@ -74,8 +74,8 @@ 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) {
+    public 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;

diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java b/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java
@@ -81,6 +81,58 @@ public static Builder builder() {
         return new Builder();
     }
 
+    public int getLbLBDMinimizingClause() {
+        return this.lbLBDMinimizingClause;
+    }
+
+    public int getLbLBDFrozenClause() {
+        return this.lbLBDFrozenClause;
+    }
+
+    public int getLbSizeMinimizingClause() {
+        return this.lbSizeMinimizingClause;
+    }
+
+    public int getFirstReduceDB() {
+        return this.firstReduceDB;
+    }
+
+    public int getSpecialIncReduceDB() {
+        return this.specialIncReduceDB;
+    }
+
+    public int getIncReduceDB() {
+        return this.incReduceDB;
+    }
+
+    public double getFactorK() {
+        return this.factorK;
+    }
+
+    public double getFactorR() {
+        return this.factorR;
+    }
+
+    public int getSizeLBDQueue() {
+        return this.sizeLBDQueue;
+    }
+
+    public int getSizeTrailQueue() {
+        return this.sizeTrailQueue;
+    }
+
+    public boolean isReduceOnSize() {
+        return this.reduceOnSize;
+    }
+
+    public int getReduceOnSizeSize() {
+        return this.reduceOnSizeSize;
+    }
+
+    public double getMaxVarDecay() {
+        return this.maxVarDecay;
+    }
+
     @Override
     public String toString() {
         final StringBuilder sb = new StringBuilder("GlucoseConfig{").append(System.lineSeparator());

diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java
@@ -167,6 +167,66 @@ public boolean isAuxiliaryVariablesInModels() {
         return this.auxiliaryVariablesInModels;
     }
 
+    public double getVarDecay() {
+        return this.varDecay;
+    }
+
+    public double getVarInc() {
+        return this.varInc;
+    }
+
+    public ClauseMinimization getClauseMin() {
+        return this.clauseMin;
+    }
+
+    public int getRestartFirst() {
+        return this.restartFirst;
+    }
+
+    public double getRestartInc() {
+        return this.restartInc;
+    }
+
+    public double getClauseDecay() {
+        return this.clauseDecay;
+    }
+
+    public boolean isRemoveSatisfied() {
+        return this.removeSatisfied;
+    }
+
+    public double getLearntsizeFactor() {
+        return this.learntsizeFactor;
+    }
+
+    public double getLearntsizeInc() {
+        return this.learntsizeInc;
+    }
+
+    public boolean isIncremental() {
+        return this.incremental;
+    }
+
+    public boolean isInitialPhase() {
+        return this.initialPhase;
+    }
+
+    public boolean isProofGeneration() {
+        return this.proofGeneration;
+    }
+
+    public boolean isBbInitialUBCheckForRotatableLiterals() {
+        return this.bbInitialUBCheckForRotatableLiterals;
+    }
+
+    public boolean isBbCheckForComplementModelLiterals() {
+        return this.bbCheckForComplementModelLiterals;
+    }
+
+    public boolean isBbCheckForRotatableLiterals() {
+        return this.bbCheckForRotatableLiterals;
+    }
+
     @Override
     public String toString() {
         final StringBuilder sb = new StringBuilder("MiniSatConfig{").append(System.lineSeparator());