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

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

Fields

Modifier and Type	Field and Description
protected Relation[]	relations

Constructor Summary

Constructors

Constructor and Description
CSPReader(ISolver solver, boolean allDiffCard)

Method Summary

Methods

Modifier and Type	Method and Description
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,
         boolean allDiffCard)

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.

manageAllowedTuples

protected void manageAllowedTuples(int relnum,
                       int arity,
                       int nbtuples)

beginInstance

public void beginInstance(String arg0)

Description copied from interface: ICSPCallback

signal the beginning of parsing

Specified by:

beginInstance in interface ICSPCallback

Parameters:

arg0 - name of the instance

beginDomainsSection

public void beginDomainsSection(int nbdomain)

Description copied from interface: ICSPCallback

callback called at the beginning of the domains declarations

Specified by:

beginDomainsSection in interface ICSPCallback

Parameters:

nbdomain - number of domains that will be declared

beginDomain

public void beginDomain(String id,
               int size)

Description copied from interface: ICSPCallback

callback called at the beginning of the declaration of one domain

Specified by:

beginDomain in interface ICSPCallback

Parameters:

id - identifier of the domain

size - number of values in the domain

addDomainValue

public void addDomainValue(int arg0)

Description copied from interface: ICSPCallback

add a single value to the current domain

Specified by:

addDomainValue in interface ICSPCallback

Parameters:

arg0 - value to add to the domain

addDomainValue

public void addDomainValue(int begin,
                  int end)

Description copied from interface: ICSPCallback

add the range of values [first..last] to the current domain

Specified by:

addDomainValue in interface ICSPCallback

Parameters:

begin - first value to add to the domain

end - last value to add to the domain

endDomain

public void endDomain()

Description copied from interface: ICSPCallback

ends the definition of the current domain

Specified by:

endDomain in interface ICSPCallback

endDomainsSection

public void endDomainsSection()

Description copied from interface: ICSPCallback

end the definition of all domains

Specified by:

endDomainsSection in interface ICSPCallback

beginVariablesSection

public void beginVariablesSection(int expectedNumberOfVariables)

Description copied from interface: ICSPCallback

callback called at the beginning of the variables declarations

Specified by:

beginVariablesSection in interface ICSPCallback

Parameters:

expectedNumberOfVariables - number of variables that will be declared

addVariable

public void addVariable(String idvar,
               String iddomain)

Description copied from interface: ICSPCallback

callback called to define a new variable

Specified by:

addVariable in interface ICSPCallback

Parameters:

idvar - identifier of the variable

iddomain - identifier of the variable domain

endVariablesSection

public void endVariablesSection()

Description copied from interface: ICSPCallback

end the definition of all variables

Specified by:

endVariablesSection in interface ICSPCallback

beginRelationsSection

public void beginRelationsSection(int nbrel)

Description copied from interface: ICSPCallback

callback called at the beginning of the relations declarations

Specified by:

beginRelationsSection in interface ICSPCallback

Parameters:

nbrel - number of relations that will be declared

beginRelation

public void beginRelation(String name,
                 int arity,
                 int nbTuples,
                 boolean isSupport)

Description copied from interface: ICSPCallback

callback called at the beginning of the declaration of one relation

Specified by:

beginRelation in interface ICSPCallback

Parameters:

name - identifier of the relation

arity - arity of the relation

nbTuples - number of tuples in the relation

isSupport - true if tuples represent support, false if tuples represent conflicts

addRelationTuple

public void addRelationTuple(int[] tuple)

Description copied from interface: ICSPCallback

add a single tuple to the current relation

Specified by:

addRelationTuple in interface ICSPCallback

Parameters:

tuple - tuple to add to the relation (contains arity elements)

endRelation

public void endRelation()

Description copied from interface: ICSPCallback

ends the definition of the current relation

Specified by:

endRelation in interface ICSPCallback

endRelationsSection

public void endRelationsSection()

Description copied from interface: ICSPCallback

end the definition of all relations

Specified by:

endRelationsSection in interface ICSPCallback

beginPredicatesSection

public void beginPredicatesSection(int arg0)

Description copied from interface: ICSPCallback

callback called at the beginning of the predicates declarations

Specified by:

beginPredicatesSection in interface ICSPCallback

Parameters:

arg0 - number of predicates that will be declared

beginPredicate

public void beginPredicate(String name)

Description copied from interface: ICSPCallback

callback called at the beginning of the declaration of one predicate

Specified by:

beginPredicate in interface ICSPCallback

Parameters:

name - identifier of the predicate

addFormalParameter

public void addFormalParameter(String name,
                      String type)

Description copied from interface: ICSPCallback

add a formal parameter to the current predicate

Specified by:

addFormalParameter in interface ICSPCallback

Parameters:

name - name of the parameter

type - type of the parameter

predicateExpression

public void predicateExpression(String expr)

Description copied from interface: ICSPCallback

provide the expression of the current predicate

Specified by:

predicateExpression in interface ICSPCallback

Parameters:

expr - the abstract syntax tree representing the expression

endPredicate

public void endPredicate()

Description copied from interface: ICSPCallback

ends the definition of the current predicate

Specified by:

endPredicate in interface ICSPCallback

endPredicatesSection

public void endPredicatesSection()

Description copied from interface: ICSPCallback

end the definition of all predicates

Specified by:

endPredicatesSection in interface ICSPCallback

beginConstraintsSection

public void beginConstraintsSection(int arg0)

Description copied from interface: ICSPCallback

callback called at the beginning of the constraints declarations

Specified by:

beginConstraintsSection in interface ICSPCallback

Parameters:

arg0 - number of constraints that will be declared

beginConstraint

public void beginConstraint(String name,
                   int arity)

Description copied from interface: ICSPCallback

callback called at the beginning of the declaration of one constraint

Specified by:

beginConstraint in interface ICSPCallback

Parameters:

name - identifier of the constraint

arity - arity of the constraint

constraintReference

public void constraintReference(String ref)

Description copied from interface: ICSPCallback

provide the definition of the current constraint

Specified by:

constraintReference in interface ICSPCallback

Parameters:

ref - the refererence to the definition of this constraint. May be a relation, a predicate or the name of a global constraint

addVariableToConstraint

public void addVariableToConstraint(String arg0)

Description copied from interface: ICSPCallback

declares that a variable is in the constraint scope

Specified by:

addVariableToConstraint in interface ICSPCallback

Parameters:

arg0 - name of the variable

addEffectiveParameter

public void addEffectiveParameter(String arg0)

Description copied from interface: ICSPCallback

add an effective parameter which is a simple variable to the current constraint

Specified by:

addEffectiveParameter in interface ICSPCallback

Parameters:

arg0 - name of the variable passed as parameter

addEffectiveParameter

public void addEffectiveParameter(int arg0)

Description copied from interface: ICSPCallback

add an effective parameter which is a simple integer

Specified by:

addEffectiveParameter in interface ICSPCallback

Parameters:

arg0 - value of the parameter

beginParameterList

public void beginParameterList()

Description copied from interface: ICSPCallback

begins the list tag for parameters of a constraint

Specified by:

beginParameterList in interface ICSPCallback

addIntegerItem

public void addIntegerItem(int arg0)

Description copied from interface: ICSPCallback

provides an integer value in a parameter list of a constraint

Specified by:

addIntegerItem in interface ICSPCallback

Parameters:

arg0 - value of current list item

addVariableItem

public void addVariableItem(String arg0)

Description copied from interface: ICSPCallback

provides the name of a variable in a parameter list of a constraint

Specified by:

addVariableItem in interface ICSPCallback

Parameters:

arg0 - name of the current list item

endParamaterList

public void endParamaterList()

Description copied from interface: ICSPCallback

ends the list tag for parameters of a constraint

Specified by:

endParamaterList in interface ICSPCallback

addConstantParameter

public void addConstantParameter(String arg0,
                        int arg1)

Description copied from interface: ICSPCallback

provides a constant value

Specified by:

addConstantParameter in interface ICSPCallback

constraintExpression

public void constraintExpression(String arg0)

Description copied from interface: ICSPCallback

provide the expression of the current constraint as an expression in a syntac chosen by the solver

Specified by:

constraintExpression in interface ICSPCallback

Parameters:

arg0 - the expression

endConstraint

public void endConstraint()

Description copied from interface: ICSPCallback

ends the definition of the current constraint

Specified by:

endConstraint in interface ICSPCallback

endConstraintsSection

public void endConstraintsSection()

Description copied from interface: ICSPCallback

end the definition of all constraints

Specified by:

endConstraintsSection in interface ICSPCallback

endInstance

public void endInstance()

Description copied from interface: ICSPCallback

signal the end of parsing

Specified by:

endInstance in interface ICSPCallback

parseInstance

public IProblem parseInstance(InputStream in)
                       throws ParseFormatException,
                              ContradictionException,
                              IOException

Description copied from class: Reader

Read a file from a stream. It is important to note that benchmarks are usually encoded in ASCII, not UTF8. As such, the only reasonable way to feed a solver from a stream is to use a stream.

Specified by:

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.