Commit bd3d186b authored by Daniel Le Berre's avatar Daniel Le Berre

Moved csp and scala packages to their own repository.

parent ccd7b10b
Pipeline #260 failed with stage
in 32 seconds
<?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
org.eclipse.jdt.core.compiler.source=1.8
activeProfiles=
eclipse.preferences.version=1
resolveWorkspaceProjects=true
version=1
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: %bundleName
Bundle-SymbolicName: org.sat4j.csp
Bundle-Version: 9.9.9.token
Bundle-ClassPath: lib/cspparserxml.jar
Export-Package: org.sat4j.csp;version="9.9.9.token",
org.sat4j.csp.constraints;version="9.9.9.token",
org.sat4j.csp.encodings;version="9.9.9.token",
org.sat4j.reader;version="9.9.9.token"
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Require-Bundle: org.mozilla.javascript;bundle-version="1.6.2",
org.sat4j.csp.xmlparser;bundle-version="1.0.1"
Built-By: Daniel Le Berre
Main-Class: org.sat4j.csp.CSPLauncher
Specification-Title: SAT4J
Specification-Version: NA
Specification-Vendor: Daniel Le Berre
Implementation-Title: SAT4J
Implementation-Version: 9.9.9.token
Implementation-Vendor: CRIL CNRS UMR 8188 - Universite d'Artois
Class-Path: org.sat4j.core.jar lib/js.jar lib/cspparserxml.jar
Bundle-RequiredExecutionEnvironment: J2SE-1.4
bin.includes = plugin.properties,\
META-INF/,\
.
source.. = src/main/java/,\
src/test/java/
bundleName = SAT4J CSP
providerName = CRIL CNRS UMR 8188 - Universite d'Artois
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.pom</artifactId>
<version>2.3.6-SNAPSHOT</version>
</parent>
<artifactId>org.ow2.sat4j.csp</artifactId>
<name>SAT4J csp</name>
<properties>
<!-- compiler params -->
<javaSource>1.8</javaSource>
<javaTarget>1.8</javaTarget>
<testSource>1.8</testSource>
<testTarget>1.8</testTarget>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<!-- common distribution locations -->
<siteRepositoryId />
<siteRepositoryUrl />
<maven.build.timestamp.format>yyyyMMdd</maven.build.timestamp.format>
<sat4j.custom.version>${project.version}.v${maven.build.timestamp}</sat4j.custom.version>
<next.eclipse.release.date>June, 2010</next.eclipse.release.date>
<bundle-manifest>${project.build.directory}/META-INF/MANIFEST.MF</bundle-manifest>
</properties>
<dependencies>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.pb</artifactId>
<version>${project.version}</version>
</dependency>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.csp.xmlparser</artifactId>
<version>${project.version}</version>
</dependency>
<dependency>
<groupId>rhino</groupId>
<artifactId>js</artifactId>
<version>1.7R2</version>
</dependency>
<dependency>
<groupId>org.xcsp3</groupId>
<artifactId>org.xcsp3.parser</artifactId>
<version>3.0</version>
<scope>system</scope>
<systemPath>${basedir}/../lib/xcsp3parser.jar</systemPath>
</dependency>
<dependency>
<groupId>org.xcsp3</groupId>
<artifactId>org.xcsp3.utils</artifactId>
<version>1.0</version>
<scope>system</scope>
<systemPath>${basedir}/../lib/org.xcsp.tests-1.0.0-SNAPSHOT.jar</systemPath>
</dependency>
</dependencies>
</project>
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* 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.
*******************************************************************************/
package org.sat4j.csp;
import java.io.IOException;
import java.util.Map;
import org.sat4j.AbstractLauncher;
import org.sat4j.ILauncherMode;
import org.sat4j.reader.ECSPFormat;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
public class CSPLauncher extends AbstractLauncher {
/**
*
*/
private static final long serialVersionUID = 1L;
private boolean shouldOnlyDisplayEncoding = false;
public CSPLauncher() {
if(System.getProperty("CompetitionOutput") != null) {
bufferizeLog();
}
}
/*
* (non-Javadoc)
*
* @see org.sat4j.Lanceur#configureSolver(java.lang.String[])
*/
@Override
protected ISolver configureSolver(String[] args) {
ICspPBSatSolver asolver;
if (args.length == 2) {
asolver = SolverFactory.instance().createSolverByName(args[0]);
} else {
asolver = new CspSatSolverDecorator(org.sat4j.pb.SolverFactory.newDefault());
}
log(asolver.toString(COMMENT_PREFIX));
this.shouldOnlyDisplayEncoding = asolver.shouldOnlyDisplayEncoding();
return asolver;
}
/*
* (non-Javadoc)
*
* @see org.sat4j.Lanceur#createReader(org.sat4j.specs.ISolver)
*/
@Override
protected Reader createReader(final ISolver aSolver,
final String problemname) {
ECSPFormat cspFormat = ECSPFormat.inferInstanceType(problemname);
this.out = cspFormat.decoratePrintWriter(this.shouldOnlyDisplayEncoding, this.out);
flushLog();
Reader aReader = cspFormat.getReader(this, aSolver);
setLauncherMode(cspFormat.isOptimizationModeRequired() ? ILauncherMode.OPTIMIZATION : ILauncherMode.DECISION);
if (System.getProperty("verbose") != null) {
log("verbose mode on");
aReader.setVerbosity(true);
aSolver.setVerbose(true);
} else {
aSolver.setVerbose(false);
}
return aReader;
}
@Override
protected IProblem readProblem(String problemname)
throws ParseFormatException, IOException, ContradictionException {
this.setSilent(true);
IProblem problem = super.readProblem(problemname);
if(this.shouldOnlyDisplayEncoding) {
displayEncoding();
}
return problem;
}
private void displayEncoding() {
if(this.reader.hasAMapping()) {
this.out.write("c CSP to SAT var mapping:\n");
Map<Integer, String> mapping = this.reader.getMapping();
for(Map.Entry<Integer, String> entry : mapping.entrySet()) {
this.out.write("c "+entry.getValue()+";"+entry.getKey()+"\n");
}
}
}
public static void main(String[] args) {
AbstractLauncher lanceur = new CSPLauncher();
if (args.length > 2 || args.length == 0) {
lanceur.usage();
return;
}
try {
lanceur.run(args);
} catch (IllegalArgumentException e) {
lanceur.log(">>>> " + e.getMessage() + " <<<<");
}
}
@Override
public void displayLicense() {
super.displayLicense();
log("That software uses the Rhino library from the Mozilla project.");
}
@Override
public void usage() {
System.out.println("Please provide a CSP instance file!"); //$NON-NLS-1$
}
@Override
protected String getInstanceName(String[] args) {
if (args.length == 1)
return args[0];
return args[1];
}
@Override
protected void displayResult() {
try {
Thread.sleep(200);
} catch (InterruptedException e) {
e.printStackTrace();
}
super.displayResult();
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* 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.
*******************************************************************************/
package org.sat4j.csp;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
@FunctionalInterface
public interface Clausifiable {
void toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
throws ContradictionException;
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* 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.
*******************************************************************************/
package org.sat4j.csp;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
public class Constant implements Evaluable {
private final int value;
private final Domain domain;
public Constant(int value) {
this.value = value;
domain = new SingletonDomain(value);
}
public Domain domain() {
return domain;
}
public int translate(int key) {
throw new UnsupportedOperationException();
}
public void toClause(ISolver solver) throws ContradictionException {
throw new UnsupportedOperationException();
}
/*
* (non-Javadoc)
*
* @see java.lang.Object#toString()
*/
@Override
public String toString() {
return String.valueOf(value);
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* 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.
*******************************************************************************/
package org.sat4j.csp;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.math.BigInteger;
import java.util.Map;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.ISolverService;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.SearchListener;
import org.sat4j.specs.TimeoutException;
import org.sat4j.specs.UnitClauseProvider;
/**
* A simple decorator allowing to use an {@link IPBSolver} as an {@link ICspPBSatSolver}.
* It provides two methods allowing to set/retrieve whether the associated CSP to SAT encoding must be displayed or not.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class CspSatSolverDecorator implements ICspPBSatSolver {
private static final long serialVersionUID = 1L;
private IPBSolver solver;
private boolean shouldDisplayEncoding = false;
public CspSatSolverDecorator(IPBSolver solver) {
this.solver = solver;
}
public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
throws ContradictionException {
return solver.addPseudoBoolean(lits, coeffs, moreThan, d);
}
public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException {
return solver.addAtMost(literals, coeffs, degree);
}
public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
throws ContradictionException {
return solver.addAtMost(literals, coeffs, degree);
}
public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException {
return solver.addAtLeast(literals, coeffs, degree);
}
public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
throws ContradictionException {
return solver.addAtLeast(literals, coeffs, degree);
}
public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight) throws ContradictionException {
return solver.addExactly(literals, coeffs, weight);
}
public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
throws ContradictionException {
return solver.addExactly(literals, coeffs, weight);
}
public void setObjectiveFunction(ObjectiveFunction obj) {
solver.setObjectiveFunction(obj);
}
public ObjectiveFunction getObjectiveFunction() {
return solver.getObjectiveFunction();
}
public boolean model(int var) {
return solver.model(var);
}
public int[] model() {
return solver.model();
}
@SuppressWarnings("deprecation")
public int newVar() {
return solver.newVar();
}
public int[] primeImplicant() {
return solver.primeImplicant();
}
public int nextFreeVarId(boolean reserve) {
return solver.nextFreeVarId(reserve);
}
public boolean primeImplicant(int p) {
return solver.primeImplicant(p);
}
public boolean isSatisfiable() throws TimeoutException {
return solver.isSatisfiable();
}
public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout) throws TimeoutException {
return solver.isSatisfiable(assumps, globalTimeout);
}
public void registerLiteral(int p) {
solver.registerLiteral(p);
}
public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
return solver.isSatisfiable(globalTimeout);
}
public void setExpectedNumberOfClauses(int nb) {
solver.setExpectedNumberOfClauses(nb);
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
return solver.isSatisfiable(assumps);
}
public IConstr addClause(IVecInt literals) throws ContradictionException {
return solver.addClause(literals);
}
public int[] findModel() throws TimeoutException {
return solver.findModel();
}
public IConstr addBlockingClause(IVecInt literals) throws ContradictionException {
return solver.addBlockingClause(literals);
}
public int[] findModel(IVecInt assumps) throws TimeoutException {
return solver.findModel(assumps);
}
public IConstr discardCurrentModel() throws ContradictionException {
return solver.discardCurrentModel();
}
public IVecInt createBlockingClauseForCurrentModel() {
return solver.createBlockingClauseForCurrentModel();
}
public boolean removeConstr(IConstr c) {
return solver.removeConstr(c);
}
public int nConstraints() {
return solver.nConstraints();
}
public int newVar(int howmany) {
return solver.newVar(howmany);
}
public boolean removeSubsumedConstr(IConstr c) {
return solver.removeSubsumedConstr(c);
}
public int nVars() {
return solver.nVars();
}
@SuppressWarnings("deprecation")
public void printInfos(PrintWriter out, String prefix) {
solver.printInfos(out, prefix);
}
public void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException {
solver.addAllClauses(clauses);
}
public void printInfos(PrintWriter out) {
solver.printInfos(out);
}
public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException {
return solver.addAtMost(literals, degree);
}
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException {
return solver.addAtLeast(literals, degree);
}
public IConstr addExactly(IVecInt literals, int n) throws ContradictionException {
return solver.addExactly(literals, n);
}
public IConstr addParity(IVecInt literals, boolean even) {
return solver.addParity(literals, even);
}