summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ChangeLog.md5
-rw-r--r--LICENSE30
-rw-r--r--README.md11
-rw-r--r--examples/queens/Main.hs67
-rw-r--r--examples/sudoku/Main.hs70
-rw-r--r--finito.cabal79
-rw-r--r--src/AI/Search/FiniteDomain/Int.hs45
-rw-r--r--src/AI/Search/FiniteDomain/Int/Cell.hs45
-rw-r--r--src/AI/Search/FiniteDomain/Int/Constraint.hs356
-rw-r--r--src/AI/Search/FiniteDomain/Int/Expression.hs99
10 files changed, 807 insertions, 0 deletions
diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
index 0000000..1c7df1e
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Changelog for finito
+
+## 0.1.0.0 (2020-02-13)
+
+- Initial release \ No newline at end of file
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..6fa5e95
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Michael Szvetits (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Michael Szvetits nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. \ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..995f77e
--- /dev/null
+++ b/README.md
@@ -0,0 +1,11 @@
+<p align="center">
+<img src="./logo.png">
+</p>
+
+# finito
+
+[![Hackage](https://img.shields.io/hackage/v/finito.svg?logo=haskell&label=finito)](https://hackage.haskell.org/package/finito)
+
+A constraint solver for finite domains, written in Haskell. The implementation is based on propagators and cells holding ranges of possible integer values (using the packages [propeller](https://github.com/typedbyte/propeller) and [numeric-domains](https://github.com/typedbyte/numeric-domains)).
+
+[Sudoku](./examples/sudoku/Main.hs) and the [n-queens problem](./examples/queens/Main.hs) with configurable board size are provided as examples on how to use the library. In addition, the [Hackage documentation](https://hackage.haskell.org/package/finito) is quite compact and covers all the provided types and functions. \ No newline at end of file
diff --git a/examples/queens/Main.hs b/examples/queens/Main.hs
new file mode 100644
index 0000000..a11712c
--- /dev/null
+++ b/examples/queens/Main.hs
@@ -0,0 +1,67 @@
+module Main where
+
+-- base
+import Control.Monad ( forM_, replicateM )
+import Data.List ( find )
+import System.Environment ( getArgs )
+
+import AI.Search.FiniteDomain.Int
+
+-- A helper function to print the chess board.
+printChess :: Int -> Int -> [(Int,Int)] -> IO ()
+printChess width height solutions = do
+ forM_ [1..height] $ \row -> do
+ putStr "[ "
+ case find ((== row) . fst) solutions of
+ Nothing ->
+ forM_ [1..width] line
+ Just (_,c) -> do
+ forM_ [1..c-1] line
+ putStr "Q "
+ forM_ [c+1..width] line
+ putStrLn "]"
+ where
+ line _ = putStr "_ "
+
+-- This function transforms a given Queens puzzle into a constraint.
+toConstraint :: Int -> Int -> Int -> FD (Labeling [(Int,Int)])
+toConstraint count width height = do
+ rows <- replicateM count newVar
+ columns <- replicateM count newVar
+ forM_ rows $ between 1 (int height)
+ forM_ columns $ between 1 (int width)
+ secureQueens (zip rows columns)
+ result <- labeling (rows ++ columns)
+ pure $ do
+ solution <- result
+ pure (zip (take count solution) (drop count solution))
+ where
+ secureQueens [] = pure ()
+ secureQueens (q:qs) = do
+ secureLines qs q
+ secureQueens qs
+ secureLines [] _ = pure ()
+ secureLines ((row,col):qs) queen@(r,c) = do
+ col #/= c
+ row #> r
+ abs (col - c) #/= row - r
+ secureLines qs queen
+
+-- Put it all together.
+main :: IO ()
+main = do
+ putStrLn "Expecting [queen count, board width, board height] as command line arguments."
+ putStrLn "Default is [8, 8, 8]."
+ args <- getArgs
+ let (count, width, height) =
+ case args of
+ [qc, w, h] -> (read qc, read w, read h)
+ _ -> ( 8, 8, 8)
+ putStrLn $ "Placing " ++ show count ++ " queen(s) ..."
+ case runFD (toConstraint count width height) of
+ Unsolvable _ -> putStrLn "Queens puzzle is unsolvable."
+ Unbounded _ -> putStrLn "The constraint formulation is wrong."
+ Solutions xs -> do
+ forM_ xs $ \solution -> do
+ putStrLn "Found a solution:"
+ printChess width height solution \ No newline at end of file
diff --git a/examples/sudoku/Main.hs b/examples/sudoku/Main.hs
new file mode 100644
index 0000000..8cbaff6
--- /dev/null
+++ b/examples/sudoku/Main.hs
@@ -0,0 +1,70 @@
+module Main where
+
+-- base
+import Control.Monad ( forM_, replicateM, mapM_, when, zipWithM_ )
+import Data.List ( transpose )
+
+-- split
+import Data.List.Split ( chunksOf )
+
+import AI.Search.FiniteDomain.Int
+
+-- This is our test scenario.
+testSudoku :: [Int]
+testSudoku =
+ [ 0, 0, 4, 0, 0, 0, 5, 0, 0,
+ 0, 0, 0, 0, 0, 0, 0, 4, 9,
+ 6, 0, 3, 0, 0, 0, 8, 0, 0,
+
+ 0, 0, 2, 0, 0, 0, 0, 9, 6,
+ 7, 0, 5, 0, 0, 0, 2, 0, 0,
+ 0, 9, 0, 8, 4, 0, 0, 0, 0,
+
+ 0, 0, 0, 6, 3, 0, 0, 0, 5,
+ 0, 0, 0, 2, 8, 0, 0, 0, 0,
+ 3, 7, 0, 1, 0, 0, 0, 0, 2 ]
+
+-- Some helper functions to prepare and print Sudoku values.
+rows :: [a] -> [[a]]
+rows = chunksOf 9
+
+columns :: [a] -> [[a]]
+columns = transpose . rows
+
+blocks :: [a] -> [[a]]
+blocks
+ = concat
+ . fmap (fmap concat . transpose)
+ . chunksOf 3
+ . chunksOf 3
+ . chunksOf 3
+
+printSudoku :: [Int] -> IO ()
+printSudoku = mapM_ (putStrLn . fmap replace . show) . rows
+ where replace '0' = '_'
+ replace ',' = ' '
+ replace c = c
+
+-- This function transforms a given Sudoku puzzle into a constraint.
+toConstraint :: [Int] -> FD (Labeling [Int])
+toConstraint sudoku = do
+ vars <- replicateM 81 newVar
+ zipWithM_ (\v n -> when (n > 0) (v #= int n)) vars sudoku
+ mapM_ (between 1 9) vars
+ mapM_ allDifferent (rows vars)
+ mapM_ allDifferent (columns vars)
+ mapM_ allDifferent (blocks vars)
+ labeling vars
+
+-- Put it all together.
+main :: IO ()
+main = do
+ putStrLn "Test Sudoku puzzle:"
+ printSudoku testSudoku
+ case runFD (toConstraint testSudoku) of
+ Unsolvable _ -> putStrLn "Sudoku is unsolvable."
+ Unbounded _ -> putStrLn "The constraint formulation is wrong."
+ Solutions xs ->
+ forM_ xs $ \solution -> do
+ putStrLn "Found a solution:"
+ printSudoku solution \ No newline at end of file
diff --git a/finito.cabal b/finito.cabal
new file mode 100644
index 0000000..f34a02c
--- /dev/null
+++ b/finito.cabal
@@ -0,0 +1,79 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: ecf8c68ef6f9899a0002862838c8ea291afd77aaf46d4cb031a5975c44f39022
+
+name: finito
+version: 0.1.0.0
+synopsis: Constraint Solver for Finite Domains
+description: Please see the README on GitHub at <https://github.com/typedbyte/finito#readme>
+category: AI
+homepage: https://github.com/typedbyte/finito#readme
+bug-reports: https://github.com/typedbyte/finito/issues
+author: Michael Szvetits
+maintainer: typedbyte@qualified.name
+copyright: 2020 Michael Szvetits
+license: BSD3
+license-file: LICENSE
+build-type: Simple
+extra-source-files:
+ README.md
+ ChangeLog.md
+
+source-repository head
+ type: git
+ location: https://github.com/typedbyte/finito
+
+library
+ exposed-modules:
+ AI.Search.FiniteDomain.Int
+ other-modules:
+ AI.Search.FiniteDomain.Int.Cell
+ AI.Search.FiniteDomain.Int.Constraint
+ AI.Search.FiniteDomain.Int.Expression
+ Paths_finito
+ hs-source-dirs:
+ src
+ ghc-options: -Wall
+ build-depends:
+ base >=4.7 && <5
+ , numeric-domains >=0.1 && <0.2
+ , propeller >=0.1 && <0.2
+ , transformers >=0.5.2.0 && <0.6
+ default-language: Haskell2010
+
+test-suite queens
+ type: exitcode-stdio-1.0
+ main-is: Main.hs
+ other-modules:
+ Paths_finito
+ hs-source-dirs:
+ examples/queens
+ ghc-options: -Wall
+ build-depends:
+ base >=4.7 && <5
+ , finito
+ , numeric-domains >=0.1 && <0.2
+ , propeller >=0.1 && <0.2
+ , transformers >=0.5.2.0 && <0.6
+ default-language: Haskell2010
+
+test-suite sudoku
+ type: exitcode-stdio-1.0
+ main-is: Main.hs
+ other-modules:
+ Paths_finito
+ hs-source-dirs:
+ examples/sudoku
+ ghc-options: -Wall
+ build-depends:
+ base >=4.7 && <5
+ , finito
+ , numeric-domains >=0.1 && <0.2
+ , propeller >=0.1 && <0.2
+ , split
+ , transformers >=0.5.2.0 && <0.6
+ default-language: Haskell2010
diff --git a/src/AI/Search/FiniteDomain/Int.hs b/src/AI/Search/FiniteDomain/Int.hs
new file mode 100644
index 0000000..9a63e73
--- /dev/null
+++ b/src/AI/Search/FiniteDomain/Int.hs
@@ -0,0 +1,45 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module : AI.Search.FiniteDomain.Int
+-- Copyright : (c) Michael Szvetits, 2020
+-- License : BSD3 (see the file LICENSE)
+-- Maintainer : typedbyte@qualified.name
+-- Stability : stable
+-- Portability : portable
+--
+-- This module exports the types and functions needed to define constraints
+-- and run the constraint solver.
+-----------------------------------------------------------------------------
+module AI.Search.FiniteDomain.Int
+ ( -- * Core Monad
+ FD
+ -- * Building Expressions
+ , Expression
+ , int
+ , newVar
+ , initNewVar
+ , sum
+ -- * Building Constraints
+ , Constraint
+ , (#=)
+ , (#/=)
+ , (#<)
+ , (#<=)
+ , (#>)
+ , (#>=)
+ , (/\)
+ , (\/)
+ , not'
+ , between
+ , allDifferent
+ -- * Running the Solver
+ , Labeling(..)
+ , labeling
+ , runFD
+ ) where
+
+-- base
+import Prelude hiding ( sum )
+
+import AI.Search.FiniteDomain.Int.Constraint
+import AI.Search.FiniteDomain.Int.Expression ( Expression, int, sum ) \ No newline at end of file
diff --git a/src/AI/Search/FiniteDomain/Int/Cell.hs b/src/AI/Search/FiniteDomain/Int/Cell.hs
new file mode 100644
index 0000000..8f83997
--- /dev/null
+++ b/src/AI/Search/FiniteDomain/Int/Cell.hs
@@ -0,0 +1,45 @@
+-- This module exports some useful join functions for propagator cells.
+-- A join function describes how an old cell value is combined with a new one.
+-- See the package @propeller@ for details on the propagator implementation.
+module AI.Search.FiniteDomain.Int.Cell
+ ( domainJoin
+ , eqJoin
+ , mustHoldJoin
+ ) where
+
+-- domain
+import Numeric.Domain ( Domain, intersect, isSubsetOf )
+
+-- propeller
+import Data.Propagator.Change ( Change(..) )
+
+-- | Compares an old and a new domain of integer values to see if the new
+-- domain is a subset of the old domain (i.e., the cell has changed).
+--
+-- Never returns 'Incompatible'.
+domainJoin :: Domain Int -> Domain Int -> Change (Domain Int)
+domainJoin old new =
+ case intersect old new of
+ reduced | reduced `isSubsetOf` old -> Changed reduced
+ | otherwise -> Unchanged
+
+-- | Compares an old and a new value to see if there was a change.
+--
+-- Never returns 'Incompatible'.
+eqJoin :: Eq a => a -> a -> Change a
+eqJoin old new
+ | old == new = Unchanged
+ | otherwise = Changed new
+
+-- | Checks if a new cell value is ...
+--
+-- * 'True', then 'Unchanged' is returned, or
+-- * 'False', then 'Incompatible' is returned.
+--
+-- This can be used to represent conditions which must always hold
+-- (i.e., the cell value must always be 'True').
+--
+-- The old value of the cell is ignored. Never returns 'Changed'.
+mustHoldJoin :: a -> Bool -> Change b
+mustHoldJoin _ True = Unchanged
+mustHoldJoin _ False = Incompatible \ No newline at end of file
diff --git a/src/AI/Search/FiniteDomain/Int/Constraint.hs b/src/AI/Search/FiniteDomain/Int/Constraint.hs
new file mode 100644
index 0000000..50d3b47
--- /dev/null
+++ b/src/AI/Search/FiniteDomain/Int/Constraint.hs
@@ -0,0 +1,356 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module AI.Search.FiniteDomain.Int.Constraint
+ ( (#=)
+ , (#/=)
+ , (#<)
+ , (#<=)
+ , (#>)
+ , (#>=)
+ , (/\)
+ , (\/)
+ , Constraint
+ , FD
+ , Labeling(..)
+ , allDifferent
+ , between
+ , initNewVar
+ , labeling
+ , newVar
+ , not'
+ , runFD
+ ) where
+
+-- base
+import Control.Monad ( forM, forM_ )
+import Control.Monad.ST ( ST, runST )
+import Data.List ( find )
+
+-- domain
+import qualified Numeric.Domain as D
+
+-- propeller
+import Data.Propagator.Cell as P ( Cell, cell, connect, label, propagateMany
+ , readCell, succeeded, sync, syncWith )
+
+-- transformers
+import Control.Monad.Trans.State ( State, evalState, execState, get, modify, put )
+
+import AI.Search.FiniteDomain.Int.Cell ( domainJoin, eqJoin, mustHoldJoin )
+import AI.Search.FiniteDomain.Int.Expression ( Expression, cellifyExpression, var )
+
+-- | All constraint solving actions are peformed in the FD monad which tracks
+-- created variables and specified constraints.
+newtype FD a = FD { unFD :: State ([IntConstraint], Int) a }
+ deriving (Applicative, Functor, Monad)
+
+-- | A constraint restricts the possible values of an involved 'Expression'.
+type Constraint = FD ()
+
+addConstraint :: IntConstraint -> FD ()
+addConstraint cons = FD $
+ modify (\(cs, ix) -> (cons : cs, ix))
+
+-- | Runs the FD monad computation.
+runFD :: FD a -> a
+runFD (FD state) = evalState state ([], 0)
+
+data IntConstraint
+ = Equals Expression Expression
+ | NotEquals Expression Expression
+ | LessThan Expression Expression
+ | And IntConstraint IntConstraint
+ | Or IntConstraint IntConstraint
+ deriving (Eq, Ord, Show)
+
+-- | Enforces that two expressions have the same value.
+infix 4 #=
+(#=) :: Expression -> Expression -> Constraint
+(#=) left right = addConstraint $ left `Equals` right
+
+-- | Enforces that two expressions have different values.
+infix 4 #/=
+(#/=) :: Expression -> Expression -> Constraint
+(#/=) left right = addConstraint $ left `NotEquals` right
+
+-- | Enforces that the value of an expression is less than the value of another
+-- expression.
+infix 4 #<
+(#<) :: Expression -> Expression -> Constraint
+(#<) left right = addConstraint $ left `LessThan` right
+
+-- | Enforces that the value of an expression is less than or equal to the
+-- value of another expression.
+infix 4 #<=
+(#<=) :: Expression -> Expression -> Constraint
+(#<=) left right =
+ addConstraint $ (left `LessThan` right) `Or` (left `Equals` right)
+
+-- | Enforces that the value of an expression is greater than the value of
+-- another expression.
+infix 4 #>
+(#>) :: Expression -> Expression -> Constraint
+(#>) = flip (#<)
+
+-- | Enforces that the value of an expression is greater than or equal to
+-- the value of another expression.
+infix 4 #>=
+(#>=) :: Expression -> Expression -> Constraint
+(#>=) = flip (#<=)
+
+-- | Conjunction of constraints, i.e. both constraints must hold.
+infixl 3 /\
+(/\) :: Constraint -> Constraint -> Constraint
+(/\) = (>>)
+
+-- | Disjunction of constraints, i.e. at least one of the two constraints must
+-- hold.
+infixl 2 \/
+(\/) :: Constraint -> Constraint -> Constraint
+(\/) left right = FD $ do
+ (cs, ix) <- get
+ let (lcs, lx) = execState (unFD left) ([], ix)
+ (rcs, nx) = execState (unFD right) ([], lx)
+ case (lcs, rcs) of
+ ( [], _) -> put (cs ++ rcs, nx)
+ ( _, []) -> put (cs ++ lcs, nx)
+ (l:ls, r:rs) ->
+ let leftAnd = foldl And l ls
+ rightAnd = foldl And r rs
+ constraint = leftAnd `Or` rightAnd
+ in put (constraint : cs, nx)
+
+-- | Negates a constraint, i.e. the specified constraint must not hold.
+not' :: Constraint -> Constraint
+not' constraint = FD $ do
+ (cons, ix) <- get
+ let (ncs, nx) = execState (unFD constraint) ([], ix)
+ case ncs of
+ [] -> put (cons, nx)
+ c:cs -> put (recNot (foldl And c cs) : cons, nx)
+ where
+ recNot (Equals l r) = NotEquals l r
+ recNot (NotEquals l r) = Equals l r
+ recNot (LessThan l r) = (r `LessThan` l) `Or` (r `Equals` l)
+ recNot (And l r) = Or (recNot l) (recNot r)
+ recNot (Or l r) = And (recNot l) (recNot r)
+
+-- | Enforces that the all the given expressions have different values.
+allDifferent :: [Expression] -> Constraint
+allDifferent [] = pure ()
+allDifferent (c:cs) = do
+ sequence_ (fmap (c #/=) cs)
+ allDifferent cs
+
+-- | Enforces that the value of an expression lies within two bounds.
+between :: 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.
+between low high target = do
+ target #>= low
+ target #<= high
+
+-- | Creates a new variable with a default value range from negative infinity
+-- to positive infinity. Values are assigned to variables during 'labeling'.
+newVar :: FD Expression
+newVar = FD $ do
+ (cs, iD) <- get
+ put (cs, iD + 1)
+ pure (var iD)
+
+-- | Creates a new variable and initializes it with a specific value.
+initNewVar :: Expression -> FD Expression
+initNewVar initExpr = do
+ v <- newVar
+ v #= initExpr
+ pure v
+
+-- | 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.
+data Labeling a
+ = Unsolvable [D.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 [D.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.
+ deriving (Eq, Show)
+
+instance Functor Labeling where
+ fmap _ (Unsolvable ds) = Unsolvable ds
+ fmap _ (Unbounded ds) = Unbounded ds
+ fmap f (Solutions xs) = Solutions (fmap f xs)
+
+instance Applicative Labeling where
+ pure a = Solutions [a]
+ Unsolvable ds <*> _ = Unsolvable ds
+ Unbounded ds <*> _ = Unbounded ds
+ _ <*> Unsolvable ds = Unsolvable ds
+ _ <*> Unbounded ds = Unbounded ds
+ Solutions f <*> Solutions a = Solutions (f <*> a)
+
+instance Monad Labeling where
+ Unsolvable ds >>= _ = Unsolvable ds
+ Unbounded ds >>= _ = Unbounded ds
+ Solutions xs >>= f = go [] xs
+ where
+ go acc [] = Solutions acc
+ go acc (y:ys) =
+ case f y of
+ Unsolvable ds -> Unsolvable ds
+ Unbounded ds -> Unbounded ds
+ Solutions bs -> go (acc ++ bs) ys
+
+-- | 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.
+labeling :: [Expression] -> FD (Labeling [Int])
+labeling vars = do
+ cons <- FD (fmap fst get)
+ pure $
+ runST $ do
+ (res, rvs, cells) <- cellifyConstraints cons []
+ trueCell <- cell True mustHoldJoin
+ allCell <- cell D.maxDomain domainJoin
+ forM_ res $ \c -> connect c trueCell pure
+ let userCells = fmap snd userView
+ userView =
+ flip fmap vars $ \v -> do
+ case find ((== v) . fst) rvs of
+ Just av -> av
+ Nothing -> (v, allCell)
+ propagation <- propagateMany cells
+ snapshot <- forM userCells P.readCell
+ if not (succeeded propagation) then
+ pure (Unsolvable snapshot)
+ else do
+ if any D.isInfinite snapshot then
+ pure (Unbounded snapshot)
+ else do
+ result <- label (concat . D.elems) D.singleton userCells
+ case result of
+ [] -> pure (Unsolvable snapshot)
+ xs -> pure (Solutions xs)
+
+type DomainCell s = Cell s (D.Domain Int)
+type LogicCell s = Cell s Bool
+type VarCell s = (Expression, DomainCell s)
+
+-- | Converts constraints to propagator cells.
+-- The result consists of the new cells that represent the constraints, a list
+-- of currently declared variables, and a list of all cells that were created
+-- for the constraints.
+cellifyConstraints
+ :: [IntConstraint]
+ -> [VarCell s]
+ -> ST s ([LogicCell s], [VarCell s], [DomainCell s])
+cellifyConstraints cons vars =
+ case cons of
+ [] -> pure ([], vars, [])
+ c:cs -> do
+ (ls, nvs, xs) <- cellifyConstraint c vars
+ (rs, rvs, ys) <- cellifyConstraints cs nvs
+ pure (ls : rs, rvs, xs ++ ys)
+
+-- | Converts a constraint to a propagator cell.
+-- The result consists of the new cell that represents the constraint, a list
+-- of currently declared variables, and a list of all cells that were created
+-- for this constraint.
+cellifyConstraint
+ :: IntConstraint
+ -> [VarCell s]
+ -> ST s (LogicCell s, [VarCell s], [DomainCell s])
+cellifyConstraint constraint vars =
+ case constraint of
+ Equals left right ->
+ binary left right sync
+ NotEquals left right ->
+ binary left right (syncWith D.notEqual D.notEqual)
+ LessThan left right ->
+ binary left right (syncWith D.greaterThanDomain D.lessThanDomain)
+ And left right -> do
+ (ls, nvs, xs) <- cellifyConstraint left vars
+ (rs, rvs, ys) <- cellifyConstraint right nvs
+ newCell <- cell True eqJoin
+ connect ls newCell (\ld -> (ld &&) <$> P.readCell rs)
+ connect rs newCell (\rd -> (&& rd) <$> P.readCell ls)
+ pure (newCell, rvs, xs ++ ys)
+ Or left right -> do
+ (ls, lvs, xs) <- cellifyConstraint left []
+ (rs, rvs, ys) <- cellifyConstraint right []
+ newCell <- cell True eqJoin
+ connect ls newCell (\ld -> (ld ||) <$> P.readCell rs)
+ connect rs newCell (\rd -> (|| rd) <$> P.readCell ls)
+ let (pairs, solos) = split lvs rvs
+ pairNews <-
+ forM pairs $ \(v,lc,rc) -> do
+ (varCell, new) <-
+ case find ((v ==) . fst) vars of
+ Just av -> pure (snd av, [])
+ Nothing -> do
+ varCell <- cell D.maxDomain domainJoin
+ pure (varCell, [(v, varCell)])
+ connect varCell lc pure
+ connect varCell rc pure
+ connect lc varCell (\ld -> D.union ld <$> P.readCell rc)
+ connect rc varCell (\rd -> (`D.union` rd) <$> P.readCell lc)
+ pure new
+ soloNews <-
+ forM solos $ \(v,sc) -> do
+ (varCell, new) <-
+ case find ((v ==) . fst) vars of
+ Just av -> pure (snd av, [])
+ Nothing -> do
+ varCell <- cell D.maxDomain domainJoin
+ pure (varCell, [(v, varCell)])
+ connect varCell sc pure
+ pure new
+ pure (newCell, concat pairNews ++ concat soloNews ++ vars, xs ++ ys)
+ where
+ binary left right wire = do
+ (ls, lcs, xs) <- cellifyExpression left vars
+ (rs, rcs, ys) <- cellifyExpression right lcs
+ newCell <- cell True eqJoin
+ _ <- wire ls rs
+ connect ls newCell (pure . not . D.null)
+ connect rs newCell (pure . not . D.null)
+ pure (newCell, rcs, xs ++ ys)
+
+-- | Tries to find an expression in a cell list. If it is found, it is removed
+-- from the list.
+extract :: Expression -> [VarCell s] -> Maybe (VarCell s, [VarCell s])
+extract _ [] = Nothing
+extract a (x:xs) | a == fst x = Just (x, xs)
+ | otherwise = do (b, rs) <- extract a xs
+ pure (b, x : rs)
+
+-- | Takes to list of cells and checks if any two entries of the lists stand
+-- for the same expression. If so, they land in the first tuple entry of the
+-- result (i.e., we pair them). All other "solo entries" of both lists with no
+-- counterpart are collected in the second tuple entry.
+split :: [VarCell s]
+ -> [VarCell s]
+ -> ([(Expression, DomainCell s, DomainCell s)], [VarCell s])
+split [] right = ([], right)
+split (x:xs) right =
+ case extract xVar right of
+ Just (a, rs) ->
+ let (ps, vs) = split xs rs
+ in ((xVar, snd x, snd a) : ps, vs)
+ Nothing ->
+ let (ps, vs) = split xs right
+ in (ps, x : vs)
+ where
+ xVar = fst x \ No newline at end of file
diff --git a/src/AI/Search/FiniteDomain/Int/Expression.hs b/src/AI/Search/FiniteDomain/Int/Expression.hs
new file mode 100644
index 0000000..feedb6e
--- /dev/null
+++ b/src/AI/Search/FiniteDomain/Int/Expression.hs
@@ -0,0 +1,99 @@
+module AI.Search.FiniteDomain.Int.Expression
+ ( Expression
+ , cellifyExpression
+ , int
+ , sum
+ , var
+ ) where
+
+-- base
+import Control.Monad.ST ( ST )
+import Data.List ( find )
+import Prelude hiding ( sum )
+
+-- domain
+import Numeric.Domain as D ( Domain, div, inverseAbs, inverseSignum, singleton
+ , maxDomain )
+
+-- propeller
+import Data.Propagator.Cell ( Cell, cell )
+import Data.Propagator.Num as P ( absWith, plus, minus, timesWith, negate
+ , signumWith )
+
+import AI.Search.FiniteDomain.Int.Cell ( domainJoin )
+
+-- | Expressions are the build blocks of constraints. Note that 'Expression' is
+-- an instance of 'Num', so arithmetic combinations of expressions are possible.
+data Expression
+ = Int Int
+ | Var Int
+ | Plus Expression Expression
+ | Minus Expression Expression
+ | Times Expression Expression
+ | Negate Expression
+ | Abs Expression
+ | Signum Expression
+ deriving (Eq, Ord, Show)
+
+instance Num Expression where
+ (+) = Plus
+ (-) = Minus
+ (*) = Times
+ negate = Negate
+ abs = Abs
+ signum = Signum
+ fromInteger = Int . fromInteger
+
+type DomainCell s = Cell s (Domain Int)
+type VarCell s = (Expression, DomainCell s)
+
+-- | Converts an expression to a propagator cell.
+-- The result consists of the new cell that represents the expression, a list
+-- of currently declared variables, and a list of all cells that were created
+-- for this expression.
+cellifyExpression
+ :: Expression
+ -> [VarCell s]
+ -> ST s (DomainCell s, [VarCell s], [DomainCell s])
+cellifyExpression expr vars =
+ case expr of
+ Int i -> atomic (singleton i)
+ Var _ -> atomic maxDomain
+ Plus left right -> binary left right plus
+ Minus left right -> binary left right minus
+ Times left right -> binary left right (timesWith D.div)
+ Negate arg -> unary arg P.negate
+ Abs arg -> unary arg (absWith inverseAbs)
+ Signum arg -> unary arg (signumWith inverseSignum)
+ where
+ atomic initValue =
+ case find ((expr ==) . fst) vars of
+ Just ce -> pure (snd ce, vars, [])
+ Nothing -> do newCell <- cell initValue domainJoin
+ pure (newCell, (expr, newCell) : vars, [newCell])
+ unary arg wire = do
+ (es, rvs, xs) <- cellifyExpression arg vars
+ newCell <- cell maxDomain domainJoin
+ _ <- wire es newCell
+ pure (newCell, rvs, xs)
+ binary left right wire = do
+ (ls, nvs, xs) <- cellifyExpression left vars
+ (rs, rvs, ys) <- cellifyExpression right nvs
+ newCell <- cell maxDomain domainJoin
+ _ <- wire ls rs newCell
+ pure (newCell, rvs, xs ++ ys)
+
+-- | Converts an integer into an expression that can be used in constraint
+-- formulations.
+int :: Int -> Expression
+int = Int
+
+-- | Converts a variable ID into an expression that can be used in constraint
+-- formulations.
+var :: Int -> Expression
+var = Var
+
+-- | Sums up a list of expressions.
+sum :: [Expression] -> Expression
+sum [] = int 0
+sum (e:es) = e + sum es \ No newline at end of file