PAKCS
Exported names: Imported modules:

Module XFD.FD

Library for finite domain constraint solving.

An FD problem is specified as an expression of type FDConstr using the constraints and expressions offered in this library. FD variables are created by the operation domain. An FD problem is solved by calling solveFD with labeling options, the FD variables whose values should be included in the output, and a constraint. Hence, the typical program structure to solve an FD problem is as follows: 

main :: [Int]
main =
  let fdvars  = take n (domain u o)
      fdmodel = {description of FD problem}
   in solveFD {options} fdvars fdmodel

where n are the number of variables and [u..o] is the range of their possible values.

Note that this library defines the operation to describe an FD problem. The actual solveFD operations are defined in the solver libraries which also exports this library.

Author: Michael Hanus, Tom Hueser

Version: March 2016

Summary of exported operations:

domainWPrefix :: String -> Int -> Int -> [FDExpr]   
Returns an infinite list of named FD variables with given domain
domain :: Int -> Int -> [FDExpr]   
Returns infinite list of named FD variables with given domain and default prefix "fdv_"
fd :: Int -> FDExpr   
Ints as FDExpr
notC :: FDConstr -> FDConstr   
Negated FD constraint
(+#) :: FDExpr -> FDExpr -> FDExpr   
Addition of FD expressions.
(-#) :: FDExpr -> FDExpr -> FDExpr   
Subtraction of FD expressions.
(*#) :: FDExpr -> FDExpr -> FDExpr   
Multiplication of FD expressions.
(=#) :: FDExpr -> FDExpr -> FDConstr   
Equality of FD expressions.
(/=#) :: FDExpr -> FDExpr -> FDConstr   
Disequality of FD expressions.
(<#) :: FDExpr -> FDExpr -> FDConstr   
"Less than" constraint on FD expressions.
(<=#) :: FDExpr -> FDExpr -> FDConstr   
"Less than or equal" constraint on FD expressions.
(>#) :: FDExpr -> FDExpr -> FDConstr   
"Greater than" constraint on FD expressions.
(>=#) :: FDExpr -> FDExpr -> FDConstr   
"Greater than or equal" constraint on FD expressions.
true :: FDConstr   
The always satisfied FD constraint.
false :: FDConstr   
The always unsatisfied constraint
(/\) :: FDConstr -> FDConstr -> FDConstr   
Conjunction of FD constraints.
(\/) :: FDConstr -> FDConstr -> FDConstr   
andC :: [FDConstr] -> FDConstr   
Conjunction of a list of FD constraints.
orC :: [FDConstr] -> FDConstr   
Disnjunction of a list of FD constraints.
allC :: (a -> FDConstr) -> [a] -> FDConstr   
Maps a constraint abstraction to a list of FD constraints and joins them.
allDifferent :: [FDExpr] -> FDConstr   
"All different" constraint on FD variables.
sum :: [FDExpr] -> FDRel -> FDExpr -> FDConstr   
Relates the sum of FD variables with some integer of FD variable.
scalarProduct :: [FDExpr] -> [FDExpr] -> FDRel -> FDExpr -> FDConstr   
(scalarProduct cs vs relop v) is satisfied if (sum (cs*vs) relop v) is satisfied.
count :: FDExpr -> [FDExpr] -> FDRel -> FDExpr -> FDConstr   
(count v vs relop c) is satisfied if (n relop c), where n is the number of elements in the list of FD variables vs that are equal to v, is satisfied.
abs :: FDExpr -> FDExpr   
Absolute value of expression.
getFDVarName :: FDExpr -> String   
Get the name of a FDVar.
getFDVal :: FDExpr -> Int   
Get value (possibly an unbound variable) of an FD expression.
allFDVars :: FDConstr -> [FDExpr]   
Compute set of all variables occurring in a constraint.
allFDVars' :: FDConstr -> [FDExpr]   
filterFDVars :: [FDExpr] -> [FDExpr]   
Compute a set of all variables occuring in a list of expressions
fdVarEq :: FDExpr -> FDExpr -> Bool   
filterVars :: [FDExpr] -> [FDExpr]   
allEFDVars :: FDExpr -> [FDExpr]   

Exported datatypes:

FDExpr

Constructors:

  • FDVar :: String -> Int -> Int -> Int -> FDExpr
  • FDInt :: Int -> FDExpr
  • FDBinExp :: FDOp -> FDExpr -> FDExpr -> FDExpr
  • FDAbs :: FDExpr -> FDExpr
FDOp

Constructors:

  • Plus :: FDOp
  • Minus :: FDOp
  • Times :: FDOp
FDRel

Possible relations between FD values.

Constructors:

  • Equ :: FDRel : Equal
  • Neq :: FDRel : Not equal
  • Lt :: FDRel : Less than
  • Leq :: FDRel : Less than or equal
  • Gt :: FDRel : Greater than
  • Geq :: FDRel : Greater than or equal
FDConstr

Constructors:

Exported operations:

domainWPrefix :: String -> Int -> Int -> [FDExpr]   

Returns an infinite list of named FD variables with given domain

Example call:
(domainWPrefix prefix lo up)
Parameters:
  • prefix : prefix to use for generated names
  • lo : minimum value for all variables in xs
  • up : maximum value for all variables in xs

domain :: Int -> Int -> [FDExpr]   

Returns infinite list of named FD variables with given domain and default prefix "fdv_"

Example call:
(domain lo up)
Parameters:
  • lo : minimum value for all variables in xs
  • up : maximum value for all variables in xs

fd :: Int -> FDExpr   

Ints as FDExpr

Further infos:
  • solution complete, i.e., able to compute all solutions

notC :: FDConstr -> FDConstr   

Negated FD constraint

Further infos:
  • solution complete, i.e., able to compute all solutions

(+#) :: FDExpr -> FDExpr -> FDExpr   

Addition of FD expressions.

Further infos:
  • defined as left-associative infix operator with precedence 6
  • solution complete, i.e., able to compute all solutions

(-#) :: FDExpr -> FDExpr -> FDExpr   

Subtraction of FD expressions.

Further infos:
  • defined as left-associative infix operator with precedence 6
  • solution complete, i.e., able to compute all solutions

(*#) :: FDExpr -> FDExpr -> FDExpr   

Multiplication of FD expressions.

Further infos:
  • defined as left-associative infix operator with precedence 7
  • solution complete, i.e., able to compute all solutions

(=#) :: FDExpr -> FDExpr -> FDConstr   

Equality of FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(/=#) :: FDExpr -> FDExpr -> FDConstr   

Disequality of FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(<#) :: FDExpr -> FDExpr -> FDConstr   

"Less than" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(<=#) :: FDExpr -> FDExpr -> FDConstr   

"Less than or equal" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(>#) :: FDExpr -> FDExpr -> FDConstr   

"Greater than" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(>=#) :: FDExpr -> FDExpr -> FDConstr   

"Greater than or equal" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

true :: FDConstr   

The always satisfied FD constraint.

Further infos:
  • solution complete, i.e., able to compute all solutions

false :: FDConstr   

The always unsatisfied constraint

Further infos:
  • solution complete, i.e., able to compute all solutions

(/\) :: FDConstr -> FDConstr -> FDConstr   

Conjunction of FD constraints.

Further infos:
  • defined as right-associative infix operator with precedence 3
  • solution complete, i.e., able to compute all solutions

(\/) :: FDConstr -> FDConstr -> FDConstr   

Further infos:
  • defined as right-associative infix operator with precedence 2
  • solution complete, i.e., able to compute all solutions

andC :: [FDConstr] -> FDConstr   

Conjunction of a list of FD constraints.

orC :: [FDConstr] -> FDConstr   

Disnjunction of a list of FD constraints.

allC :: (a -> FDConstr) -> [a] -> FDConstr   

Maps a constraint abstraction to a list of FD constraints and joins them.

allDifferent :: [FDExpr] -> FDConstr   

"All different" constraint on FD variables.

Example call:
(allDifferent xs)
Parameters:
  • xs : list of FD variables
Returns:
satisfied if the FD variables in the argument list xs have pairwise different values.
Further infos:
  • solution complete, i.e., able to compute all solutions

sum :: [FDExpr] -> FDRel -> FDExpr -> FDConstr   

Relates the sum of FD variables with some integer of FD variable.

Further infos:
  • solution complete, i.e., able to compute all solutions

scalarProduct :: [FDExpr] -> [FDExpr] -> FDRel -> FDExpr -> FDConstr   

(scalarProduct cs vs relop v) is satisfied if (sum (cs*vs) relop v) is satisfied. The first argument must be a list of integers. The other arguments are as in sum.

Further infos:
  • solution complete, i.e., able to compute all solutions

count :: FDExpr -> [FDExpr] -> FDRel -> FDExpr -> FDConstr   

(count v vs relop c) is satisfied if (n relop c), where n is the number of elements in the list of FD variables vs that are equal to v, is satisfied. The first argument must be an integer. The other arguments are as in sum.

Further infos:
  • solution complete, i.e., able to compute all solutions

abs :: FDExpr -> FDExpr   

Absolute value of expression.

Further infos:
  • solution complete, i.e., able to compute all solutions

getFDVarName :: FDExpr -> String   

Get the name of a FDVar.

getFDVal :: FDExpr -> Int   

Get value (possibly an unbound variable) of an FD expression.

allFDVars :: FDConstr -> [FDExpr]   

Compute set of all variables occurring in a constraint.

allFDVars' :: FDConstr -> [FDExpr]   

filterFDVars :: [FDExpr] -> [FDExpr]   

Compute a set of all variables occuring in a list of expressions

fdVarEq :: FDExpr -> FDExpr -> Bool   

filterVars :: [FDExpr] -> [FDExpr]   

allEFDVars :: FDExpr -> [FDExpr]