CSPReader (SAT4J 2.3.1 API)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.sat4j.reader
Class CSPReader

java.lang.Object
  org.sat4j.reader.Reader
      org.sat4j.reader.CSPReader

All Implemented Interfaces:: ICSPCallback

Direct Known Subclasses:: CSPExtSupportReader, CSPSupportReader

public class CSPReader
extends Reader
implements ICSPCallback
extends Reader
implements ICSPCallback

This class is a CSP to SAT translator that is able to read a CSP problem using the First CSP solver competition input format and that translates it into clausal and cardinality (equality) constraints. That code has not been tested very thoroughly yet and was written very quickly to meet the competition deadline :=)) There is plenty of room for improvement.

Author:: leberre

Field Summary
`protected Relation[]`	`relations`

Constructor Summary
`CSPReader(ISolver solver)`

Method Summary
`void`	`addConstantParameter(String arg0, int arg1)` provides a constant value
`void`	`addDomainValue(int arg0)` add a single value to the current domain
`void`	`addDomainValue(int begin, int end)` add the range of values [first..last] to the current domain
`void`	`addEffectiveParameter(int arg0)` add an effective parameter which is a simple integer
`void`	`addEffectiveParameter(String arg0)` add an effective parameter which is a simple variable to the current constraint
`void`	`addFormalParameter(String name, String type)` add a formal parameter to the current predicate
`void`	`addIntegerItem(int arg0)` provides an integer value in a parameter list of a constraint
`void`	`addRelationTuple(int[] tuple)` add a single tuple to the current relation
`void`	`addVariable(String idvar, String iddomain)` callback called to define a new variable
`void`	`addVariableItem(String arg0)` provides the name of a variable in a parameter list of a constraint
`void`	`addVariableToConstraint(String arg0)` declares that a variable is in the constraint scope
`void`	`beginConstraint(String name, int arity)` callback called at the beginning of the declaration of one constraint
`void`	`beginConstraintsSection(int arg0)` callback called at the beginning of the constraints declarations
`void`	`beginDomain(String id, int size)` callback called at the beginning of the declaration of one domain
`void`	`beginDomainsSection(int nbdomain)` callback called at the beginning of the domains declarations
`void`	`beginInstance(String arg0)` signal the beginning of parsing
`void`	`beginParameterList()` begins the list tag for parameters of a constraint
`void`	`beginPredicate(String name)` callback called at the beginning of the declaration of one predicate
`void`	`beginPredicatesSection(int arg0)` callback called at the beginning of the predicates declarations
`void`	`beginRelation(String name, int arity, int nbTuples, boolean isSupport)` callback called at the beginning of the declaration of one relation
`void`	`beginRelationsSection(int nbrel)` callback called at the beginning of the relations declarations
`void`	`beginVariablesSection(int expectedNumberOfVariables)` callback called at the beginning of the variables declarations
`void`	`constraintExpression(String arg0)` provide the expression of the current constraint as an expression in a syntac chosen by the solver
`void`	`constraintReference(String ref)` provide the definition of the current constraint
`String`	`decode(int[] model)` Produce a model using the reader format.
`void`	`decode(int[] model, PrintWriter out)` Produce a model using the reader format on a provided printwriter.
`void`	`endConstraint()` ends the definition of the current constraint
`void`	`endConstraintsSection()` end the definition of all constraints
`void`	`endDomain()` ends the definition of the current domain
`void`	`endDomainsSection()` end the definition of all domains
`void`	`endInstance()` signal the end of parsing
`void`	`endParamaterList()` ends the list tag for parameters of a constraint
`void`	`endPredicate()` ends the definition of the current predicate
`void`	`endPredicatesSection()` end the definition of all predicates
`void`	`endRelation()` ends the definition of the current relation
`void`	`endRelationsSection()` end the definition of all relations
`void`	`endVariablesSection()` end the definition of all variables
`protected void`	`manageAllowedTuples(int relnum, int arity, int nbtuples)`
`IProblem`	`parseInstance(InputStream in)` Read a file from a stream.
`IProblem`	`parseInstance(Reader in)` Read a file from a reader.
`void`	`predicateExpression(String expr)` provide the expression of the current predicate

Methods inherited from class org.sat4j.reader.Reader
`isVerbose, parseInstance, setVerbosity`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

relations

protected Relation[] relations

Constructor Detail

CSPReader

public CSPReader(ISolver solver)

Method Detail

parseInstance

public final IProblem parseInstance(Reader in)
                             throws ParseFormatException,
                                    ContradictionException,
                                    IOException

Description copied from class: Reader

Read a file from a reader. Do not use that method, it is no longer supported.

Overrides:: 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.
See Also:: Reader.parseInstance(InputStream)

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

decode

public String decode(int[] model)

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.