finito-0.1.0.0: Constraint Solver for Finite Domains

Copyright(c) Michael Szvetits 2020
LicenseBSD3 (see the file LICENSE)
Maintainertypedbyte@qualified.name
Stabilitystable
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

AI.Search.FiniteDomain.Int

Contents

Description

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

Synopsis

Core Monad

data FD a Source #

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

Instances
Monad FD Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

(>>=) :: FD a -> (a -> FD b) -> FD b #

(>>) :: FD a -> FD b -> FD b #

return :: a -> FD a #

fail :: String -> FD a #

Functor FD Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

fmap :: (a -> b) -> FD a -> FD b #

(<$) :: a -> FD b -> FD a #

Applicative FD Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

pure :: a -> FD a #

(<*>) :: FD (a -> b) -> FD a -> FD b #

liftA2 :: (a -> b -> c) -> FD a -> FD b -> FD c #

(*>) :: FD a -> FD b -> FD b #

(<*) :: FD a -> FD b -> FD a #

Building Expressions

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.

between Source #

Arguments

:: 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

data Labeling a Source #

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.

Constructors

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.

Instances
Monad Labeling Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

(>>=) :: Labeling a -> (a -> Labeling b) -> Labeling b #

(>>) :: Labeling a -> Labeling b -> Labeling b #

return :: a -> Labeling a #

fail :: String -> Labeling a #

Functor Labeling Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

fmap :: (a -> b) -> Labeling a -> Labeling b #

(<$) :: a -> Labeling b -> Labeling a #

Applicative Labeling Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

pure :: a -> Labeling a #

(<*>) :: Labeling (a -> b) -> Labeling a -> Labeling b #

liftA2 :: (a -> b -> c) -> Labeling a -> Labeling b -> Labeling c #

(*>) :: Labeling a -> Labeling b -> Labeling b #

(<*) :: Labeling a -> Labeling b -> Labeling a #

Eq a => Eq (Labeling a) Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

(==) :: Labeling a -> Labeling a -> Bool #

(/=) :: Labeling a -> Labeling a -> Bool #

Show a => Show (Labeling a) Source # 
Instance details

Defined in AI.Search.FiniteDomain.Int.Constraint

Methods

showsPrec :: Int -> Labeling a -> ShowS #

show :: Labeling a -> String #

showList :: [Labeling a] -> ShowS #

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.

runFD :: FD a -> a Source #

Runs the FD monad computation.