org.sat4j.tools
Class DimacsArrayReader

java.lang.Object
  extended by 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()


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.