org.sat4j.reader
Class DimacsReader

java.lang.Object
  extended by 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

Constructor Summary
DimacsReader(ISolver solver)
           
 
Method Summary
 java.lang.String decode(int[] model)
          Produce a model using the reader format.
 void disableNumberOfConstraintCheck()
           
 void parseInstance(java.io.LineNumberReader in)
           
 IProblem parseInstance(java.lang.String filename)
          Remplit un prouveur ?
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

DimacsReader

public DimacsReader(ISolver solver)
Method Detail

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.