Module "CLPFD.curry"

Library for finite domain constraint solving.

The general structure of a specification of an FD problem is as follows:
domain_constraint & fd_constraint & labeling
where:
domain_constraint specifies the possible range of the FD variables (see constraint domain)
fd_constraint specifies the constraint to be satisfied by a valid solution (see constraints #+, #-, allDifferent, etc below)
labeling is a labeling function to search for a concrete solution.
Note: This library is based on the corresponding library of Sicstus-Prolog but does not implement the complete functionality of the Sicstus-Prolog library. However, using the PAKCS interface for external functions, it is relatively easy to provide the complete functionality.

 Exported names:

Datatypes:
Constraint | LabelingOption

Constructors:
All | Assumptions | Bisect | Down | Enum | FirstFail | FirstFailConstrained | LeftMost | Max | Maximize | Min | Minimize | Step | Up

Functions:
#/=# | #<# | #<=# | #<=># | #=# | #=># | #># | #>=# | *# | +# | -# | /=# | <# | <=# | =# | ># | >=# | allDifferent | all_different | count | domain | indomain | labeling | scalarProduct | solve | sum

 Summary of exported functions:
domain  :: [Int] -> Int -> Int -> Success  deterministic 
          Constraint to specify the domain of all finite domain variables.
(+#)  :: Int -> Int -> Int  deterministic 
          Addition of FD variables.
(-#)  :: Int -> Int -> Int  deterministic 
          Subtraction of FD variables.
(*#)  :: Int -> Int -> Int  deterministic 
          Multiplication of FD variables.
(=#)  :: Int -> Int -> Success  deterministic 
          Equality of FD variables.
(/=#)  :: Int -> Int -> Success  deterministic 
          Disequality of FD variables.
(<#)  :: Int -> Int -> Success  deterministic 
          "Less than" constraint on FD variables.
(<=#)  :: Int -> Int -> Success  deterministic 
          "Less than or equal" constraint on FD variables.
(>#)  :: Int -> Int -> Success  deterministic 
          "Greater than" constraint on FD variables.
(>=#)  :: Int -> Int -> Success  deterministic 
          "Greater than or equal" constraint on FD variables.
(#=#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable equality constraint on FD variables.
(#/=#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable inequality constraint on FD variables.
(#<#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable "less than" constraint on FD variables.
(#<=#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable "less than or equal" constraint on FD variables.
(#>#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable "greater than" constraint on FD variables.
(#>=#)  :: Int -> Int -> Constraint  deterministic 
          Reifyable "greater than or equal" constraint on FD variables.
(#=>#)  :: Constraint -> Constraint -> Constraint  deterministic 
          The resulting constraint is satisfied if the first argument constraint do not hold or both argument constraints are satisfied.
(#<=>#)  :: Constraint -> Constraint -> Constraint  deterministic 
          The resulting constraint is satisfied if both argument constraint are either satisfied and do not hold.
solve  :: Constraint -> Success  deterministic 
          Solves a reified constraint.
sum  :: [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 
          Relates the sum of FD variables with some integer of FD variable.
scalarProduct  :: [Int] -> [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 
          (scalarProduct cs vs relop v) is satisfied if ((cs*vs) relop v) is satisfied.
count  :: Int -> [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 
          (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.
allDifferent  :: [Int] -> Success  deterministic 
          "All different" constraint on FD variables.
all_different  :: [Int] -> Success  deterministic 
          For backward compatibility.
indomain  :: Int -> Success  deterministic 
          Instantiate a single FD variable to its values in the specified domain.
labeling  :: [LabelingOption] -> [Int] -> Success  deterministic 
          Instantiate FD variables to their values in the specified domain.
 Imported modules:
Prelude
 Exported datatypes:

Constraint

A datatype to represent reifyable constraints.

Constructors:

LabelingOption

This datatype contains all options to control the instantiated of FD variables with the enumeration constraint labeling.

Constructors:

LeftMost :: LabelingOption

LeftMost - The leftmost variable is selected for instantiation (default)

FirstFail :: LabelingOption

FirstFail - The leftmost variable with the smallest domain is selected (also known as first-fail principle)

FirstFailConstrained :: LabelingOption

FirstFailConstrained - The leftmost variable with the smallest domain and the most constraints on it is selected.

Min :: LabelingOption

Min - The leftmost variable with the smalled lower bound is selected.

Max :: LabelingOption

Max - The leftmost variable with the greatest upper bound is selected.

Step :: LabelingOption

Step - Make a binary choice between x=#b and x/=#b for the selected variable x where b is the lower or upper bound of x (default).

Enum :: LabelingOption

Enum - Make a multiple choice for the selected variable for all the values in its domain.

Bisect :: LabelingOption

Bisect - Make a binary choice between x<=#m and x>#m for the selected variable x where m is the midpoint of the domain x (also known as domain splitting).

Up :: LabelingOption

Up - The domain is explored for instantiation in ascending order (default).

Down :: LabelingOption

Down - The domain is explored for instantiation in descending order.

All :: LabelingOption

All - Enumerate all solutions by backtracking (default).

Minimize :: Int -> LabelingOption

Minimize v - Find a solution that minimizes the domain variable v (using a branch-and-bound algorithm).

Maximize :: Int -> LabelingOption

Maximize v - Find a solution that maximizes the domain variable v (using a branch-and-bound algorithm).

Assumptions :: Int -> LabelingOption

Assumptions x - The variable x is unified with the number of choices made by the selected enumeration strategy when a solution is found.

 Exported functions:
domain :: [Int] -> Int -> Int -> Success  deterministic 

Constraint to specify the domain of all finite domain variables.

Example call:  (domain xs min max)

Parameters:
xs - list of finite domain variables
min - minimum value for all variables in xs
max - maximum value for all variables in xs
(+#) :: Int -> Int -> Int  deterministic 

Addition of FD variables.

Further infos:
  • defined as left-associative infix operator with precedence 6
(-#) :: Int -> Int -> Int  deterministic 

Subtraction of FD variables.

Further infos:
  • defined as left-associative infix operator with precedence 6
(*#) :: Int -> Int -> Int  deterministic 

Multiplication of FD variables.

Further infos:
  • defined as left-associative infix operator with precedence 7
(=#) :: Int -> Int -> Success  deterministic 

Equality of FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(/=#) :: Int -> Int -> Success  deterministic 

Disequality of FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(<#) :: Int -> Int -> Success  deterministic 

"Less than" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(<=#) :: Int -> Int -> Success  deterministic 

"Less than or equal" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(>#) :: Int -> Int -> Success  deterministic 

"Greater than" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(>=#) :: Int -> Int -> Success  deterministic 

"Greater than or equal" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
(#=#) :: Int -> Int -> Constraint  deterministic 

Reifyable equality constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#/=#) :: Int -> Int -> Constraint  deterministic 

Reifyable inequality constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#<#) :: Int -> Int -> Constraint  deterministic 

Reifyable "less than" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#<=#) :: Int -> Int -> Constraint  deterministic 

Reifyable "less than or equal" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#>#) :: Int -> Int -> Constraint  deterministic 

Reifyable "greater than" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#>=#) :: Int -> Int -> Constraint  deterministic 

Reifyable "greater than or equal" constraint on FD variables.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions
(#=>#) :: Constraint -> Constraint -> Constraint  deterministic 

The resulting constraint is satisfied if the first argument constraint do not hold or both argument constraints are satisfied.

Further infos:
  • defined as right-associative infix operator with precedence 1
  • solution complete, i.e., able to compute all solutions
(#<=>#) :: Constraint -> Constraint -> Constraint  deterministic 

The resulting constraint is satisfied if both argument constraint are either satisfied and do not hold.

Further infos:
  • defined as right-associative infix operator with precedence 1
  • solution complete, i.e., able to compute all solutions
solve :: Constraint -> Success  deterministic 

Solves a reified constraint.

sum :: [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 

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

scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 

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

count :: Int -> [Int] -> (Int -> Int -> Success) -> Int -> Success  deterministic 

(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.

allDifferent :: [Int] -> Success  deterministic 

"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.
all_different :: [Int] -> Success  deterministic 

For backward compatibility. Use allDifferent.

indomain :: Int -> Success  deterministic 

Instantiate a single FD variable to its values in the specified domain.

labeling :: [LabelingOption] -> [Int] -> Success  deterministic 

Instantiate FD variables to their values in the specified domain.

Example call:  (labeling options xs)

Parameters:
options - list of option to control the instantiation of FD variables
xs - list of FD variables that are non-deterministically instantiated to their possible values.
Generated by CurryDoc (Version 0.4.1 of June 7, 2007) at Nov 9 18:10:11 2009