From b6e69752a8ae694f3ff0d93c9cf8699b9f79fa53 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Sat, 4 May 2024 14:07:20 +0200 Subject: [PATCH] Preparations for formula and solver serializiation --- .../logicng/collections/LNGBooleanVector.java | 7 ++- .../org/logicng/collections/LNGIntVector.java | 7 ++- .../logicng/collections/LNGLongVector.java | 7 ++- .../datastructures/LNGBoundedIntQueue.java | 16 ++--- .../datastructures/LNGBoundedLongQueue.java | 16 ++--- .../solvers/datastructures/LNGHeap.java | 14 +++-- .../solvers/datastructures/MSClause.java | 8 +-- .../solvers/datastructures/MSVariable.java | 4 +- .../logicng/solvers/sat/GlucoseConfig.java | 52 ++++++++++++++++ .../logicng/solvers/sat/MiniSatConfig.java | 60 +++++++++++++++++++ 10 files changed, 162 insertions(+), 29 deletions(-) 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..c3afef8d 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());