org.sat4j.tools
Class DimacsArrayReader

java.lang.Object
  org.sat4j.tools.DimacsArrayReader

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

ExtendedDimacsArrayReader

public class DimacsArrayReader
extends Object
implements Serializable

Very simple Dimacs array reader. Allow solvers to read the constraints from arrays that effectively contain Dimacs formatted lines (without the terminating 0). Adaptation of org.sat4j.reader.DimacsReader.

Author:

dlb, fuhs

See Also:

Serialized Form

Field Summary

protected ISolver

solver

Constructor Summary

DimacsArrayReader(ISolver solver)

Method Summary

String	decode(int[] model)
protected ISolver	getSolver()
protected boolean	handleConstr(int gateType, int output, int[] inputs)
ISolver	parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)

Methods inherited from class java.lang.Object

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

Field Detail

solver

protected final ISolver solver

Constructor Detail

DimacsArrayReader

public DimacsArrayReader(ISolver solver)

Method Detail

handleConstr

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

Throws:

ContradictionException

parseInstance

public ISolver parseInstance(int[] gateType,
                             int[] outputs,
                             int[][] inputs,
                             int maxVar)
                      throws ContradictionException

Parameters:

gateType - gateType[i] is the type of gate i according to the Extended Dimacs specs; ignored in DimacsArrayReader, but important for inheriting classes

outputs - outputs[i] is the number of the output; ignored in DimacsArrayReader

inputs - inputs[i] contains the clauses in DimacsArrayReader; an overriding class might have it contain the inputs of the current gate

maxVar - the maximum number of assigned ids

Throws:

ContradictionException - si le probleme est trivialement inconsitant

decode

public String decode(int[] model)

getSolver

protected ISolver getSolver()