Commit 281e8cc0 authored by Anne Parrain's avatar Anne Parrain

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

parents d0bd4984 6f7b21ec
Pipeline #268 failed with stages
in 11 minutes and 27 seconds
image: maven:3.3.9-jdk-8
cache:
untracked: true
variables:
# This will supress any download for dependencies and plugins or upload messages which would clutter the console log.
# `showDateTime` will show the passed time in milliseconds. You need to specify `--batch-mode` to make this work.
MAVEN_OPTS: "-Dmaven.repo.local=.m2/repository -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=WARN -Dorg.slf4j.simpleLogger.showDateTime=true -Djava.awt.headless=true"
# As of Maven 3.3.0 instead of this you may define these options in `.mvn/maven.config` so the same config is used
# when running from the command line.
# `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"
mybuild:
java8:
image: maven:3.3.9-jdk-8
stage: build
script:
- mvn $MAVEN_CLI_OPTS clean org.jacoco:jacoco-maven-plugin:prepare-agent --settings settings.xml deploy -Dmaven.test.failure.ignore=true
- mvn $MAVEN_CLI_OPTS sonar:sonar
cache:
paths:
- .m2/repository
jars-j8:
image: frekele/ant:1.10.1-jdk8
stage: build
script:
- mvn clean org.jacoco:jacoco-maven-plugin:prepare-agent install sonar:sonar -Dmaven.test.failure.ignore=true -Dmaven.repo.local=/cache/maven.repo
- ant -Drelease=NIGHTLY sat
artifacts:
paths:
- org.*/target/*.jar
- dist/NIGHTLY/*.jar
expire_in: 4 weeks
java7:
image: maven:3.3.9-jdk-7
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.test.failure.ignore=true -Dmaven.javadoc.skip=true
java9:
image: maven:3.5.0-jdk-9
stage: test
script:
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.test.failure.ignore=true -Dmaven.javadoc.skip=true
allow_failure: true
HOW TO BUILD SAT4J FROM SOURCE
# HOW TO BUILD SAT4J FROM SOURCE
+ Using Maven
## Using Maven (library users)
Just launch
$ mvn -Dmaven.test.skip=true install
```shell
$ mvn -DskipTests=true install
```
to build the SAT4J modules from the source tree.
All the dependencies will be gathered by Maven.
+ Using ant
## Using ant (solvers users)
Download the missing libraries and put them in the lib directory:
+ Apache commons CLI
......@@ -19,7 +23,26 @@ Download the missing libraries and put them in the lib directory:
Just type:
$ ant
```shell
$ ant [core,pseudo,maxsat,sat]
```
to build the solvers from source.
The solvers will be available in the directory `dist/CUSTOM`.
You may want to use a custom release name.
```shell
$ ant -Drelease=MINE maxsat
```
In that case, the solvers will be available in the directory `dist/MINE`.
Type
to build the modules from source.
```shell
$ ant -p
```
to see available options.
No preview for this file type
......@@ -74,8 +74,6 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
protected long beginTime;
protected ExitCode exitCode = ExitCode.UNKNOWN;
protected Reader reader;
protected boolean feedWithDecorated = false;
......@@ -265,7 +263,6 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
} catch (IOException e) {
System.err.println("FATAL " + e.getLocalizedMessage());
} catch (ContradictionException e) {
this.exitCode = ExitCode.UNSATISFIABLE;
this.launcherMode.setExitCode(ExitCode.UNSATISFIABLE);
log("(trivial inconsistency)"); //$NON-NLS-1$
} catch (ParseFormatException e) {
......@@ -319,7 +316,6 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
protected void solve(IProblem problem) throws TimeoutException {
launcherMode.solve(problem, reader, this, out, beginTime);
this.setExitCode(launcherMode.getCurrentExitCode());
}
/**
......@@ -340,7 +336,7 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
* the new ExitCode
*/
public final void setExitCode(ExitCode exitCode) {
this.exitCode = exitCode;
this.launcherMode.setExitCode(exitCode);
}
/**
......@@ -349,7 +345,7 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
* @return the current value of the Exitcode
*/
public final ExitCode getExitCode() {
return this.exitCode;
return this.launcherMode.getCurrentExitCode();
}
/**
......@@ -433,7 +429,9 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
}
protected void flushLog() {
this.out.print(logBuffer.toString());
if (logBuffer != null) {
this.out.print(logBuffer.toString());
}
logBuffer = null;
}
......
......@@ -82,7 +82,8 @@ public class BasicLauncher<T extends ISolver> extends AbstractLauncher {
asolver = this.factory.defaultSolver();
}
asolver.setTimeout(Integer.MAX_VALUE);
if (!"BRESIL".equals(System.getProperty("prime"))) {
if (!"BRESIL".equals(System.getProperty("prime"))
&& System.getProperty("all") == null) {
asolver.setDBSimplificationAllowed(true);
}
getLogWriter().println(asolver.toString(COMMENT_PREFIX));
......
......@@ -47,7 +47,7 @@ import org.sat4j.tools.Backbone;
*
*/
final class DecisionMode implements ILauncherMode {
private ExitCode exitCode = ExitCode.UNKNOWN;
private volatile ExitCode exitCode = ExitCode.UNKNOWN;
private int nbSolutionFound;
private PrintWriter out;
private long beginTime;
......
......@@ -47,8 +47,8 @@ import org.sat4j.tools.xplain.Xplain;
public class MUSLauncher extends AbstractLauncher {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
private int[] mus;
......@@ -94,8 +94,8 @@ public class MUSLauncher extends AbstractLauncher {
this.xplain = hlxp;
solver = hlxp;
} else {
Xplain<ISolver> xp = new Xplain<ISolver>(
SolverFactory.newDefault(), false);
Xplain<ISolver> xp = new Xplain<ISolver>(SolverFactory.newDefault(),
false);
this.xplain = xp;
solver = xp;
}
......@@ -109,9 +109,9 @@ public class MUSLauncher extends AbstractLauncher {
String className = "org.sat4j.tools.xplain." + args[0]
+ "Strategy";
try {
this.xplain
.setMinimizationStrategy((MinimizationStrategy) Class
.forName(className).newInstance());
this.xplain.setMinimizationStrategy(
(MinimizationStrategy) Class.forName(className)
.newInstance());
} catch (Exception e) {
log(e.getMessage());
}
......@@ -125,16 +125,17 @@ public class MUSLauncher extends AbstractLauncher {
@Override
protected void displayResult() {
if (this.solver != null) {
double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
double wallclocktime = (System.currentTimeMillis() - this.beginTime)
/ 1000.0;
this.solver.printStat(this.out);
this.solver.printInfos(this.out);
this.out.println(ILauncherMode.ANSWER_PREFIX + this.exitCode);
if (this.exitCode == ExitCode.SATISFIABLE) {
this.out.println(ILauncherMode.ANSWER_PREFIX + this.getExitCode());
if (this.getExitCode() == ExitCode.SATISFIABLE) {
int[] model = this.solver.model();
this.out.print(ILauncherMode.SOLUTION_PREFIX);
this.reader.decode(model, this.out);
this.out.println();
} else if (this.exitCode == ExitCode.UNSATISFIABLE
} else if (this.getExitCode() == ExitCode.UNSATISFIABLE
&& this.mus != null) {
this.out.print(ILauncherMode.SOLUTION_PREFIX);
this.reader.decode(this.mus, this.out);
......@@ -148,8 +149,9 @@ public class MUSLauncher extends AbstractLauncher {
public void run(String[] args) {
this.mus = null;
super.run(args);
double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
if (this.exitCode == ExitCode.UNSATISFIABLE) {
double wallclocktime = (System.currentTimeMillis() - this.beginTime)
/ 1000.0;
if (this.getExitCode() == ExitCode.UNSATISFIABLE) {
try {
log("Unsat detection wall clock time (in seconds) : "
+ wallclocktime);
......
......@@ -52,7 +52,7 @@ import org.sat4j.tools.LexicoDecorator;
*/
final class OptimizationMode implements ILauncherMode {
private int nbSolutions;
private ExitCode exitCode = ExitCode.UNKNOWN;
private volatile ExitCode exitCode = ExitCode.UNKNOWN;
private boolean isIncomplete = false;
private PrintWriter out;
private long beginTime;
......@@ -62,8 +62,8 @@ final class OptimizationMode implements ILauncherMode {
this.isIncomplete = isIncomplete;
}
public void displayResult(ISolver solver, IProblem problem,
ILogAble logger, PrintWriter out, Reader reader, long beginTime,
public void displayResult(ISolver solver, IProblem problem, ILogAble logger,
PrintWriter out, Reader reader, long beginTime,
boolean displaySolutionLine) {
if (solver == null) {
return;
......@@ -73,8 +73,8 @@ final class OptimizationMode implements ILauncherMode {
solver.printStat(out);
out.println(ANSWER_PREFIX + exitCode);
if (exitCode == ExitCode.SATISFIABLE
|| exitCode == ExitCode.OPTIMUM_FOUND || isIncomplete
&& exitCode == ExitCode.UPPER_BOUND) {
|| exitCode == ExitCode.OPTIMUM_FOUND
|| isIncomplete && exitCode == ExitCode.UPPER_BOUND) {
assert this.nbSolutions > 0;
logger.log("Found " + this.nbSolutions + " solution(s)");
......
......@@ -29,8 +29,6 @@
*******************************************************************************/
package org.sat4j.core;
import java.util.Iterator;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
......@@ -80,8 +78,8 @@ public class ConstrGroup implements IConstr {
}
public void removeFrom(ISolver solver) {
for (Iterator<IConstr> it = this.constrs.iterator(); it.hasNext();) {
solver.removeConstr(it.next());
for (int i = constrs.size() - 1; i >= 0; i--) {
solver.removeConstr(constrs.get(i));
}
}
......
......@@ -124,6 +124,10 @@ public final class ReadOnlyVec<T> implements IVec<T> {
throw new UnsupportedOperationException();
}
public void removeFromLast(T elem) {
throw new UnsupportedOperationException();
}
public void set(int i, T o) {
throw new UnsupportedOperationException();
}
......
......@@ -262,6 +262,26 @@ public final class Vec<T> implements IVec<T> {
this.myarray[--this.nbelem] = null;
}
/**
* Remove an element that belongs to the Vector. The method will break if
* the element does not belong to the vector. While {@link #remove(T)} look
* from the beginning of the vector, this method starts from the end of the
* vector.
*
* @param elem
* an element from the vector.
*/
public void removeFromLast(T elem) {
int j = this.nbelem - 1;
for (; this.myarray[j] != elem; j--) {
if (j == -1)
throw new NoSuchElementException();
}
// arraycopy is always faster than manual copy
System.arraycopy(this.myarray, j + 1, this.myarray, j, size() - j - 1);
this.myarray[--this.nbelem] = null;
}
/**
* Delete the ith element of the vector. The latest element of the vector
* replaces the removed element at the ith indexer.
......
......@@ -433,7 +433,7 @@ public class Solver<D extends DataStructureFactory>
}
Constr c = (Constr) co;
c.remove(this);
this.constrs.remove(c);
this.constrs.removeFromLast(c);
clearLearntClauses();
String type = c.getClass().getName();
this.constrTypes.get(type).dec();
......
......@@ -32,6 +32,7 @@ package org.sat4j.specs;
import java.io.Serializable;
import java.util.Comparator;
import java.util.Iterator;
import java.util.NoSuchElementException;
/**
* An abstraction on the type of vector used in the library.
......@@ -110,13 +111,26 @@ public interface IVec<T> extends Serializable, Cloneable {
void set(int i, T o);
/**
* Enleve un element qui se trouve dans le vecteur!!!
* Remove an element from the vector.
*
* @param elem
* un element du vecteur
* an element of the vector
* @throws NoSuchElementException
* if elem is not found in the vector.
*/
void remove(T elem);
/**
* Remove an element from the vector, starting with the last element.
*
* @param elem
* an element of the vector
* @throws NoSuchElementException
* if elem is not found in the vector.
* @since 2.3.6
*/
void removeFromLast(T elem);
/**
* Delete the ith element of the vector. The latest element of the vector
* replaces the removed element at the ith indexer.
......
......@@ -171,7 +171,8 @@ public class ModelIteratorTest {
@Test
public void testInplicantCoverIterator() {
try {
ModelIterator solver = new ModelIterator(SolverFactory.newDefault());
ModelIterator solver = new ModelIterator(
SolverFactory.newDefault());
solver.newVar(3);
IVecInt clause = new VecInt();
clause.push(1);
......@@ -422,8 +423,8 @@ public class ModelIteratorTest {
}
@Test(timeout = 12000)
public void testSpecificValues() throws ContradictionException,
TimeoutException {
public void testSpecificValues()
throws ContradictionException, TimeoutException {
assertEquals(3L, count(2));
assertEquals(7L, count(3));
assertEquals(15L, count(4));
......@@ -434,8 +435,8 @@ public class ModelIteratorTest {
assertEquals(511L, count(9));
}
private long count(int size) throws ContradictionException,
TimeoutException {
private long count(int size)
throws ContradictionException, TimeoutException {
SolutionCounter counter = new SolutionCounter(
SolverFactory.newDefault());
IVecInt clause = new VecInt();
......@@ -446,4 +447,104 @@ public class ModelIteratorTest {
counter.setTimeout(10);
return counter.countSolutions();
}
@Test
public void testInternalEnumerationOnExampleForRomain() {
try {
ISolver solver = SolverFactory.newDefault();
SolutionFoundListener sfl = new SolutionFoundListener() {
public void onSolutionFound(int[] solution) {
// do nothing
}
public void onSolutionFound(IVecInt solution) {
throw new UnsupportedOperationException(
"Not implemented yet!");
}
public void onUnsatTermination() {
// do nothing
}
};
SearchEnumeratorListener enumerator = new SearchEnumeratorListener(
sfl);
solver.setSearchListener(enumerator);
solver.newVar(6);
IVecInt clause = new VecInt();
clause.push(1).push(3).push(5);
solver.addClause(clause);
clause.clear();
clause.push(1).push(3).push(6);
solver.addClause(clause);
clause.clear();
clause.push(1).push(4).push(5);
solver.addClause(clause);
clause.clear();
clause.push(1).push(4).push(6);
solver.addClause(clause);
clause.clear();
clause.push(2).push(3).push(5);
solver.addClause(clause);
clause.clear();
clause.push(2).push(3).push(6);
solver.addClause(clause);
clause.clear();
clause.push(2).push(4).push(5);
solver.addClause(clause);
clause.clear();
clause.push(2).push(4).push(6);
solver.addClause(clause);
clause.clear();
assertTrue(solver.isSatisfiable());
assertEquals(37, enumerator.getNumberOfSolutionFound());
} catch (ContradictionException e) {
fail();
} catch (TimeoutException e) {
fail();
}
}
@Test
public void testExternalEnumerationOnExampleForRomain() {
try {
ISolver solver = SolverFactory.newDefault();
ModelIterator iterator = new ModelIterator(solver);
solver.newVar(6);
IVecInt clause = new VecInt();
clause.push(1).push(3).push(5);
solver.addClause(clause);
clause.clear();
clause.push(1).push(3).push(6);
solver.addClause(clause);
clause.clear();
clause.push(1).push(4).push(5);
solver.addClause(clause);
clause.clear();
clause.push(1).push(4).push(6);
solver.addClause(clause);
clause.clear();
clause.push(2).push(3).push(5);
solver.addClause(clause);
clause.clear();
clause.push(2).push(3).push(6);
solver.addClause(clause);
clause.clear();
clause.push(2).push(4).push(5);
solver.addClause(clause);
clause.clear();
clause.push(2).push(4).push(6);
solver.addClause(clause);
clause.clear();
while (iterator.isSatisfiable()) {
iterator.model();
}
assertEquals(37, iterator.numberOfModelsFoundSoFar());
} catch (ContradictionException e) {
fail();
} catch (TimeoutException e) {
fail();
}
}
}
\ No newline at end of file
......@@ -33,10 +33,10 @@ import java.util.Comparator;
import java.util.Iterator;
import java.util.NoSuchElementException;
import junit.framework.TestCase;
import org.sat4j.specs.IVec;
import junit.framework.TestCase;
/*
* Created on 16 oct. 2003
*
......@@ -324,6 +324,23 @@ public class VecTest extends TestCase {
assertEquals(0, nvec.size());
}
public void testRemoveFromLast() {
IVec<Integer> nvec = new Vec<Integer>();
for (int i = 0; i < 100; i++) {
nvec.push(new Integer(i));
}
Integer toRemove = nvec.get(10);
nvec.removeFromLast(toRemove);
assertEquals(99, nvec.size());
assertEquals(new Integer(11), nvec.get(10));
nvec.clear();
toRemove = new Integer(1);
nvec.push(toRemove);
assertEquals(1, nvec.size());
nvec.removeFromLast(toRemove);
assertEquals(0, nvec.size());
}
public void testEquals() {
IVec<Integer> nvec = new Vec<Integer>(3, new Integer(2));
IVec<Integer> vect = new Vec<Integer>(3, new Integer(2));
......
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" output="target/classes" path="src/main/java">
<attributes>
<attribute name="optional" value="true"/>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="src" output="target/test-classes" path="src/test/java">
<attributes>
<attribute name="optional" value="true"/>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry excluding="**" kind="src" output="target/classes" path="src/main/resources">
<attributes>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6">
<attributes>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.m2e.MAVEN2_CLASSPATH_CONTAINER">
<attributes>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="lib" path="/org.ow2.sat4j.pom/lib/xcsp3parser.jar"/>
<classpathentry kind="output" path="target/classes"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.sat4j.csp</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.sonarlint.eclipse.core.sonarlintBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.m2e.core.maven2Builder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.m2e.core.maven2Nature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>org.eclipse.pde.PluginNature</nature>
</natures>
</projectDescription>
eclipse.preferences.version=1
encoding//src/main/java=UTF-8
encoding//src/main/resources=UTF-8
encoding//src/test/java=UTF-8
encoding/<project>=UTF-8
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning