org.sat4j.sat
Class Lanceur

java.lang.Object
  extended by org.sat4j.AbstractLauncher
      extended by org.sat4j.sat.Lanceur
All Implemented Interfaces:
Serializable

public class Lanceur
extends AbstractLauncher

This class is used to launch the SAT solvers from the command line. It is compliant with the SAT competition (www.satcompetition.org) I/O format. The launcher is to be used as follows:

                [solvername] filename [key=value]*
 
If no solver name is given, then the default solver of the solver factory is used (@see org.sat4j.core.ASolverFactory#defaultSolver()).

Author:
leberre
See Also:
Serialized Form

Field Summary
protected  ASolverFactory<ISolver> factory
           
 
Fields inherited from class org.sat4j.AbstractLauncher
ANSWER_PREFIX, beginTime, COMMENT_PREFIX, exitCode, out, reader, shutdownHook, SOLUTION_PREFIX, solver
 
Constructor Summary
Lanceur()
           
 
Method Summary
protected  ISolver configureSolver(String[] args)
          Configure the solver according to the command line parameters.
protected  Reader createReader(ISolver theSolver, String problemname)
           
 void displayLicense()
           
protected  String getInstanceName(String[] args)
           
static void main(String[] args)
          Lance le prouveur sur un fichier Dimacs.
protected  IProblem readProblem(String problemname)
          Reads a problem file from the command line.
 void usage()
           
 
Methods inherited from class org.sat4j.AbstractLauncher
displayHeader, displayResult, getBeginTime, getExitCode, getLogWriter, getReader, log, run, setExitCode, setLogWriter, setSilent, showAvailableSolvers, solve
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

factory

protected ASolverFactory<ISolver> factory
Constructor Detail

Lanceur

public Lanceur()
Method Detail

main

public static void main(String[] args)
Lance le prouveur sur un fichier Dimacs.

Parameters:
args - doit contenir le nom d'un fichier Dimacs, eventuellement compress?.

configureSolver

protected ISolver configureSolver(String[] args)
Configure the solver according to the command line parameters.

Specified by:
configureSolver in class AbstractLauncher
Parameters:
args - the command line
Returns:
a solver properly configured.

createReader

protected Reader createReader(ISolver theSolver,
                              String problemname)
Specified by:
createReader in class AbstractLauncher

displayLicense

public void displayLicense()
Overrides:
displayLicense in class AbstractLauncher

usage

public void usage()
Specified by:
usage in class AbstractLauncher

getInstanceName

protected String getInstanceName(String[] args)
Specified by:
getInstanceName in class AbstractLauncher

readProblem

protected IProblem readProblem(String problemname)
                        throws FileNotFoundException,
                               ParseFormatException,
                               IOException,
                               ContradictionException
Description copied from class: AbstractLauncher
Reads a problem file from the command line.

Overrides:
readProblem in class AbstractLauncher
Parameters:
problemname - the fully qualified name of the problem.
Returns:
a reference to the problem to solve
Throws:
FileNotFoundException - if the file is not found
ParseFormatException - if the problem is not expressed using the right format
IOException - for other IO problems
ContradictionException - if the problem is found trivially unsat


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.