org.sat4j.reader
Class DimacsReader

java.lang.Object
  extended by org.sat4j.reader.Reader
      extended by org.sat4j.reader.DimacsReader
All Implemented Interfaces:
Serializable
Direct Known Subclasses:
GroupedCNFReader

public class DimacsReader
extends Reader
implements 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  String formatString
           
protected  IVecInt literals
           
protected  EfficientScanner scanner
           
protected  ISolver solver
           
 
Constructor Summary
DimacsReader(ISolver solver)
           
DimacsReader(ISolver solver, String format)
           
 
Method Summary
 String decode(int[] model)
          Produce a model using the reader format.
 void decode(int[] model, PrintWriter out)
          Produce a model using the reader format on a provided printwriter.
 void disableNumberOfConstraintCheck()
           
protected  void flushConstraint()
           
protected  ISolver getSolver()
           
protected  boolean handleLine()
           
 IProblem parseInstance(InputStream in)
          Read a file from a stream.
protected  void readConstrs()
           
protected  void readProblemLine()
           
protected  void skipComments()
          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

formatString

protected final String formatString

scanner

protected EfficientScanner scanner
Since:
2.1

literals

protected IVecInt literals
Since:
2.1
Constructor Detail

DimacsReader

public DimacsReader(ISolver solver)

DimacsReader

public DimacsReader(ISolver solver,
                    String format)
Method Detail

disableNumberOfConstraintCheck

public void disableNumberOfConstraintCheck()

skipComments

protected void skipComments()
                     throws IOException
Skip comments at the beginning of the input stream.

Parameters:
in - the input stream
Throws:
IOException - if an IO problem occurs.
Since:
2.1

readProblemLine

protected void readProblemLine()
                        throws IOException,
                               ParseFormatException
Parameters:
in - the input stream
Throws:
IOException - iff an IO occurs
ParseFormatException - if the input stream does not comply with the DIMACS format.
Since:
2.1

readConstrs

protected void readConstrs()
                    throws IOException,
                           ParseFormatException,
                           ContradictionException
Parameters:
in - the input stream
Throws:
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.
Since:
2.1

flushConstraint

protected void flushConstraint()
                        throws ContradictionException
Throws:
ContradictionException
Since:
2.1

handleLine

protected boolean handleLine()
                      throws ContradictionException,
                             IOException,
                             ParseFormatException
Throws:
ContradictionException
IOException
ParseFormatException
Since:
2.1

parseInstance

public IProblem parseInstance(InputStream in)
                       throws ParseFormatException,
                              ContradictionException,
                              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:
in - 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.
IOException - if an I/O error occurs.

decode

public 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,
                   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()


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