org.sat4j.pb.reader
Class OPBReader2005

java.lang.Object
  org.sat4j.reader.Reader
      org.sat4j.pb.reader.OPBReader2005

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

OPBReader2006

public class OPBReader2005
extends Reader
implements Serializable

Based on the "Official" reader for the Pseudo Boolean evaluation 2005. http://www.cril.univ-artois.fr/PB05/parser/SimpleParser.java provided by Olivier Roussel and Vasco Manquinho. Modified to comply with SAT4J architecture by Mederic Baron Updated since then by Daniel Le Berre

Author:

or, vm, mederic baron, leberre

See Also:

Serialized Form

Field Summary

protected IVec<BigInteger>	coeffs
protected BigInteger	d
protected boolean	hasObjFunc
protected boolean	hasVariablesExplanation
protected IVecInt	lits
protected int	nbConstr
protected int	nbConstraintsRead
protected int	nbVars
protected String	operator
protected IPBSolver	solver

Constructor Summary

OPBReader2005(IPBSolver solver)

Method Summary

protected void	beginConstraint() callback called before we read a constraint
protected void	beginObjective() callback called before we read the objective function
protected void	checkId(StringBuffer s)
protected void	constraintRelOp(String relop) callback called when we read the relational operator of a constraint
protected void	constraintRightTerm(BigInteger val) callback called when we read the right term of a constraint (also known as the degree)
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.
protected void	endConstraint()
protected void	endObjective() callback called after we've read the objective function
protected boolean	eof() return true iff we've reached EOF
protected boolean	eol()
protected char	get() get the next character from the stream
IVec<BigInteger>	getCoeffs()
IVecInt	getListOfVariables()
ObjectiveFunction	getObjectiveFunction()
IVecInt	getVars()
protected boolean	isGoodFirstCharacter(char c)
protected boolean	isGoodFollowingCharacter(char c)
protected void	metaData(int nbvar, int nbconstr) callback called when we get the number of variables and the expected number of constraints
void	parse() parses the file and uses the callbacks to send to send the data back to the program
IProblem	parseInstance(InputStream in) Read a file from a stream.
IProblem	parseInstance(Reader input) Read a file from a reader.
protected void	putback(char c) put back a character into the stream (only one chr can be put back)
protected void	readConstraint() read a constraint calls beginConstraint, constraintTerm and endConstraint
protected boolean	readIdentifier(StringBuffer s) read an identifier from stream and store it in s
void	readInteger(StringBuffer s) read a integer from file
protected void	readMetaData() read the first comment line to get the number of variables and the number of constraints in the file calls metaData with the data that was read
protected void	readObjective() read the objective line (if any) calls beginObjective, objectiveTerm and endObjective
protected void	readTerm(StringBuffer coeff, StringBuffer var) read a term into coeff and var
protected void	readVariablesExplanation()
String	readWord() read a word from file
protected void	skipSpaces() skip white spaces
protected int	translateVarToId(String var)

Methods inherited from class org.sat4j.reader.Reader

isVerbose, parseInstance, setVerbosity

Methods inherited from class java.lang.Object

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

Field Detail

solver

protected final IPBSolver solver

lits

protected final IVecInt lits

coeffs

protected final IVec<BigInteger> coeffs

d

protected BigInteger d

operator

protected String operator

hasObjFunc

protected boolean hasObjFunc

hasVariablesExplanation

protected boolean hasVariablesExplanation

nbVars

protected int nbVars

nbConstr

protected int nbConstr

nbConstraintsRead

protected int nbConstraintsRead

Constructor Detail

OPBReader2005

public OPBReader2005(IPBSolver solver)

Method Detail

metaData

protected void metaData(int nbvar,
                        int nbconstr)

callback called when we get the number of variables and the expected number of constraints

Parameters:

nbvar - the number of variables

nbconstr - the number of contraints

beginObjective

protected void beginObjective()

callback called before we read the objective function

endObjective

protected void endObjective()

callback called after we've read the objective function

beginConstraint

protected void beginConstraint()

callback called before we read a constraint

endConstraint

protected void endConstraint()
                      throws ContradictionException

Throws:

ContradictionException

translateVarToId

protected int translateVarToId(String var)
                        throws ParseFormatException

Throws:

ParseFormatException

constraintRelOp

protected void constraintRelOp(String relop)

callback called when we read the relational operator of a constraint

Parameters:

relop - the relational oerator (>= or =)

constraintRightTerm

protected void constraintRightTerm(BigInteger val)

callback called when we read the right term of a constraint (also known as the degree)

Parameters:

val - the degree of the constraint

get

protected char get()
            throws IOException

get the next character from the stream

Throws:

IOException

getVars

public IVecInt getVars()

getCoeffs

public IVec<BigInteger> getCoeffs()

putback

protected void putback(char c)

put back a character into the stream (only one chr can be put back)

eof

protected boolean eof()

return true iff we've reached EOF

eol

protected boolean eol()

skipSpaces

protected void skipSpaces()
                   throws IOException

skip white spaces

Throws:

IOException

readWord

public String readWord()
                throws IOException

read a word from file

Returns:

the word we read

Throws:

IOException

readInteger

public void readInteger(StringBuffer s)
                 throws IOException

read a integer from file

Parameters:

s - a StringBuffer to store the integer that was read

Throws:

IOException

readIdentifier

protected boolean readIdentifier(StringBuffer s)
                          throws IOException,
                                 ParseFormatException

read an identifier from stream and store it in s

Returns:

the identifier we read or null

Throws:

IOException

ParseFormatException

isGoodFirstCharacter

protected boolean isGoodFirstCharacter(char c)

isGoodFollowingCharacter

protected boolean isGoodFollowingCharacter(char c)

checkId

protected void checkId(StringBuffer s)
                throws ParseFormatException

Throws:

ParseFormatException

readMetaData

protected void readMetaData()
                     throws IOException,
                            ParseFormatException

read the first comment line to get the number of variables and the number of constraints in the file calls metaData with the data that was read

Throws:

IOException

ParseException

ParseFormatException

readTerm

protected void readTerm(StringBuffer coeff,
                        StringBuffer var)
                 throws IOException,
                        ParseFormatException

read a term into coeff and var

Parameters:

coeff - the coefficient of the variable

var - the identifier we read

Throws:

IOException

ParseException

ParseFormatException

readVariablesExplanation

protected void readVariablesExplanation()
                                 throws IOException,
                                        ParseFormatException

Throws:

IOException

ParseFormatException

readObjective

protected void readObjective()
                      throws IOException,
                             ParseFormatException

read the objective line (if any) calls beginObjective, objectiveTerm and endObjective

Throws:

IOException

ParseException

ParseFormatException

readConstraint

protected void readConstraint()
                       throws IOException,
                              ParseFormatException,
                              ContradictionException

read a constraint calls beginConstraint, constraintTerm and endConstraint

Throws:

ParseException

IOException

ContradictionException

ParseFormatException

parse

public void parse()
           throws IOException,
                  ParseFormatException,
                  ContradictionException

parses the file and uses the callbacks to send to send the data back to the program

Throws:

IOException

ParseException

ContradictionException

ParseFormatException

parseInstance

public IProblem parseInstance(Reader input)
                       throws ParseFormatException,
                              ContradictionException

Description copied from class: Reader

Read a file from a reader. Do not use that method, it is no longer supported.

Overrides:

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.

See Also:

Reader.parseInstance(InputStream)

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

getObjectiveFunction

public ObjectiveFunction getObjectiveFunction()

getListOfVariables

public IVecInt getListOfVariables()

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.