monadiccp 0.4.1 → 0.5
raw patch · 8 files changed
+270/−166 lines, 8 files
Files
- Control/CP/Herbrand/Herbrand.hs +109/−38
- Control/CP/Herbrand/HerbrandT.hs +11/−3
- Control/CP/Herbrand/Prolog.hs +86/−0
- Control/CP/Herbrand/PrologTerm.hs +6/−1
- Control/CP/Main.hs +0/−90
- Control/CP/SearchTree.hs +32/−23
- Control/CP/Solver.hs +22/−8
- monadiccp.cabal +4/−3
Control/CP/Herbrand/Herbrand.hs view
@@ -4,6 +4,9 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-}+-- |This module provides a Herbrand solver.+--+-- The type of terms is parameterized by the "HTerm" type class. module Control.CP.Herbrand.Herbrand where import Control.Monad.State.Lazy@@ -13,7 +16,7 @@ import Control.CP.Solver --- Herbrand terms+-- |Herbrand terms type VarId = Int @@ -22,37 +25,50 @@ isVar :: t -> Maybe VarId children :: t -> ([t], [t] -> t) nonvar_unify- :: (MonadState (HState t) m) => t -> t -> m Bool+ :: (MonadState (HState t m) m) => t -> t -> m Bool --- Herbrand monad+-- |Herbrand monad -newtype Herbrand t a = Herbrand { unH :: State (HState t) a }- deriving (Monad, MonadState (HState t))+data Herbrand t a = Herbrand { unH :: State (HState t (Herbrand t)) a } +instance Monad (Herbrand t) where+ return x = Herbrand $ return x+ m >>= f = Herbrand $ unH m >>= unH . f++instance MonadState (HState t (Herbrand t)) (Herbrand t) where+ get = Herbrand $ get+ put = Herbrand . put+ instance Functor (Herbrand t) where fmap f fa = fa >>= return . f - instance Applicative (Herbrand t) where pure = return (<*>) ff fa = do f <- ff a <- fa return $ f a -type Subst t = Map VarId t+-- |State -data HState t = HState {var_supply :: VarId- ,subst :: Subst t- }+type Heap t m = Map VarId (Binding t m) -updateState :: (HTerm t, MonadState (HState t) m) => (HState t -> HState t) -> m ()+data Binding t m + = VAR VarId -- | indirection to other variable+ | NONVAR t -- | bound to term+ | ACTION (m Bool) -- | attributed variable, with given action++data HState t m = HState {var_supply :: VarId+ ,heap :: Heap t m+ }++updateState :: (HTerm t, MonadState (HState t m) m) => (HState t m -> HState t m) -> m () updateState f = get >>= put . f --- Solver instance +-- |Solver instance instance HTerm t => Solver (Herbrand t) where type Constraint (Herbrand t) = Unify t - type Label (Herbrand t) = HState t+ type Label (Herbrand t) = HState t (Herbrand t) add = addH mark = get goto = put@@ -66,54 +82,109 @@ -- New variable -newvarH :: (HTerm t,MonadState (HState t) m) => m t+newvarH :: (HTerm t,MonadState (HState t m) m) => m t newvarH = do state <- get let varid = var_supply state put state{var_supply = varid + 1} return $ mkVar varid +{- Representatin of variables+ --------------------------++ Each variable is represented by+ * a VarId+ * a possible Binding on the Heap+ - if there is a binding, then the variable's meaning + is that of the binding+ - if there is no binding, then variable's meaning is + that of an unbound variable++-}+ -- Unification data Unify t = t `Unify` t -addH :: (HTerm t, MonadState (HState t) m) => Unify t -> m Bool+addH :: (HTerm t, MonadState (HState t m) m) => Unify t -> m Bool addH (Unify t1 t2) = unify t1 t2 -unify :: (HTerm t, MonadState (HState t) m) => t -> t -> m Bool+-- | unify two arbitrary terms+unify :: (HTerm t, MonadState (HState t m) m) => t -> t -> m Bool unify t1 t2 = do nt1 <- shallow_normalize t1 nt2 <- shallow_normalize t2 case (isVar nt1, isVar nt2) of (Just v1, Just v2) | v1 == v2 -> success- (Just v1, _ ) -> bind v1 nt2 >> success- (_ , Just v2) -> bind v2 nt1 >> success- (_ , _ ) -> nonvar_unify nt1 nt2+ | otherwise -> bindv v1 v2+ (Just v1, Nothing) -> bindt v1 nt2+ (Nothing, Just v2) -> bindt v2 nt1+ (Nothing, Nothing) -> nonvar_unify nt1 nt2 success, failure :: Monad m => m Bool success = return True failure = return False+m1 `andM` m2 = m1 >>= \b -> if b then m2 else return b -bind :: (HTerm t, MonadState (HState t) m) => VarId -> t -> m ()-bind v t = updateState $ \state -> state{subst = insert v t (subst state)}+-- | bind a variable to a term+bindt :: (HTerm t, MonadState (HState t m) m) => VarId -> t -> m Bool+bindt v t = do r <- lookupVar v+ updater v (NONVAR t)+ case r of+ Just (ACTION action) -> action+ Nothing -> success +-- | alias one variable to another+bindv :: (HTerm t, MonadState (HState t m) m) => VarId -> VarId -> m Bool+bindv v1 v2 = do r1 <- lookupVar v1+ r2 <- lookupVar v2+ case (r1,r2) of+ (Just (ACTION a1), Just (ACTION a2)) + -> let r3 = noACTION+ in do updater v1 r3+ updater v2 r3+ a1 `andM` a2+ (Just _, Nothing) -> updater v1 (VAR v2) >> success+ (Nothing, Just _) -> updater v2 (VAR v1) >> success+ (Nothing,Nothing) -> updater v1 (VAR v2) >> success++ where noACTION = ACTION success++updater v r = updateState $ \state -> state{heap = insert v r (heap state)}++lookupVar v = do state <- get+ return $ Data.Map.lookup v (heap state)++-- Actions++registerAction :: (HTerm t, MonadState (HState t m) m) => t -> m Bool -> m ()+registerAction t action =+ do nt <- shallow_normalize t+ case isVar nt of+ Just v ->+ do r <- lookupVar v+ case r of+ Nothing -> updater v (ACTION action)+ Just (ACTION a1) -> updater v (ACTION (a1 `andM` action))+ Nothing -> return ()++-- TODO: unregister action?+ -- Normalization -shallow_normalize :: (HTerm t, MonadState (HState t) m) => t -> m t-shallow_normalize t- | Just v <- isVar t - = do state <- get- case Data.Map.lookup v (subst state) of- Just t' -> shallow_normalize t'- Nothing -> return t - | otherwise - = return t+shallow_normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t+shallow_normalize t = gnormalize return t -normalize :: (HTerm t, MonadState (HState t) m) => t -> m t-normalize t- | Just v <- isVar t = do state <- get- case Data.Map.lookup v (subst state) of- Just t' -> normalize t'- Nothing -> return t- | otherwise = let (ts,mkt) = children t- in mapM normalize ts >>= return . mkt+normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t+normalize t = gnormalize nvnormalize t+ where nvnormalize t = let (ts,mkt) = children t+ in mapM normalize ts >>= return . mkt++gnormalize nvnormalize t+ | Just v <- isVar t = vnormalize v+ | otherwise = nvnormalize t+ where vnormalize v = do state <- get+ case Data.Map.lookup v (heap state) of+ Just (VAR v') -> vnormalize v'+ Just (NONVAR t) -> nvnormalize t+ _ -> return $ mkVar v
Control/CP/Herbrand/HerbrandT.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-} -- |This module provides a Herbrand solver as a monad transformer. --@@ -19,12 +20,19 @@ import Control.CP.Solver import Control.CP.Herbrand.Herbrand (HState, Unify, HTerm,initState,addH,newvarH) -newtype HerbrandT t m a = HerbrandT { unHT :: StateT (HState t) m a }- deriving (MonadTrans, Monad, MonadState (HState t))+newtype HerbrandT t s a = HerbrandT { unHT :: StateT (HState t (HerbrandT t s)) s a }+ deriving Monad +instance MonadTrans (HerbrandT t) where+ lift = HerbrandT . lift++instance Solver s =>MonadState (HState t (HerbrandT t s)) (HerbrandT t s) where+ get = HerbrandT get+ put = HerbrandT . put+ instance (Solver s, HTerm t) => Solver (HerbrandT t s) where type Constraint (HerbrandT t s) = Either (Unify t) (Constraint s)- type Label (HerbrandT t s) = (HState t, Label s)+ type Label (HerbrandT t s) = (HState t (HerbrandT t s), Label s) add (Left c) = addH c add (Right c) = lift $ add c mark = do l <- get
+ Control/CP/Herbrand/Prolog.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Control.CP.Herbrand.Prolog + ( Prolog+ , module Control.CP.Herbrand.PrologTerm+ , PConstraint (..) + ) where ++import Control.Monad (zipWithM)++import Control.CP.Solver+import Control.CP.Herbrand.Herbrand+import Control.CP.Herbrand.PrologTerm++-- Prolog Solver++newtype Prolog a = Prolog { runProlog :: Herbrand PrologTerm a }+ deriving Monad++instance Solver Prolog where+ type Constraint Prolog = PConstraint + type Label Prolog = Label (Herbrand PrologTerm)+ add = addProlog+ mark = Prolog $ mark+ goto = Prolog . goto+ run = run . runProlog++instance Term Prolog PrologTerm where+ newvar = Prolog $ newvar++data PConstraint = PrologTerm := PrologTerm+ | NotFunctor PrologTerm String + | PrologTerm :/= PrologTerm++addProlog :: PConstraint -> Prolog Bool+addProlog (x := y) = Prolog (unify x y)+addProlog (x :/= y) = Prolog (diff x y)+addProlog (NotFunctor x f) = Prolog (notFunctor x f)++notFunctor :: PrologTerm -> String -> Herbrand PrologTerm Bool+notFunctor x f = do t <- shallow_normalize x+ case t of+ PVar _ ->+ registerAction t (notFunctor t f) >> success+ PTerm g _ ->+ if g == f then failure+ else success++diff :: PrologTerm -> PrologTerm -> Herbrand PrologTerm Bool+diff x y =+ do x' <- shallow_normalize x+ y' <- shallow_normalize y+ b <- diff' x' y'+ case b of+ DYes -> success+ DNo -> failure+ DMaybe vars -> mapM (\v -> registerAction v (diff x y)) vars >> success+ ++ where diff' x@(PVar v1) (PVar v2) =+ if v1 == v2 then return $ DNo+ else return $ DMaybe [x]+ diff' x@(PVar _) (PTerm _ _) =+ return $ DMaybe [x]+ diff' (PTerm _ _) y@(PVar _) =+ return $ DMaybe [y]+ diff' (PTerm f xs) (PTerm g ys) + | x /= y = return $ DYes+ | length xs /= length ys = return $ DYes + | otherwise =+ do xs' <- mapM shallow_normalize xs+ ys' <- mapM shallow_normalize ys+ bs <- zipWithM diff' xs' ys'+ return $ foldr dand DYes bs+ +data DiffBool = DYes | DNo | DMaybe [PrologTerm]++dand DNo _ = DNo+dand _ DNo = DNo+dand (DMaybe x) (DMaybe y) = DMaybe (x ++ y)+dand DYes x = x+dand x DYes = x+
Control/CP/Herbrand/PrologTerm.hs view
@@ -1,6 +1,12 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+ module Control.CP.Herbrand.PrologTerm where import Data.List (intersperse)+ import Control.CP.Herbrand.Herbrand data PrologTerm = PTerm String [PrologTerm] | PVar VarId@@ -26,4 +32,3 @@ instance Show PrologTerm where show (PVar v) = 'V' : show v show (PTerm f args) = f ++ "(" ++ (concat $ intersperse "," $ map show args) ++ ")"-
− Control/CP/Main.hs
@@ -1,90 +0,0 @@-{- - - Monadic Constraint Programming- - http://www.cs.kuleuven.be/~toms/Haskell/- - Tom Schrijvers- -}-module Control.CP.Main where--import Control.CP.ComposableTransformers-import Control.CP.FD-import Control.CP.FDSugar-import List (tails)-import Control.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..] - ]
Control/CP/SearchTree.hs view
@@ -123,27 +123,42 @@ -} -------------------------------------------------------------------------------+----------------------------------- Monad Subclass ----------------------------+-------------------------------------------------------------------------------++infixl 2 \/++class (Monad m, Solver (TreeSolver m)) => MonadTree m where+ type TreeSolver m :: * -> *+ addTo :: Constraint (TreeSolver m) -> m a -> m a+ false :: m a+ (\/) :: m a -> m a -> m a+ exists :: Term (TreeSolver m) t => (t -> m a) -> m a+ label :: (TreeSolver m) (m a) -> m a++instance Solver solver => MonadTree (Tree solver) where+ type TreeSolver (Tree solver) = solver+ addTo = Add+ false = Fail+ (\/) = Try+ exists = NewVar+ label = Label++------------------------------------------------------------------------------- ----------------------------------- Sugar ------------------------------------- ------------------------------------------------------------------------------- infixr 3 /\-(/\) :: Solver s => Tree s a -> Tree s b -> Tree s b+(/\) :: MonadTree tree => tree a -> tree b -> tree 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 ()+true :: MonadTree tree => tree ()+true = return () -disj :: Solver s => [Tree s a] -> Tree s a+disj :: MonadTree tree => [tree a] -> tree a disj = foldr (\/) false -conj :: Solver s => [Tree s ()] -> Tree s ()+conj :: MonadTree tree => [tree ()] -> tree () conj = foldr (/\) true disj2 :: Solver s => [Tree s a] -> Tree s a@@ -154,10 +169,7 @@ in (a:cs,bs) in Try (disj2 xs) (disj2 ys) -exists :: Term s t => (t -> Tree s a) -> Tree s a-exists f = NewVar f--exist :: (Solver s, Term s t) => Int -> ([t] -> Tree s a) -> Tree s a+exist :: (MonadTree tree, Term (TreeSolver tree) t) => Int -> ([t] -> tree a) -> tree a exist n ftree = f n [] where f 0 acc = ftree acc f n acc = exists $ \v -> f (n-1) (v:acc)@@ -165,11 +177,8 @@ forall :: (Solver s, Term s t) => [t] -> (t -> 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)+prim :: MonadTree tree => TreeSolver tree a -> tree a+prim action = label (action >>= return . return) -add :: Solver s => Constraint s -> Tree s ()-add c = Add c true+add :: MonadTree tree => Constraint (TreeSolver tree) -> tree ()+add c = c `addTo` true
Control/CP/Solver.hs view
@@ -8,23 +8,37 @@ -} module Control.CP.Solver where +import Control.Monad.Writer+import Data.Monoid+ class Monad solver => Solver solver where- -- the constraints+ -- | the constraints type Constraint solver :: *- -- the labels+ -- | the labels type Label solver :: *- -- add a constraint to the current state, and- -- return whethe the resulting state is consistent+ -- | add a constraint to the current state, and+ -- return whethe the resulting state is consistent add :: Constraint solver -> solver Bool- -- run a computation+ -- | run a computation run :: solver a -> a- -- mark the current state, and return its label+ -- | mark the current state, and return its label mark :: solver (Label solver)- -- go to the state with given label+ -- | go to the state with given label goto :: Label solver -> solver () class Solver solver => Term solver term where- -- produce a fresh constraint variable+ -- | produce a fresh constraint variable newvar :: solver term +-- | WriterT decoration of a solver+-- useful for producing statistics during solving+instance (Monoid w, Solver s) => Solver (WriterT w s) where+ type Constraint (WriterT w s) = Constraint s+ type Label (WriterT w s) = Label s+ add = lift . add+ run = fst . run . runWriterT+ mark = lift mark+ goto = lift . goto +instance (Monoid w, Term s t) => Term (WriterT w s) t where+ newvar = lift newvar
monadiccp.cabal view
@@ -1,5 +1,5 @@ Name: monadiccp-Version: 0.4.1+Version: 0.5 Description: Monadic Constraint Programming framework License: BSD3 License-file: LICENSE@@ -7,8 +7,9 @@ Maintainer: tom.schrijvers@cs.kuleuven.be Build-Depends: base, containers, mtl, haskell98, random Build-Type: Simple-Exposed-modules: Control.CP.ComposableTransformers Control.CP.PriorityQueue Control.CP.Queue Control.CP.Solver Control.CP.SearchTree Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.HerbrandT+Exposed-modules: Control.CP.ComposableTransformers Control.CP.PriorityQueue Control.CP.Queue Control.CP.Solver Control.CP.SearchTree Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog Control.CP.Herbrand.HerbrandT ghc-options: Category: control-Synopsis: Package for Constraint Programming+Synopsis: Constraint Programming Homepage: http://www.cs.kuleuven.be/~toms/Haskell/+bug-reports: http://trac.haskell.org/monadiccp/