org.sat4j.reader
Class DimacsReader

java.lang.Object
  org.sat4j.reader.Reader
      org.sat4j.reader.DimacsReader

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

CardDimacsReader, ExtendedDimacsReader

public class DimacsReader
extends Reader
implements 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

Field Summary

protected int	expectedNbOfConstr
protected ISolver	solver

Constructor Summary

DimacsReader(ISolver solver)

DimacsReader(ISolver solver, java.lang.String format)

Method Summary

java.lang.String	decode(int[] model) Produce a model using the reader format.
void	decode(int[] model, java.io.PrintWriter out) Produce a model using the reader format on a provided printwriter.
void	disableNumberOfConstraintCheck()
protected ISolver	getSolver()
protected boolean	handleConstr(java.lang.String line, IVecInt literals)
IProblem	parseInstance(java.io.Reader in)
protected void	readConstrs(java.io.LineNumberReader in)
protected void	readProblemLine(java.io.LineNumberReader in)
protected void	skipComments(java.io.LineNumberReader in) Skip comments at the beginning of the input stream.

Methods inherited from class org.sat4j.reader.Reader

isVerbose, parseInstance, parseInstance, setVerbosity

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

expectedNbOfConstr

protected int expectedNbOfConstr

solver

protected final ISolver solver

Constructor Detail

DimacsReader

public DimacsReader(ISolver solver)

DimacsReader

public DimacsReader(ISolver solver,
                    java.lang.String format)

Method Detail

disableNumberOfConstraintCheck

public void disableNumberOfConstraintCheck()

skipComments

protected void skipComments(java.io.LineNumberReader in)
                     throws java.io.IOException

Skip comments at the beginning of the input stream.

Parameters:

in - the input stream

Throws:

java.io.IOException - if an IO problem occurs.

readProblemLine

protected void readProblemLine(java.io.LineNumberReader in)
                        throws java.io.IOException,
                               ParseFormatException

Parameters:

in - the input stream

Throws:

java.io.IOException - iff an IO occurs

ParseFormatException - if the input stream does not comply with the DIMACS format.

readConstrs

protected void readConstrs(java.io.LineNumberReader in)
                    throws java.io.IOException,
                           ParseFormatException,
                           ContradictionException

Parameters:

in - the input stream

Throws:

java.io.IOException - iff an IO problems occurs

ParseFormatException - if the input stream does not comply with the DIMACS format.

ContradictionException - si le probl?me est trivialement inconsistant.

handleConstr

protected boolean handleConstr(java.lang.String line,
                               IVecInt literals)
                        throws ContradictionException

Throws:

ContradictionException

parseInstance

public final IProblem parseInstance(java.io.Reader in)
                             throws ParseFormatException,
                                    ContradictionException,
                                    java.io.IOException

Specified by:

parseInstance in class Reader

Throws:

ParseFormatException

ContradictionException

java.io.IOException

decode

public java.lang.String decode(int[] model)

Description copied from class: Reader

Produce a model using the reader format.

Specified by:

decode in class Reader

Parameters:

model - a model using the Dimacs format.

Returns:

a human readable view of the model.

decode

public void decode(int[] model,
                   java.io.PrintWriter out)

Description copied from class: Reader

Produce a model using the reader format on a provided printwriter.

Specified by:

decode in class Reader

Parameters:

model - a model using the Dimacs format.

out - the place where to display the model

getSolver

protected ISolver getSolver()