org.sat4j.reader

Class LecteurDimacs

java.lang.Object

org.sat4j.reader.Reader

org.sat4j.reader.LecteurDimacs

All Implemented Interfaces:

java.io.Serializable

public class LecteurDimacs
extends Reader
implements java.io.Serializable

Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader because it does not split the input file into strings but reads and interpret the input char by char. Hence, it is a bit more difficult to read and to modify than DimacsReader. This reader is used during the SAT Competitions.

Author:

laihem, leberre

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
LecteurDimacs(ISolver s)

Method Summary

Modifier and Type	Method and Description
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.
IProblem	parseInstance(java.io.InputStream input) Read a file from a 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

Constructor Detail

LecteurDimacs

public LecteurDimacs(ISolver s)

Method Detail

parseInstance

public final IProblem parseInstance(java.io.InputStream input)
                             throws ParseFormatException,
                                    ContradictionException,
                                    java.io.IOException

Description copied from class: Reader

Read a file from a stream. It is important to note that benchmarks are usually encoded in ASCII, not UTF8. As such, the only reasonable way to feed a solver from a stream is to use a stream.

Specified by:

parseInstance in class Reader

Parameters:

input - a stream containing the benchmark.

Returns:

the problem to solve (an ISolver in fact).

Throws:

ParseFormatException - if an error occurs during parsing.

ContradictionException - if the problem is found trivially inconsistent.

java.io.IOException - if an I/O error occurs.

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