org.sat4j.tools
Class ExtendedDimacsArrayToDimacsConverter

java.lang.Object
  org.sat4j.tools.DimacsArrayToDimacsConverter
      org.sat4j.tools.ExtendedDimacsArrayToDimacsConverter

All Implemented Interfaces:

java.io.Serializable

public class ExtendedDimacsArrayToDimacsConverter
extends DimacsArrayToDimacsConverter

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

Author:

leberre, fuhs

See Also:

Serialized Form

Field Summary

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.DimacsArrayToDimacsConverter

clauses, dimacs

Constructor Summary

ExtendedDimacsArrayToDimacsConverter(int bufSize)

Method Summary

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.DimacsArrayToDimacsConverter

decode, init, 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

ExtendedDimacsArrayToDimacsConverter

public ExtendedDimacsArrayToDimacsConverter(int bufSize)

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 DimacsArrayToDimacsConverter

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

Returns:

true

Throws:

ContradictionException