Merge pull request #53 from logic-ng/development

Development
logic-ng · Jul 31, 2024 · 42ece18 · 42ece18
2 parents 87a662f + 79bb7b0
commit 42ece18
Show file tree

Hide file tree

Showing 13 changed files with 175 additions and 34 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -2,6 +2,14 @@
 
 LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [2.5.1] - 2024-07-31
+
+### Changed
+
+- Changed visibility from some methods from package-private to public for formula and solver serializiation via the 
+  new https://github.com/logic-ng/serialization library
+
+
 ## [2.5.0] - 2024-05-02
 
 ### Removed (Potentially Breaking Change!)

diff --git a/README.md b/README.md
@@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.5.0</version>
+  <version>2.5.1</version>
 </dependency>
 ```
 

diff --git a/pom.xml b/pom.xml
@@ -26,17 +26,17 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.5.0</version>
+  <version>2.5.1</version>
   <packaging>bundle</packaging>
 
   <name>LogicNG</name>
   <description>The Next Generation Logic Library</description>
-  <url>http://www.logicng.org</url>
+  <url>https://www.logicng.org</url>
 
   <licenses>
     <license>
       <name>The Apache License, Version 2.0</name>
-      <url>http://www.apache.org/licenses/LICENSE-2.0.txt</url>
+      <url>https://www.apache.org/licenses/LICENSE-2.0.txt</url>
     </license>
   </licenses>
 

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());
@@ -346,7 +406,7 @@ public Builder proofGeneration(final boolean proofGeneration) {
 
         /**
          * Sets the CNF method for converting formula which are not in CNF for the solver.  The default value
-         * is {@code FACTORY_CNF}.
+         * is {@code PG_ON_SOLVER}.
          * @param cnfMethod the CNF method
          * @return the builder
          */