From a90abda56e46a9dede60e6c75d0820fa6d873233 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Sat, 3 Feb 2024 13:02:28 +0100 Subject: [PATCH] Necessary adjustements for formula and solver serializiation --- .../logicng/collections/LNGBooleanVector.java | 5 +++ .../org/logicng/collections/LNGIntVector.java | 5 +++ .../logicng/collections/LNGLongVector.java | 5 +++ .../java/org/logicng/solvers/MiniSat.java | 38 ++++++++++++++-- .../datastructures/LNGBoundedIntQueue.java | 34 ++++++++++++++ .../datastructures/LNGBoundedLongQueue.java | 34 ++++++++++++++ .../solvers/datastructures/LNGHeap.java | 14 ++++++ .../solvers/datastructures/MSClause.java | 19 ++++++++ .../solvers/datastructures/MSVariable.java | 10 +++++ .../org/logicng/solvers/sat/GlucoseSyrup.java | 35 +++++++-------- .../org/logicng/solvers/sat/MiniCard.java | 44 +++++++++---------- .../logicng/solvers/sat/MiniSat2Solver.java | 34 +++++++------- .../solvers/sat/MiniSatStyleSolver.java | 19 ++++---- .../logicng/solvers/sat/GlucoseSyrupTest.java | 2 - .../org/logicng/solvers/sat/MiniCardTest.java | 2 - 15 files changed, 227 insertions(+), 73 deletions(-) diff --git a/src/main/java/org/logicng/collections/LNGBooleanVector.java b/src/main/java/org/logicng/collections/LNGBooleanVector.java index 363715d1..cca8786b 100644 --- a/src/main/java/org/logicng/collections/LNGBooleanVector.java +++ b/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 diff --git a/src/main/java/org/logicng/collections/LNGIntVector.java b/src/main/java/org/logicng/collections/LNGIntVector.java index f2eac46f..c732168b 100644 --- a/src/main/java/org/logicng/collections/LNGIntVector.java +++ b/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 diff --git a/src/main/java/org/logicng/collections/LNGLongVector.java b/src/main/java/org/logicng/collections/LNGLongVector.java index 42ba48dd..738bf030 100644 --- a/src/main/java/org/logicng/collections/LNGLongVector.java +++ b/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 diff --git a/src/main/java/org/logicng/solvers/MiniSat.java b/src/main/java/org/logicng/solvers/MiniSat.java index 4428b014..797dffe5 100644 --- a/src/main/java/org/logicng/solvers/MiniSat.java +++ b/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 diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java index 80db3aee..e9988e6b 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java +++ b/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}", diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java index b091d5ce..753ccd30 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java +++ b/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}", diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java index 40074a3b..5b1db19f 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java +++ b/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{"); diff --git a/src/main/java/org/logicng/solvers/datastructures/MSClause.java b/src/main/java/org/logicng/solvers/datastructures/MSClause.java index 1f0d71f3..1feb20bc 100644 --- a/src/main/java/org/logicng/solvers/datastructures/MSClause.java +++ b/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(); diff --git a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java index 926d8011..f7545b0b 100644 --- a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java +++ b/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 diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java index 84276b6b..8ba2b44a 100644 --- a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java +++ b/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; } } - diff --git a/src/main/java/org/logicng/solvers/sat/MiniCard.java b/src/main/java/org/logicng/solvers/sat/MiniCard.java index 09df3ab4..4e09f3f9 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniCard.java +++ b/src/main/java/org/logicng/solvers/sat/MiniCard.java @@ -392,14 +392,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.isAtMost()) { for (int i = 0; i < c.size(); i++) { if (value(c.get(i)) != Tristate.TRUE) { @@ -409,13 +409,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; } } @@ -426,13 +426,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; } } @@ -808,14 +808,14 @@ protected void analyze(final MSClause conflictClause, final LNGIntVector outLear protected void simplifyClause(final LNGIntVector outLearnt) { int i; int j; - 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)); } } @@ -850,8 +850,8 @@ protected void simplifyClause(final LNGIntVector outLearnt) { outLearnt.set(1, p); this.analyzeBtLevel = v(p).level(); } - for (int l = 0; l < this.analyzeToClear.size(); l++) { - this.seen.set(var(this.analyzeToClear.get(l)), false); + for (int l = 0; l < analyzeToClear.size(); l++) { + this.seen.set(var(analyzeToClear.get(l)), false); } } diff --git a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java index 95e64afc..f042cc23 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java +++ b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java @@ -416,26 +416,26 @@ 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(); for (int i = 1; i < c.size(); i++) { final int q = c.get(i); 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; } } @@ -684,14 +684,14 @@ protected void analyze(final MSClause conflictClause, final LNGIntVector outLear protected void simplifyClause(final LNGIntVector outLearnt) { int i; int j; - 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)); } } @@ -726,8 +726,8 @@ protected void simplifyClause(final LNGIntVector outLearnt) { outLearnt.set(1, p); this.analyzeBtLevel = v(p).level(); } - for (int l = 0; l < this.analyzeToClear.size(); l++) { - this.seen.set(var(this.analyzeToClear.get(l)), false); + for (int l = 0; l < analyzeToClear.size(); l++) { + this.seen.set(var(analyzeToClear.get(l)), false); } } diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java b/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java index ec967348..c65bd45e 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java +++ b/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java @@ -85,7 +85,7 @@ public abstract class MiniSatStyleSolver { public static final int LIT_UNDEF = -1; // external solver configuration - protected final MiniSatConfig config; + protected MiniSatConfig config; // internal solver state protected boolean ok; @@ -101,8 +101,6 @@ public abstract class MiniSatStyleSolver { protected LNGIntVector conflict; protected LNGIntVector assumptions; protected LNGBooleanVector seen; - protected LNGIntVector analyzeStack; - protected LNGIntVector analyzeToClear; protected int analyzeBtLevel; protected double claInc; protected int simpDBAssigns; @@ -244,8 +242,6 @@ protected void initialize() { this.conflict = new LNGIntVector(); this.assumptions = new LNGIntVector(); this.seen = new LNGBooleanVector(); - this.analyzeStack = new LNGIntVector(); - this.analyzeToClear = new LNGIntVector(); this.analyzeBtLevel = 0; this.claInc = 1; this.simpDBAssigns = -1; @@ -633,9 +629,10 @@ protected void claBumpActivity(final MSClause c) { * Returns {@code true} if a given literal is redundant in the current conflict analysis, {@code false} otherwise. * @param p the literal * @param abstractLevels an abstraction of levels + * @param analyzeToClear the clear analysis vector * @return {@code true} if a given literal is redundant in the current conflict analysis */ - protected abstract boolean litRedundant(int p, int abstractLevels); + protected abstract boolean litRedundant(int p, int abstractLevels, LNGIntVector analyzeToClear); /** * Analysis the final conflict if there were assumptions. @@ -743,8 +740,6 @@ public String toString() { sb.append("conflict ").append(this.conflict).append(System.lineSeparator()); sb.append("assumptions ").append(this.assumptions).append(System.lineSeparator()); sb.append("#seen ").append(this.seen.size()).append(System.lineSeparator()); - sb.append("#stack ").append(this.analyzeStack.size()).append(System.lineSeparator()); - sb.append("#toclear ").append(this.analyzeToClear.size()).append(System.lineSeparator()); sb.append("claInc ").append(this.claInc).append(System.lineSeparator()); sb.append("simpDBAssigns ").append(this.simpDBAssigns).append(System.lineSeparator()); @@ -1122,4 +1117,12 @@ public void setSelectionOrder(final List selectionOrder) { public void resetSelectionOrder() { this.selectionOrder.clear(); } + + /** + * Returns the solver config. + * @return the solver config + */ + public MiniSatConfig getConfig() { + return this.config; + } } diff --git a/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java b/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java index abf904cf..c0f76995 100644 --- a/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java +++ b/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java @@ -78,8 +78,6 @@ public void testToString() { "conflict []%n" + "assumptions []%n" + "#seen 4%n" + - "#stack 0%n" + - "#toclear 0%n" + "claInc 1.0%n" + "simpDBAssigns -1%n" + "simpDBProps 0%n" + diff --git a/src/test/java/org/logicng/solvers/sat/MiniCardTest.java b/src/test/java/org/logicng/solvers/sat/MiniCardTest.java index 23bfa5f7..026b80f6 100644 --- a/src/test/java/org/logicng/solvers/sat/MiniCardTest.java +++ b/src/test/java/org/logicng/solvers/sat/MiniCardTest.java @@ -136,8 +136,6 @@ public void testToString() { "conflict []%n" + "assumptions []%n" + "#seen 4%n" + - "#stack 0%n" + - "#toclear 0%n" + "claInc 1.0%n" + "simpDBAssigns -1%n" + "simpDBProps 0%n" +