monadiccp (empty) → 0.1
raw patch · 13 files changed
+1578/−0 lines, 13 filesdep +basedep +containersdep +haskell98setup-changed
Dependencies added: base, containers, haskell98, mtl, random
Files
- LICENSE +26/−0
- Language/CP/ComposableTransformers.hs +274/−0
- Language/CP/Domain.hs +167/−0
- Language/CP/FD.hs +412/−0
- Language/CP/FDSugar.hs +129/−0
- Language/CP/Main.hs +90/−0
- Language/CP/PriorityQueue.hs +110/−0
- Language/CP/Queue.hs +44/−0
- Language/CP/SearchTree.hs +175/−0
- Language/CP/Solver.hs +30/−0
- Language/CP/Transformers.hs +104/−0
- Setup.hs +4/−0
- monadiccp.cabal +13/−0
+ LICENSE view
@@ -0,0 +1,26 @@+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.++The names of its contributors may not 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.+
+ Language/CP/ComposableTransformers.hs view
@@ -0,0 +1,274 @@+{- + - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE FlexibleContexts #-}++module Language.CP.ComposableTransformers where ++import Language.CP.Transformers+import Language.CP.SearchTree+import Language.CP.Solver+import Language.CP.Queue++import System.Random (mkStdGen, randoms)++--------------------------------------------------------------------------------+-- EVALUATION+--------------------------------------------------------------------------------++solve :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,+ Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) + => q -> c -> Tree solver (CForResult c) -> (Int,[CForResult c])+solve q c model = runSM $ eval model q (TStack c)++--------------------------------------------------------------------------------+-- COMPOSABLE TRANSFORMERS+--------------------------------------------------------------------------------++data TStack es ts (solver :: * -> *) a where+ TStack :: (CTransformer c, CForSolver c ~ solver, CForResult c ~ a) + => c -> TStack (CEvalState c) (CTreeState c) solver a++instance Solver solver => Transformer (TStack es ts solver a) where+ type EvalState (TStack es ts solver a) = es+ type TreeState (TStack es ts solver a) = ts+ type ForSolver (TStack es ts solver a) = solver+ type ForResult (TStack es ts solver a) = a+ initT (TStack c) _ = return $ initCT c+ leftT (TStack c) _ = leftCT c+ rightT (TStack c) _ = rightCT c+ nextT = nextTStack + returnT i wl t@(TStack c) es = returnCT c es (\es' -> continue i wl t es') (\es' -> endT i wl t es')++nextTStack :: + (Solver solver, Queue q, Elem q ~ (Label solver,Tree solver a,ts))+ => Int -> Tree solver a -> q -> (TStack es ts solver a) -> es -> ts -> solver (Int,[a])+nextTStack i tree q t es ts =+ case t of+ TStack c ->+ nextCT tree c es ts (\tree' es' ts' -> eval' i tree' q t es' ts') + (\es' -> continue i q t es')+ (\es' -> endT i q t es')++--------------------------------------------------------------------------------+type CSearchSig c a =+ (Solver (CForSolver c), CTransformer c) + => Tree (CForSolver c) a -> c -> CEvalState c -> CTreeState c -> (EVAL c a) -> (CONTINUE c a) -> (EXIT c a) -> (CForSolver c) (Int,[a])++type CContinueSig c a =+ (Solver (CForSolver c), CTransformer c) + => c -> CEvalState c -> (CONTINUE c a) -> (EXIT c a) -> (CForSolver c) (Int,[a])++type EVAL c a = (Tree (CForSolver c) a -> CEvalState c -> CTreeState c-> (CForSolver c) (Int,[a]))+type CONTINUE c a = (CEvalState c -> (CForSolver c) (Int,[a]))+type EXIT c a = (CEvalState c) -> (CForSolver c) (Int,[a]) ++class Solver (CForSolver c) => CTransformer c where+ type CEvalState c :: *+ type CTreeState c :: *+ type CForSolver c :: (* -> *)+ type CForResult c :: *+ initCT :: c -> (CEvalState c, CTreeState c)+ leftCT, rightCT :: c -> CTreeState c -> CTreeState c+ leftCT _ = id+ rightCT = leftCT+ nextCT :: CSearchSig c (CForResult c)+ nextCT = evalCT+ returnCT :: CContinueSig c (CForResult c) + returnCT = continueCT+ completeCT :: c -> CEvalState c -> Bool+ completeCT _ _ = True++evalCT :: CSearchSig c a+evalCT tree c es ts eval continue exit =+ eval tree es ts++continueCT :: CContinueSig c a+continueCT c es continue exit =+ continue es++exitCT :: CContinueSig c a+exitCT c es continue exit =+ exit es++newtype CNodeBoundedST (solver :: * -> *) a = CNBST Int++instance Solver solver => CTransformer (CNodeBoundedST solver a) where+ type CEvalState (CNodeBoundedST solver a) = Int+ type CTreeState (CNodeBoundedST solver a) = ()+ type CForSolver (CNodeBoundedST solver a) = solver+ type CForResult (CNodeBoundedST solver a) = a+ initCT (CNBST n) = (n,()) + nextCT tree c es ts eval' continue exit+ | es == 0 = exit es+ | otherwise = eval' tree (es - 1) ts++newtype CDepthBoundedST (solver :: * -> *) a = CDBST Int++instance Solver solver => CTransformer (CDepthBoundedST solver a) where+ type CEvalState (CDepthBoundedST solver a) = Bool+ type CTreeState (CDepthBoundedST solver a) = Int+ type CForSolver (CDepthBoundedST solver a) = solver+ type CForResult (CDepthBoundedST solver a) = a+ initCT (CDBST n) = (True,n)+ leftCT _ ts = ts - 1+ nextCT tree c es ts eval' continue exit+ | ts == 0 = continue False+ | otherwise = eval' tree es ts+ completeCT _ es = es++newtype CLimitedDiscrepancyST (solver :: * -> *) a = CLDST Int++instance Solver solver => CTransformer (CLimitedDiscrepancyST solver a) where+ type CEvalState (CLimitedDiscrepancyST solver a) = ()+ type CTreeState (CLimitedDiscrepancyST solver a) = Int+ type CForSolver (CLimitedDiscrepancyST solver a) = solver+ type CForResult (CLimitedDiscrepancyST solver a) = a+ initCT (CLDST n) = ((),n)+ rightCT _ n = n - 1+ nextCT tree c es ts eval' continue exit+ | ts == 0 = continue es+ | otherwise = eval' tree es ts++newtype CRandomST (solver :: * -> *) a = CRST Int++instance Solver solver => CTransformer (CRandomST solver a) where+ type CEvalState (CRandomST solver a) = [Bool]+ type CTreeState (CRandomST solver a) = ()+ type CForSolver (CRandomST solver a) = solver+ type CForResult (CRandomST solver a) = a+ initCT (CRST n) = (randoms $ mkStdGen n,())+ nextCT tree@(Try l r) c (switch:es)+ | switch = evalCT (Try r l) c es+ | otherwise = evalCT tree c es+ nextCT tree@(Add d (Try l r)) c (switch:es)+ | switch = evalCT (Add d (Try r l)) c es+ | otherwise = evalCT tree c es+ nextCT tree c es = evalCT tree c es++data CIdentityCST (solver :: * -> *) a = CIST++instance Solver solver => CTransformer (CIdentityCST solver a) where+ type CEvalState (CIdentityCST solver a) = ()+ type CTreeState (CIdentityCST solver a) = ()+ type CForSolver (CIdentityCST solver a) = solver+ type CForResult (CIdentityCST solver a) = a+ initCT _ = ((),())++data CFirstSolutionST (solver :: * -> *) a = CFSST++instance Solver solver => CTransformer (CFirstSolutionST solver a) where+ type CEvalState (CFirstSolutionST solver a) = Bool+ type CTreeState (CFirstSolutionST solver a) = ()+ type CForSolver (CFirstSolutionST solver a) = solver+ type CForResult (CFirstSolutionST solver a) = a+ initCT _ = (True,())+ returnCT _ es continue exit =+ exit False+ completeCT _ es = es +++--------------------------------------------------------------------------------+data Composition es ts solver a where+ (:-) :: (CTransformer c1, CTransformer c2,+ CForSolver c1 ~ solver, CForSolver c2 ~ solver,+ CForResult c1 ~ a, CForResult c2 ~ a+ ) + => c1 -> c2 -> Composition (CEvalState c1,CEvalState c2) (CTreeState c1,CTreeState c2) solver a++instance Solver solver => CTransformer (Composition es ts solver a) where+ type CEvalState (Composition es ts solver a) = es+ type CTreeState (Composition es ts solver a) = ts+ type CForSolver (Composition es ts solver a) = solver+ type CForResult (Composition es ts solver a) = a+ initCT (c1 :- c2) = let (es1,ts1) = initCT c1 + (es2,ts2) = initCT c2 + in ((es1,es2),(ts1,ts2))+ leftCT (c1 :- c2) (ts1,ts2) = (leftCT c1 ts1,leftCT c2 ts2)+ rightCT (c1 :- c2) (ts1,ts2) = (rightCT c1 ts1,rightCT c2 ts2)+ nextCT tree (c1 :- c2) (es1,es2) (ts1,ts2) eval' continue exit =+ nextCT tree c1 es1 ts1 + (\tree' es1' ts1' -> nextCT tree' c2 es2 ts2 + (\tree'' es2' ts2' -> eval' tree'' (es1',es2') (ts1',ts2'))+ (\es2' -> continue (es1',es2'))+ (\es2' -> exit (es1',es2')) ) + (\es1' -> continue (es1',es2))+ (\es1' -> exit (es1',es2))+ returnCT (c1 :- c2) (es1,es2) continue exit =+ returnCT c1 es1 (\es1' -> returnCT c2 es2 (\es2' -> continue (es1',es2')) (\es2' -> exit (es1',es2'))) + (\es1' -> exit (es1',es2))+ completeCT (c1 :- c2) (es1,es2) = completeCT c1 es1 && completeCT c2 es2++--------------------------------------------------------------------------------+-- BRANCH & BOUND+--------------------------------------------------------------------------------++newtype CBranchBoundST (solver :: * -> *) a = CBBST (NewBound solver) +data BBEvalState solver = BBP Int (Bound solver)++type Bound solver = forall a. Tree solver a -> Tree solver a+type NewBound solver = solver (Bound solver)++instance Solver solver => CTransformer (CBranchBoundST solver a) where+ type CEvalState (CBranchBoundST solver a) = BBEvalState solver+ type CTreeState (CBranchBoundST solver a) = Int+ type CForSolver (CBranchBoundST solver a) = solver+ type CForResult (CBranchBoundST solver a) = a+ initCT _ = (BBP 0 id,0)+ nextCT tree c es@(BBP nv bound) v eval continue exit+ | nv > v = eval (bound tree) es nv+ | otherwise = eval tree es v+ returnCT (CBBST newBound) (BBP v bound) continue exit =+ do bound' <- newBound+ continue $ BBP (v + 1) bound' ++--------------------------------------------------------------------------------+-- RESTARTING+--------------------------------------------------------------------------------++data SealedCST es ts solver a where+ Seal :: CTransformer c => c -> SealedCST (CEvalState c) (CTreeState c) (CForSolver c) (CForResult c)++instance Solver solver => CTransformer (SealedCST es ts solver a) where+ type CEvalState (SealedCST es ts solver a) = es+ type CTreeState (SealedCST es ts solver a) = ts+ type CForSolver (SealedCST es ts solver a) = solver+ type CForResult (SealedCST es ts solver a) = a+ leftCT (Seal c) = leftCT c+ rightCT (Seal c) = rightCT c+ initCT (Seal c) = initCT c+ nextCT tree (Seal c) = nextCT tree c+ returnCT (Seal c) = returnCT c+ completeCT (Seal c) = completeCT c++data RestartST es ts (solver :: * -> *) a = RestartST [SealedCST es ts solver a] (Tree solver a -> solver (Tree solver a))++instance Solver solver => Transformer (RestartST es ts solver a) where+ type EvalState (RestartST es ts solver a) = (SealedCST es ts solver a,[SealedCST es ts solver a],es,Label solver,Tree solver a)+ type TreeState (RestartST es ts solver a) = ts+ type ForSolver (RestartST es ts solver a) = solver+ type ForResult (RestartST es ts solver a) = a+ initT (RestartST (c:cs) _) tree = + let (es,ts) = initCT c+ in do l <- markSM+ return ((c,cs,es,l,tree),ts)+ leftT _ (c,_,_,_,_) = leftCT c+ rightT _ (c,_,_,_,_) = rightCT c+ nextT i tree q t es@(c,cs,es_c,l,tree0) ts = + nextCT tree c es_c ts (\tree' es_c' ts' -> eval' i tree' q t (c,cs,es_c',l,tree0) ts') + (\es_c' -> continue i q t (c,cs,es_c',l,tree0))+ (\es_c' -> endT i q t (c,cs,es_c',l,tree0))+ returnT i wl t es@(c,cs,es_c,l,tree0) = returnCT c es_c (\es_c' -> continue i wl t (c,cs,es_c',l,tree0)) (\es_c' -> endT i wl t (c,cs,es_c',l,tree0))+ endT i wl t es@(_,[],_,_,_) = return (i,[])+ endT i wl t@(RestartST _ f) es@(c0,(c:cs),es_c0,l,tree0) + | completeCT c0 es_c0 = return (i,[])+ | otherwise = let (es,ts) = initCT c+ in do tree' <- f tree0+ continue i (pushQ (l,tree',ts) $ emptyQ wl) t (c,cs,es,l,tree0)+
+ Language/CP/Domain.hs view
@@ -0,0 +1,167 @@+{- + - Origin:+ - Constraint Programming in Haskell + - http://overtond.blogspot.com/2008/07/pre.html+ - author: David Overton, Melbourne Australia+ -+ - Modifications:+ - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -} ++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE IncoherentInstances #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.CP.Domain (+ Domain,+ ToDomain,+ toDomain,+ member,+ isSubsetOf,+ elems,+ intersection,+ difference,+ union,+ empty,+ null,+ singleton,+ isSingleton,+ filterLessThan,+ filterGreaterThan,+ findMax,+ findMin,+ size,+ shiftDomain+) where++import qualified Data.IntSet as IntSet+import Data.IntSet (IntSet)+import Prelude hiding (null)++data Domain+ = Set IntSet+ | Range Int Int+ deriving Show++size :: Domain -> Int+size (Range l u) = u - l + 1+size (Set set) = IntSet.size set++-- Domain constructors+class ToDomain a where+ toDomain :: a -> Domain++instance ToDomain Domain where+ toDomain = id++instance ToDomain IntSet where+ toDomain = Set++instance Integral a => ToDomain [a] where+ toDomain = toDomain . IntSet.fromList . map fromIntegral++instance (Integral a, Integral b) => ToDomain (a, b) where+ toDomain (a, b) = Range (fromIntegral a) (fromIntegral b)++instance ToDomain () where+ toDomain () = Range minBound maxBound++instance Integral a => ToDomain a where+ toDomain a = toDomain (a, a)++-- Operations on Domains+instance Eq Domain where+ (Range xl xh) == (Range yl yh) = xl == yl && xh == yh+ xs == ys = elems xs == elems ys++member :: Int -> Domain -> Bool+member n (Set xs) = n `IntSet.member` xs+member n (Range xl xh) = n >= xl && n <= xh++isSubsetOf :: Domain -> Domain -> Bool+isSubsetOf (Set xs) (Set ys) = xs `IntSet.isSubsetOf` ys+isSubsetOf (Range xl xh) (Range yl yh) = xl >= yl && xh <= yh+isSubsetOf (Set xs) yd@(Range yl yh) =+ isSubsetOf (Range xl xh) yd where+ xl = IntSet.findMin xs+ xh = IntSet.findMax xs+isSubsetOf (Range xl xh) (Set ys) =+ all (`IntSet.member` ys) [xl..xh]++elems :: Domain -> [Int]+elems (Set xs) = IntSet.elems xs+elems (Range xl xh) = [xl..xh]++intersection :: Domain -> Domain -> Domain+intersection (Set xs) (Set ys) = Set (xs `IntSet.intersection` ys)+intersection (Range xl xh) (Range yl yh) = Range (max xl yl) (min xh yh)+intersection (Set xs) (Range yl yh) =+ Set $ IntSet.filter (\x -> x >= yl && x <= yh) xs+intersection x y = intersection y x++union :: Domain -> Domain -> Domain+union (Set xs) (Set ys) = Set (xs `IntSet.union` ys)+union (Range xl xh) (Range yl yh) + | xh + 1 >= yl || yh+1 >= xl = Range (min xl yl) (max xh yh)+ | otherwise = union (Set $ IntSet.fromList [xl..xh]) + (Set $ IntSet.fromList [yl..yh]) +union x@(Set xs) y@(Range yl yh) =+ if null x then y + else+ let xmin = IntSet.findMin xs+ xmax = IntSet.findMax xs+ in + if (xmin + 1 >= yl && xmax - 1 <= yh) + then Range (min xmin yl) (max xmax yh)+ else union (Set xs) (Set $ IntSet.fromList [yl..yh])+union x y = union y x++difference :: Domain -> Domain -> Domain+difference (Set xs) (Set ys) = Set (xs `IntSet.difference` ys)+difference xd@(Range xl xh) (Range yl yh)+ | yl > xh || yh < xl = xd+ | otherwise = Set $ IntSet.fromList [x | x <- [xl..xh], x < yl || x > yh]+difference (Set xs) (Range yl yh) =+ Set $ IntSet.filter (\x -> x < yl || x > yh) xs+difference (Range xl xh) (Set ys)+ | IntSet.findMin ys > xh || IntSet.findMax ys < xl = Range xl xh+ | otherwise = Set $+ IntSet.fromList [x | x <- [xl..xh], not (x `IntSet.member` ys)]++null :: Domain -> Bool+null (Set xs) = IntSet.null xs+null (Range xl xh) = xl > xh++singleton :: Int -> Domain+singleton x = Set (IntSet.singleton x)++isSingleton :: Domain -> Bool+isSingleton (Set xs) = case IntSet.elems xs of+ [x] -> True+ _ -> False+isSingleton (Range xl xh) = xl == xh++filterLessThan :: Int -> Domain -> Domain+filterLessThan n (Set xs) = Set $ IntSet.filter (< n) xs+filterLessThan n (Range xl xh) = Range xl (min (n-1) xh)++filterGreaterThan :: Int -> Domain -> Domain+filterGreaterThan n (Set xs) = Set $ IntSet.filter (> n) xs+filterGreaterThan n (Range xl xh) = Range (max (n+1) xl) xh++findMax :: Domain -> Int+findMax (Set xs) = IntSet.findMax xs+findMax (Range xl xh) = xh++findMin :: Domain -> Int+findMin (Set xs) = IntSet.findMin xs+findMin (Range xl xh) = xl++empty :: Domain+empty = Range 1 0++shiftDomain :: Domain -> Int -> Domain+shiftDomain (Range l u) d = Range (l + d) (u + d)+shiftDomain (Set xs) d = Set $ IntSet.fromList $ map (+d) (IntSet.elems xs)
+ Language/CP/FD.hs view
@@ -0,0 +1,412 @@+{- + - Origin:+ - Constraint Programming in Haskell + - http://overtond.blogspot.com/2008/07/pre.html+ - author: David Overton, Melbourne Australia+ -+ - Modifications:+ - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -} ++{-# OPTIONS_GHC -fglasgow-exts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE OverlappingInstances #-}+module Language.CP.FD where ++import Prelude hiding (lookup)+import Maybe (fromJust,isJust)+import Control.Monad.State.Lazy+import Control.Monad.Trans+import qualified Data.Map as Map+import Data.Map ((!), Map)+import Control.Monad (liftM,(<=<))++import Language.CP.Domain as Domain++import Language.CP.Solver++-- import Debug.Trace+trace = flip const+--------------------------------------------------------------------------------+-- Solver instance -------------------------------------------------------------+--------------------------------------------------------------------------------++instance Solver FD where+ type Constraint FD = FD_Constraint+ type Term FD = FD_Term+ type Label FD = FDState++ newvarSM = newVar () >>= return . FD_Var + addSM = addFD+ storeSM = undefined+ runSM p = runFD p++ markSM = get+ gotoSM = put ++data FD_Term where+ FD_Var :: FDVar -> FD_Term+ deriving Show++un_fd (FD_Var v) = v++data FD_Constraint where+ FD_Diff :: FD_Term -> FD_Term -> FD_Constraint+ FD_Same :: FD_Term -> FD_Term -> FD_Constraint+ FD_Less :: FD_Term -> FD_Term -> FD_Constraint+ FD_LT :: FD_Term -> Int -> FD_Constraint+ FD_GT :: FD_Term -> Int -> FD_Constraint+ FD_HasValue :: FD_Term -> Int -> FD_Constraint+ FD_Eq :: (ToExpr a, ToExpr b) => a -> b -> FD_Constraint+ FD_NEq :: (ToExpr a, ToExpr b) => a -> b -> FD_Constraint+ FD_AllDiff :: [FD_Term] -> FD_Constraint+ FD_Dom :: FD_Term -> (Int,Int) -> FD_Constraint++addFD (FD_Diff (FD_Var v1) (FD_Var v2)) = different v1 v2+addFD (FD_Same (FD_Var v1) (FD_Var v2)) = same v1 v2+addFD (FD_Less (FD_Var v1) (FD_Var v2)) = v1 .<. v2 +addFD (FD_HasValue (FD_Var v1) i) = hasValue v1 i+addFD (FD_Eq e1 e2) = e1 .==. e2+addFD (FD_NEq e1 e2) = e1 ./=. e2 +-- addFD (FD_AllDiff vs) = allDifferent (map un_fd vs)+addFD (FD_Dom v (l,u)) = v `in_range` (l-1,u+1)+addFD (FD_LT (FD_Var v) i) = do iv <- exprVar $ toExpr i+ v .<. iv+addFD (FD_GT (FD_Var v) i) = do iv <- exprVar $ toExpr i+ iv .<. v+++(#<) :: (To_FD_Term a, To_FD_Term b) => a -> b -> FD Bool+x #< y =+ do xt <- to_fd_term x+ yt <- to_fd_term y+ addFD (FD_Less xt yt)++in_range :: FD_Term -> (Int,Int) -> FD Bool+in_range x (l,u) =+ do l #< x+ x #< u++all_different = addFD . FD_AllDiff++instance ToExpr FD_Term where+ toExpr (FD_Var v) = toExpr v++fd_domain :: FD_Term -> FD [Int]+fd_domain (FD_Var v) = do d <- lookup v+ return $ elems d++fd_objective :: FD FD_Term+fd_objective =+ do s <- get+ return $ FD_Var $ objective s++class To_FD_Term a where+ to_fd_term :: a -> FD FD_Term++instance To_FD_Term FD_Term where+ to_fd_term = return . id++instance To_FD_Term Int where+ to_fd_term i = newVar i >>= return . FD_Var++instance To_FD_Term Expr where+ to_fd_term e = unExpr e >>= return . FD_Var++--------------------------------------------------------------------------------++-- The FD monad+newtype FD a = FD { unFD :: StateT FDState Maybe a }+ deriving (Monad, MonadState FDState, MonadPlus)++-- FD variables+newtype FDVar = FDVar { unFDVar :: Int } deriving (Ord, Eq, Show)++type VarSupply = FDVar++data VarInfo = VarInfo+ { delayedConstraints :: FD Bool, domain :: Domain }++instance Show VarInfo where+ show x = show $ domain x++type VarMap = Map FDVar VarInfo++data FDState = FDState+ { varSupply :: VarSupply, varMap :: VarMap, objective :: FDVar }+ deriving Show++instance Eq FDState where+ s1 == s2 = f s1 == f s2+ where f s = head $ elems $ domain $ varMap s ! (objective s) ++instance Ord FDState where+ compare s1 s2 = compare (f s1) (f s2)+ where f s = head $ elems $ domain $ varMap s ! (objective s) ++ -- TOM: inconsistency is not observable within the FD monad+consistentFD :: FD Bool+consistentFD = return True++-- Run the FD monad and produce a lazy list of possible solutions.+runFD :: FD a -> a+runFD fd = fromJust $ evalStateT (unFD fd') initState+ where fd' = fd -- fd' = newVar () >> fd++initState :: FDState+initState = FDState { varSupply = FDVar 0, varMap = Map.empty, objective = FDVar 0 }++-- Get a new FDVar+newVar :: ToDomain a => a -> FD FDVar+newVar d = do+ s <- get+ let v = varSupply s+ put $ s { varSupply = FDVar (unFDVar v + 1) }+ modify $ \s ->+ let vm = varMap s+ vi = VarInfo {+ delayedConstraints = return True,+ domain = toDomain d}+ in+ s { varMap = Map.insert v vi vm }+ return v++newVars :: ToDomain a => Int -> a -> FD [FDVar]+newVars n d = replicateM n (newVar d)++-- Lookup the current domain of a variable.+lookup :: FDVar -> FD Domain+lookup x = do+ s <- get+ return . domain $ varMap s ! x++-- Update the domain of a variable and fire all delayed constraints+-- associated with that variable.+update :: FDVar -> Domain -> FD Bool+update x i = do+ trace (show x ++ " <- " ++ show i) (return ())+ s <- get+ let vm = varMap s+ let vi = vm ! x+ trace ("where old domain = " ++ show (domain vi)) (return ())+ put $ s { varMap = Map.insert x (vi { domain = i}) vm }+ delayedConstraints vi++-- Add a new constraint for a variable to the constraint store.+addConstraint :: FDVar -> FD Bool -> FD ()+addConstraint x constraint = do+ s <- get+ let vm = varMap s+ let vi = vm ! x+ let cs = delayedConstraints vi+ put $ s { varMap =+ Map.insert x (vi { delayedConstraints = do b <- cs + if b then constraint+ else return False}) vm }+ +-- Useful helper function for adding binary constraints between FDVars.+type BinaryConstraint = FDVar -> FDVar -> FD Bool+addBinaryConstraint :: BinaryConstraint -> BinaryConstraint +addBinaryConstraint f x y = do+ let constraint = f x y+ b <- constraint + when b $ (do addConstraint x constraint+ addConstraint y constraint)+ return b++-- Constrain a variable to a particular value.+hasValue :: FDVar -> Int -> FD Bool+var `hasValue` val = do+ vals <- lookup var+ if val `member` vals+ then do let i = singleton val+ if (i /= vals) + then update var i+ else return True+ else return False++-- Constrain two variables to have the same value.+same :: FDVar -> FDVar -> FD Bool+same = addBinaryConstraint $ \x y -> do+ xv <- lookup x+ yv <- lookup y+ let i = xv `intersection` yv+ if not $ Domain.null i+ then whenwhen (i /= xv) (i /= yv) (update x i) (update y i)+ else return False++whenwhen c1 c2 a1 a2 =+ if c1+ then do b1 <- a1+ if b1 + then if c2+ then a2+ else return True+ else return False + else if c2+ then a2+ else return True++-- Constrain two variables to have different values.+different :: FDVar -> FDVar -> FD Bool+different = addBinaryConstraint $ \x y -> do+ xv <- lookup x+ yv <- lookup y+ if not (isSingleton xv) || not (isSingleton yv) || xv /= yv+ then whenwhen (isSingleton xv && xv `isSubsetOf` yv)+ (isSingleton yv && yv `isSubsetOf` xv)+ (update y (yv `difference` xv))+ (update x (xv `difference` yv))+ else return False++-- Constrain a list of variables to all have different values.+allDifferent :: [FDVar ] -> FD ()+allDifferent (x:xs) = do+ mapM_ (different x) xs+ allDifferent xs+allDifferent _ = return ()++-- Constrain one variable to have a value less than the value of another+-- variable.+infix 4 .<.+(.<.) :: FDVar -> FDVar -> FD Bool+(.<.) = addBinaryConstraint $ \x y -> do+ xv <- lookup x+ yv <- lookup y+ let xv' = filterLessThan (findMax yv) xv+ let yv' = filterGreaterThan (findMin xv) yv+ if not $ Domain.null xv'+ then if not $ Domain.null yv'+ then whenwhen (xv /= xv') (yv /= yv') (update x xv') (update y yv')+ else return False+ else return False++{-+-- Get all solutions for a constraint without actually updating the+-- constraint store.+solutions :: FD s a -> FD s [a]+solutions constraint = do+ s <- get+ return $ evalStateT (unFD constraint) s++-- Label variables using a depth-first left-to-right search.+labelling :: [FDVar s] -> FD s [Int]+labelling = mapM label where+ label var = do+ vals <- lookup var+ val <- FD . lift $ elems vals+ var `hasValue` val+ return val+-}++dump :: [FDVar] -> FD [Domain]+dump = mapM lookup++newtype Expr = Expr { unExpr :: FD (FDVar) }++class ToExpr a where+ toExpr :: a -> Expr++instance ToExpr FDVar where+ toExpr = Expr . return++instance ToExpr Expr where+ toExpr = id++instance Integral i => ToExpr i where+ toExpr n = Expr $ newVar n++exprVar :: ToExpr a => a -> FD FDVar+exprVar = unExpr . toExpr++-- Add constraint (z = x `op` y) for new var z+addArithmeticConstraint :: (ToExpr a, ToExpr b) =>+ (Domain -> Domain -> Domain) ->+ (Domain -> Domain -> Domain) ->+ (Domain -> Domain -> Domain) ->+ a -> b -> Expr+addArithmeticConstraint getZDomain getXDomain getYDomain xexpr yexpr = Expr $ do+ x <- exprVar xexpr+ y <- exprVar yexpr+ xv <- lookup x+ yv <- lookup y+ z <- newVar (getZDomain xv yv)+ let constraint z x y getDomain = do+ xv <- lookup x+ yv <- lookup y+ zv <- lookup z+ let znew = zv `intersection` (getDomain xv yv)+ trace (show z ++ " before: " ++ show zv ++ show "; after: " ++ show znew) (return ())+ if not $ Domain.null znew+ then if (znew /= zv) + then update z znew+ else return True+ else return False+ let zConstraint = constraint z x y getZDomain+ xConstraint = constraint x z y getXDomain+ yConstraint = constraint y z x getYDomain+ addConstraint z xConstraint+ addConstraint z yConstraint+ addConstraint x zConstraint+ addConstraint x yConstraint+ addConstraint y zConstraint+ addConstraint y xConstraint+ return z++infixl 6 .+.+(.+.) :: (ToExpr a, ToExpr b) => a -> b -> Expr+(.+.) = addArithmeticConstraint getDomainPlus getDomainMinus getDomainMinus++infixl 6 .-.+(.-.) :: (ToExpr a, ToExpr b) => a -> b -> Expr+(.-.) = addArithmeticConstraint getDomainMinus getDomainPlus+ (flip getDomainMinus)++infixl 7 .*.+(.*.) :: (ToExpr a, ToExpr b) => a -> b -> Expr+(.*.) = addArithmeticConstraint getDomainMult getDomainDiv getDomainDiv++getDomainPlus :: Domain -> Domain -> Domain+getDomainPlus xs ys = toDomain (zl, zh) where+ zl = findMin xs + findMin ys+ zh = findMax xs + findMax ys++getDomainMinus :: Domain -> Domain -> Domain+getDomainMinus xs ys = toDomain (zl, zh) where+ zl = findMin xs - findMax ys+ zh = findMax xs - findMin ys++getDomainMult :: Domain -> Domain -> Domain+getDomainMult xs ys = toDomain (zl, zh) where+ zl = minimum products+ zh = maximum products+ products = [x * y |+ x <- [findMin xs, findMax xs],+ y <- [findMin ys, findMax ys]]++getDomainDiv :: Domain -> Domain -> Domain+getDomainDiv xs ys = toDomain (zl, zh) where+ zl = minimum quotientsl+ zh = maximum quotientsh+ quotientsl = [if y /= 0 then x `div` y else minBound |+ x <- [findMin xs, findMax xs],+ y <- [findMin ys, findMax ys]]+ quotientsh = [if y /= 0 then x `div` y else maxBound |+ x <- [findMin xs, findMax xs],+ y <- [findMin ys, findMax ys]]++infix 4 .==.+(.==.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool+xexpr .==. yexpr = do+ x <- exprVar xexpr+ y <- exprVar yexpr+ x `same` y++infix 4 ./=.+(./=.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool+xexpr ./=. yexpr = do+ x <- exprVar xexpr+ y <- exprVar yexpr+ x `different` y
+ Language/CP/FDSugar.hs view
@@ -0,0 +1,129 @@+{- + - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}+{-# LANGUAGE TransformListComp #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeFamilies #-}++module Language.CP.FDSugar where ++import Language.CP.SearchTree hiding (label)+import Language.CP.Transformers+import Language.CP.ComposableTransformers+import Language.CP.Queue+import Language.CP.Solver++import GHC.Exts (sortWith)+import qualified Language.CP.PriorityQueue as PriorityQueue+import qualified Data.Sequence+import Language.CP.FD++dfs = []+bfs = Data.Sequence.empty+pfs :: Ord a => PriorityQueue.PriorityQueue a (a,b,c)+pfs = PriorityQueue.empty++nb :: Int -> CNodeBoundedST FD a+nb = CNBST+db :: Int -> CDepthBoundedST FD a+db = CDBST+bb :: NewBound FD -> CBranchBoundST FD a+bb = CBBST+fs :: CFirstSolutionST FD a+fs = CFSST+it :: CIdentityCST FD a+it = CIST+ra :: Int -> CRandomST FD a+ra = CRST+ld :: Int -> CLimitedDiscrepancyST FD a+ld = CLDST++newBound :: NewBound FD+newBound = do obj <- fd_objective+ (val:_) <- fd_domain obj + l <- markSM+ return ((\tree -> tree `insertTree` (obj @< val)) :: forall b . Tree FD b -> Tree FD b)++newBoundBis :: NewBound FD +newBoundBis = do obj <- fd_objective+ (val:_) <- fd_domain obj + let m = val `div` 2+ return ((\tree -> (obj @< (m + 1) \/ ( obj @> m /\ obj @< val)) /\ tree) :: forall b . Tree FD b -> Tree FD b)++restart :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,+ Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) + => q -> [c] -> Tree solver (CForResult c) -> (Int,[CForResult c])+restart q cs model = runSM $ eval model q (RestartST (map Seal cs) return)++restartOpt :: (Queue q, CTransformer c, CForSolver c ~ FD,+ Elem q ~ (Label FD,Tree FD (CForResult c),CTreeState c)) + => q -> [c] -> Tree FD (CForResult c) -> (Int,[CForResult c])+restartOpt q cs model = runSM $ eval model q (RestartST (map Seal cs) opt)+ where opt tree = newBound >>= \f -> return (f tree)++--------------------------------------------------------------------------------+-- ENUMERATION+--------------------------------------------------------------------------------++enumerate = Label . (label in_order) +-- enumerate = Label . (label firstfail) ++label sel qs = do qs' <- sel qs + label' qs' + where label' [] = return true+ label' (q:qs) = do d <- fd_domain q +-- return $ enum q (middleout d) /\ enumerate qs+ return $ enum q d /\ enumerate qs++in_order :: Monad m => a -> m a+in_order = return ++firstfail qs = do ds <- mapM fd_domain qs + return [ q | (d,q) <- zip ds qs + , then sortWith by (length d) ] +enum queen values = + disj [ queen @= value + | value <- values + ] ++value var = do [val] <- fd_domain var+ return val++middleout l = let n = (length l) `div` 2 in+ interleave (drop n l) (reverse $ take n l)++endsout l = let n = (length l) `div` 2 in+ interleave (reverse $ drop n l) (take n l)++interleave [] ys = ys+interleave (x:xs) ys = x:interleave ys xs+--------------------------------------------------------------------------------+-- RESULT+--------------------------------------------------------------------------------++assignments = mapM assignment +assignment q = Label $ value q >>= (return . Return)+--------------------------------------------------------------------------------+-- SYNTACTIC SUGAR+--------------------------------------------------------------------------------++in_domain v (l,u) = Add (FD_Dom v (l,u)) true+(@\=) :: FD_Term -> FD_Term -> Tree FD ()+v1 @\= v2 = Add (FD_NEq v1 v2) true++(@=) :: FD_Term -> Int -> Tree FD ()+v1 @= v2 = Add (FD_Eq v1 v2) true++data Plus = FD_Term :+ Int +(@+) = (:+)++(@\==) :: FD_Term -> Plus -> Tree FD ()+v1 @\== (v2 :+ i) = Add (FD_NEq v1 (v2 .+. i)) true++(@<) :: FD_Term -> Int -> Tree FD ()+v @< i = Add (FD_LT v i) true++(@>) :: FD_Term -> Int -> Tree FD ()+v @> i = Add (FD_GT v i) true
+ Language/CP/Main.hs view
@@ -0,0 +1,90 @@+{- + - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}+module Language.CP.Main where++import Language.CP.ComposableTransformers+import Language.CP.FD+import Language.CP.FDSugar+import List (tails)+import Language.CP.SearchTree hiding (label)+import System (getArgs)++--------------------------------------------------------------------------------+-- MAIN FUNCTIONS+--------------------------------------------------------------------------------++main = main1+++main1 = getArgs >>= print . solve dfs it . nqueens . read . head+main2 = getArgs >>= print . solve dfs (nb 100 :- db 25 :- bb newBound) . nqueens . read . head++main3 = getArgs >>= print . solve dfs (db 9) . nqueens . read . head++main4 = do (n1:_) <- getArgs + let n = read n1+ loop 1 n+ where loop i n+ | i > n = return ()+ | otherwise =+ do -- print . (\(i,l) -> (i,not $ Prelude.null l)) . solve dfs (it :- fs :- ra 13 :- ld l) . nqueens $ i+ print . (\(i,l) -> (i, {- not $ Prelude.null-} l)) . restart dfs (map db [3..10]) . nqueens $ i+ -- print . (\(i,l) -> (i, {- not $ Prelude.null-} l)) . restartOpt dfs (replicate 10 fs) . nqueens $ i+ loop (i+1) n++main5 = getArgs >>= loop 1 . read . head+ where loop i n+ | i > n = return ()+ | otherwise =+ do print . (\(i,l) -> (i,minimum l)) . solve dfs (ld 5 :- bb newBoundBis) . gmodel $ i+ loop (i+1) n++--------------------------------------------------------------------------------+-- PATH MODEL+--------------------------------------------------------------------------------++gmodel n = NewVar $ \_ -> path 1 n 0++path :: Int -> Int -> Int -> Tree FD Int+path x y d = if x == y + then Return d+ else disj [ Label (fd_objective >>= \o -> return (o @> (d+d' - 1) /\ (path z y (d+d')))) + | (z,d') <- edge x+ ]++edge i | i < 20 = [ (i+1,4), (i+2,1) ]+ | otherwise = []++--------------------------------------------------------------------------------+-- N QUEENS MODEL+--------------------------------------------------------------------------------++nqueens n = + exist n $ \queens -> queens `allin` (1,n) /\ + alldifferent queens /\ + diagonals queens /\+ -- enumerate ({- middleout -} endsout queens) /\+ -- enumerate (middleout queens) /\+ enumerate (queens) /\+ assignments queens++allin queens range = + conj [q `in_domain` range + | q <- queens + ] ++alldifferent :: [ FD_Term ] -> Tree FD ()+alldifferent queens =+ conj [ qi @\= qj + | qi:qjs <- tails queens + , qj <- qjs + ]+ +diagonals queens = + conj [ qi @\== (qj @+ d) /\ qj @\== (qi @+ d) + | qi:qjs <- tails queens + , (qj,d) <- zip qjs [1..] + ]
+ Language/CP/PriorityQueue.hs view
@@ -0,0 +1,110 @@+{- Copyright (c) 2008 the authors listed at the following URL, and/or+the authors of referenced articles or incorporated external code:+http://en.literateprograms.org/Priority_Queue_(Haskell)?action=history&offset=20080608152146++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.++Retrieved from: http://en.literateprograms.org/Priority_Queue_(Haskell)?oldid=13634+-}++module Language.CP.PriorityQueue (+ PriorityQueue,+ empty,+ is_empty,+ minKey,+ minKeyValue,+ insert,+ deleteMin,+ deleteMinAndInsert+) where++ +import Prelude+++-- Declare the data type constructors.++data Ord k => PriorityQueue k a = Nil | Branch k a (PriorityQueue k a) (PriorityQueue k a)+ ++-- Declare the exported interface functions.++-- Return an empty priority queue.++is_empty Nil = True+is_empty _ = False++empty :: Ord k => PriorityQueue k a+empty = Nil+++-- Return the highest-priority key.++minKey :: Ord k => PriorityQueue k a -> k+minKey = fst . minKeyValue+++-- Return the highest-priority key plus its associated value.++minKeyValue :: Ord k => PriorityQueue k a -> (k, a)+minKeyValue Nil = error "empty queue"+minKeyValue (Branch k a _ _) = (k, a)+++-- Insert a key/value pair into a queue.++insert :: Ord k => k -> a -> PriorityQueue k a -> PriorityQueue k a+insert k a q = union (singleton k a) q++deleteMin :: Ord k => PriorityQueue k a -> ((k,a), PriorityQueue k a)+deleteMin(Branch k a l r) = ((k,a),union l r)++-- Delete the highest-priority key/value pair and insert a new key/value pair into the queue.++deleteMinAndInsert :: Ord k => k -> a -> PriorityQueue k a -> PriorityQueue k a+deleteMinAndInsert k a Nil = singleton k a+deleteMinAndInsert k a (Branch _ _ l r) = union (insert k a l) r++++-- Declare the private helper functions.++-- Join two queues in sorted order.++union :: Ord k => PriorityQueue k a -> PriorityQueue k a -> PriorityQueue k a+union l Nil = l+union Nil r = r+union l@(Branch kl _ _ _) r@(Branch kr _ _ _)+ | kl <= kr = link l r+ | otherwise = link r l+++-- Join two queues without regard to order.++-- (This is a helper to the union helper.)++link (Branch k a Nil m) r = Branch k a r m+link (Branch k a ll lr) r = Branch k a lr (union ll r)+++-- Return a queue with a single item from a key/value pair.++singleton :: Ord k => k -> a -> PriorityQueue k a+singleton k a = Branch k a Nil Nil
+ Language/CP/Queue.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE FlexibleInstances #-}+{-+ - The Queue data type, a worklist data type for search.+ -+ - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}++module Language.CP.Queue where++import qualified Data.Sequence+import qualified Language.CP.PriorityQueue as PriorityQueue++class Queue q where + type Elem q :: *+ emptyQ :: q -> q+ isEmptyQ :: q -> Bool+ popQ :: q -> (Elem q,q)+ pushQ :: Elem q -> q -> q++instance Queue [a] where+ type Elem [a] = a+ emptyQ _ = []+ isEmptyQ = Prelude.null+ popQ (x:xs) = (x,xs)+ pushQ = (:)++instance Queue (Data.Sequence.Seq a) where+ type Elem (Data.Sequence.Seq a) = a+ emptyQ _ = Data.Sequence.empty+ isEmptyQ = Data.Sequence.null + popQ (Data.Sequence.viewl -> x Data.Sequence.:< xs) = (x,xs)+ pushQ = flip (Data.Sequence.|>)++instance Ord a => Queue (PriorityQueue.PriorityQueue a (a,b,c)) where+ type Elem (PriorityQueue.PriorityQueue a (a,b,c)) = (a,b,c)+ emptyQ _ = PriorityQueue.empty+ isEmptyQ = PriorityQueue.is_empty + pushQ x@(k,_,_) = PriorityQueue.insert k x+ popQ q = let ((_,x),q') = PriorityQueue.deleteMin q+ in (x,q')
+ Language/CP/SearchTree.hs view
@@ -0,0 +1,175 @@+{-# OPTIONS_GHC -fglasgow-exts #-}+{-+ - The Tree data type, a generic modelling language for constraint solvers.+ -+ - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}++module Language.CP.SearchTree where++import Monad+import Language.CP.Solver++-------------------------------------------------------------------------------+----------------------------------- Tree --------------------------------------+-------------------------------------------------------------------------------++data Tree s a+ = Fail -- failure+ | Return a -- finished+ | Try (Tree s a) (Tree s a) -- disjunction+ | Add (Constraint s) (Tree s a) -- sequentially adding a constraint to a tree+ | NewVar (Term s -> Tree s a) -- add a new variable to a tree+ | Label (s (Tree s a)) -- label with a strategy++instance Show (Tree s a) where+ show Fail = "Fail"+ show (Return _) = "Return"+ show (Try l r) = "Try (" ++ show l ++ ") (" ++ show r ++ ")"+ show (Add _ t) = "Add (" ++ show t ++ ")"+ show (NewVar _) = "NewVar"+ show (Label _) = "Label"++instance Solver s => Functor (Tree s) where+ fmap = liftM + +instance Solver s => Monad (Tree s) where+ return = Return+ (>>=) = bindTree+ ++bindTree :: Solver s => Tree s a -> (a -> Tree s b) -> Tree s b+Fail `bindTree` k = Fail+(Return x) `bindTree` k = k x+(Try m n) `bindTree` k = Try (m `bindTree` k) (n `bindTree` k)+(Add c m) `bindTree` k = Add c (m `bindTree` k)+(NewVar f) `bindTree` k = NewVar (\x -> f x `bindTree` k) +(Label m) `bindTree` k = Label (m >>= \t -> return (t `bindTree` k))++insertTree :: Solver s => Tree s a -> Tree s () -> Tree s a+(NewVar f) `insertTree` t = NewVar (\x -> f x `insertTree` t) +(Add c o) `insertTree` t = Add c (o `insertTree` t)+other `insertTree` t = t /\ other+++{- Monad laws:+ -+ - 1. return x >>= f == f x+ -+ - return a >>= f + - == Return a >>= f (return def)+ - == f x (bind def) + -+ - 2. m >>= return = m+ -+ - By induction+ - case m of+ - 1) Return x -> + - Return x >>= return+ - == return x (bind def)+ - == Return x (return def)+ - 2) Fail ->+ - Fail >>= return+ - == Fail (bind def)+ - 3) Try l r >>= return+ - == Try (l >>= return) (r >>= return) (bind def)+ - == Try l r (induction)+ - 4) Add c m >>= return+ - == Add c (m >>= return) (bind def)+ - == Add c m (induction) + - 5) NewVar f >>= return+ - == NewVar (\v -> f v >>= return) (bind def) + - == NewVar (\v -> f v) ((co)-induction?)+ - == NewVar f (eta reduction)+ - 6) Label sm >>= return+ - == Label (sm >>= \m -> return (m >>= return)) (bind def)+ - == Label (sm >>= \m -> return m) (co-induction)+ - == Label (sm >>= return) (eta reduction)+ - == Label sm (2nd monad law for Monad s)+ -+ - 3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)+ - + - By induction+ - case m of+ - 1) (Return y >>= f) >>= g + - == f y >>= g (bind def)+ - == (\x -> f x >>= g) y (beta expansion)+ - == Return y >>= (\x -> f x >>= g) (bind def)+ - 2) (Fail >>= f) >>= g+ - == Fail >>= g (bind def)+ - == Fail (bind def)+ - == Fail >>= (\x -> f x >>= g) (bind def) + - 3) (Try l r >>= f) >>= g+ - == Try (l >>= f) (r >>= f)) >>= g (bind def)+ - == Try ((l >>= f) >>= g) ((r >>= f) >>= g) (bind def)+ - == Try (l >>= (\x -> f x >>= g)) (r >>= (\x -> f x >>= g)) (induction)+ - == Try l r >>= (\x -> f x >>= g) (bind def)+ - 4) (NewVar m >>= f) >>= g+ - == NewVar (\v -> m v >>= f) >>= g (bind def)+ - == NewVar (\w -> (\v -> m v >>= f) w >>= g) (bind def)+ - == NewVar (\w -> (m w >>= f) >>= g) (beta reduction) + - == NewVar (\w -> m w >>= (\x -> f x >>= g)) (co-induction)+ - == NewVar m >>= (\x -> f x >>= g) (bind def)+ - 5) (Label sm >>= f) >>= g+ - == Label (sm >>= \m -> return (m >>= f)) >>= g (bind def) + - == Label ((sm >>= \m -> return (m >>= f)) >>= \m' -> return (m' >>= g))+ - == Label (sm >>= (\m -> return (m >>= f) >>= \m' -> return (m' >>= g)))+ - == Label (sm >>= \m -> return ((m >>= f) >>= g))+ - == Label (sm >>= \m -> return (m >>= (\x -> f x >>= g)))+ - == Label sm >>= (\x -> f x >>= g)+ -+ -}++-------------------------------------------------------------------------------+----------------------------------- Sugar -------------------------------------+-------------------------------------------------------------------------------+ +infixr 3 /\+(/\) :: Solver s => Tree s a -> Tree s b -> Tree s b+(/\) = (>>)+ +infixl 2 \/+(\/) :: Solver s => Tree s a -> Tree s a -> Tree s a+(\/) = Try++false :: Tree s a+false = Fail+ +true :: Tree s ()+true = Return ()++disj :: Solver s => [Tree s a] -> Tree s a+disj = foldr (\/) false++conj :: Solver s => [Tree s ()] -> Tree s ()+conj = foldr (/\) true++disj2 :: Solver s => [Tree s a] -> Tree s a+disj2 (x: []) = x+disj2 l = let (xs,ys) = split l+ split [] = ([],[])+ split (a:as) = let (bs,cs) = split as+ in (a:cs,bs)+ in Try (disj2 xs) (disj2 ys)+ +exists :: (Term s -> Tree s a) -> Tree s a+exists f = NewVar f++exist :: Solver s => Int -> ([Term s] -> Tree s a) -> Tree s a+exist n ftree = f n []+ where f 0 acc = ftree acc+ f n acc = exists $ \v -> f (n-1) (v:acc)++forall :: Solver s => [Term s] -> (Term s -> Tree s ()) -> Tree s ()+forall list ftree = conj $ map ftree list+ +label :: Solver s => s (Tree s a) -> Tree s a+label = Label++prim :: Solver s => (s a) -> Tree s a+prim action = Label (action >>= return . return)++add :: Solver s => Constraint s -> Tree s ()+add c = Add c true
+ Language/CP/Solver.hs view
@@ -0,0 +1,30 @@+{-# OPTIONS_GHC -fglasgow-exts #-}+{-+ - The Solver class, a generic interface for constraint solvers.+ -+ - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}+module Language.CP.Solver where ++class Monad solver => Solver solver where+ -- the constraints+ type Constraint solver :: *+ -- the terms+ type Term solver :: *+ -- the labels+ type Label solver :: *+ -- produce a fresh constraint variable+ newvarSM :: solver (Term solver)+ -- add a constraint to the current state, and+ -- return whethe the resulting state is consistent+ addSM :: Constraint solver -> solver Bool+ -- reify the current state+ storeSM :: solver [Constraint solver]+ -- run a computation+ runSM :: solver a -> a+ -- mark the current state, and return its label+ markSM :: solver (Label solver)+ -- go to the state with given label+ gotoSM :: Label solver -> solver ()
+ Language/CP/Transformers.hs view
@@ -0,0 +1,104 @@+{- + - Monadic Constraint Programming+ - http://www.cs.kuleuven.be/~toms/Haskell/+ - Tom Schrijvers+ -}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE Rank2Types #-}+module Language.CP.Transformers where ++import Language.CP.Solver+import Language.CP.SearchTree+import Language.CP.Queue++--------------------------------------------------------------------------------+-- EVALUATION+--------------------------------------------------------------------------------++eval :: (Solver solver, Queue q, Elem q ~ (Label solver,Tree solver (ForResult t),TreeState t), Transformer t,+ ForSolver t ~ solver) + => Tree solver (ForResult t) -> q -> t -> solver (Int,[ForResult t])+eval tree q t = do (es,ts) <- initT t tree+ eval' 0 tree q t es ts++eval' :: SearchSig solver q t (ForResult t) +eval' i (Return x) wl t es ts = do (j,xs) <- returnT (i+1) wl t es+ return (j,(x:xs)) +eval' i (Add c k) wl t es ts = do b <- addSM c + if b then eval' (i+1) k wl t es ts+ else continue (i+1) wl t es+eval' i (NewVar f) wl t es ts = do v <- newvarSM + eval' (i+1) (f v) wl t es ts+eval' i (Try l r) wl t es ts = + do now <- markSM + let wl' = pushQ (now,l,leftT t es ts) $ pushQ (now,r,rightT t es ts) wl+ continue (i+1) wl' t es+eval' i Fail wl t es ts = continue (i+1) wl t es+eval' i (Label m) wl t es ts = do tree <- m+ eval' (i+1) tree wl t es ts+ +continue :: ContinueSig solver q t (ForResult t) +continue i wl t es + | isEmptyQ wl = endT i wl t es -- return (i,[])+ | otherwise = let ((past,tree,ts),wl') = popQ wl+ in do gotoSM past+ nextT i tree wl' t es ts ++--------------------------------------------------------------------------------+-- TRANSFORMER+--------------------------------------------------------------------------------++type SearchSig solver q t a =+ (Solver solver, Queue q, Transformer t, + Elem q ~ (Label solver,Tree solver a,TreeState t),+ ForSolver t ~ solver) + => Int -> Tree solver a -> q -> t -> EvalState t -> TreeState t -> solver (Int,[a])++type ContinueSig solver q t a =+ (Solver solver, Queue q, Transformer t, + Elem q ~ (Label solver,Tree solver a,TreeState t),+ ForSolver t ~ solver) + => Int -> q -> t -> EvalState t -> solver (Int,[a])++class Transformer t where+ type EvalState t :: *+ type TreeState t :: *+ type ForSolver t :: (* -> *)+ type ForResult t :: *+ leftT, rightT :: t -> EvalState t -> TreeState t -> TreeState t+ leftT _ _ = id+ rightT = leftT+ nextT :: SearchSig (ForSolver t) q t (ForResult t)+ nextT = eval'+ initT :: t -> Tree (ForSolver t) (ForResult t) -> (ForSolver t) (EvalState t,TreeState t)+ returnT :: ContinueSig solver q t (ForResult t) + returnT i wl t es = continue i wl t es+ endT :: ContinueSig solver q t (ForResult t)+ endT i wl t es = return (i,[])++newtype DepthBoundedST (solver :: * -> *) a = DBST Int++instance Solver solver => Transformer (DepthBoundedST solver a) where+ type EvalState (DepthBoundedST solver a) = ()+ type TreeState (DepthBoundedST solver a) = Int+ type ForSolver (DepthBoundedST solver a) = solver+ type ForResult (DepthBoundedST solver a) = a+ initT (DBST n) _ = return ((),n)+ leftT _ _ ts = ts - 1+ nextT i tree q t es ts+ | ts == 0 = continue i q t es+ | otherwise = eval' i tree q t es ts++newtype NodeBoundedST (solver :: * -> *) a = NBST Int++instance Solver solver => Transformer (NodeBoundedST solver a) where+ type EvalState (NodeBoundedST solver a) = Int+ type TreeState (NodeBoundedST solver a) = ()+ type ForSolver (NodeBoundedST solver a) = solver+ type ForResult (NodeBoundedST solver a) = a+ initT (NBST n) _ = return (n,())+ nextT i tree q t es ts+ | es == 0 = return (i,[])+ | otherwise = eval' i tree q t (es - 1) ts+
+ Setup.hs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell+ +import Distribution.Simple+main = defaultMain
+ monadiccp.cabal view
@@ -0,0 +1,13 @@+Name: monadiccp+Version: 0.1+Description: Monadic Constraint Programming framework+License: BSD3+License-file: LICENSE+Author: Tom Schrijvers +Maintainer: tom.schrijvers@cs.kuleuven.be+Build-Depends: base, containers, mtl, haskell98, random+Build-Type: Simple+Exposed-modules: Language.CP.Solver Language.CP.FD Language.CP.Domain Language.CP.FDSugar Language.CP.PriorityQueue Language.CP.SearchTree Language.CP.Transformers+ghc-options: +Category: control+Synopsis: Package for Constraint Programming