Commit 83bf54e5 authored by leberre's avatar leberre

Reused project.version in dependencies.

Deleted unused multicore project (now included in core or pb modules).


git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@879 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 37e9a85f
...@@ -11,12 +11,12 @@ ...@@ -11,12 +11,12 @@
<dependency> <dependency>
<groupId>org.sat4j</groupId> <groupId>org.sat4j</groupId>
<artifactId>org.sat4j.core</artifactId> <artifactId>org.sat4j.core</artifactId>
<version>2.3.0-SNAPSHOT</version> <version>${project.version}</version>
</dependency> </dependency>
<dependency> <dependency>
<groupId>org.sat4j</groupId> <groupId>org.sat4j</groupId>
<artifactId>org.sat4j.csp.xmlparser</artifactId> <artifactId>org.sat4j.csp.xmlparser</artifactId>
<version>2.3.0-SNAPSHOT</version> <version>${project.version}</version>
</dependency> </dependency>
<dependency> <dependency>
<groupId>rhino</groupId> <groupId>rhino</groupId>
......
...@@ -11,13 +11,13 @@ ...@@ -11,13 +11,13 @@
<dependency> <dependency>
<groupId>org.sat4j</groupId> <groupId>org.sat4j</groupId>
<artifactId>org.sat4j.core</artifactId> <artifactId>org.sat4j.core</artifactId>
<version>2.3.0-SNAPSHOT</version> <version>${project.version}</version>
<scope>compile</scope> <scope>compile</scope>
</dependency> </dependency>
<dependency> <dependency>
<groupId>org.sat4j</groupId> <groupId>org.sat4j</groupId>
<artifactId>org.sat4j.pb</artifactId> <artifactId>org.sat4j.pb</artifactId>
<version>2.3.0-SNAPSHOT</version> <version>${project.version}</version>
<scope>compile</scope> <scope>compile</scope>
</dependency> </dependency>
<dependency> <dependency>
......
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src/main/java"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="output" path="bin"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.sat4j.multicore</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>
</buildSpec>
<natures>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>org.eclipse.pde.PluginNature</nature>
</natures>
</projectDescription>
#Wed Aug 06 17:07:08 CEST 2008
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.5
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.source=1.5
#Tue Jun 16 17:52:40 CEST 2009
eclipse.preferences.version=1
editor_save_participant_org.eclipse.jdt.ui.postsavelistener.cleanup=true
sp_cleanup.add_default_serial_version_id=true
sp_cleanup.add_generated_serial_version_id=false
sp_cleanup.add_missing_annotations=true
sp_cleanup.add_missing_deprecated_annotations=true
sp_cleanup.add_missing_methods=false
sp_cleanup.add_missing_nls_tags=false
sp_cleanup.add_missing_override_annotations=true
sp_cleanup.add_serial_version_id=false
sp_cleanup.always_use_blocks=true
sp_cleanup.always_use_parentheses_in_expressions=false
sp_cleanup.always_use_this_for_non_static_field_access=false
sp_cleanup.always_use_this_for_non_static_method_access=false
sp_cleanup.convert_to_enhanced_for_loop=false
sp_cleanup.correct_indentation=false
sp_cleanup.format_source_code=true
sp_cleanup.format_source_code_changes_only=false
sp_cleanup.make_local_variable_final=false
sp_cleanup.make_parameters_final=false
sp_cleanup.make_private_fields_final=true
sp_cleanup.make_type_abstract_if_missing_method=false
sp_cleanup.make_variable_declarations_final=true
sp_cleanup.never_use_blocks=false
sp_cleanup.never_use_parentheses_in_expressions=true
sp_cleanup.on_save_use_additional_actions=true
sp_cleanup.organize_imports=true
sp_cleanup.qualify_static_field_accesses_with_declaring_class=false
sp_cleanup.qualify_static_member_accesses_through_instances_with_declaring_class=true
sp_cleanup.qualify_static_member_accesses_through_subtypes_with_declaring_class=true
sp_cleanup.qualify_static_member_accesses_with_declaring_class=false
sp_cleanup.qualify_static_method_accesses_with_declaring_class=false
sp_cleanup.remove_private_constructors=true
sp_cleanup.remove_trailing_whitespaces=false
sp_cleanup.remove_trailing_whitespaces_all=true
sp_cleanup.remove_trailing_whitespaces_ignore_empty=false
sp_cleanup.remove_unnecessary_casts=true
sp_cleanup.remove_unnecessary_nls_tags=false
sp_cleanup.remove_unused_imports=false
sp_cleanup.remove_unused_local_variables=false
sp_cleanup.remove_unused_private_fields=true
sp_cleanup.remove_unused_private_members=false
sp_cleanup.remove_unused_private_methods=true
sp_cleanup.remove_unused_private_types=true
sp_cleanup.sort_members=false
sp_cleanup.sort_members_all=false
sp_cleanup.use_blocks=false
sp_cleanup.use_blocks_only_for_return_and_throw=false
sp_cleanup.use_parentheses_in_expressions=false
sp_cleanup.use_this_for_non_static_field_access=false
sp_cleanup.use_this_for_non_static_field_access_only_if_necessary=true
sp_cleanup.use_this_for_non_static_method_access=false
sp_cleanup.use_this_for_non_static_method_access_only_if_necessary=true
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Multicore
Bundle-SymbolicName: org.sat4j.multicore
Bundle-Version: 9.9.9.token
Require-Bundle: org.sat4j.core,org.sat4j.pb
Main-Class: org.sat4j.multicore.MultiCoreLauncher
Class-Path: org.sat4j.core.jar org.sat4j.pb.jar
Bundle-RequiredExecutionEnvironment: J2SE-1.5
source.. = src/main/java/
bin.includes = .,\
META-INF/
<?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.sat4j</groupId>
<artifactId>org.sat4j.pom</artifactId>
<version>2.3.0-SNAPSHOT</version>
</parent>
<artifactId>org.sat4j.multicore</artifactId>
<name>SAT4J multicore</name>
<developers>
<developer>
<id>leberre</id>
<name>Daniel Le Berre</name>
<email>leberre@cril.univ-artois.fr</email>
<url>http://www.cril.univ-artois.fr/~leberre/</url>
<organization>CRIL</organization>
<organizationUrl>http://www.cril.univ-artois.fr/</organizationUrl>
<roles>
<role>architect</role>
<role>developer</role>
</roles>
</developer>
</developers>
<dependencies>
<dependency>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.core</artifactId>
<version>2.3.0-SNAPSHOT</version>
</dependency>
<dependency>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.pb</artifactId>
<version>2.3.0-SNAPSHOT</version>
</dependency>
</dependencies>
</project>
package org.sat4j.multicore;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import org.sat4j.core.ASolverFactory;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.SearchListener;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.ConstrGroup;
public class ManyCore<S extends ISolver> implements ISolver, OutcomeListener {
/**
*
*/
private static final long serialVersionUID = 1L;
private final String[] availableSolvers; // = { };
protected final List<S> solvers;
protected final int numberOfSolvers;
private int winnerId;
private boolean resultFound;
private volatile int remainingSolvers;
private volatile boolean solved;
public ManyCore(ASolverFactory<S> factory, String... solverNames) {
availableSolvers = solverNames;
Runtime runtime = Runtime.getRuntime();
long memory = runtime.maxMemory();
int numberOfCores = runtime.availableProcessors();
if (memory > 500000000L) {
numberOfSolvers = solverNames.length < numberOfCores ? solverNames.length
: numberOfCores;
} else {
numberOfSolvers = 1;
}
solvers = new ArrayList<S>(numberOfSolvers);
for (int i = 0; i < numberOfSolvers; i++) {
solvers.add(factory.createSolverByName(availableSolvers[i]));
}
}
public void addAllClauses(IVec<IVecInt> clauses)
throws ContradictionException {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).addAllClauses(clauses);
}
}
public IConstr addAtLeast(IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
for (int i = 0; i < numberOfSolvers; i++) {
group.add(solvers.get(i).addAtLeast(literals, degree));
}
return group;
}
public IConstr addAtMost(IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
for (int i = 0; i < numberOfSolvers; i++) {
group.add(solvers.get(i).addAtMost(literals, degree));
}
return group;
}
public IConstr addClause(IVecInt literals) throws ContradictionException {
ConstrGroup group = new ConstrGroup();
for (int i = 0; i < numberOfSolvers; i++) {
group.add(solvers.get(i).addClause(literals));
}
return group;
}
public void clearLearntClauses() {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).clearLearntClauses();
}
}
public void expireTimeout() {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).expireTimeout();
}
}
public Map<String, Number> getStat() {
return solvers.get(winnerId).getStat();
}
public int getTimeout() {
return solvers.get(0).getTimeout();
}
public long getTimeoutMs() {
return solvers.get(0).getTimeoutMs();
}
public int newVar() {
throw new UnsupportedOperationException();
}
public int newVar(int howmany) {
int result = 0;
for (int i = 0; i < numberOfSolvers; i++) {
result = solvers.get(i).newVar(howmany);
}
return result;
}
@Deprecated
public void printStat(PrintStream out, String prefix) {
solvers.get(winnerId).printStat(out, prefix);
}
public void printStat(PrintWriter out, String prefix) {
solvers.get(winnerId).printStat(out, prefix);
}
public boolean removeConstr(IConstr c) {
ConstrGroup group = (ConstrGroup) c;
boolean removed = true;
for (int i = 0; i < numberOfSolvers; i++) {
removed = removed & solvers.get(i).removeConstr(group.getConstr(i));
}
return removed;
}
public void reset() {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).reset();
}
}
public void setExpectedNumberOfClauses(int nb) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setExpectedNumberOfClauses(nb);
}
}
public void setTimeout(int t) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setTimeout(t);
}
}
public void setTimeoutMs(long t) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setTimeoutMs(t);
}
}
public void setTimeoutOnConflicts(int count) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setTimeoutOnConflicts(count);
}
}
public String toString(String prefix) {
StringBuffer res = new StringBuffer();
res.append(prefix);
res.append("ManyCore solver with ");
res.append(numberOfSolvers);
res.append(" solvers running in parallel");
res.append("\n");
for (int i = 0; i < numberOfSolvers; i++) {
res.append(solvers.get(i).toString(prefix));
res.append("\n");
}
return res.toString();
}
public int[] findModel() throws TimeoutException {
throw new UnsupportedOperationException();
}
public int[] findModel(IVecInt assumps) throws TimeoutException {
throw new UnsupportedOperationException();
}
public boolean isSatisfiable() throws TimeoutException {
return isSatisfiable(VecInt.EMPTY, false);
}
public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
throws TimeoutException {
remainingSolvers = numberOfSolvers;
solved = false;
for (int i = 0; i < numberOfSolvers; i++) {
new Thread(new RunnableSolver(i, solvers.get(i), assumps,
globalTimeout, this)).start();
}
try {
do {
Thread.sleep(500);
} while (remainingSolvers > 0);
} catch (InterruptedException e) {
// TODO: handle exception
}
if (!solved) {
assert remainingSolvers == 0;
throw new TimeoutException();
}
return resultFound;
}
public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
throw new UnsupportedOperationException();
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
throw new UnsupportedOperationException();
}
public int[] model() {
return solvers.get(winnerId).model();
}
public boolean model(int var) {
return solvers.get(winnerId).model(var);
}
public int nConstraints() {
return solvers.get(0).nConstraints();
}
public int nVars() {
return solvers.get(0).nVars();
}
public void printInfos(PrintWriter out, String prefix) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).printInfos(out, prefix);
}
}
public synchronized void onFinishWithAnswer(boolean finished,
boolean result, int index) {
if (finished && !solved) {
winnerId = index;
solved = true;
resultFound = result;
for (int i = 0; i < numberOfSolvers; i++) {
if (i != winnerId)
solvers.get(i).expireTimeout();
}
System.out.println("c And the winner is "
+ availableSolvers[winnerId]);
}
remainingSolvers--;
}
public boolean isDBSimplificationAllowed() {
return solvers.get(0).isDBSimplificationAllowed();
}
public void setDBSimplificationAllowed(boolean status) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(0).setDBSimplificationAllowed(status);
}
}
public void setSearchListener(SearchListener sl) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setSearchListener(sl);
}
}
/**
* @since 2.2
*/
public SearchListener getSearchListener() {
return solvers.get(0).getSearchListener();
}
public int nextFreeVarId(boolean reserve) {
return solvers.get(0).nextFreeVarId(reserve);
}
public IConstr addBlockingClause(IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
for (int i = 0; i < numberOfSolvers; i++) {
group.add(solvers.get(i).addBlockingClause(literals));
}
return group;
}
public boolean removeSubsumedConstr(IConstr c) {
ConstrGroup group = (ConstrGroup) c;
boolean removed = true;
for (int i = 0; i < numberOfSolvers; i++) {
removed = removed
& solvers.get(i).removeSubsumedConstr(group.getConstr(i));
}
return removed;
}
public boolean isVerbose() {
return false;
}
public void setVerbose(boolean value) {
// do nothing
}
public void setLogPrefix(String prefix) {
for (int i = 0; i < numberOfSolvers; i++) {
solvers.get(i).setLogPrefix(prefix);
}
}
public String getLogPrefix() {
return solvers.get(0).getLogPrefix();
}
public IVecInt unsatExplanation() {
return solvers.get(0).unsatExplanation();
}
}
interface OutcomeListener {
void onFinishWithAnswer(boolean finished, boolean result, int index);
}
class RunnableSolver implements Runnable {
private final int index;
private final ISolver solver;
private final OutcomeListener ol;
private final IVecInt assumps;
private final boolean globalTimeout;
public RunnableSolver(int i, ISolver solver, IVecInt assumps,
boolean globalTimeout, OutcomeListener ol) {
index = i;
this.solver = solver;
this.ol = ol;
this.assumps = assumps;
this.globalTimeout = globalTimeout;
}
public void run() {
try {
boolean result = solver.isSatisfiable(assumps, globalTimeout);
ol.onFinishWithAnswer(true, result, index);
} catch (Exception e) {
ol.onFinishWithAnswer(false, false, index);
}
}
}
package org.sat4j.multicore;
import java.math.BigInteger;
import org.sat4j.core.ASolverFactory;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.tools.ConstrGroup;
public class ManyCorePB extends ManyCore<IPBSolver> implements IPBSolver {
/**
*
*/
private static final long serialVersionUID = 1L;
public ManyCorePB(ASolverFactory<IPBSolver> factory, String... solverNames) {
super(factory, solverNames);
}