Commit 4b3b905c authored by tfalque.ext's avatar tfalque.ext
Browse files

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j

parents ada230c6 3610d72b
Pipeline #17055 failed with stages
in 21 seconds
......@@ -7,9 +7,8 @@ variables:
# `installAtEnd` and `deployAtEnd`are only effective with recent version of the corresponding plugins.
MAVEN_CLI_OPTS: "--batch-mode --errors --fail-at-end --show-version -DinstallAtEnd=true -DdeployAtEnd=true"
java8-sonar:
image: maven:3.5.4-jdk-8-alpine
maven38-java11-sonar:
image: maven:3.8.1-jdk-11-slim
stage: build
only:
- master
......@@ -20,50 +19,19 @@ java8-sonar:
paths:
- .m2/repository
java8:
image: maven:3.5.4-jdk-8-alpine
maven38-java11:
image: maven:3.8.1-jdk-11-slim
stage: build
except:
- master
script:
- mvn $MAVEN_CLI_OPTS clean org.jacoco:jacoco-maven-plugin:prepare-agent --settings settings.xml deploy
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
cache:
paths:
- .m2/repository
jars-j8:
image: frekele/ant:1.10.1-jdk8
stage: build
script:
- ant -Drelease=NIGHTLY sat
artifacts:
paths:
- dist/NIGHTLY/*.jar
expire_in: 4 weeks
java7:
image: maven:3.5.4-jdk-7-alpine
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
allow_failure: true
maven36-java8:
image: maven:3.6.2-jdk-8-slim
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
allow_failure: true
maven36-java11:
image: maven:3.6.2-jdk-11-slim
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
allow_failure: true
maven36-java13:
image: maven:3.6.2-jdk-13
maven38-java16:
image: maven:3.8.1-openjdk-16-slim
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
......
......@@ -3,7 +3,7 @@
<parent>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.pom</artifactId>
<version>2.3.6</version>
<version>3.0.0-SNAPSHOT</version>
</parent>
<artifactId>org.ow2.sat4j.core</artifactId>
<name>SAT4J core</name>
......
......@@ -72,8 +72,6 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
*/
private static final long serialVersionUID = 1L;
public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$
protected long beginTime;
protected transient Reader reader;
......@@ -105,7 +103,7 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
protected boolean prime = System.getProperty("prime") != null;
private ILauncherMode launcherMode = ILauncherMode.DECISION;
private ILauncherMode launcherMode = DecisionMode.instance();
protected void setLauncherMode(ILauncherMode launcherMode) {
this.launcherMode = launcherMode;
......@@ -305,9 +303,10 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
if (this.isSilent())
return;
if (this.logBuffer != null) {
this.logBuffer.append(COMMENT_PREFIX).append(message).append('\n');
this.logBuffer.append(OutputPrefix.COMMENT_PREFIX).append(message)
.append('\n');
} else {
this.out.println(COMMENT_PREFIX + message);
this.out.println(OutputPrefix.COMMENT_PREFIX + message);
}
}
......
......@@ -87,11 +87,12 @@ public class BasicLauncher<T extends ISolver> extends AbstractLauncher {
} else {
asolver.setTimeout(Integer.MAX_VALUE);
}
if (!"BRESIL".equals(System.getProperty("prime"))
if (System.getProperty("prime") == null
&& System.getProperty("all") == null) {
asolver.setDBSimplificationAllowed(true);
}
getLogWriter().println(asolver.toString(COMMENT_PREFIX));
getLogWriter().println(
asolver.toString(OutputPrefix.COMMENT_PREFIX.toString()));
return asolver;
}
......
......@@ -48,14 +48,28 @@ import org.sat4j.tools.Backbone;
*
*/
@Feature("solutionlistener")
final class DecisionMode implements ILauncherMode {
public final class DecisionMode implements ILauncherMode {
/**
*
*/
private static final long serialVersionUID = 1L;
private ExitCode exitCode = ExitCode.UNKNOWN;
private int nbSolutionFound;
private PrintWriter out;
private transient PrintWriter out;
private long beginTime;
private Reader reader;
private ISolver solver;
private static final DecisionMode instance = new DecisionMode();
/**
* The launcher is in decision mode: the answer is either SAT, UNSAT or
* UNKNOWN
*/
public static DecisionMode instance() {
return instance;
}
public void displayResult(ISolver solver, IProblem problem, ILogAble logger,
PrintWriter out, Reader reader, long beginTime,
boolean displaySolutionLine) {
......@@ -64,7 +78,7 @@ final class DecisionMode implements ILauncherMode {
double wallclocktime = (System.currentTimeMillis() - beginTime)
/ 1000.0;
solver.printStat(out);
out.println(ANSWER_PREFIX + exitCode);
out.printf("%s%s%n", OutputPrefix.ANSWER_PREFIX, exitCode);
if (exitCode != ExitCode.UNKNOWN
&& exitCode != ExitCode.UNSATISFIABLE) {
int[] model = problem.model();
......@@ -109,7 +123,7 @@ final class DecisionMode implements ILauncherMode {
private void printSolution(ISolver solver, PrintWriter out, Reader reader,
int[] model) {
out.print(SOLUTION_PREFIX);
out.print(OutputPrefix.SOLUTION_PREFIX);
if (System.getProperty("color") == null) {
reader.decode(model, out);
out.println();
......@@ -160,6 +174,7 @@ final class DecisionMode implements ILauncherMode {
}
public void setIncomplete(boolean isIncomplete) {
// Not applicable for decision problems
}
public ExitCode getCurrentExitCode() {
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j;
import java.io.Serializable;
/**
* Enumeration allowing to manage easily exit code for the SAT and PB
* Competitions.
......@@ -36,13 +38,11 @@ package org.sat4j;
* @author leberre
*
*/
public enum ExitCode {
public enum ExitCode implements Serializable {
OPTIMUM_FOUND(30, "OPTIMUM FOUND"),
UPPER_BOUND(30, "UPPER BOUND"),
SATISFIABLE(10, "SATISFIABLE"),
UNKNOWN(0, "UNKNOWN"),
UNSATISFIABLE(20, "UNSATISFIABLE");
OPTIMUM_FOUND(30, "OPTIMUM FOUND"), UPPER_BOUND(30,
"UPPER BOUND"), SATISFIABLE(10, "SATISFIABLE"), UNKNOWN(0,
"UNKNOWN"), UNSATISFIABLE(20, "UNSATISFIABLE");
/** value of the exit code. */
private final int value;
......
......@@ -47,12 +47,6 @@ import org.sat4j.tools.SolutionFoundListener;
*/
public interface ILauncherMode extends SolutionFoundListener {
String SOLUTION_PREFIX = "v "; //$NON-NLS-1$
String ANSWER_PREFIX = "s "; //$NON-NLS-1$
String CURRENT_OPTIMUM_VALUE_PREFIX = "o ";
/**
* Output of the launcher when the solver stops
*
......@@ -120,19 +114,4 @@ public interface ILauncherMode extends SolutionFoundListener {
* the status of the problem to solve
*/
void setExitCode(ExitCode exitCode);
/**
* The launcher is in decision mode: the answer is either SAT, UNSAT or
* UNKNOWN
*/
ILauncherMode DECISION = new DecisionMode();
/**
* The launcher is in optimization mode: the answer is either SAT,
* UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN. Using the incomplete
* property, the solver returns an upper bound of the optimal solution when
* a time out occurs.
*/
ILauncherMode OPTIMIZATION = new OptimizationMode();
}
......@@ -118,7 +118,8 @@ public class MUSLauncher extends AbstractLauncher {
}
}
solver.setTimeout(Integer.MAX_VALUE);
getLogWriter().println(solver.toString(COMMENT_PREFIX));
getLogWriter().println(
solver.toString(OutputPrefix.COMMENT_PREFIX.toString()));
return solver;
}
......@@ -129,15 +130,16 @@ public class MUSLauncher extends AbstractLauncher {
/ 1000.0;
this.solver.printStat(this.out);
this.solver.printInfos(this.out);
this.out.println(ILauncherMode.ANSWER_PREFIX + this.getExitCode());
this.out.printf("%s %s%n", OutputPrefix.ANSWER_PREFIX,
this.getExitCode());
if (this.getExitCode() == ExitCode.SATISFIABLE) {
int[] model = this.solver.model();
this.out.print(ILauncherMode.SOLUTION_PREFIX);
this.out.print(OutputPrefix.SOLUTION_PREFIX);
this.reader.decode(model, this.out);
this.out.println();
} else if (this.getExitCode() == ExitCode.UNSATISFIABLE
&& this.mus != null) {
this.out.print(ILauncherMode.SOLUTION_PREFIX);
this.out.print(OutputPrefix.SOLUTION_PREFIX);
this.reader.decode(this.mus, this.out);
this.out.println();
}
......@@ -182,7 +184,7 @@ public class MUSLauncher extends AbstractLauncher {
public void onSolutionFound(IVecInt solution) {
System.out.println(solver.getLogPrefix()
+ "found mus number " + ++muscount);
out.print(ILauncherMode.SOLUTION_PREFIX);
out.print(OutputPrefix.SOLUTION_PREFIX);
int[] localMus = new int[solution.size()];
solution.copyTo(localMus);
reader.decode(localMus, out);
......
......@@ -52,14 +52,30 @@ import org.sat4j.tools.LexicoDecorator;
*
*/
@Feature("solutionlistener")
final class OptimizationMode implements ILauncherMode {
public final class OptimizationMode implements ILauncherMode {
/**
*
*/
private static final long serialVersionUID = 1L;
private int nbSolutions;
private ExitCode exitCode = ExitCode.UNKNOWN;
private boolean isIncomplete = false;
private PrintWriter out;
private transient PrintWriter out;
private long beginTime;
private IOptimizationProblem problem;
private static final OptimizationMode instance = new OptimizationMode();
/**
* The launcher is in optimization mode: the answer is either SAT,
* UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN. Using the incomplete
* property, the solver returns an upper bound of the optimal solution when
* a time out occurs.
*/
public static OptimizationMode instance() {
return instance;
}
public void setIncomplete(boolean isIncomplete) {
this.isIncomplete = isIncomplete;
}
......@@ -73,7 +89,7 @@ final class OptimizationMode implements ILauncherMode {
System.out.flush();
out.flush();
solver.printStat(out);
out.println(ANSWER_PREFIX + exitCode);
out.printf("%s%s%n", OutputPrefix.ANSWER_PREFIX, exitCode);
if (exitCode == ExitCode.SATISFIABLE
|| exitCode == ExitCode.OPTIMUM_FOUND
|| isIncomplete && exitCode == ExitCode.UPPER_BOUND) {
......@@ -81,7 +97,7 @@ final class OptimizationMode implements ILauncherMode {
logger.log("Found " + this.nbSolutions + " solution(s)");
if (displaySolutionLine) {
out.print(SOLUTION_PREFIX);
out.print(OutputPrefix.SOLUTION_PREFIX);
reader.decode(problem.model(), out);
out.println();
}
......@@ -137,8 +153,8 @@ final class OptimizationMode implements ILauncherMode {
}
logger.log("Got one! Elapsed wall clock time (in seconds):" //$NON-NLS-1$
+ (System.currentTimeMillis() - beginTime) / 1000.0);
out.println(CURRENT_OPTIMUM_VALUE_PREFIX
+ optproblem.getObjectiveValue());
out.printf("%s%s%n", OutputPrefix.CURRENT_OPTIMUM_VALUE_PREFIX,
optproblem.getObjectiveValue());
optproblem.discardCurrentSolution();
}
if (isSatisfiable) {
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2021 Artois University and CNRS
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
* Contributors:
* CRIL - initial API and implementation
*******************************************************************************/
package org.sat4j;
/**
* Enumeration allowing to manage easily solvers output prefixes.
*
* @author leberre
* @since 3.0
*/
public enum OutputPrefix {
COMMENT_PREFIX("c "), SOLUTION_PREFIX("v "), ANSWER_PREFIX(
"s "), CURRENT_OPTIMUM_VALUE_PREFIX("o ");
private String prefix;
OutputPrefix(String prefix) {
this.prefix = prefix;
}
@Override
public String toString() {
return prefix;
}
}
......@@ -359,7 +359,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
// remet la clause dans la liste des clauses regardees
this.voc.watch(p, this);
......@@ -374,7 +374,6 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
}
}
return true;
}
public boolean canBeSatisfiedByCountingLiterals() {
......
......@@ -478,7 +478,7 @@ public final class MaxWatchCard
throw new UnsupportedOperationException("Not implemented yet!");
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
}
......
......@@ -667,7 +667,7 @@ public class MinWatchCard
private int savedindex = this.degree + 1;
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
// Recherche du litt?ral falsifi?
int indFalsified = 0;
while ((this.lits[indFalsified] ^ 1) != p) {
......@@ -693,7 +693,7 @@ public class MinWatchCard
l.isMandatory(this.lits[i]);
}
}
return true;
return;
}
this.savedindex = indSwap + 1;
// Si un litt?ral a ?t? trouv? on les ?change
......@@ -703,9 +703,6 @@ public class MinWatchCard
// On observe le nouveau litt?ral
this.voc.watch(tmpInt ^ 1, this);
return true;
}
public boolean canBeSatisfiedByCountingLiterals() {
......
......@@ -126,7 +126,7 @@ public abstract class BinaryClause
return s.enqueue(this.head, this);
}
public boolean propagatePI(MandatoryLiteralListener m, int p) {
public void propagatePI(MandatoryLiteralListener m, int p) {
this.voc.watch(p, this);
if (this.head == neg(p)) {
m.isMandatory(this.tail);
......@@ -134,7 +134,6 @@ public abstract class BinaryClause
assert this.tail == neg(p);
m.isMandatory(this.head);
}
return true;
}
/*
......
......@@ -228,11 +228,10 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
throw new UnsupportedOperationException("Not implemented yet!");
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
for (int i = 0; i < clauses.size(); i++) {
l.isMandatory(clauses.get(i));
}
return true;
}
public Constr toConstraint() {
......
......@@ -328,7 +328,7 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
throw new UnsupportedOperationException("Not implemented yet!");
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
// TODO: implement this method !
throw new UnsupportedOperationException("Not implemented yet!");
}
......
......@@ -104,7 +104,7 @@ public class LearntHTClause extends HTClause {
this.activity = d;
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
}
......
......@@ -96,8 +96,7 @@ public final class LearntWLClause extends WLClause {
this.activity += claInc;
}
public boolean propagatePI(MandatoryLiteralListener s, int p) {
public void propagatePI(MandatoryLiteralListener s, int p) {
this.voc.watch(p, this);
return true;
}
}
......@@ -185,7 +185,7 @@ public final class Lits implements Serializable, ILits {
}
public boolean isSatisfied(int lit) {
return this.falsified[lit ^ 1];
return this.falsified[lit ^ 1] && !this.falsified[lit];
}
public boolean isFalsified(int lit) {
......
......@@ -104,7 +104,7 @@ public class OriginalHTClause extends HTClause {
// do nothing
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
public void propagatePI(MandatoryLiteralListener l, int p) {
if (this.head == neg(p)) {
final int[] mylits = this.middleLits;
// moving head on the right
......@@ -137,7 +137,6 @@ public class OriginalHTClause extends HTClause {
this.voc.watch(neg(this.tail), this);
}
}
return true;
}
private int savedindexhead;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment