org.sat4j.reader

Class JSONReader<S extends ISolver>

java.lang.Object

org.sat4j.reader.Reader

org.sat4j.reader.JSONReader<S>

Type Parameters:

S - the type of solver to feed.

Direct Known Subclasses:

JSONPBReader

public class JSONReader<S extends ISolver>
extends Reader

Simple JSON reader for clauses and cardinality constraints. Clauses are represented as an array of Dimacs literals (non zero integers). Cardinality constraints are represented like a clause for its left hand side, a comparator (a string) and a number. [[-1,-2,-3],[[1,-2,3],'>',2],[4,-3,6]] for instance represents three constraints, two clauses and the cardinality constraint x1 + not x2 + x3 > 2.

Since:

2.3.3

Author:

leberre

Field Summary

Fields

Modifier and Type	Field and Description
static String	CARD
static String	CLAUSE
String	constraint
String	formula
protected S	solver

Constructor Summary

Constructors

Constructor and Description
JSONReader(S solver)

Method Summary

Methods

Modifier and Type	Method and Description
protected String	constraintRegexp()
String	decode(int[] model) Deprecated.
void	decode(int[] model, PrintWriter out) Produce a model using the reader format on a provided printwriter.
protected IVecInt	getLiterals(String constraint)
protected void	handleCard(String constraint)
protected void	handleNotHandled(String constraint)
IProblem	parseInstance(InputStream in) Read a file from a stream.
ISolver	parseString(String json)

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

solver

protected final S extends ISolver solver

CLAUSE

public static final String CLAUSE

See Also:

Constant Field Values

CARD

public static final String CARD

See Also:

Constant Field Values

constraint

public final String constraint

formula

public final String formula

Constructor Detail

JSONReader

public JSONReader(S solver)

Method Detail

constraintRegexp

protected String constraintRegexp()

handleNotHandled

protected void handleNotHandled(String constraint)
                         throws ParseFormatException,
                                ContradictionException

Throws:

ParseFormatException

ContradictionException

getLiterals

protected IVecInt getLiterals(String constraint)
                       throws ParseFormatException

Throws:

ParseFormatException

handleCard

protected void handleCard(String constraint)
                   throws ParseFormatException,
                          ContradictionException

Throws:

ParseFormatException

ContradictionException

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.

parseString

public ISolver parseString(String json)
                    throws ParseFormatException,
                           ContradictionException

Throws:

ParseFormatException

ContradictionException

decode

@Deprecated
public String decode(int[] model)

Deprecated.

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