org.sat4j.tools

Class ExtendedDimacsArrayReader

java.lang.Object

org.sat4j.tools.DimacsArrayReader

org.sat4j.tools.ExtendedDimacsArrayReader

All Implemented Interfaces:

Serializable

public class ExtendedDimacsArrayReader
extends DimacsArrayReader

Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby Walsh in array representation (without the terminating 0). Adaptation of org.sat4j.reader.ExtendedDimacsReader.

Author:

leberre, fuhs

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
static int	AND
static int	ATLEAST
static int	ATMOST
static int	COUNT
static int	FALSE
static int	IFF
static int	IFTHENELSE
static int	IMPLIES
static int	NAND
static int	NOR
static int	NOT
static int	OR
static int	TRUE
static int	XNOR
static int	XOR

Fields inherited from class org.sat4j.tools.DimacsArrayReader

solver

Constructor Summary

Constructors

Constructor and Description
ExtendedDimacsArrayReader(ISolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
protected boolean	handleConstr(int gateType, int output, int[] inputs) Handles a single constraint (constraint == Extended Dimacs circuit gate).

Methods inherited from class org.sat4j.tools.DimacsArrayReader

decode, getSolver, parseInstance

Methods inherited from class java.lang.Object

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

Field Detail

FALSE

public static final int FALSE

See Also:

Constant Field Values

TRUE

public static final int TRUE

See Also:

Constant Field Values

NOT

public static final int NOT

See Also:

Constant Field Values

AND

public static final int AND

See Also:

Constant Field Values

NAND

public static final int NAND

See Also:

Constant Field Values

OR

public static final int OR

See Also:

Constant Field Values

NOR

public static final int NOR

See Also:

Constant Field Values

XOR

public static final int XOR

See Also:

Constant Field Values

XNOR

public static final int XNOR

See Also:

Constant Field Values

IMPLIES

public static final int IMPLIES

See Also:

Constant Field Values

IFF

public static final int IFF

See Also:

Constant Field Values

IFTHENELSE

public static final int IFTHENELSE

See Also:

Constant Field Values

ATLEAST

public static final int ATLEAST

See Also:

Constant Field Values

ATMOST

public static final int ATMOST

See Also:

Constant Field Values

COUNT

public static final int COUNT

See Also:

Constant Field Values

Constructor Detail

ExtendedDimacsArrayReader

public ExtendedDimacsArrayReader(ISolver solver)

Method Detail

handleConstr

protected boolean handleConstr(int gateType,
                   int output,
                   int[] inputs)
                        throws ContradictionException

Handles a single constraint (constraint == Extended Dimacs circuit gate).

Overrides:

handleConstr in class DimacsArrayReader

Parameters:

gateType - the type of the gate in question

output - the number of the output of the gate in question

inputs - the numbers of the inputs of the gates in question; the array must have the corresponding length for the gate type unless arbitrary lengths are allowed (i.e., 0 for TRUE and FALSE, 1 for NOT, or 3 for ITE)

Returns:

true

Throws:

ContradictionException