Copyright | (c) Michael Szvetits 2020 |
---|---|

License | BSD3 (see the file LICENSE) |

Maintainer | typedbyte@qualified.name |

Stability | stable |

Portability | portable |

Safe Haskell | None |

Language | Haskell2010 |

This module exports the types and functions needed to define constraints and run the constraint solver.

## Synopsis

- data FD a
- data Expression
- int :: Int -> Expression
- newVar :: FD Expression
- initNewVar :: Expression -> FD Expression
- sum :: [Expression] -> Expression
- type Constraint = FD ()
- (#=) :: Expression -> Expression -> Constraint
- (#/=) :: Expression -> Expression -> Constraint
- (#<) :: Expression -> Expression -> Constraint
- (#<=) :: Expression -> Expression -> Constraint
- (#>) :: Expression -> Expression -> Constraint
- (#>=) :: Expression -> Expression -> Constraint
- (/\) :: Constraint -> Constraint -> Constraint
- (\/) :: Constraint -> Constraint -> Constraint
- not' :: Constraint -> Constraint
- between :: Expression -> Expression -> Expression -> Constraint
- allDifferent :: [Expression] -> Constraint
- data Labeling a
- labeling :: [Expression] -> FD (Labeling [Int])
- runFD :: FD a -> a

# Core Monad

All constraint solving actions are peformed in the FD monad which tracks created variables and specified constraints.

# Building Expressions

data Expression Source #

Expressions are the build blocks of constraints. Note that `Expression`

is
an instance of `Num`

, so arithmetic combinations of expressions are possible.

## Instances

int :: Int -> Expression Source #

Converts an integer into an expression that can be used in constraint formulations.

newVar :: FD Expression Source #

Creates a new variable with a default value range from negative infinity
to positive infinity. Values are assigned to variables during `labeling`

.

initNewVar :: Expression -> FD Expression Source #

Creates a new variable and initializes it with a specific value.

sum :: [Expression] -> Expression Source #

Sums up a list of expressions.

# Building Constraints

type Constraint = FD () Source #

A constraint restricts the possible values of an involved `Expression`

.

(#=) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that two expressions have the same value.

(#/=) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that two expressions have different values.

(#<) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that the value of an expression is less than the value of another expression.

(#<=) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that the value of an expression is less than or equal to the value of another expression.

(#>) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that the value of an expression is greater than the value of another expression.

(#>=) :: Expression -> Expression -> Constraint infix 4 Source #

Enforces that the value of an expression is greater than or equal to the value of another expression.

(/\) :: Constraint -> Constraint -> Constraint infixl 3 Source #

Conjunction of constraints, i.e. both constraints must hold.

(\/) :: Constraint -> Constraint -> Constraint infixl 2 Source #

Disjunction of constraints, i.e. at least one of the two constraints must hold.

not' :: Constraint -> Constraint Source #

Negates a constraint, i.e. the specified constraint must not hold.

:: Expression | The inclusive lower bound of the expression. |

-> Expression | The inclusive upper bound of the expression. |

-> Expression | The expression to be constrained. |

-> Constraint | The resulting constraint. |

Enforces that the value of an expression lies within two bounds.

allDifferent :: [Expression] -> Constraint Source #

Enforces that the all the given expressions have different values.

# Running the Solver

A labeling is the result of the solver when trying to assign values to
variables according to the given constraints. Solutions have the same
ordering as the expressions specified during `labeling`

, so operations like
`zip`

can be used to relate expressions to their solution values.

Unsolvable [Domain Int] | Indicates that the given set of constraints cannot be solved, i.e. there is no combination of values for the labelled variables to fulfil all the constraints. The provided list contains the values that were narrowed down during the search. |

Unbounded [Domain Int] | Indicates that the given set of constraints cannot be solved in its current form because at least one variable has a lower bound of negative infinity or an upper bound of positive infinity (i.e., potential solutions cannot be enumerated). The provided list contains the values that were narrowed down during the search. |

Solutions [a] | Indicates a successful assignment of values to the labelled variables. The list contains all possible solutions. |

labeling :: [Expression] -> FD (Labeling [Int]) Source #

Searches all combinations of values for the given expressions (variables, most likely) which fulfil all the constraints defined in the FD monad.

The result list has the same ordering as the expressions, so operations like
`zip`

are possible to relate the given expressions to their solution values.