org.sat4j.reader
Class DimacsReader
java.lang.Object
org.sat4j.reader.DimacsReader
- All Implemented Interfaces:
- java.io.Serializable, Reader
- Direct Known Subclasses:
- CardDimacsReader, ExtendedDimacsReader
public class DimacsReader
- extends java.lang.Object
- implements Reader, java.io.Serializable
Very simple Dimacs file parser. Allow solvers to read the constraints from a
Dimacs formatted file. It should be used that way:
DimacsReader solver = new DimacsReader(SolverFactory.OneSolver());
solver.readInstance("mybench.cnf");
if (solver.isSatisfiable()) {
// SAT case
} else {
// UNSAT case
}
That parser is not used for efficiency reasons. It will be updated with Java
1.5 scanner feature.
- Version:
- 1.0
- Author:
- dlb, or
- See Also:
- Serialized Form
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
DimacsReader
public DimacsReader(ISolver solver)
disableNumberOfConstraintCheck
public void disableNumberOfConstraintCheck()
parseInstance
public IProblem parseInstance(java.lang.String filename)
throws java.io.FileNotFoundException,
ParseFormatException,
java.io.IOException,
ContradictionException
- Remplit un prouveur ? partir d'un fichier Dimacs.
- Specified by:
parseInstance
in interface Reader
- Parameters:
filename
- le nom du fichier Dimacs (?ventuellement compress?)
- Throws:
java.io.FileNotFoundException
- si le fichier n'est pas trouv?
ParseFormatException
- si le fichier ne respecte pas le format Dimacs
java.io.IOException
- pour un autre probl?me d'entr?e/sortie
ContradictionException
- si le probl?me est trivialement inconsitant
parseInstance
public void parseInstance(java.io.LineNumberReader in)
throws ParseFormatException,
ContradictionException
- Parameters:
in
- the input stream
- Throws:
ParseFormatException
- if the input stream does not comply with the DIMACS format.
ContradictionException
- si le probl?me est trivialement inconsitant
decode
public java.lang.String decode(int[] model)
- Description copied from interface:
Reader
- Produce a model using the reader format.
- Specified by:
decode
in interface Reader
- Parameters:
model
- a model using the Dimacs format.
- Returns:
- a human readable view of the model.