Commit 353da38a authored by Daniel Le Berre's avatar Daniel Le Berre

Initial attempt to create a maven structure for sat4j core.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@8 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent cd37f877
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src/main/java"/>
<classpathentry kind="src" path="src/test/java"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/3.8.1"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry kind="output" path="bin"/>
</classpath>
.settings
bin
.checkstyle
.fbwarnings
.teamtask_meta
sat4j.jardesc
*.sxw
#FindBugs User Preferences
#Fri Mar 23 14:23:38 CET 2007
default_directory=/home/leberre
detectorBadAppletConstructor=BadAppletConstructor|false
detectorBadResultSetAccess=BadResultSetAccess|true
detectorBadSyntaxForRegularExpression=BadSyntaxForRegularExpression|true
detectorBadUseOfReturnValue=BadUseOfReturnValue|true
detectorBadlyOverriddenAdapter=BadlyOverriddenAdapter|true
detectorCheckImmutableAnnotation=CheckImmutableAnnotation|true
detectorCloneIdiom=CloneIdiom|true
detectorComparatorIdiom=ComparatorIdiom|true
detectorConfusedInheritance=ConfusedInheritance|true
detectorConfusionBetweenInheritedAndOuterMethod=ConfusionBetweenInheritedAndOuterMethod|true
detectorDoInsideDoPrivileged=DoInsideDoPrivileged|true
detectorDontCatchIllegalMonitorStateException=DontCatchIllegalMonitorStateException|true
detectorDroppedException=DroppedException|true
detectorDumbMethodInvocations=DumbMethodInvocations|true
detectorDumbMethods=DumbMethods|true
detectorDuplicateBranches=DuplicateBranches|true
detectorEmptyZipFileEntry=EmptyZipFileEntry|true
detectorFindBadCast2=FindBadCast2|true
detectorFindBadForLoop=FindBadForLoop|true
detectorFindCircularDependencies=FindCircularDependencies|false
detectorFindDeadLocalStores=FindDeadLocalStores|true
detectorFindDoubleCheck=FindDoubleCheck|true
detectorFindEmptySynchronizedBlock=FindEmptySynchronizedBlock|true
detectorFindFieldSelfAssignment=FindFieldSelfAssignment|true
detectorFindFinalizeInvocations=FindFinalizeInvocations|true
detectorFindFloatEquality=FindFloatEquality|true
detectorFindHEmismatch=FindHEmismatch|true
detectorFindInconsistentSync2=FindInconsistentSync2|true
detectorFindJSR166LockMonitorenter=FindJSR166LockMonitorenter|true
detectorFindLocalSelfAssignment2=FindLocalSelfAssignment2|true
detectorFindMaskedFields=FindMaskedFields|true
detectorFindMismatchedWaitOrNotify=FindMismatchedWaitOrNotify|true
detectorFindNakedNotify=FindNakedNotify|true
detectorFindNonSerializableStoreIntoSession=FindNonSerializableStoreIntoSession|true
detectorFindNonSerializableValuePassedToWriteObject=FindNonSerializableValuePassedToWriteObject|true
detectorFindNonShortCircuit=FindNonShortCircuit|true
detectorFindNullDeref=FindNullDeref|true
detectorFindOpenStream=FindOpenStream|true
detectorFindPuzzlers=FindPuzzlers|true
detectorFindRefComparison=FindRefComparison|true
detectorFindReturnRef=FindReturnRef|true
detectorFindRunInvocations=FindRunInvocations|true
detectorFindSelfComparison=FindSelfComparison|true
detectorFindSelfComparison2=FindSelfComparison2|true
detectorFindSleepWithLockHeld=FindSleepWithLockHeld|true
detectorFindSpinLoop=FindSpinLoop|true
detectorFindSqlInjection=FindSqlInjection|true
detectorFindTwoLockWait=FindTwoLockWait|true
detectorFindUncalledPrivateMethods=FindUncalledPrivateMethods|true
detectorFindUnconditionalWait=FindUnconditionalWait|true
detectorFindUninitializedGet=FindUninitializedGet|true
detectorFindUnrelatedTypesInGenericContainer=FindUnrelatedTypesInGenericContainer|true
detectorFindUnreleasedLock=FindUnreleasedLock|true
detectorFindUnsyncGet=FindUnsyncGet|true
detectorFindUselessControlFlow=FindUselessControlFlow|true
detectorHugeSharedStringConstants=HugeSharedStringConstants|true
detectorIDivResultCastToDouble=IDivResultCastToDouble|true
detectorIncompatMask=IncompatMask|true
detectorInefficientMemberAccess=InefficientMemberAccess|false
detectorInefficientToArray=InefficientToArray|true
detectorInfiniteLoop=InfiniteLoop|true
detectorInfiniteRecursiveLoop=InfiniteRecursiveLoop|true
detectorInfiniteRecursiveLoop2=InfiniteRecursiveLoop2|false
detectorInheritanceUnsafeGetResource=InheritanceUnsafeGetResource|true
detectorInitializationChain=InitializationChain|true
detectorInstantiateStaticClass=InstantiateStaticClass|true
detectorInvalidJUnitTest=InvalidJUnitTest|true
detectorIteratorIdioms=IteratorIdioms|true
detectorLazyInit=LazyInit|true
detectorLoadOfKnownNullValue=LoadOfKnownNullValue|true
detectorMethodReturnCheck=MethodReturnCheck|true
detectorMultithreadedInstanceAccess=MultithreadedInstanceAccess|true
detectorMutableLock=MutableLock|true
detectorMutableStaticFields=MutableStaticFields|true
detectorNaming=Naming|true
detectorNumberConstructor=NumberConstructor|true
detectorPreferZeroLengthArrays=PreferZeroLengthArrays|true
detectorPublicSemaphores=PublicSemaphores|false
detectorQuestionableBooleanAssignment=QuestionableBooleanAssignment|true
detectorReadReturnShouldBeChecked=ReadReturnShouldBeChecked|true
detectorRedundantInterfaces=RedundantInterfaces|true
detectorRuntimeExceptionCapture=RuntimeExceptionCapture|true
detectorSerializableIdiom=SerializableIdiom|true
detectorStartInConstructor=StartInConstructor|true
detectorStringConcatenation=StringConcatenation|true
detectorSuperfluousInstanceOf=SuperfluousInstanceOf|true
detectorSuspiciousThreadInterrupted=SuspiciousThreadInterrupted|true
detectorSwitchFallthrough=SwitchFallthrough|true
detectorURLProblems=URLProblems|true
detectorUncallableMethodOfAnonymousClass=UncallableMethodOfAnonymousClass|true
detectorUnnecessaryMath=UnnecessaryMath|true
detectorUnreadFields=UnreadFields|true
detectorUseObjectEquals=UseObjectEquals|false
detectorUselessSubclassMethod=UselessSubclassMethod|false
detectorVarArgsProblems=VarArgsProblems|true
detectorVolatileUsage=VolatileUsage|true
detectorWaitInLoop=WaitInLoop|true
detectorWrongMapIterator=WrongMapIterator|true
detectorXMLFactoryBypass=XMLFactoryBypass|true
detector_threshold=2
filter_settings=Medium|STYLE,MALICIOUS_CODE,BAD_PRACTICE,CORRECTNESS,I18N,PERFORMANCE,MT_CORRECTNESS|false
filter_settings_neg=|
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.sat4j.core</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>com.omondo.uml.enterprise.Builder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>net.sourceforge.metrics.builder</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>net.sourceforge.metrics.nature</nature>
<nature>org.eclipse.pde.PluginNature</nature>
</natures>
</projectDescription>
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: %bundleName
Bundle-SymbolicName: org.sat4j.core
Bundle-Version: 9.9.9.token
Export-Package: org.sat4j,
org.sat4j.core,
org.sat4j.minisat,
org.sat4j.minisat.constraints,
org.sat4j.minisat.constraints.card,
org.sat4j.minisat.constraints.cnf,
org.sat4j.minisat.core,
org.sat4j.minisat.learning,
org.sat4j.minisat.orders,
org.sat4j.minisat.restarts,
org.sat4j.minisat.uip,
org.sat4j.opt,
org.sat4j.reader,
org.sat4j.specs,
org.sat4j.tools
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Built-By: Daniel Le Berre
Main-Class: org.sat4j.BasicLauncher
Specification-Title: SAT4J
Specification-Version: NA
Specification-Vendor: Daniel Le Berre
Implementation-Title: SAT4J
Implementation-Version: 2.0
Implementation-Vendor: CRIL CNRS UMR 8188 - Universite d'Artois
Bundle-RequiredExecutionEnvironment: J2SE-1.4
source.. = src/
bin.includes = META-INF/,\
.,\
plugin.properties,\
src/main/resources/about.html
###############################################################################
# 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.
#
# 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++.
#
###############################################################################
bundleName = SAT4J Core
providerName = CRIL CNRS UMR 8188 - Universite d'Artois
<?xml version="1.0" encoding="UTF-8"?><project>
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.pom</artifactId>
<version>2.0.0</version>
</parent>
<artifactId>org.sat4j.core</artifactId>
<name>SAT4J core</name>
</project>
This diff is collapsed.
/*******************************************************************************
* 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.
*
* 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++.
*
*******************************************************************************/
package org.sat4j;
import java.io.PrintWriter;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.TimeoutException;
/**
* This class is intended to be used by launchers to solve optimization
* problems, i.e. problems for which a loop is needed to find the optimal
* solution.
*
* @author leberre
*
*/
public abstract class AbstractOptimizationLauncher extends AbstractLauncher {
/**
*
*/
private static final long serialVersionUID = 1L;
private static final String CURRENT_OPTIMUM_VALUE_PREFIX = "o "; //$NON-NLS-1$
@Override
protected void displayResult() {
displayAnswer();
log("Total wall clock time (ms): " //$NON-NLS-1$
+ (System.currentTimeMillis() - getBeginTime()) / 1000.0);
}
protected void displayAnswer(){
if (solver == null)
return;
PrintWriter out = getLogWriter();
solver.printStat(out, COMMENT_PREFIX);
ExitCode exitCode = getExitCode();
out.println(ANSWER_PREFIX + exitCode);
if (exitCode == ExitCode.SATISFIABLE
|| exitCode == ExitCode.OPTIMUM_FOUND) {
out.print(SOLUTION_PREFIX);
getReader().decode(solver.model(), out);
out.println();
IOptimizationProblem optproblem = (IOptimizationProblem) solver;
if (!optproblem.hasNoObjectiveFunction()) {
log("objective function=" + optproblem.calculateObjective()); //$NON-NLS-1$
}
}
}
@Override
protected void solve(IProblem problem) throws TimeoutException {
boolean isSatisfiable = false;
IOptimizationProblem optproblem = (IOptimizationProblem) problem;
try {
while (optproblem.admitABetterSolution()) {
if (!isSatisfiable) {
if (optproblem.nonOptimalMeansSatisfiable()) {
setExitCode(ExitCode.SATISFIABLE);
if (optproblem.hasNoObjectiveFunction()) {
return;
}
log("SATISFIABLE"); //$NON-NLS-1$
}
isSatisfiable = true;
log("OPTIMIZING..."); //$NON-NLS-1$
}
log("Got one! Elapsed wall clock time (in seconds):" //$NON-NLS-1$
+ (System.currentTimeMillis() - getBeginTime())
/ 1000.0);
getLogWriter().println(
CURRENT_OPTIMUM_VALUE_PREFIX
+ optproblem.calculateObjective());
optproblem.discard();
}
if (isSatisfiable) {
setExitCode(ExitCode.OPTIMUM_FOUND);
} else {
setExitCode(ExitCode.UNSATISFIABLE);
}
} catch (ContradictionException ex) {
assert isSatisfiable;
setExitCode(ExitCode.OPTIMUM_FOUND);
}
}
}
/*******************************************************************************
* 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.
*
* 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++.
*
*******************************************************************************/
package org.sat4j;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
/**
* Very simple launcher, to be used during the SAT competition or the SAT race
* for instance.
*
* @author daniel
*
*/
public class BasicLauncher<T extends ISolver> extends AbstractLauncher {
/**
*
*/
private static final long serialVersionUID = 1L;
private final ASolverFactory<T> factory;
public BasicLauncher(ASolverFactory<T> factory) {
this.factory = factory;
}
/**
* Lance le prouveur sur un fichier Dimacs.
*
* @param args
* doit contenir le nom d'un fichier Dimacs, eventuellement compress?.
*/
public static void main(final String[] args) {
BasicLauncher<ISolver> lanceur = new BasicLauncher<ISolver>(
SolverFactory.instance());
lanceur.run(args);
System.exit(lanceur.getExitCode().value());
}
protected ISolver configureSolver(String[] args) {
ISolver asolver = factory.defaultSolver();
asolver.setTimeout(Integer.MAX_VALUE);
asolver.setDBSimplificationAllowed(true);
log(asolver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
return asolver;
}
@Override
protected Reader createReader(ISolver solver, String problemname) {
return new InstanceReader(solver);
}
@Override
public void usage() {
log("java -jar sat4j-core.jar <cnffile>");
}
@Override
protected String getInstanceName(String[] args) {
assert args.length == 1;
return args[0];
}
}
/*******************************************************************************
* 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.
*
* 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++.
*
*******************************************************************************/
package org.sat4j;
/**
* Enumeration allowing to manage easily exit code for the SAT and PB
* Competitions.
*
* @author leberre
*
*/
public class ExitCode {
public static final ExitCode OPTIMUM_FOUND = new ExitCode(30, "OPTIMUM FOUND");
public static final ExitCode SATISFIABLE = new ExitCode(10, "SATISFIABLE");
public static final ExitCode UNKNOWN = new ExitCode(0, "UNKNOWN");
public static final ExitCode UNSATISFIABLE = new ExitCode(20,"UNSATISFIABLE");
/** value of the exit code. */
private final int value;
/** alternative textual representation of the exit code. */
private final String str;
/**
* creates an exit code with a given value and an alternative textual
* representation.
*
* @param i
* the value of the exit code
* @param str
* the alternative textual representation
*/
private ExitCode(final int i, final String str) {
this.value = i;
this.str = str;
}
/**
* @return the exit code value
*/
public int value() {
return value;
}
/**
* @return the name of the enum or the alternative textual representation if
* any.
*/
@Override
public String toString() {
return str;
}
}
/*******************************************************************************
* 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.
*
* 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++.
*
*******************************************************************************/
package org.sat4j;
import java.util.MissingResourceException;
import java.util.ResourceBundle;
/**
* That class is intented to manage internationalisation within the application.
*
* @author leberre
*
*/
public class Messages {
private static final String BUNDLE_NAME = "org.sat4j.messages"; //$NON-NLS-1$
private static final ResourceBundle RESOURCE_BUNDLE = ResourceBundle
.getBundle(BUNDLE_NAME);
/**
* No instances should be used. Use Messages.getString(key) to get localized
* message for key.
*
*/
private Messages() {
super();
}
public static String getString(String key) {
// TODO Auto-generated method stub
try {
return RESOURCE_BUNDLE.getString(key);
} catch (MissingResourceException e) {
return '!' + key + '!';
}
}
}
/*******************************************************************************
* 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.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the