diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fb1c7d6..40ca17f6 100644 --- 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 index 376679a6..9bc07c4b 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add org.logicng logicng - 2.5.0 + 2.5.1 ``` diff --git a/pom.xml b/pom.xml index 6066e06f..70ebfd72 100644 --- a/pom.xml +++ b/pom.xml @@ -26,17 +26,17 @@ 4.0.0 org.logicng logicng - 2.5.0 + 2.5.1 bundle LogicNG The Next Generation Logic Library - http://www.logicng.org + https://www.logicng.org The Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + https://www.apache.org/licenses/LICENSE-2.0.txt diff --git a/src/main/java/org/logicng/collections/LNGBooleanVector.java b/src/main/java/org/logicng/collections/LNGBooleanVector.java index cca8786b..0cf8c14c 100644 --- 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 index c732168b..5f28b027 100644 --- 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 index 738bf030..6e05e22d 100644 --- 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 index e9988e6b..83c2b343 100644 --- 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 index 753ccd30..63a1199e 100644 --- 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 index 5b1db19f..cfbb2a8a 100644 --- 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 index 1feb20bc..acc4c633 100644 --- 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 index f7545b0b..249290b9 100644 --- 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 index 626f96a5..26b41ab1 100644 --- 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 index 691fc9a1..f60a9211 100644 --- 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 */