diff --git a/Control/CP/ComposableTransformers.hs b/Control/CP/ComposableTransformers.hs --- a/Control/CP/ComposableTransformers.hs +++ b/Control/CP/ComposableTransformers.hs @@ -3,18 +3,35 @@ - http://www.cs.kuleuven.be/~toms/Haskell/ - Tom Schrijvers -} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE FlexibleContexts #-} -module Control.CP.ComposableTransformers where +module Control.CP.ComposableTransformers ( + solve, + NewBound, + CTransformer, + CForSolver, + CForResult, + CTreeState, + RestartST(..) , + SealedCST(..), + CNodeBoundedST(..), + CDepthBoundedST(..), + CBranchBoundST(..), + CFirstSolutionST(..), + CIdentityCST(..), + CRandomST(..), + CLimitedDiscrepancyST(..) +) where import Control.CP.Transformers import Control.CP.SearchTree import Control.CP.Solver import Control.CP.Queue +import Control.CP.Debug import System.Random (mkStdGen, randoms) diff --git a/Control/CP/Debug.hs b/Control/CP/Debug.hs new file mode 100644 --- /dev/null +++ b/Control/CP/Debug.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE CPP #-} + +module Control.CP.Debug ( + debug +) where + +import Debug.Trace + +#ifdef DEBUG +debug = trace +#else +debug = flip const +#endif diff --git a/Control/CP/EnumTerm.hs b/Control/CP/EnumTerm.hs new file mode 100644 --- /dev/null +++ b/Control/CP/EnumTerm.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TransformListComp #-} +{-# LANGUAGE FlexibleContexts #-} + +module Control.CP.EnumTerm ( + EnumTerm, + TermDomain, + get_domain_size, + get_value, + split_domain_partial, + split_domain, + split_domains, + in_order, + firstfail, + middleout, + endsout, + interleave, + assignment, + assignments, + enumerate, + label +) where + +import GHC.Exts (sortWith) + +import Data.List (splitAt) +import Control.CP.SearchTree hiding (label) +import Control.CP.Solver + +-------------------------------------------------------------------------------- +-- ENUMERATION +-------------------------------------------------------------------------------- + +class (Term s t, Enum (TermDomain s t)) => EnumTerm s t where + type TermDomain s t :: * + get_domain_size :: t -> s Int + get_value :: t -> s (Maybe (TermDomain s t)) + split_domain_partial :: t -> s [Tree s ()] + + split_domain :: t -> s (Tree s ()) + split_domain v = do + let rec tree = do + tree + Label $ do + x <- get_value v + case x of + Nothing -> split_domain v + Just _ -> return $ return () + lst <- split_domain_partial v + return $ levelList $ map rec lst + + split_domains :: [t] -> s (Tree s ()) + split_domains [] = return $ return () + split_domains [a] = split_domain a + split_domains (a:b) = do + ta <- split_domain a + tb <- split_domains b + return $ ta /\ tb + + label :: ([t] -> s [t]) -> [t] -> Tree s () + label o l = Label $ do + x <- o l + split_domains x + + enumerate :: [t] -> Tree s () + enumerate l = label firstfail l + +levelList :: Solver s => [Tree s ()] -> Tree s () +levelList [] = Fail +levelList [a] = a +levelList l = + let len = length l + (p1,p2) = splitAt (len `div` 2) l + in Try (levelList p1) (levelList p2) + + +in_order :: Monad m => a -> m a +in_order = return + +firstfail qs = do ds <- mapM get_domain_size qs + return [ q | (d,q) <- zip ds qs + , then sortWith by d ] + +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 +-------------------------------------------------------------------------------- + +assignment :: EnumTerm s t => t -> Tree s (TermDomain s t) +assignment q = Label $ get_value q >>= \(Just x) -> return $ Return x + +assignments :: EnumTerm s t => [t] -> Tree s [TermDomain s t] +assignments = mapM assignment diff --git a/Control/CP/FD/Domain.hs b/Control/CP/FD/Domain.hs deleted file mode 100644 --- a/Control/CP/FD/Domain.hs +++ /dev/null @@ -1,167 +0,0 @@ -{- - - 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 Control.CP.FD.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) diff --git a/Control/CP/FD/Example/Example.hs b/Control/CP/FD/Example/Example.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Example/Example.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE CPP #-} + +module Control.CP.FD.Example.Example ( + example_main, + example_main_void, + example_main_single, + FDModel +) where + + +import System (getArgs) + +import Control.CP.ComposableTransformers +import Control.CP.FD.Gecode.Translate +import Control.CP.FD.Solvers +import Control.CP.FD.FD +import Control.CP.EnumTerm +import Control.CP.SearchTree hiding (label) + +#ifdef RGECODE +import Control.CP.FD.Gecode.RuntimeSolver +#endif + +example_main :: (forall s. FDSolver s => [String] -> FDTree s [FDExpr s]) -> IO () +example_main f = do + args <- getArgs + case args of + ("gecode_compile":r) -> putStr $ generate_gecode $ as_gecode_codegen $ f r +#ifdef RGECODE + ("gecode_run":r) -> print $ solve dfs fs $ as_gecode_runtime $ f r >>= \l -> enumerate l /\ assignments l + ("gecode_search":r) -> print $ solve dfs fs $ as_gecode_search $ f r >>= \l -> enumerate l /\ assignments l +#endif + ("overton_run":r) -> print $ solve dfs fs $ as_overtonfd $ f r >>= \l -> enumerate l /\ assignments l + [] -> putStr "Solver type required\n" + (a:r) -> putStr ("Unsupported solver: " ++ a ++ "\n") + +example_main_void :: (forall s. FDSolver s => FDTree s [FDExpr s]) -> IO () +example_main_void f = example_main (const f) + +example_main_single :: Read n => (forall s. FDSolver s => n -> FDTree s [FDExpr s]) -> IO () +example_main_single f = example_main (f . read . head) + +type FDModel = FDSolver s => Tree (FDWrapper s) [FDExpr s] diff --git a/Control/CP/FD/Expr.hs b/Control/CP/FD/Expr.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Expr.hs @@ -0,0 +1,236 @@ +{- + - Monadic Constraint Programming + - http://www.cs.kuleuven.be/~toms/Haskell/ + - Tom Schrijvers & Pieter Wuille + -} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Control.CP.FD.Expr ( + Expr(..), + ToExpr(..), + ExprKey(..), + unExprKey +) where + +import GHC.Exts (sortWith) +import qualified Control.CP.PriorityQueue as PriorityQueue +import qualified Data.Sequence + +import Control.CP.SearchTree hiding (label) +import Control.CP.Transformers +import Control.CP.ComposableTransformers +import Control.CP.Queue +import Control.CP.Solver +import Control.CP.EnumTerm +import Control.CP.Debug +import Control.CP.Mixin + +-- some simple kinds of expressions +data Expr t = + Term t + | Const Integer + | Plus (Expr t) (Expr t) + | Minus (Expr t) (Expr t) + | Mult (Expr t) (Expr t) + | Div (Expr t) (Expr t) + | Mod (Expr t) (Expr t) + | Abs (Expr t) + deriving (Show,Eq) + +varrefs :: forall s. Expr s -> Int +varrefs (Term _) = 1 +varrefs (Const _) = 0 +varrefs (Plus a b) = varrefs a + varrefs b +varrefs (Minus a b) = varrefs a + varrefs b +varrefs (Mult a b) = varrefs a + varrefs b +varrefs (Div a b) = varrefs a + varrefs b +varrefs (Mod a b) = varrefs a + varrefs b +varrefs (Abs a) = varrefs a + +simplify :: (Eq s, Show s) => Expr s -> Expr s +-- simplification rules (either decrease # of variable references, or leave that equal and decrease # of tree nodes) +--- level 0 (result in a final expression) +simplify (Mult (Const 0) _) = Const 0 +simplify (Div (Const 0) _) = Const 0 +simplify (Mod (Const 0) _) = Const 0 +simplify (Mod _ (Const 1)) = Const 0 +simplify (Mod _ (Const (-1))) = Const 0 +simplify (Mod (Mult (Const a) b) (Const c)) | (a `mod` c)==0 = Const 0 +simplify (Minus a b) | a==b = Const 0 +simplify (Plus (Const a) (Const b)) = Const (a+b) +simplify (Minus (Const a) (Const b)) = Const (a-b) +simplify (Mult (Const a) (Const b)) = Const (a*b) +simplify (Div (Const a) (Const b)) = Const $ (a `div` b) +simplify (Abs (Const a)) = Const (abs a) +simplify (Mod (Const a) (Const b)) = Const $ (a `div` b) +simplify (Plus (Const 0) a) = a +simplify (Mult (Const 1) a) = a +simplify (Div a (Const 1)) = a +--- level 1 (result in one recursive call to simplify) +simplify (Plus a b) | a==b = 2 * a +simplify (Div a (Const (-1))) = negate a +simplify (Plus (Const c) (Plus (Const a) b)) = (Const $ c+a) + b +simplify (Plus (Const c) (Minus (Const a) b)) = (Const $ c+a) - b +simplify (Minus (Const c) (Plus (Const a) b)) = (Const $ c-a) - b +simplify (Minus (Const c) (Minus (Const a) b)) = (Const $ c-a) + b +simplify (Mult (Const c) (Mult (Const a) b)) = (Const $ a*c) * b +simplify (Div (Mult (Const a) b) (Const c)) | (a `mod` c)==0 = (Const (a `div` c)) * b +--- level 2 (result in two recursive calls to simplify) +simplify (Plus a (Mult b c)) | a==b && ((varrefs a)>0) = (c+1) * a +simplify (Plus a (Mult b c)) | a==c && ((varrefs a)>0) = (b+1) * a +simplify (Plus (Mult b c) a) | a==b && ((varrefs a)>0) = (c+1) * a +simplify (Plus (Mult b c) a) | a==c && ((varrefs a)>0) = (b+1) * a +simplify (Plus (Mult a b) (Mult c d)) | a==c = (b+d) * a +simplify (Plus (Mult a b) (Mult c d)) | a==d = (b+c) * a +simplify (Plus (Mult a b) (Mult c d)) | b==c = (a+d) * b +simplify (Plus (Mult a b) (Mult c d)) | b==d = (a+c) * b +simplify (Minus a (Mult b c)) | a==b && ((varrefs a)>0) = (1-c) * a +simplify (Minus a (Mult b c)) | a==c && ((varrefs a)>0) = (1-b) * a +simplify (Minus (Mult b c) a) | a==b && ((varrefs a)>0) = (c-1) * a +simplify (Minus (Mult b c) a) | a==c && ((varrefs a)>0) = (b-1) * a +simplify (Minus (Mult a b) (Mult c d)) | a==c = (b-d) * a +simplify (Minus (Mult a b) (Mult c d)) | a==d = (b-c) * a +simplify (Minus (Mult a b) (Mult c d)) | b==c = (a-d) * b +simplify (Minus (Mult a b) (Mult c d)) | b==d = (a-c) * b +simplify (Mult (Abs a) (Abs b)) = abs (a*b) +simplify (Div (Abs a) (Abs b)) = abs (a `div` b) +-- reordering rules (do not decrease # of variables or # of tree nodes, but normalize an expression in such a way that the same normalization cannot be applied anymore - possibly because that can only occur in a case already matched by a simplification rule above) +--- level 1 +simplify (Plus a (Const c)) = (Const c) + a +simplify (Minus a (Const c)) = (Const (-c)) + a +simplify (Mult a (Const c)) = (Const c) * a +simplify (Mult (Const (-1)) a) = negate a +--- level 2 +simplify (Mult (Const c) (Plus (Const a) b)) = (Const (a*c)) + ((Const c)*b) +simplify (Mult (Const c) (Minus (Const a) b)) = (Const (a*c)) - ((Const c)*b) +simplify (Plus a (Plus (Const b) c)) = (Const b) + (a+c) +simplify (Plus a (Minus (Const b) c)) = (Const b) + (a-c) +simplify (Minus a (Plus (Const b) c)) = (Const (-b)) + (a-c) +simplify (Minus a (Minus (Const b) c)) = (Const (-b)) + (a+c) +simplify (Mult a (Mult (Const b) c)) = (Const b) * (a*c) +simplify (Plus (Plus (Const a) b) c) = (Const a) + (b+c) +simplify (Plus (Minus (Const a) b) c) = (Const a) + (c-b) +simplify (Minus (Plus (Const a) b) c) = (Const a) + (b-c) +simplify (Minus (Minus (Const a) b) c) = (Const a) - (b+c) +simplify (Mult (Mult (Const a) b) c) = (Const a) * (b*c) +simplify (Mult a (Minus (Const 0) b)) = negate (a*b) +simplify (Mult (Minus (Const 0) b) a) = negate (a*b) +simplify (Div (Minus (Const 0) a) b) = negate $ a `div` b +simplify (Div a (Minus (Const 0) b)) = negate $ a `div` b +-- fallback rule +simplify a = a + +instance (Eq s, Show s) => Num (Expr s) where + a + b = simplify $ Plus a b + a - b = simplify $ Minus a b + a * b = simplify $ Mult a b + abs a = simplify $ Abs a + negate a = 0 - a + fromInteger c = Const $ fromInteger c + signum (Const a) = Const (signum a) + signum a = error "signum not possible for generic Expr" + +instance (Eq s, Show s) => Ord (Expr s) where + compare (Const x) (Const y) = compare x y + compare _ _ = error "compare not possible for generic Expr" + +instance (Eq s, Show s) => Real (Expr s) where + toRational (Const x) = toRational x + toRational _ = error "toRational not possible for generic Expr" + +instance (Eq s, Show s) => Enum (Expr s) where + succ a = a + 1 + pred a = a - 1 + toEnum = Const . toEnum + fromEnum (Const a) = fromEnum a + fromEnum _ = error "fromEnum not possible for generic Expr" + +instance (Eq s, Show s) => Integral (Expr s) where + toInteger (Const a) = toInteger a + toInteger _ = error "toInteger not possible for generic Expr" + divMod a b = (simplify $ Div a b, simplify $ Mod a b) + quotRem (Const a) (Const b) = case quotRem a b of (c,d) -> (Const c,Const d) + quotRem (Const 0) b = (Const 0,Const 0) + quotRem a (Const 1) = (a,Const 0) + quotRem a (Const (-1)) = (negate a,Const 0) + quotRem _ _ = error "quotRem not possible for generic Expr" + +-- a class of types convertible to expressions +class ToExpr tt t where + toExpr :: t -> Expr tt + +-- integers can be used as constant expressions +instance ToExpr tt Integer where + toExpr = Const + +-- ints can be used as constant expressions +instance ToExpr tt Int where + toExpr = Const . toInteger + +-- expressions themselves are trivially convertible to expressions +instance ToExpr t (Expr t) where + toExpr = id + +-- the terms used by the solver can be used as expressions referring +-- to a variable +instance ToExpr t t where + toExpr = Term + +-------------------------------------------------------------------------------- +-- ExprKey +-------------------------------------------------------------------------------- + +newtype ExprKey s = ExprKey (Expr s) + deriving (Eq, Show) + +unExprKey :: ExprKey s -> Expr s +unExprKey (ExprKey x) = x + +instance Ord s => Ord (ExprKey s) where + -- consts + compare (ExprKey (Const i1)) (ExprKey (Const i2)) = compare i1 i2 + compare (ExprKey (Const _)) _ = LT + compare _ (ExprKey (Const _)) = GT + -- abs + compare (ExprKey (Abs i1)) (ExprKey (Abs i2)) = compare (ExprKey i1) (ExprKey i2) + compare (ExprKey (Abs _)) _ = LT + compare _ (ExprKey (Abs _)) = GT + -- plus + compare (ExprKey (Plus a1 a2)) (ExprKey (Plus b1 b2)) = case (compare (ExprKey a1) (ExprKey b1)) of + LT -> LT + GT -> GT + EQ -> compare (ExprKey a2) (ExprKey b2) + compare (ExprKey (Plus _ _)) _ = LT + compare _ (ExprKey (Plus _ _)) = GT + -- minus + compare (ExprKey (Minus a1 a2)) (ExprKey (Minus b1 b2)) = case (compare (ExprKey a1) (ExprKey b1)) of + LT -> LT + GT -> GT + EQ -> compare (ExprKey a2) (ExprKey b2) + compare (ExprKey (Minus _ _)) _ = LT + compare _ (ExprKey (Minus _ _)) = GT + -- mult + compare (ExprKey (Mult a1 a2)) (ExprKey (Mult b1 b2)) = case (compare (ExprKey a1) (ExprKey b1)) of + LT -> LT + GT -> GT + EQ -> compare (ExprKey a2) (ExprKey b2) + compare (ExprKey (Mult _ _)) _ = LT + compare _ (ExprKey (Mult _ _)) = GT + -- div + compare (ExprKey (Div a1 a2)) (ExprKey (Div b1 b2)) = case (compare (ExprKey a1) (ExprKey b1)) of + LT -> LT + GT -> GT + EQ -> compare (ExprKey a2) (ExprKey b2) + compare (ExprKey (Div _ _)) _ = LT + compare _ (ExprKey (Div _ _)) = GT + -- mod + compare (ExprKey (Mod a1 a2)) (ExprKey (Mod b1 b2)) = case (compare (ExprKey a1) (ExprKey b1)) of + LT -> LT + GT -> GT + EQ -> compare (ExprKey a2) (ExprKey b2) + compare (ExprKey (Mod _ _)) _ = LT + compare _ (ExprKey (Mod _ _)) = GT + -- variables + compare (ExprKey (Term v1)) (ExprKey (Term v2)) = compare v1 v2 diff --git a/Control/CP/FD/FD.hs b/Control/CP/FD/FD.hs --- a/Control/CP/FD/FD.hs +++ b/Control/CP/FD/FD.hs @@ -1,411 +1,244 @@ {- - - 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 #-} + - Tom Schrijvers & Pieter Wuille + -} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE OverlappingInstances #-} - -module Control.CP.FD.FD where +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} -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,(<=<)) +module Control.CP.FD.FD ( + FDSolver(..), + fresh_var, + decompose, + compile_constraint, + FDExpr, + FDConstraint(..), + FDWrapper(..), + FDTree, + FDLabel(..), + wrap, + unwrap, + (@:), (@<), (@>), (@<=), (@>=), (@=), (@/=), + (@+), (@-), (@*), (@/), (@%), + cte, + allDiff, + sorted, + sSorted, + allin +)where -import Control.CP.FD.Domain as Domain +import GHC.Exts (sortWith) +import Control.CP.SearchTree hiding (label) +import Control.CP.Transformers +import Control.CP.ComposableTransformers +import Control.CP.Queue import Control.CP.Solver +import Control.CP.EnumTerm +import Control.CP.Debug +import Control.CP.Mixin +import Control.CP.FD.Expr --- import Debug.Trace -trace = flip const -------------------------------------------------------------------------------- --- Solver instance ------------------------------------------------------------- +-- SYNTACTIC SUGAR -------------------------------------------------------------------------------- -instance Solver FD where - type Constraint FD = FD_Constraint - type Label FD = FDState - add = addFD - run p = runFD p - mark = get - goto = put +-- define class FDSolver, instances of which must define a compile_constraint +-- function, to convert a constraint specified in syntactic sugar to a +-- corresponding search Tree. Instances must furthermore specify a +-- FDTerm x type, referring to the type of terms used +class (Show (FDTerm s), Eq (FDTerm s), Term s (FDTerm s)) => FDSolver s where + -- types + type FDTerm s :: * + -- functions + specific_compile_constraint :: Mixin (FDConstraint s -> Tree s Bool) + specific_decompose :: Mixin (Expr (FDTerm s) -> Tree s (FDTerm s)) + specific_fresh_var :: Mixin (Tree s (FDTerm s)) + -- default implementations + specific_decompose = mixinId + specific_fresh_var = mixinId -instance Term FD FD_Term where - newvar = newVar () >>= return . FD_Var +-- compile constraint + defaults +compile_constraint :: FDSolver s => FDConstraint s -> Tree s Bool +compile_constraint = mixin (specific_compile_constraint <@> default_compile_constraint) +default_compile_constraint :: FDSolver so => Mixin (FDConstraint so -> Tree so Bool) +default_compile_constraint = default_compile_alldiff + <@> default_compile_sorted + <@> default_compile_dom -data FD_Term where - FD_Var :: FDVar -> FD_Term - deriving Show +-- decompose + default +decompose :: FDSolver s => Expr (FDTerm s) -> Tree s (FDTerm s) +decompose = mixin (front_decompose <@> specific_decompose <@> default_decompose) +default_decompose :: FDSolver s => Mixin (Expr (FDTerm s) -> Tree s (FDTerm s)) +default_decompose _ _ x = debug "default_decompose" $ do + v <- fresh_var + compile_constraint (Same x (Term v)) + return v +front_decompose :: FDSolver s => Mixin (Expr (FDTerm s) -> Tree s (FDTerm s)) +front_decompose s t (Term x) = debug "front_decompose Term" $ return x +front_decompose s t x = debug "front_decompose _" $ s x -un_fd (FD_Var v) = v +-- fresh_var + default +fresh_var :: FDSolver s => Tree s (FDTerm s) +fresh_var = mixin (specific_fresh_var <@> default_fresh_var) +default_fresh_var :: FDSolver s => Mixin (Tree s (FDTerm s)) +default_fresh_var _ _ = debug "default_fresh_var" $ NewVar $ \v -> return 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 +type FDExpr s = Expr (FDTerm s) -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 +-- currently 4 simple constraints + more complex (see default compiler at the bottom) +data Show (FDTerm s) => FDConstraint s = + Less (Expr (FDTerm s)) (Expr (FDTerm s)) + | Diff (Expr (FDTerm s)) (Expr (FDTerm s)) + | Same (Expr (FDTerm s)) (Expr (FDTerm s)) + | Dom (Expr (FDTerm s)) Integer Integer + | AllDiff [Expr (FDTerm s)] + | Sorted [Expr (FDTerm s)] Bool -- True = less-or-equal, False = less +deriving instance Show (FDTerm s) => Show (FDConstraint s) -(#<) :: (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 +----------------------- FDWrapper -all_different = addFD . FD_AllDiff +newtype FDWrapper s a = FDWrapper { subFD :: s a } -instance ToExpr FD_Term where - toExpr (FD_Var v) = toExpr v +type FDTree s a = Tree (FDWrapper s) a -fd_domain :: FD_Term -> FD [Int] -fd_domain (FD_Var v) = do d <- lookup v - return $ elems d +newtype FDLabel s = FDLabel (Label s) -fd_objective :: FD FD_Term -fd_objective = - do s <- get - return $ FD_Var $ objective s +instance FDSolver s => Monad (FDWrapper s) where + FDWrapper { subFD = a } >>= f = FDWrapper { subFD = a >>= (\x -> subFD $ f x) } + return x = FDWrapper { subFD = return x } -class To_FD_Term a where - to_fd_term :: a -> FD FD_Term +instance FDSolver s => Solver (FDWrapper s) where + type Constraint (FDWrapper s) = FDConstraint s + type Label (FDWrapper s) = FDLabel s + add c = FDWrapper { subFD = untree False $ compile_constraint c } + run (FDWrapper { subFD = x}) = run x + mark = FDWrapper { subFD = mark >>= \x -> return (FDLabel x) } + goto (FDLabel l) = FDWrapper { subFD = goto l } -instance To_FD_Term FD_Term where - to_fd_term = return . id +data EQHelp a b where + EQHelp :: EQHelp a a -instance To_FD_Term Int where - to_fd_term i = newVar i >>= return . FD_Var +instance (FDSolver s, t ~ Expr (FDTerm s)) => Term (FDWrapper s) t where + type Help (FDWrapper s) t = EQHelp t (Expr (FDTerm s)) + help _ _ = EQHelp + newvar = FDWrapper { subFD = newvar >>= (\x -> return (Term x)) } -instance To_FD_Term Expr where - to_fd_term e = unExpr e >>= return . FD_Var +instance (FDSolver s, FDTerm s ~ t, Eq t, EnumTerm s t, Integral (TermDomain s t)) => EnumTerm (FDWrapper s) (Expr t) where + type TermDomain (FDWrapper s) (Expr t) = TermDomain s t + get_domain_size (Const c) = return 1 + get_domain_size (Term v) = FDWrapper (get_domain_size v) + get_value (Const c) = return $ Just $ fromInteger c + get_value (Term v) = FDWrapper $ get_value v + split_domain_partial (Const c) = return [return ()] + split_domain_partial (Term v) = FDWrapper $ split_domain_partial v >>= return . map wrap + split_domain (Const c) = return $ return () + split_domain (Term v) = FDWrapper $ split_domain v >>= return . wrap + split_domains l = FDWrapper $ split_domains (map (\x -> case x of Term t -> t) l) >>= return . wrap --------------------------------------------------------------------------------- +unwrap :: forall s a .FDSolver s => Tree (FDWrapper s) a -> Tree s a +unwrap Fail = Fail +unwrap (Return a) = Return a +unwrap (Try l r) = Try (unwrap l) (unwrap r) +unwrap (NewVar (f :: t -> Tree (FDWrapper s) a)) = NewVar ((\v -> + case help (undefined :: FDWrapper s ()) (undefined :: t) of + EQHelp -> unwrap (f (Term v :: Expr (FDTerm s)))) + :: FDTerm s -> Tree s a) +unwrap (Add c t) = compile_constraint c >>= (\b -> if b then (unwrap t) else Fail) +unwrap (Label (FDWrapper { subFD = m })) = Label (m >>= \x -> return (unwrap x)) --- The FD monad -newtype FD a = FD { unFD :: StateT FDState Maybe a } - deriving (Monad, MonadState FDState, MonadPlus) +wrap :: forall s a .FDSolver s => Tree s a -> Tree (FDWrapper s) a +wrap Fail = Fail +wrap (Return a) = Return a +wrap (Try l r) = Try (wrap l) (wrap r) +wrap (Label m) = Label $ FDWrapper $ m >>= return . wrap +wrap (Add c t) = Label $ FDWrapper $ add c >>= \res -> if res then return $ wrap t else return $ false +wrap (NewVar f) = Label $ FDWrapper $ newvar >>= return . wrap . f --- FD variables -newtype FDVar = FDVar { unFDVar :: Int } deriving (Ord, Eq, Show) -type VarSupply = FDVar +-- TODO: wrap afmaken +-- TODO: Tree opsplitsen in Tree (Try nodes) en Conjunction (de rest) -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) } +----------------------- Operators -class ToExpr a where - toExpr :: a -> Expr +-- syntactic sugar for expressions +infixl 6 @+ +infixl 6 @- +infixl 7 @* +infixl 7 @/ +infixl 7 @% +a @+ b = (toExpr a) + (toExpr b) +a @- b = (toExpr a) - (toExpr b) +a @* b = (toExpr a) * (toExpr b) +a @/ b = (toExpr a) `div` (toExpr b) +a @% b = (toExpr a) `mod` (toExpr b) +cte x = fromInteger $ toInteger x -instance ToExpr FDVar where - toExpr = Expr . return +-- syntactic sugar for relations -instance ToExpr Expr where - toExpr = id +infix 4 @: +a @: (b,c) = addC $ Dom a (toInteger b) (toInteger c) -instance Integral i => ToExpr i where - toExpr n = Expr $ newVar n +infix 4 @< +a @< b = addC $ Less a b -exprVar :: ToExpr a => a -> FD FDVar -exprVar = unExpr . toExpr +infix 4 @<= +a @<= b = addC $ Less a (b + 1) --- 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 +infix 4 @> +a @> b = addC $ Less b a -infixl 6 .+. -(.+.) :: (ToExpr a, ToExpr b) => a -> b -> Expr -(.+.) = addArithmeticConstraint getDomainPlus getDomainMinus getDomainMinus +infix 4 @>= +a @>= b = addC $ Less b (a + 1) -infixl 6 .-. -(.-.) :: (ToExpr a, ToExpr b) => a -> b -> Expr -(.-.) = addArithmeticConstraint getDomainMinus getDomainPlus - (flip getDomainMinus) +infix 4 @= +a @= b = addC $ Same a b -infixl 7 .*. -(.*.) :: (ToExpr a, ToExpr b) => a -> b -> Expr -(.*.) = addArithmeticConstraint getDomainMult getDomainDiv getDomainDiv +infix 4 @/= +a @/= b = addC $ Diff a b -getDomainPlus :: Domain -> Domain -> Domain -getDomainPlus xs ys = toDomain (zl, zh) where - zl = findMin xs + findMin ys - zh = findMax xs + findMax ys +allDiff l = addC $ AllDiff l +sorted l = addC $ Sorted l True +sSorted l = addC $ Sorted l False -getDomainMinus :: Domain -> Domain -> Domain -getDomainMinus xs ys = toDomain (zl, zh) where - zl = findMin xs - findMax ys - zh = findMax xs - findMin ys +allin list range = foldr1 (/\) $ map (@: range) list -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]] +--------------------------------------------------------------------------------- +-- Default compilations +--------------------------------------------------------------------------------- -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]] +default_compile_alldiff :: FDSolver so => Mixin (FDConstraint so -> Tree so Bool) +default_compile_alldiff s t c = case c of + (AllDiff []) -> return True + (AllDiff (x:xs)) -> do + conj [ (t $ Diff x e) /\ return () | e <- xs ] + t $ AllDiff xs + return True + _ -> s c -infix 4 .==. -(.==.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool -xexpr .==. yexpr = do - x <- exprVar xexpr - y <- exprVar yexpr - x `same` y +default_compile_sorted :: FDSolver so => Mixin (FDConstraint so -> Tree so Bool) +default_compile_sorted s t c = case c of + (Sorted [] _) -> return True + (Sorted (x:xs) eq) -> do + conj [ (t $ Less x (if eq then e+1 else e)) /\ return () | e <- xs ] + t $ Sorted xs eq + return True + _ -> s c -infix 4 ./=. -(./=.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool -xexpr ./=. yexpr = do - x <- exprVar xexpr - y <- exprVar yexpr - x `different` y +default_compile_dom :: FDSolver so => Mixin (FDConstraint so -> Tree so Bool) +default_compile_dom s t c = case c of + (Dom _ l u) | l>u -> Fail + (Dom x l u) -> do + t $ Less x (Const $ u+1) + t $ Less (Const $ l-1) x + return True + _ -> s c diff --git a/Control/CP/FD/FDSugar.hs b/Control/CP/FD/FDSugar.hs deleted file mode 100644 --- a/Control/CP/FD/FDSugar.hs +++ /dev/null @@ -1,129 +0,0 @@ -{- - - Monadic Constraint Programming - - http://www.cs.kuleuven.be/~toms/Haskell/ - - Tom Schrijvers - -} -{-# LANGUAGE TransformListComp #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE TypeFamilies #-} - -module Control.CP.FD.FDSugar where - -import Control.CP.SearchTree hiding (label) -import Control.CP.Transformers -import Control.CP.ComposableTransformers -import Control.CP.Queue -import Control.CP.Solver - -import GHC.Exts (sortWith) -import qualified Control.CP.PriorityQueue as PriorityQueue -import qualified Data.Sequence -import Control.CP.FD.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 <- mark - 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 = run $ 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 = run $ 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 diff --git a/Control/CP/FD/Gecode/CodegenSolver.hs b/Control/CP/FD/Gecode/CodegenSolver.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Gecode/CodegenSolver.hs @@ -0,0 +1,476 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +module Control.CP.FD.Gecode.CodegenSolver ( + CodegenSolver(..), + compile, + Store(..), + StoreNode(..), + StoreNodeType(..), + getVarType, + isVarImplicit, + VarBound(..), + getAllBounds +) where + +import Maybe (fromMaybe,catMaybes,isJust,fromJust) +import List (findIndex,find) +import Data.Map hiding (map,filter) + +import Control.Monad.State.Lazy +import Control.Monad.Trans +import Control.Monad.Cont + + +import Control.CP.SearchTree hiding (label) +import Control.CP.Solver +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.Debug +import Control.CP.Mixin + +import Control.CP.FD.Gecode.Common + +-------------------------------------------------------------------------------- +-- | Helper functions +-------------------------------------------------------------------------------- + +repl l i v = case l of + [] -> [v] + a:ar -> if i==0 + then v:ar + else repl ar (i-1) v + +revrepl l i v = repl l ((length l)-i-1) v + +revget l i = l !! ((length l)-i-1) + +dump n l = case l of + [] -> [] + (a:b) -> if (n==0) then b else a:(dump (n-1) b) + +-------------------------------------------------------------------------------- +-- | Gecode Solver instance declaration +-------------------------------------------------------------------------------- +instance Solver CodegenSolver where + type Constraint CodegenSolver = GConstraint + type Label CodegenSolver = Store + add = addGecode + run = runGecode + mark = get + goto = put + +-------------------------------------------------------------------------------- +-- | CodegenSolver terms +-------------------------------------------------------------------------------- + +instance Term CodegenSolver IntTerm where + newvar = newVar False TypeInt >>= return . IntVar + type Help CodegenSolver IntTerm = () + help _ _ = () + +instance Term CodegenSolver BoolTerm where + newvar = newVar False TypeBool >>= return . BoolVar + type Help CodegenSolver BoolTerm = () + help _ _ = () + +-------------------------------------------------------------------------------- +-- | CodegenSolver monad definition +-------------------------------------------------------------------------------- + +newtype CodegenSolver a = CodegenSolver { state :: State Store a } + deriving (Monad, MonadState Store) + +-- instance Show (CodegenSolver a) where +-- show c = show $ execState (state c) initState + + +type VarId = Int +type LowerBound = Maybe Integer +type UpperBound = Maybe Integer + +data VarBound = VarBound { varid :: VarId, lbound :: LowerBound, ubound :: UpperBound } + deriving (Show, Eq) + +type VarBoundMap = Map VarId VarBound +type VarBoundPropagator = VarBoundMap -> [ VarBound ] + +-------------------------------------------------------------------------------- +{- | + StoreNode represents a node in the search tree. + * Each node adds new constraints and variables. + * A node is a leaf node or an internal node + -} +data StoreNode = + StoreNode { cons :: [ GConstraint ] + -- ^ new constraints added in this node + , nbounds :: [ VarBoundPropagator ] + -- ^ new bound-generator functions in this node + , nvars :: [ Int ] + -- ^ id's of variables added in this node + , dis :: StoreNodeType + -- ^ either no children, or one left and one right child + } + +data StoreNodeType = SNLeaf | SNIntl StoreNode StoreNode + deriving Show + +instance Show StoreNode + where show sn = "StoreNode { cons=" ++ (show $ cons sn) ++ + ", nbounds=" ++ (show $ length $ nbounds sn) ++ + ", nvars=" ++ (show $ nvars sn) ++ + ", dus=" ++ (show $ dis sn) ++ + "}" +-------------------------------------------------------------------------------- + +data VarData = VarData { vtype :: GType, vimpl :: Bool } + deriving Show + +data Store = Store { vars :: Int, vardata :: [ VarData ], ctree :: StoreNode, cpath :: [ Bool ], cexpr :: Map (ExprKey (FDTerm CodegenSolver)) Int } + deriving Show + + +setVarImplicitHelper :: Store -> Int -> Bool -> Store +setVarImplicitHelper s p v = s { vardata = revrepl (vardata s) p ( (revget (vardata s) p) { vimpl = v } ) } + +initNode = StoreNode { cons = [], dis = SNLeaf, nvars = [], nbounds=[] } +initState = Store { vars=0, vardata=[], ctree=initNode, cpath=[], cexpr=empty } + +addStateTree node path con vars bounds = case (dis node,path) of + (_,[]) -> node { cons = con++(cons node), nvars = vars++(nvars node), nbounds = bounds++(nbounds node) } + (SNLeaf,s:sr) -> node { dis = if s then SNIntl initNode (addStateTree initNode sr con vars bounds) + else SNIntl (addStateTree initNode sr con vars bounds) initNode } + (SNIntl l r,s:sr) -> node { dis = if s then SNIntl l (addStateTree r sr con vars bounds) + else SNIntl (addStateTree l sr con vars bounds) r } + +addState store con vars bounds = store { ctree = addStateTree (ctree store) (cpath store) con vars bounds } + +getConstraintsTree tree path = (cons tree) ++ case (dis tree,path) of + (SNLeaf,_) -> [] + (SNIntl l _, False:s) -> getConstraintsTree l s + (SNIntl l _, []) -> getConstraintsTree l [] + (SNIntl _ r, True:s) -> getConstraintsTree r s + + +getConstraints state = getConstraintsTree (ctree state) (cpath state) + +-------------------------------------------------------------------------------- +-- | CodegenSolver compilation +-------------------------------------------------------------------------------- + +compile :: Tree CodegenSolver a -> Store +compile x = execGecode (buildState x) + +execGecode :: CodegenSolver a -> Store +execGecode x = execState (state x) initState + +buildState :: Tree CodegenSolver a -> CodegenSolver () +buildState (Add c v) = do add c + buildState v +buildState (NewVar f) = do v <- newvar + buildState $ f v +buildState (Try l r) = do v1 <- get + let opath = cpath v1 + let ocexpr = cexpr v1 + put $ v1 { cpath = opath ++ [ False ], cexpr = ocexpr } + buildState l + v2 <- get + put $ v2 { cpath = opath ++ [ True ], cexpr = ocexpr } + buildState r + v3 <- get + put $ v3 { cpath = opath, cexpr = ocexpr } +buildState (Label m) = m >>= buildState +buildState _ = return () + +-------------------------------------------------------------------------------- +-- | Bounds +-------------------------------------------------------------------------------- + +data XInt = XInfMin | XInfPlus | XInt Integer + +toXInt isUpper Nothing = if isUpper then XInfPlus else XInfMin +toXInt _ (Just i) = XInt i + +bndMult (XInt a) (XInt b) _ _ = [XInt (a*b)] +bndMult XInfMin XInfMin _ _ = [XInfPlus] +bndMult XInfPlus XInfMin _ _ = [XInfMin] +bndMult XInfPlus XInfPlus _ _ = [XInfPlus] +bndMult (XInt a) XInfPlus la _ + | a < 0 = [XInfMin] + | a > 0 = [XInfPlus] + | a == 0 && la = [XInfPlus] + | a == 0 && not la = [XInfMin] +bndMult (XInt a) XInfMin la _ + | a < 0 = [XInfPlus] + | a > 0 = [XInfMin] + | a == 0 && la = [XInfMin] + | a == 0 && not la = [XInfPlus] +bndMult a b c d = bndMult b a d c + +bndDiv _ _ _ _ = [XInfMin,XInfPlus] + +boundFn f v1 v2 l1 l2 = f (toXInt l1 v1) (toXInt l2 v2) l1 l2 + +lowestBound :: [XInt] -> XInt +lowestBound = foldl1 m + where m XInfMin _ = XInfMin + m _ XInfMin = XInfMin + m (XInt a) (XInt b) = XInt $ min a b + m (XInt a) _ = XInt a + m _ (XInt a) = XInt a + m XInfPlus XInfPlus = XInfPlus + +highestBound :: [XInt] -> XInt +highestBound = foldl1 m + where m XInfPlus _ = XInfPlus + m _ XInfPlus = XInfPlus + m (XInt a) (XInt b) = XInt $ max a b + m (XInt a) _ = XInt a + m _ (XInt a) = XInt a + m XInfMin XInfMin = XInfMin + +boundRelation f (i1,i2,o) b = + let (i1l,i1u) = getBounds b i1 + (i2l,i2u) = getBounds b i2 + bns = foldl1 (++) $ map (\(a,b,c,d) -> boundFn f a b c d) + [(i1l,i2l,False,False) + ,(i1l,i2u,False,True) + ,(i1u,i2l,True,False) + ,(i1u,i2u,True,True) + ] + xl = lowestBound bns + xu = highestBound bns + fromXInt XInfPlus = Nothing + fromXInt XInfMin = Nothing + fromXInt (XInt a) = Just a + in case (xl,xu) of + (XInfPlus,_) -> [] + (_,XInfMin) -> [] + (_,_) -> [VarBound { varid = o, lbound = fromXInt xl, ubound = fromXInt xu }] + +catPropagators p = foldl1 (\a b -> \x -> (a x) ++ (b x)) p + +linearPropagator l p c = \b -> + let (IntVar i,cc) = l !! p + (low,high) = foldl + (\x y -> case (x,y) of + ((Just l1,Just h1),(Just l2,Just h2)) -> (Just (l1-h2),Just (h1-l2)) + ((Nothing,Just h1),(Just l2,_)) -> (Nothing,Just (h1-l2)) + ((_,Just h1),(Just l2,Nothing)) -> (Nothing,Just (h1-l2)) + ((Just l1,Nothing),(_,Just h2)) -> (Just (l1-h2),Nothing) + ( (Just l1,_),(Nothing,Just h2)) -> (Just (l1-h2),Nothing) + _ -> (Nothing,Nothing) + ) (Just c,Just c) cbounds + cbounds = map + (\x -> case x of + (c,(Just l,Just h)) -> if c<0 then (Just (c*h),Just (c*l)) else (Just (c*l),Just (c*h)) + (c,(Nothing,Just h)) -> if c<0 then (Just (c*h),Nothing) else (Nothing,Just (c*h)) + (c,(Just l,Nothing)) -> if c<0 then (Nothing,Just (c*l)) else (Just (c*l),Nothing) + _ -> (Nothing,Nothing) + ) dbounds + dbounds = dump p bounds + bounds = map (\(IntVar v,c) -> {- debug ("var "++(show v)++" is in "++(show $ getBounds b v)) $ -} (c,getBounds b v)) l + in (i,cc,low,high) + +linearEqPropagator ll p c = \b -> case linearPropagator ll p c b of + (_,0,_,_) -> [] + (i,cc,Just l,Just h) -> {- debug ("["++(if l>h then "AAAARGH! " else "")++(show ll)++"="++(show c)++"/"++(show cc)++"->["++(show p)++"]: var "++(show i)++" in ["++(show l)++".."++(show h)++"]]\n") $ -} if (cc<0) + then let x=[ VarBound i (Just ((-h) `div` (-cc))) (Just (l `div` cc)) ] in {- debug (show x) -} x + else let x=[ VarBound i (Just ((-l) `div` (-cc))) (Just (h `div` cc)) ] in {- debug (show x) -} x + (i,cc,Nothing,Just h) -> {- debug ("["++(show ll)++"="++(show c)++"/"++(show cc)++"->["++(show p)++"]: var "++(show i)++" in [.."++(show h)++"]]\n") $ -} if (cc<0) + then let x=[ VarBound i (Just ((-h) `div` (-cc))) Nothing ] in {- debug (show x) -} x + else let x=[ VarBound i Nothing (Just (h `div` cc)) ] in {- debug (show x) -} x + (i,cc,Just l,Nothing) -> {- debug ("["++(show ll)++"="++(show c)++"/"++(show cc)++"->["++(show p)++"]: var "++(show i)++" in ["++(show l)++"..]]\n") $ -} if (cc<0) + then let x=[ VarBound i Nothing (Just (l `div` cc)) ] in {- debug (show x) -} x + else let x=[ VarBound i (Just ((-l) `div` (-cc))) Nothing ] in {- debug (show x) -} x + (i,cc,_,_) -> {- debug ("["++(show ll)++"="++(show c)++"/"++(show cc)++"->["++(show p)++"]: var "++(show i)++" in [..]]\n") $ -} [] + +linearLessPropagator l p c = \b -> case (linearPropagator l p c b) of + (_,0,_,_) -> [] + (i,cc,_,Just h) -> if (cc<0) + then [ VarBound i (Just ((1-h) `div` (-cc))) Nothing ] + else [ VarBound i Nothing (Just ((h-1) `div` cc)) ] + _ -> [] + +debugBoundsPropagator :: GConstraint -> VarBoundPropagator +debugBoundsPropagator c = let cc = boundsPropagator c in + \b -> let ccc = cc b in {- debug ("debugBounds: "++(show c)++" -> "++(show ccc)) -} ccc + +boundsPropagator :: GConstraint -> VarBoundPropagator +boundsPropagator c = case c of + CValue (IntVar i) v -> (\_ -> [ VarBound i (Just v) (Just v) ]) + CDom (IntVar i) l u -> (\_ -> [ VarBound i (Just l) (Just u) ]) + CRel (IntVar i) OLess (IntVar j) -> \b -> + let (jbl,jbu) = getBounds b j + (ibl,ibu) = getBounds b i + in catMaybes [ if isJust jbu then Just $ VarBound i Nothing (Just $ (fromJust jbu)-1) else Nothing, + if isJust ibl then Just $ VarBound j (Just $ (fromJust ibl)+1) Nothing else Nothing + ] + CRel (IntVar i) OEqual (IntVar j) -> \b -> + let (jbl,jbu) = getBounds b j + (ibl,ibu) = getBounds b i + in [ VarBound i jbl jbu, VarBound j ibl ibu ] + CRel (IntVar i) OEqual (IntConst c) -> boundsPropagator $ CValue (IntVar i) c + CRel (IntConst c) OEqual (IntVar i) -> boundsPropagator $ CValue (IntVar i) c + CRel (IntVar i) OLess (IntConst c) -> (\_ -> [ VarBound i Nothing (Just (c-1)) ]) + CRel (IntConst c) OLess (IntVar i) -> (\_ -> [ VarBound i (Just (c+1)) Nothing ]) + CLinear [(IntVar i,f)] OEqual c | (c `mod` f)==0 -> boundsPropagator $ CValue (IntVar i) (c `div` f) + CLinear l OEqual c -> catPropagators $ map (\p -> linearEqPropagator l p c) [0..((length l)-1)] + CLinear l OLess c -> catPropagators $ map (\p -> linearLessPropagator l p c) [0..((length l)-1)] + CMult (IntVar f1) (IntVar f2) (IntVar m) -> catPropagators + [ boundRelation bndMult (f1,f2,m) + , boundRelation bndDiv (m,f1,f2) + , boundRelation bndDiv (m,f2,f1) + ] + CAbs (IntVar v1) (IntVar v2) -> \b -> + let (v1l,v1h) = getBounds b v1 + (v2l,v2h) = getBounds b v2 + in [ case v2h of + Nothing -> VarBound v1 Nothing Nothing + Just h -> VarBound v1 (Just (-h)) (Just h) + , case (v1l,v1h) of + (Nothing,Nothing) -> VarBound v2 (Just 0) (Nothing) + (Just l,Nothing) | l<0 -> VarBound v2 (Just 0) Nothing + (Nothing,Just h) | h>0 -> VarBound v2 (Just 0) Nothing + (Just l,Nothing) | l>=0 -> VarBound v2 (Just l) Nothing + (Nothing,Just h) | h<=0 -> VarBound v2 (Just (-h)) Nothing + (Just l,Just h) | l<=0 && h>=0 -> VarBound v2 (Just 0) (Just ((-l) `max` h)) + (Just l,Just h) | h<0 -> VarBound v2 (Just (-h)) (Just (-l)) + (Just l,Just h) | l>0 -> VarBound v2 (Just l) (Just h) + ] + _ -> (\_ -> []) + +-- Combination +propagateVarBounds :: [ VarBoundPropagator ] -> VarBoundMap -> VarBoundMap +propagateVarBounds propagators vbmap = fixP propagators vbmap + where + fixP :: [VarBoundPropagator] -> VarBoundMap -> VarBoundMap + fixP [] src = src + fixP (p:ps) src = case propagate p src of + Nothing -> fixP ps src + Just src' -> fixP propagators src' + propagate p src = + either (const Nothing) Just $ foldl combine (Left src) (p src) + where combine prev vb = prev `fromMaybe` (intersectBound vb src >>= return . Right) + where src = either id id prev + +-- add a new bound to a bounds map - returns Nothing if map remains unchanged, Just otherwise +intersectBound :: VarBound -> VarBoundMap -> Maybe VarBoundMap +intersectBound nw k + | oldValue == newValue = Nothing + | otherwise = Just result + where + (oldValue,result) = insertLookupWithKey (\k n o -> n) (varid nw) (fromJust newValue) k + newValue = + (do ov <- oldValue + return $ adj ov + ) `orElse` (Just nw) + adj fnd@(VarBound {lbound = olb, ubound = oub}) = nb + where + nlb = newmax 1 olb $ lbound nw + nub = newmax (-1) oub $ ubound nw + nb = fnd { lbound = nlb, ubound = nub } + newmax f b1 b2 = + (do x <- b1 + y <- b2 + return $ ((f*x) `max` (f*y)) `div` f + ) `orElse` b1 `orElse` b2 + +unionBounds :: VarBoundMap -> VarBoundMap -> VarBoundMap +unionBounds = unionWith unioner + where unioner (VarBound i1 l1 u1) (VarBound i2 l2 u2) = VarBound i1 (newmax (-1) l1 l2) (newmax 1 u1 u2) + newmax f b1 b2 = + do x <- b1 + y <- b2 + return $ ((f*x) `max` (f*y)) `div` f + +getBounds :: VarBoundMap -> VarId -> (LowerBound, UpperBound) +getBounds b v = + let bnd = case Data.Map.lookup v b of + Nothing -> (Nothing,Nothing) + Just k -> (lbound k,ubound k) + in {- debug ("v"++(show v)++": "++(show bnd)) -} bnd + +getNodeBounds :: StoreNode -> [ Bool ] -> [ VarBoundPropagator ] -> [ VarId ] -> [VarBoundMap] +getNodeBounds node path bnds vars = + let nvrs = nvars node ++ vars + nbnds = nbounds node ++ bnds + in case dis node of + SNLeaf -> [ propagateVarBounds nbnds $ fromList $ map (\x -> (x,VarBound x Nothing Nothing)) nvrs ] + SNIntl l r -> case path of + [] -> (getNodeBounds l [] nbnds nvrs) ++ (getNodeBounds r [] nbnds nvrs) + x:rp -> getNodeBounds (if x then r else l) rp nbnds nvrs + + +getPathBounds :: Store -> [Bool] -> VarBoundMap +getPathBounds s p = foldl (flip unionBounds) empty (getNodeBounds (ctree s) p [] []) + +getAllBounds s = getPathBounds s [] +getCurBounds s = getPathBounds s (cpath s) + +-------------------------------------------------------------------------------- +-- | CodegenSolver solver implementation +-------------------------------------------------------------------------------- + +addGecode c = do + s <- get + put $ addState s [c] [] [boundsPropagator c] + return True + +newVar :: Bool -> GType -> CodegenSolver Int +newVar impl tp = do + s <- get + let vn = vars s + put $ addState (s { vars = vn + 1, vardata = (VarData { vtype=tp, vimpl=impl }) : (vardata s) }) [] [vn] [] + return $ vn + +runGecode :: CodegenSolver p -> p +runGecode x = evalState (state x) initState + +-------------------------------------------------------------------------------- +-- | CodegenSolver FDSolver instance +-------------------------------------------------------------------------------- + +instance GecodeSolver CodegenSolver where + caching_decompose super this x = Label $ do + s <- get + let wx = ExprKey x + case Data.Map.lookup wx (cexpr s) of + Nothing -> return $ do + n@(IntVar i) <- super x + Label $ do + s <- get + put $ s { cexpr = insert wx i $ cexpr s } + return $ return n + Just i -> return $ return $ IntVar i + setVarImplicit (IntVar i) b = do + s <- get + put $ setVarImplicitHelper s i b + +instance FDSolver CodegenSolver where + type FDTerm CodegenSolver = IntTerm + specific_compile_constraint = linearCompile <@> basicCompile + specific_decompose = caching_decompose + specific_fresh_var super this = do + v@(IntVar i) <- super + Label $ do + setVarImplicit (IntVar i) True + return $ Return v + +-- | utility + +getNumVars :: Store -> Int +getNumVars s = vars s + +getVarData :: Store -> Int -> VarData +getVarData s i = (vardata s) !! ((length $ vardata s)-1-i) + +modVarData :: Store -> Int -> VarData -> Store +modVarData s i d = s { vardata = revrepl (vardata s) i d } + +getVarType :: Store -> Int -> GType +getVarType s i = vtype $ getVarData s i + +isVarImplicit :: Store -> Int -> Bool +isVarImplicit s i = vimpl $ getVarData s i diff --git a/Control/CP/FD/Gecode/Common.hs b/Control/CP/FD/Gecode/Common.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Gecode/Common.hs @@ -0,0 +1,277 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} + +module Control.CP.FD.Gecode.Common ( + GTerm(..), + GType(..), + IntTerm(..), + BoolTerm(..), + GConstraint(..), + GOperator(..), + GecodeSolver(..), + orElse, + linearCompile, + basicCompile +) where + +import Maybe (fromMaybe,catMaybes,isJust,fromJust) +import List (findIndex,find) +import Data.Map hiding (map,filter) + +import Control.Monad.State.Lazy +import Control.Monad.Trans +import Control.Monad.Cont + + +import Control.CP.SearchTree hiding (label) +import Control.CP.Solver +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.Debug +import Control.CP.Mixin +-- import Control.CP.Gecode.Gecode + +-------------------------------------------------------------------------------- +-- | Gecode terms +-------------------------------------------------------------------------------- + +class GTerm t where + getVarId :: t -> Maybe Int + getIntValue :: t -> Maybe Integer + getDefBounds :: t -> (Integer,Integer) + +data GType = TypeInt | TypeBool + deriving (Show, Eq) + +-- | integer terms +data IntTerm + = IntVar Int + | IntConst Integer + deriving Eq + +instance Ord IntTerm where + compare (IntVar i1) (IntVar i2) = compare i1 i2 + compare (IntVar _) _ = LT + compare _ (IntVar _) = GT + compare (IntConst c1) (IntConst c2) = compare c1 c2 + +instance Show IntTerm where + show (IntVar i) = "i" ++ (show i) + show (IntConst i) = (show i) + +instance GTerm IntTerm where + getVarId (IntVar i) = Just i + getVarId (IntConst _) = Nothing + getIntValue (IntVar _) = Nothing + getIntValue (IntConst c) = Just c + getDefBounds _ = (-1000000000,1000000000) + +-- | boolean terms +data BoolTerm where + BoolVar :: Int -> BoolTerm + BoolConst :: Bool -> BoolTerm + deriving Eq + +instance Show BoolTerm where + show (BoolVar i) = "b" ++ (show i) + show (BoolConst b) = show b + +instance GTerm BoolTerm where + getVarId (BoolVar i) = Just i + getVarId (BoolConst _) = Nothing + getIntValue (BoolVar _) = Nothing + getIntValue (BoolConst c) = Just $ if c then 1 else 0 + getDefBounds _ = (0,1) + +-- instance Term Gecode BoolTerm where +-- type TermInfo Gecode BoolTerm = Bool +-- newvar = newVar False TypeBool >>= return . BoolVar +-- +-- instance Term Gecode IntTerm where +-- type TermInfo Gecode IntTerm = Bool +-- newvar = newVar False TypeInt >>= return . IntVar + + +-------------------------------------------------------------------------------- +-- | Gecode constraints +-------------------------------------------------------------------------------- + +data GConstraint + = forall t . GTerm t => CDiff t t + | forall t . GTerm t => CSame t t + | CRel IntTerm GOperator IntTerm + | CMult IntTerm IntTerm IntTerm + | CAbs IntTerm IntTerm + | CDiv IntTerm IntTerm IntTerm + | CMod IntTerm IntTerm IntTerm + | CValue IntTerm Integer + | CDom IntTerm Integer Integer + | CLinear [(IntTerm,Integer)] GOperator Integer + | CAllDiff [IntTerm] + | CSorted [IntTerm] Bool + +instance Show GConstraint where + show (CRel x o y) = "(Rel: " ++ (show x) ++ (show o) ++ (show y) ++ ")" + show (CMult x y z) = "(Mult: " ++ (show x) ++ " * " ++ (show y) ++ " = " ++ (show z) ++ ")" + show (CDiv x y z) = "(Div: " ++ (show x) ++ " / " ++ (show y) ++ " = " ++ (show z) ++ ")" + show (CMod x y z) = "(Mod: " ++ (show x) ++ " % " ++ (show y) ++ " = " ++ (show z) ++ ")" + show (CAbs x y) = "(Abs: abs " ++ (show x) ++ " = " ++ (show y) ++ ")" + show (CDom x y z) = "(Dom: " ++ (show x) ++ " in [" ++ (show y) ++ "," ++ (show z) ++ "])" + show (CValue x y) = "(Value: " ++ (show x) ++ " is " ++ (show y) ++ ")" + show (CLinear l o c) = "(Linear: " ++ (show l) ++ (show o) ++ (show c) ++ ")" + show (CAllDiff l) = "(AllDiff: " ++ (show l) ++ ")" + +data GOperator + = OEqual + | ODiff + | OLess + +instance Show GOperator where + show OEqual = "==" + show ODiff = "/=" + show OLess = "<" + +-------------------------------------------------------------------------------- +-- | Gecode FDSolver instance +-------------------------------------------------------------------------------- + +class (Solver s, Term s IntTerm) => GecodeSolver s where + setVarImplicit :: IntTerm -> Bool -> s () + setVarImplicit _ _ = return () + caching_decompose :: GecodeSolver s => Mixin (Expr (FDTerm s) -> Tree s IntTerm) + caching_decompose s _ x = s x + +-- | basic compilation + +basicCompile :: (FDSolver s, Constraint s ~ GConstraint, FDTerm s ~ IntTerm) => Mixin (FDConstraint s -> Tree s Bool) +basicCompile s t (Same a (Plus b c)) = do + va <- getAsVar a + vb <- getAsVar b + vc <- getAsVar c + addT (CLinear [(va,1),(vb,-1),(vc,-1)] OEqual 0) +basicCompile s t (Same a (Minus b c)) = do + va <- getAsVar a + vb <- getAsVar b + vc <- getAsVar c + addT (CLinear [(va,1),(vb,1),(vc,1)] OEqual 0) +basicCompile s t (Same a (Mult b c)) = do + va <- getAsVar a + vb <- getAsVar b + vc <- getAsVar c + addT (CMult vb vc va) +basicCompile s t (Same a (Div b c)) = do + va <- getAsVar a + vb <- getAsVar b + vc <- getAsVar c + addT (CDiv vb vc va) +basicCompile s t (Same a (Mod b c)) = do + va <- getAsVar a + vb <- getAsVar b + vc <- getAsVar c + addT (CMod vb vc va) +basicCompile s t (Same a (Abs b)) = do + va <- getAsVar a + vb <- getAsVar b + addT (CAbs vb va) +basicCompile s t (Same a@(Plus _ _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Minus _ _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Mult _ _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Div _ _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Mod _ _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Abs _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a@(Const _) b) = basicCompile s t $ Same b a +basicCompile s t (Same a (Const i)) = do + va <- getAsVar a + addT (CValue va i) +basicCompile s t (x@(Same a b)) = do + va <- getAsVar a + vb <- getAsTerm b + addT (CRel va OEqual vb) +basicCompile s t (Diff a b) = do + va <- getAsVar a + vb <- getAsTerm b + addT (CRel va ODiff vb) +basicCompile s t (Less a b) = do + va <- getAsVar a + vb <- getAsTerm b + addT (CRel va OLess vb) +basicCompile s t (Dom a l h) = do + va <- getAsVar a + addT (CDom va l h) +basicCompile s t (AllDiff l) = do + vl <- mapM getAsVar l + addT (CAllDiff vl) +basicCompile s t (Sorted l e) = do + vl <- mapM getAsVar l + addT (CSorted vl e) +-- basicCompile s _ x = s x + +getAsVar :: (FDSolver s, Constraint s ~ GConstraint, FDTerm s ~ IntTerm) => Expr IntTerm -> Tree s IntTerm +getAsVar = decompose +getAsTerm :: (FDSolver s, Constraint s ~ GConstraint, FDTerm s ~ IntTerm) => Expr IntTerm -> Tree s IntTerm +getAsTerm (Const c) = return $ IntConst c +getAsTerm x = decompose x + +-- | linear constraint compilation + +linearCompile :: (FDSolver s, Constraint s ~ GConstraint, FDTerm s ~ IntTerm) => Mixin (FDConstraint s -> Tree s Bool) +linearCompile s t (Same a@(Plus _ _) b) = linearCompileX a b OEqual +linearCompile s t (Same a@(Minus _ _) b) = linearCompileX a b OEqual +linearCompile s t (Same b a@(Plus _ _)) = linearCompileX a b OEqual +linearCompile s t (Same b a@(Minus _ _)) = linearCompileX a b OEqual +linearCompile s t (Diff a@(Plus _ _) b) = linearCompileX a b ODiff +linearCompile s t (Diff a@(Minus _ _) b) = linearCompileX a b ODiff +linearCompile s t (Diff a b@(Plus _ _)) = linearCompileX a b ODiff +linearCompile s t (Diff a b@(Minus _ _)) = linearCompileX a b ODiff +linearCompile s t (Less a@(Plus _ _) b) = linearCompileX a b OLess +linearCompile s t (Less a@(Minus _ _) b) = linearCompileX a b OLess +linearCompile s t (Less a b@(Plus _ _)) = linearCompileX a b OLess +linearCompile s t (Less a b@(Minus _ _)) = linearCompileX a b OLess +linearCompile s t x = s x + +linearCompileX a b o = + do t1 <- linearExprCompile a + t2 <- linearExprCompile b + let (x,a,c) = linearAdd t1 t2 1 (-1) + addT (CLinear (filter (\(_,a) -> a /= 0) $ map (\(xe,ae) -> (IntVar xe,ae)) $ zip x a) o c) + +linearExprCompile :: (FDSolver s, Constraint s ~ GConstraint, FDTerm s ~ IntTerm) => Expr (FDTerm s) -> Tree s ([Int],[Integer],Integer) +linearExprCompile (Term (IntVar i)) = + return ([i],[1],0) +linearExprCompile (Term (IntConst c)) = + return ([],[],-c) +linearExprCompile (Const c) = + return ([],[],-c) +linearExprCompile (Plus a b) = + do t1 <- linearExprCompile a + t2 <- linearExprCompile b + return $ linearAdd t1 t2 1 1 +linearExprCompile (Minus a b) = + do t1 <- linearExprCompile a + t2 <- linearExprCompile b + return $ linearAdd t1 t2 1 (-1) +linearExprCompile (Mult (Const c) a) = + do t <- linearExprCompile a + return $ linearAdd t ([],[],0) c 1 +linearExprCompile (Mult a (Const c)) = + linearExprCompile (Mult (Const c) a) +linearExprCompile x = + do (IntVar i) <- getAsVar x + return ([i],[1],0) + +linearAdd (x1,a1,c1) (x2,a2,c2) m1 m2 = case (x1,a1) of + ([],[]) -> (x2,map (*m2) a2,m1*c1+m2*c2) + (x1e:x1s,a1e:a1s) -> linearAdd (x1s,a1s,c1) (linearAddTerm (x2,a2,c2) x1e a1e m2 m1 [] []) m1 1 + +linearAddTerm (x1,a1,c1) x2e a2e m1 m2 xc ac = case (x1,a1) of + ([],[]) -> (x2e:xc,(a2e*m2):ac,c1*m1) + (x1e:x1s,a1e:a1s) -> if x1e == x2e + then ((x2e:x1s) ++ xc,((a1e*m1+a2e*m2):(map (*m1) a1s)) ++ ac,c1*m1) + else linearAddTerm (x1s,a1s,c1) x2e a2e m1 m2 (x1e:xc) ((a1e*m1):ac) + +-- | utility + +orElse :: Maybe a -> Maybe a -> Maybe a +orElse = mplus diff --git a/Control/CP/FD/Gecode/Interface.hsc b/Control/CP/FD/Gecode/Interface.hsc new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Gecode/Interface.hsc @@ -0,0 +1,173 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ForeignFunctionInterface #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +{-# CFILES glue/interface.cpp #-} + +module Control.CP.FD.Gecode.Interface ( + CGOperator(..), + CGIntVar(..), + CGBoolVar(..), + CGBool(..), + CGVal(..), + toCGIntVar, + toCGBoolVar, + toCGVal, + fromCGVal, + toCGBool, + fromCGBool, + Space, + Search, + newSpace, + copySpace, + newSearch, + runSearch, + IntTermInfo(..), + getIntTermInfo, + mapGOperator, + c_gecode_int_dom, + c_gecode_int_rel, + c_gecode_int_rel_cf, + c_gecode_int_rel_cs, + c_gecode_int_value, + c_gecode_int_mult, + c_gecode_int_div, + c_gecode_int_mod, + c_gecode_int_abs, + c_gecode_int_linear, + c_gecode_int_alldiff, + c_gecode_int_sorted, + c_gecode_int_newvar, + c_gecode_int_branch, + c_gecode_bool_newvar +) where + +#ifdef RGECODE + +import Foreign +import Foreign.C +import Foreign.C.Types +import Foreign.ForeignPtr + +import Control.CP.FD.Gecode.Common + +#include "gecodeglue.h" + +newtype CGOperator = CGOperator CInt + deriving Storable +newtype CGIntVar = CGIntVar CInt + deriving Storable +newtype CGBoolVar = CGBoolVar CInt + deriving Storable +newtype CGBool = CGBool CInt + deriving Storable +newtype CGVal = CGVal CInt + deriving Storable + +mapGOperator :: GOperator -> CGOperator +mapGOperator OEqual = CGOperator #const GOPERATOR_OEQUAL +mapGOperator ODiff = CGOperator #const GOPERATOR_ODIFF +mapGOperator OLess = CGOperator #const GOPERATOR_OLESS + +newtype GecodeModel = GecodeModel (Ptr GecodeModel) +newtype GecodeSearch = GecodeSearch (Ptr GecodeSearch) + +foreign import ccall unsafe "gecode_model_create" c_gecode_model_create :: IO (Ptr GecodeModel) +foreign import ccall unsafe "gecode_model_destroy" c_gecode_model_destroy :: Ptr GecodeModel -> IO () +foreign import ccall unsafe "&gecode_model_destroy" c_gecode_model_finalize :: FunPtr (Ptr GecodeModel -> IO ()) +foreign import ccall unsafe "gecode_model_copy" c_gecode_model_copy :: Ptr GecodeModel -> IO (Ptr GecodeModel) +foreign import ccall unsafe "gecode_model_fail" c_gecode_model_fail :: Ptr GecodeModel -> IO () +foreign import ccall unsafe "gecode_int_newvar" c_gecode_int_newvar :: Ptr GecodeModel -> IO CGIntVar +foreign import ccall unsafe "gecode_int_rel" c_gecode_int_rel :: Ptr GecodeModel -> CGIntVar -> CGOperator -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_rel_cf" c_gecode_int_rel_cf :: Ptr GecodeModel -> CGVal -> CGOperator -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_rel_cs" c_gecode_int_rel_cs :: Ptr GecodeModel -> CGIntVar -> CGOperator -> CGVal -> IO CGBool +foreign import ccall unsafe "gecode_int_value" c_gecode_int_value :: Ptr GecodeModel -> CGIntVar -> CGVal -> IO CGBool +foreign import ccall unsafe "gecode_int_mult" c_gecode_int_mult :: Ptr GecodeModel -> CGIntVar -> CGIntVar -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_div" c_gecode_int_div :: Ptr GecodeModel -> CGIntVar -> CGIntVar -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_mod" c_gecode_int_mod :: Ptr GecodeModel -> CGIntVar -> CGIntVar -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_abs" c_gecode_int_abs :: Ptr GecodeModel -> CGIntVar -> CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_dom" c_gecode_int_dom :: Ptr GecodeModel -> CGIntVar -> CGVal -> CGVal -> IO CGBool +foreign import ccall unsafe "gecode_int_linear" c_gecode_int_linear :: Ptr GecodeModel -> CInt -> Ptr CGIntVar -> Ptr CGVal -> CGOperator -> CGVal -> IO CGBool +foreign import ccall unsafe "gecode_int_alldiff" c_gecode_int_alldiff :: Ptr GecodeModel -> CInt -> Ptr CGIntVar -> IO CGBool +foreign import ccall unsafe "gecode_int_sorted" c_gecode_int_sorted :: Ptr GecodeModel -> CInt -> Ptr CGIntVar -> CGBool -> IO CGBool +foreign import ccall unsafe "gecode_int_info" c_gecode_int_info :: Ptr GecodeModel -> CGIntVar -> Ptr CGVal -> Ptr CGVal -> Ptr CGVal -> Ptr CInt -> Ptr CGVal -> IO () +foreign import ccall unsafe "gecode_int_branch" c_gecode_int_branch :: Ptr GecodeModel -> CInt -> Ptr CGIntVar -> IO () +foreign import ccall unsafe "gecode_bool_newvar" c_gecode_bool_newvar :: Ptr GecodeModel -> IO CGBoolVar +foreign import ccall unsafe "gecode_bool_branch" c_gecode_bool_branch :: Ptr GecodeModel -> CInt -> Ptr CGBoolVar -> IO () + +foreign import ccall unsafe "gecode_search_create" c_gecode_search_create :: Ptr GecodeModel -> IO (Ptr GecodeSearch) +foreign import ccall unsafe "&gecode_search_destroy" c_gecode_search_finalize :: FunPtr (Ptr GecodeSearch -> IO ()) +foreign import ccall unsafe "gecode_search_destroy" c_gecode_search_destroy :: Ptr GecodeSearch -> IO () +foreign import ccall unsafe "gecode_search_next" c_gecode_search_next :: Ptr GecodeSearch -> IO (Ptr GecodeModel) + +---- accessor functions + +toCGIntVar :: Integral a => a -> CGIntVar +toCGIntVar n = CGIntVar $ fromIntegral n + +toCGBoolVar :: Integral a => a -> CGBoolVar +toCGBoolVar n = CGBoolVar $ fromIntegral n + +toCGVal :: Integral a => a -> CGVal +toCGVal n = CGVal $ fromIntegral n + +fromCGVal :: Num a => CGVal -> a +fromCGVal (CGVal x) = fromIntegral x + +toCGBool :: Bool -> CGBool +toCGBool n = CGBool $ if n then 1 else 0 + +fromCGBool :: CGBool -> Bool +fromCGBool (CGBool x) = x /= 0 + +type Space = ForeignPtr GecodeModel +type Search = ForeignPtr GecodeSearch + +newSpace :: IO Space +newSpace = do + x <- c_gecode_model_create + newForeignPtr c_gecode_model_finalize x + +copySpace :: Space -> IO Space +copySpace s = withForeignPtr s $ \ptr -> do + x <- c_gecode_model_copy ptr + newForeignPtr c_gecode_model_finalize x + +newSearch :: Space -> IO Search +newSearch s = withForeignPtr s $ \ptr -> do + x <- c_gecode_search_create ptr + newForeignPtr c_gecode_search_finalize x + +runSearch :: Search -> IO (Maybe Space) +runSearch s = withForeignPtr s $ \ptr -> do + x <- c_gecode_search_next ptr + if (x == nullPtr) + then return Nothing + else do + res <- newForeignPtr c_gecode_model_finalize x + return $ Just res + +data IntTermInfo = IntTermInfo { iti_low :: CInt, iti_high :: CInt, iti_med :: CInt, iti_size :: CInt, iti_val :: Maybe CInt } + +getIntTermInfo :: Integral a => Space -> a -> IO IntTermInfo +getIntTermInfo s i = do + alloca $ \pLow -> + alloca $ \pHigh -> + alloca $ \pMed -> + alloca $ \pSize -> + alloca $ \pVal -> do + withForeignPtr s $ \ptr -> c_gecode_int_info ptr (toCGIntVar i) pLow pHigh pMed pSize pVal + vLow <- peek pLow + vHigh <- peek pHigh + vMed <- peek pMed + vSize <- peek pSize + vVal <- peek pVal + return $ IntTermInfo { + iti_low = fromCGVal vLow, + iti_high = fromCGVal vHigh, + iti_med = fromCGVal vMed, + iti_size = fromIntegral vSize, + iti_val = if (vSize==1) then Just (fromCGVal vVal) else Nothing + } + +#endif diff --git a/Control/CP/FD/Gecode/RuntimeSolver.hs b/Control/CP/FD/Gecode/RuntimeSolver.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Gecode/RuntimeSolver.hs @@ -0,0 +1,291 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +#ifdef RGECODE + +module Control.CP.FD.Gecode.RuntimeSolver ( + SearchSolver(..), + RuntimeSolver(..) +) where + +import Maybe (fromMaybe,catMaybes,isJust,fromJust) +import List (findIndex,find) +import Data.Map hiding (map,filter) + +import Control.Monad.State.Lazy +import Control.Monad.Trans +import Control.Monad.Cont + +import Data.Bits +import Data.Word +import Foreign +import Foreign.Storable +import Foreign.Marshal +import Foreign.Marshal.Array +import Foreign.Ptr +import Foreign.ForeignPtr +import Foreign.C.String +import Foreign.C.Types + +import Control.CP.SearchTree hiding (label) +import Control.CP.Solver +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.Debug +import Control.CP.Mixin +import Control.CP.EnumTerm + +import Control.CP.FD.Gecode.Common +import Control.CP.FD.Gecode.Interface + +class (Monad s, MonadState (GecodeState s) s, MonadIO s, Term s IntTerm) => RuntimeGecodeSolver s where + stateM :: s a -> StateT (GecodeState s) IO a + +instance Solver RuntimeSolver where + type Constraint RuntimeSolver = GConstraint + type Label RuntimeSolver = GecodeState RuntimeSolver + add = addRuntimeGecode + run = fst . runRuntimeGecode False + mark = do + s <- get + copyState s + goto s = do + x <- copyState s + put x + +instance Solver SearchSolver where + type Constraint SearchSolver = GConstraint + type Label SearchSolver = GecodeState SearchSolver + add = addRuntimeGecode + run = fst . runRuntimeGecode False + mark = do + s <- get + copyState s + goto s = do + x <- copyState s + put x + +-------------------------------------------------------------------------------- +-- | Gecode terms +-------------------------------------------------------------------------------- + +instance Term SearchSolver IntTerm where + newvar = newVarInt + type Help SearchSolver IntTerm = () + help _ _ = () +instance Term RuntimeSolver IntTerm where + newvar = newVarInt + type Help RuntimeSolver IntTerm = () + help _ _ = () +instance Term SearchSolver BoolTerm where + newvar = newVarBool + type Help SearchSolver BoolTerm = () + help _ _ = () +instance Term RuntimeSolver BoolTerm where + newvar = newVarBool + type Help RuntimeSolver BoolTerm = () + help _ _ = () + + +-------------------------------------------------------------------------------- +-- | Gecode monad definition +-------------------------------------------------------------------------------- + +data RuntimeGecodeSolver s => GecodeState s = GecodeState { spaceRef :: Space, cexpr :: Map (ExprKey (FDTerm s)) Int } + + +newtype RuntimeSolver a = RuntimeSolver { rStateM :: StateT (GecodeState RuntimeSolver) IO a } + deriving (Monad, MonadState (GecodeState RuntimeSolver), MonadIO) +newtype SearchSolver a = SearchSolver { sStateM :: StateT (GecodeState SearchSolver) IO a } + deriving (Monad, MonadState (GecodeState SearchSolver), MonadIO) + +newState :: RuntimeGecodeSolver s => Bool -> IO (GecodeState s) +newState gcs = do + initSpace <- newSpace + return $ GecodeState { spaceRef = initSpace, cexpr = Data.Map.empty } + +copyState :: RuntimeGecodeSolver s => GecodeState s -> s (GecodeState s) +copyState state = do + x <- liftIO $ copySpace (spaceRef state) + return $ state { spaceRef = x } + +runRuntimeGecode :: RuntimeGecodeSolver s => Bool -> s a -> (a, GecodeState s) +runRuntimeGecode gcs p = unsafePerformIO $ do + initState <- newState gcs + runStateT (stateM p) initState + +continueRuntimeGecode :: RuntimeGecodeSolver s => GecodeState s -> s a -> (a, GecodeState s) +continueRuntimeGecode st p = unsafePerformIO $ runStateT (stateM p) st + +intTermInfo :: RuntimeGecodeSolver s => IntTerm -> s IntTermInfo +intTermInfo (IntVar i) = do + GecodeState { spaceRef = s } <- get + liftIO $ getIntTermInfo s i + +addRuntimeGecode :: RuntimeGecodeSolver s => GConstraint -> s Bool +addRuntimeGecode (CDom (IntVar i) low high) = proc $ \ptr -> c_gecode_int_dom ptr (toCGIntVar i) (toCGVal low) (toCGVal high) +addRuntimeGecode (CRel (IntVar i1) op (IntVar i2)) = proc $ \ptr -> c_gecode_int_rel ptr (toCGIntVar i1) (mapGOperator op) (toCGIntVar i2) +addRuntimeGecode (CRel (IntConst c1) op (IntVar i2)) = proc $ \ptr -> c_gecode_int_rel_cf ptr (toCGVal c1) (mapGOperator op) (toCGIntVar i2) +addRuntimeGecode (CRel (IntVar i1) op (IntConst c2)) = proc $ \ptr -> c_gecode_int_rel_cs ptr (toCGIntVar i1) (mapGOperator op) (toCGVal c2) +addRuntimeGecode (CValue (IntVar i) val) = proc $ \ptr -> c_gecode_int_value ptr (toCGIntVar i) (toCGVal val) +addRuntimeGecode (CMult (IntVar i1) (IntVar i2) (IntVar ir)) = proc $ \ptr -> c_gecode_int_mult ptr (toCGIntVar i1) (toCGIntVar i2) (toCGIntVar ir) +addRuntimeGecode (CDiv (IntVar i1) (IntVar i2) (IntVar ir)) = proc $ \ptr -> c_gecode_int_div ptr (toCGIntVar i1) (toCGIntVar i2) (toCGIntVar ir) +addRuntimeGecode (CMod (IntVar i1) (IntVar i2) (IntVar ir)) = proc $ \ptr -> c_gecode_int_mod ptr (toCGIntVar i1) (toCGIntVar i2) (toCGIntVar ir) +addRuntimeGecode (CAbs (IntVar i) (IntVar ir)) = proc $ \ptr -> c_gecode_int_abs ptr (toCGIntVar i) (toCGIntVar ir) +addRuntimeGecode (CLinear l op val) = do + GecodeState { spaceRef = s } <- get + let len = length l + let vars = map (\(IntVar var,_) -> toCGIntVar var) l + let coefs = map (\(_,coef) -> toCGVal coef) l + liftIO $ + withArray vars $ \pVars -> + withArray coefs $ \pCoefs -> do + b <- withForeignPtr s $ \ptr -> c_gecode_int_linear ptr (fromIntegral len) pVars pCoefs (mapGOperator op) (toCGVal val) + return $ fromCGBool b +addRuntimeGecode (CAllDiff l) = do + GecodeState { spaceRef = s } <- get + let len = length l + let vars = map (\(IntVar i) -> toCGIntVar i) l + liftIO $ + withArray vars $ \pVars -> do + b <- withForeignPtr s $ \ptr -> c_gecode_int_alldiff ptr (fromIntegral len) pVars + return $ fromCGBool b +addRuntimeGecode (CSorted l strict) = do + GecodeState { spaceRef = s } <- get + let len = length l + let vars = map (\(IntVar i) -> toCGIntVar i) l + liftIO $ + withArray vars $ \pVars -> do + b <- withForeignPtr s $ \ptr -> c_gecode_int_sorted ptr (fromIntegral len) pVars (toCGBool strict) + return $ fromCGBool b + +proc f = do + GecodeState { spaceRef = s } <- get + liftIO $ do + b <- withForeignPtr s f + return $ fromCGBool b + +-------------------------------------------------------------------------------- +-- | RuntimeSolver solver implementation +-------------------------------------------------------------------------------- + +newVarInt :: RuntimeGecodeSolver s => s IntTerm +newVarInt = do + GecodeState { spaceRef = s } <- get + (CGIntVar r) <- liftIO $ withForeignPtr s $ c_gecode_int_newvar + return (IntVar $ fromIntegral r) + +newVarBool :: RuntimeGecodeSolver s => s BoolTerm +newVarBool = do + GecodeState { spaceRef = s } <- get + (CGBoolVar r) <- liftIO $ withForeignPtr s $ c_gecode_bool_newvar + return (BoolVar $ fromIntegral r) + +-------------------------------------------------------------------------------- +-- | RuntimeSolver FDSolver instance +-------------------------------------------------------------------------------- + +instance (RuntimeGecodeSolver s, Ord (FDTerm s)) => GecodeSolver s where + caching_decompose super this x = Label $ do + s <- get + let wx = ExprKey x + case Data.Map.lookup wx (cexpr s) of + Nothing -> return $ do + n@(IntVar i) <- super x + Label $ do + s <- get + put $ s { cexpr = insert wx i $ cexpr s } + return $ return n + Just i -> return $ return $ IntVar i + setVarImplicit (IntVar i) b = return () + +instance FDSolver RuntimeSolver where + type FDTerm RuntimeSolver = IntTerm + specific_compile_constraint = linearCompile <@> basicCompile + specific_decompose = caching_decompose + specific_fresh_var super this = do + v@(IntVar i) <- super + Label $ do + setVarImplicit (IntVar i) True + return $ Return v + +instance FDSolver SearchSolver where + type FDTerm SearchSolver = IntTerm + specific_compile_constraint = linearCompile <@> basicCompile + specific_decompose = caching_decompose + specific_fresh_var super this = do + v@(IntVar i) <- super + Label $ do + setVarImplicit (IntVar i) True + return $ Return v + + +instance EnumTerm RuntimeSolver IntTerm where + type TermDomain RuntimeSolver IntTerm = CInt + get_domain_size v = do + IntTermInfo { iti_size = size } <- intTermInfo v + return $ fromIntegral size + get_value v = do + IntTermInfo { iti_val = val } <- intTermInfo v + return val + split_domain_partial v@(IntVar it) = do + IntTermInfo { iti_val = val, iti_med = med, iti_size = size } <- intTermInfo v + return $ if size == 0 + then [] + else if isJust val + then [return ()] + else [Add (CRel v OLess (IntConst $ (fromIntegral med)+1)) $ enumerate [v],Add (CRel (IntConst $ fromIntegral med) OLess v) $ enumerate [v]] + + +instance EnumTerm SearchSolver IntTerm where + type TermDomain SearchSolver IntTerm = CInt + get_domain_size v = do + IntTermInfo { iti_size = size } <- intTermInfo v + return $ fromIntegral size + get_value v = do + IntTermInfo { iti_val = val } <- intTermInfo v + return val + + split_domains lst = do + let + folder a b = case a of + IntVar i -> (i:b) + _ -> b + let vars = map toCGIntVar $ foldr folder [] lst + state <- get + liftIO $ withArray vars $ \ptr -> withForeignPtr (spaceRef state) $ \sptr -> c_gecode_int_branch sptr (fromIntegral $ length vars) ptr + search <- liftIO $ newSearch $ spaceRef state + let + go i = unsafePerformIO $ do + res <- runSearch search + case res of + Nothing -> return $ return () + Just x -> return $ Try (Label $ do + put state { spaceRef = x } + return $ return () + ) (go $ i+1) + return $ go 0 + + split_domain_partial v = do + x <- split_domains [v] + return [x] + + label _ = Label . split_domains + enumerate = Label . split_domains + +--------------------------------------------- +-- | RuntimeGecodeSolver instances +--------------------------------------------- + +instance RuntimeGecodeSolver RuntimeSolver where + stateM = rStateM + +instance RuntimeGecodeSolver SearchSolver where + stateM = sStateM + +#endif diff --git a/Control/CP/FD/Gecode/Translate.hs b/Control/CP/FD/Gecode/Translate.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Gecode/Translate.hs @@ -0,0 +1,203 @@ +-- optimalisaties: zie http://www.cs.mu.oz.au/~pjs/papers/padl2008.pdf +-- zie ook http://www.cs.mu.oz.au/~pjs/papers/constraints08b.pdf +-- mcp paper: http://www.cs.kuleuven.be/~toms/Research/papers/monadic_cp_draft.pdf + +module Control.CP.FD.Gecode.Translate ( + generate_gecode +) where + +import Maybe (fromJust,isNothing,isJust) +import List (findIndex) +import Data.Map (elems,Map,lookup) + +import Control.CP.FD.Gecode.CodegenSolver +import Control.CP.FD.Gecode.Common +import Control.CP.Solver + +-------------------------------------------------------------------------------- +-- Main compilation function +-------------------------------------------------------------------------------- + +generate_gecode = stateToProg . compile +-- generate_gecode = show . compile + +-------------------------------------------------------------------------------- +-- Implementation +-------------------------------------------------------------------------------- + +countTypeVars :: Store -> GType -> Int -> Int +countTypeVars s t u = foldl (+) 0 $ map (\x -> 1) $ filter (\x -> (u<0 || x Int +maxDepth (StoreNode { cons=_, dis=SNLeaf}) = 1 +maxDepth (StoreNode { cons=_, dis=SNIntl l r }) = 1 + (maxDepth l `max` maxDepth r) + +typeList = [TypeBool, TypeInt] + +varsUsed :: StoreNode -> [ Bool ] -> [ Int ] +varsUsed node path = (nvars node) ++ case (dis node,path) of + (SNLeaf,_) -> [] + (SNIntl l _,[]) -> (varsUsed l []) + (SNIntl l _,False:o) -> varsUsed l o + (SNIntl _ r,True:o) -> varsUsed r o + +typeToString :: GType -> String +typeToString TypeInt = "IntVar" +typeToString TypeBool = "BoolVar" + +typeToDefArgs :: GType -> (String,String) +typeToDefArgs TypeInt = ("-1000000000","1000000000") +typeToDefArgs TypeBool = ("0","1") + +getVarName :: Store -> String -> Int -> String +getVarName s pre i = pre ++ "bb" ++ (typeToString $ getVarType s i) ++ "[" ++ (show $ countTypeVars s (getVarType s i) i) ++ "]" + +getName :: GTerm t => Store -> String -> t -> String +getName s pre v = case (getVarId v) of + Nothing -> case (getIntValue v) of + Nothing -> error "oei" + Just n -> show n + Just i -> getVarName s pre i + +stateToExplList :: Store -> [ (String,String,String) ] +stateToExplList s = map (fm) $ filter (\x -> not $ isVarImplicit s x) $ [0..((vars s)-1)] + where fm i = (typeToString $ getVarType s i,"v"++(show i),getVarName s "" i) + +stateToConstList :: Store -> Map Int VarBound -> [ String ] +stateToConstList s b = map fm $ elems $ b + where fm (VarBound i l u) = (getVarName s "" i) ++ "(*this," ++ (if isJust l then show $ fromJust l else defl) ++ "," ++ (if isJust u then show $ fromJust u else defu) ++ ")" + where (defl,defu) = typeToDefArgs $ getVarType s i + +gopToGCRel :: GOperator -> String +gopToGCRel OEqual = "IRT_EQ" +gopToGCRel ODiff = "IRT_NQ" +gopToGCRel OLess = "IRT_LE" + +gopToInvGCRel :: GOperator -> String +gopToInvGCRel OEqual = "IRT_EQ" +gopToInvGCRel ODiff = "IRT_NQ" +gopToInvGCRel OLess = "IRT_GR" + +stateToPostList :: Store -> [ GConstraint ] -> [ String ] +stateToPostList s c = map fm $ reverse $ c + where fm (CRel t1 o t2) = "rel(home," ++ (gn t1) ++ "," ++ (gopToGCRel o) ++ "," ++ (gn t2) ++ ")" + fm (CMult t1 t2 t3) = "mult(home," ++ (gn t1) ++ "," ++ (gn t2) ++ "," ++ (gn t3) ++ ")" + fm (CDiv t1 t2 t3) = "div(home," ++ (gn t1) ++ "," ++ (gn t2) ++ "," ++ (gn t3) ++ ")" + fm (CMod t1 t2 t3) = "mod(home," ++ (gn t1) ++ "," ++ (gn t2) ++ "," ++ (gn t3) ++ ")" + fm (CAbs t1 t2) = "abs(home," ++ (gn t1) ++ "," ++ (gn t2) ++ ")" + fm (CDom t l u) = "dom(home," ++ (gn t) ++ "," ++ (show l) ++ "," ++ (show u) ++ ")" + fm (CValue t v) = "rel(home," ++ (gn t) ++ ",IRT_EQ," ++ (show v) ++ ")" + fm (CLinear l o c) = case (c,l) of + (0,[(v1,a),(v2,b)]) | a+b==0 && a>0 -> "rel(home," ++ (gn v1) ++ "," ++ (gopToGCRel o) ++ "," ++ (gn v2) ++ ")" + (0,[(v1,a),(v2,b)]) | a+b==0 && a<0 -> "rel(home," ++ (gn v1) ++ "," ++ (gopToInvGCRel o) ++ "," ++ (gn v2) ++ ")" + (_,[(v1,a)]) | a>0 && ((c `mod` a)==0) -> "rel(home," ++ (gn v1) ++ "," ++ (gopToGCRel o) ++ "," ++ (show (c `div` a)) ++ ")" + (_,[(v1,a)]) | a<0 && ((c `mod` (-a))==0) -> "rel(home," ++ (gn v1) ++ "," ++ (gopToInvGCRel o) ++ "," ++ (show (c `div` a)) ++ ")" + (_,l) | all (\(_,a) -> a==1) l -> case unzip l of + (x,a) -> "{ " ++ (bl "iva" x) ++ " linear(home,iva," ++ (gopToGCRel o) ++ "," ++ (show c) ++ "); }" + _ -> case unzip l of + (x,a) -> "{ IntArgs ia(" ++ (show $ length a) ++ (foldl (\x y -> x ++ "," ++ (show y)) "" a) ++ "); "++(bl "iva" x) ++ " linear(home,ia,iva," ++ (gopToGCRel o) ++ "," ++ (show c) ++ "); }" + fm (CAllDiff l) = "{ " ++ (bl "ia" l) ++ "; distinct(home,ia); }" + fm (CSorted l e) = "{ " ++ (bl "ia" l) ++ "; rel(home,ia,"++(if e then "IRT_LQ" else "IRT_LE")++"); }" + gn t = getName s "p->" t + bl n l = "IntVarArgs "++n++"(" ++ (show $ length l) ++ "); " ++ (foldl (++) "" (map (\i -> n++"[" ++ (show i) ++ "]=" ++ (getVarName s "p->" $ fromJust $ getVarId $ l !! i) ++ "; ") [0..(length l)-1])) + +stateToBranchList :: Store -> GType -> [ String ] +stateToBranchList s t = map fm $ filter ff $ [0..((vars s)-1)] + where ff i = (not $ isVarImplicit s i) && (t == getVarType s i) + fm i = getVarName s "" i + +stateToBranchCode s t = " " ++ tn ++ "Args b" ++ tn ++ "(" ++ (show (length vars)) ++ ");\n" ++ ( + foldl (\x y -> x ++ " b" ++ tn ++ "[" ++ (show y) ++ "]=" ++ (vars !! y) ++ ";\n") "" [0..(length vars)-1]) ++ + " branch(*this, b"++tn++", INT_VAR_SIZE_MIN, INT_VAL_SPLIT_MIN);\n" + where tn = typeToString t + vars = stateToBranchList s t + +stateToBranches s = foldl (++) [] $ map (stateToBranchCode s) typeList + +-- countExplicits :: Store -> GType -> Int +-- countExplicits s t = foldl (+) 0 $ map (\x -> if isVarImplicit s x then 0 else 1) $ filter (\x -> t == getVarType s x) $ varsUsed (ctree s) [] + +nodeToProg :: Store -> Map Int VarBound -> StoreNode -> [ Bool ] -> String +nodeToProg store bnds node path = + " static void node" ++ pathS ++ "(Space &home) {\n" ++ + " /* varsused" ++ (show vrs) ++ "*/\n" ++ + " HaskellProg *p = (HaskellProg *)(&home);\n" ++ + (foldl (\x y -> x ++ " " ++ y ++ ";\n") "" $ map (\x -> (getVarName store "p->" x)++".init(home,"++(lowest x)++","++(highest x)++")") $ nvars node) ++ + (foldl (\x y -> x ++ " " ++ y ++ ";\n") "" $ stateToPostList store $ cons node) ++ + (case dis node of + SNLeaf -> (foldl (++) "" $ map (\x -> " rel(home,p->i["++(show x)++"],IRT_EQ,0);\n") [(length path)..(maxDepth $ ctree store)-2]) ++ + (foldl (++) "" $ map (\x -> " rel(home," ++ (getVarName store "p->" x) ++ ",IRT_EQ,"++(lowest x)++");\n") $ filter (\x -> isNothing $ findIndex (== x) vrs) [0..(vars store)-1]) + SNIntl _ _ -> " when(home,p->i[" ++ lenS ++ "],&node"++pathS++"R,&node"++pathS++"L);\n" + ) ++ + " }\n" ++ + (case (dis node) of + SNLeaf -> "" + SNIntl l r -> nodeToProg store bnds l (path ++ [ False ]) ++ nodeToProg store bnds r (path ++ [ True ]) + ) + where pathS = foldl (++) "" $ map (\x -> if x then "R" else "L") path + lenS = show $ length path + vrs = varsUsed (ctree store) path + lowest i = case Data.Map.lookup i bnds of + Nothing -> case typeToDefArgs $ getVarType store i of + (x,_) -> x + Just (VarBound _ Nothing _) -> case typeToDefArgs $ getVarType store i of + (x,_) -> x + Just (VarBound _ (Just l) _) -> show l + highest i = case Data.Map.lookup i bnds of + Nothing -> case typeToDefArgs $ getVarType store i of + (_,x) -> x + Just (VarBound _ _ Nothing) -> case typeToDefArgs $ getVarType store i of + (_,x) -> x + Just (VarBound _ _ (Just l)) -> show l + + +stateToProg :: Store -> String +stateToProg s = + "#include \"gecode/kernel.hh\"\n"++ + "#include \"gecode/support.hh\"\n"++ + "#include \"gecode/int.hh\"\n"++ + "#include \"gecode/search.hh\"\n"++ + "#include \"gecode/minimodel.hh\"\n"++ + "\n"++ + "using namespace Gecode;\n"++ + "\n"++ + "class HaskellProg : public Space {\n"++ + "protected:\n"++ +-- (foldl (\x (y1,y2) -> x ++ " " ++ y1 ++ " " ++ y2 ++ ";\n") "" (stateToDefList s)) ++ + " BoolVarArray i;\n\n"++ + (foldl (++) "" $ map (\x -> " " ++ (typeToString x) ++ "Array bb" ++ (typeToString x) ++ ";\n") typeList) ++ + "public:\n"++ + " HaskellProg() : " ++ + (foldl (\x y -> (if x=="" then "" else x ++ ", ") ++ y) "" $ map (\x -> "bb" ++ typeToString x ++ "(*this," ++ (show $ countTypeVars s x (-1)) ++ ")") typeList) ++ + ", i(*this,"++(show $ (maxDepth (ctree s)) - 1)++",0,1) {\n"++ + " node(*this);\n"++ + " branch(*this, i, INT_VAR_SIZE_MIN, INT_VAL_MIN);\n" ++ stateToBranches s ++ + " };\n"++ + " virtual void print(std::ostream& os) {\n"++ + (foldl (\x (vType,vName,vExpr) -> x ++ " os << \"" ++ vName ++ ": \" << " ++ vExpr ++ " << std::endl;\n") "" (stateToExplList s)) ++ + " }\n"++ + " HaskellProg(bool share, HaskellProg &s) : Space(share,s) {\n"++ +-- (foldl (\x (vType,vName,vExpr) -> x ++ " " ++ vExpr ++ ".update(*this, share, s." ++ vExpr ++ ");\n") "" (stateToExplList s)) ++ + " i.update(*this,share,s.i);\n" ++ + (foldl (\x y -> x ++ " " ++ y ++ ";\n") "" $ map (\x -> "bb" ++ (typeToString x) ++ ".update(*this,share,s.bb"++(typeToString x)++")") typeList) ++ + " }\n"++ + " virtual Space* copy(bool share) {\n"++ + " return new HaskellProg(share, *this);\n"++ + " }\n"++ + nodeToProg s bounds (ctree s) [] ++ + "};\n"++ + "\n"++ + "int main(void) {\n"++ + " HaskellProg *prog=new HaskellProg();\n"++ + " DFS srch(prog);\n"++ + " delete prog;\n"++ + " do {\n"++ + " HaskellProg *sol=srch.next();\n"++ + " if (sol==NULL) break;\n"++ + " sol->print(std::cout);\n"++ + " } while(0);\n"++ + " return 0;\n"++ + "}\n" + where bounds = getAllBounds s + vrs = varsUsed (ctree s) [] diff --git a/Control/CP/FD/OvertonFD/Domain.hs b/Control/CP/FD/OvertonFD/Domain.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/OvertonFD/Domain.hs @@ -0,0 +1,176 @@ +{- + - 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 IncoherentInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +module Control.CP.FD.OvertonFD.Domain ( + Domain, + ToDomain, + toDomain, + member, + isSubsetOf, + elems, + intersection, + difference, + union, + empty, + null, + singleton, + isSingleton, + filterLessThan, + filterGreaterThan, + findMax, + findMin, + size, + shiftDomain, + mapDomain +) where + +import qualified Data.IntSet as IntSet +import Data.IntSet (IntSet) +import Prelude hiding (null) +import Control.CP.Debug + +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 (-10000) 10000 -- minBound maxBound (too sensitive to overflow, e.g. 2 * minBound == 0) + +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 x@(Set xs) = debugDom "[Domain.member]" x $ n `IntSet.member` xs +member n x@(Range xl xh) = debugDom "[Domain.member]" x $ n >= xl && n <= xh + +isSubsetOf :: Domain -> Domain -> Bool +isSubsetOf x@(Set xs) (Set ys) = debugDom "[Domain.isso]" x $ xs `IntSet.isSubsetOf` ys +isSubsetOf x@(Range xl xh) (Range yl yh) = debugDom "[Domain.isso]" x $ xl >= yl && xh <= yh +isSubsetOf x@(Set xs) yd@(Range yl yh) = debugDom "[Domain.isso]" x $ + isSubsetOf (Range xl xh) yd where + xl = IntSet.findMin xs + xh = IntSet.findMax xs +isSubsetOf (Range xl xh) x@(Set ys) = debugDom "[Domain.isso]" x $ + all (`IntSet.member` ys) [xl..xh] + +elems :: Domain -> [Int] +elems x@(Set xs) = debugDom "[Domain.elems]" x $ IntSet.elems xs +elems x@(Range xl xh) = debugDom "[Domain.elems]" x $ [xl..xh] + +intersection :: Domain -> Domain -> Domain +intersection x@(Set xs) (Set ys) = debugDom "[Domain.intersection]" x $ Set (xs `IntSet.intersection` ys) +intersection x@(Range xl xh) (Range yl yh) = debugDom "[Domain.intersection]" x $ Range (max xl yl) (min xh yh) +intersection x@(Set xs) (Range yl yh) = debugDom "[Domain.intersection]" x $ + Set $ IntSet.filter (\x -> x >= yl && x <= yh) xs +intersection x y = intersection y x + +union :: Domain -> Domain -> Domain +union x@(Set xs) (Set ys) = debugDom "[Domain.union]" x $ Set (xs `IntSet.union` ys) +union x@(Range xl xh) (Range yl yh) + | xh + 1 >= yl || yh+1 >= xl = debugDom "[Domain.union]" x $ Range (min xl yl) (max xh yh) + | otherwise = debugDom "[Domain.union]" x $ union (Set $ IntSet.fromList [xl..xh]) (Set $ IntSet.fromList [yl..yh]) +union x@(Set xs) y@(Range yl yh) = debugDom "[Domain.union]" x $ + 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 (x@(Set xs)) (y@(Set ys)) = debugDom "[Domain.difference]" x $ Set (xs `IntSet.difference` ys) +difference xd@(Range xl xh) (Range yl yh) + | yl > xh || yh < xl = debugDom "[Domain.difference]" xd $ xd + | otherwise = debugDom "[Domain.difference]" xd $ Set $ IntSet.fromList [x | x <- [xl..xh], x < yl || x > yh] +difference (x@(Set xs)) (Range yl yh) = + debugDom "[Domain.difference]" x $ Set $ IntSet.filter (\x -> x < yl || x > yh) xs +difference (x@(Range xl xh)) (Set ys) + | IntSet.findMin ys > xh || IntSet.findMax ys < xl = debugDom "[Domain.difference]" x $ Range xl xh + | otherwise = debugDom "[Domain.difference]" x $ Set $ + IntSet.fromList [x | x <- [xl..xh], not (x `IntSet.member` ys)] + +null :: Domain -> Bool +null (x@(Set xs)) = debug ("[Domain.null] " ++ printDom x) $ IntSet.null xs +null (x@(Range xl xh)) = debug ("[Domain.null] " ++ printDom x) $ xl > xh + +singleton :: Int -> Domain +singleton x = Set (IntSet.singleton x) + +isSingleton :: Domain -> Bool +isSingleton (x@(Set xs)) = debugDom "[Domain.isSingleton]" x $ (IntSet.size xs)==1 +isSingleton (x@(Range xl xh)) = debug ("[Domain.isSingleton] " ++ printDom x) $ xl == xh + +filterLessThan :: Int -> Domain -> Domain +filterLessThan n (x@(Set xs)) = debug ("[Domain.filterLess] " ++ printDom x) $ Set $ IntSet.filter (< n) xs +filterLessThan n (x@(Range xl xh)) = debug ("[Domain.filterLess] " ++ printDom x) $ Range xl (min (n-1) xh) + +filterGreaterThan :: Int -> Domain -> Domain +filterGreaterThan n (x@(Set xs)) = debug ("[Domain.filterGreater] " ++ printDom x) $ Set $ IntSet.filter (> n) xs +filterGreaterThan n (x@(Range xl xh)) = debug ("[Domain.filterGreater] " ++ printDom x) $ Range (max (n+1) xl) xh + +findMax :: Domain -> Int +findMax (x@(Set xs)) = debug ("[Domain.findMax] " ++ printDom x) $ IntSet.findMax xs +findMax (x@(Range xl xh)) = debug ("[Domain.findMax] " ++ printDom x) $ 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 (x@(Range l u)) d = debug ("[Domain.shift] " ++ printDom x) $ Range (l + d) (u + d) +shiftDomain (x@(Set xs)) d = debug ("[Domain.shift] " ++ printDom x) $ Set $ IntSet.fromList $ map (+d) (IntSet.elems xs) + +mapDomain :: Domain -> (Int -> [Int]) -> Domain +mapDomain d f = debug ("[Domain.map] " ++ printDom d) $ Set $ IntSet.fromList $ concatMap f $ elems d + +printDom :: Domain -> String +printDom (Set cs) = "dom:Set(#" ++ (show $ IntSet.size cs) ++ ")" +printDom (Range l h) = "dom:Range(#" ++ (show $ h-l+1) ++ ":" ++ (show l) ++ "-" ++ (show h) ++ ")" + +debugDom :: String -> Domain -> a -> a +debugDom s d a = debug ("[Domain.findMax] " ++ printDom d) a diff --git a/Control/CP/FD/OvertonFD/OvertonFD.hs b/Control/CP/FD/OvertonFD/OvertonFD.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/OvertonFD/OvertonFD.hs @@ -0,0 +1,384 @@ +{- + - 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 TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +module Control.CP.FD.OvertonFD.OvertonFD ( + OvertonFD, + fd_objective, + fd_domain, + FDVar, + OConstraint(..), +) 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 Control.CP.FD.OvertonFD.Domain as Domain +import Control.CP.FD.FD +import Control.CP.EnumTerm +import Control.CP.Solver +import Control.CP.SearchTree + +import Control.CP.Debug + +-------------------------------------------------------------------------------- +-- Solver instance ------------------------------------------------------------- +-------------------------------------------------------------------------------- + +data OConstraint = + OHasValue FDVar Int + | OSame FDVar FDVar + | ODiff FDVar FDVar + | OLess FDVar FDVar + | OAdd FDVar FDVar FDVar + | OSub FDVar FDVar FDVar + | OMult FDVar FDVar FDVar + | OAbs FDVar FDVar + +instance Solver OvertonFD where + type Constraint OvertonFD = OConstraint + type Label OvertonFD = FDState + add c = addFD c + run p = runFD p + mark = get + goto = put + +instance Term OvertonFD FDVar where + newvar = newVar () + type Help OvertonFD FDVar = () + help _ _ = () + +instance EnumTerm OvertonFD FDVar where + type TermDomain OvertonFD FDVar = Int + get_domain_size v = do + dom <- debug "get_domain_size:fd_domain" $ fd_domain v + return $ length dom + split_domain_partial v = do + dom <- debug "split_domain:fd_domain" $ fd_domain v + case dom of + [] -> return [ return () ] + _ -> return [ addC $ v `OHasValue` c | c <- dom ] + get_value v = do + x <- debug "get_value:fd_domain" $ fd_domain v + case x of + [val] -> return $ Just val + _ -> return Nothing + +-------------------------------------------------------------------------------- +-- Constraints ----------------------------------------------------------------- +-------------------------------------------------------------------------------- + +addFD (OHasValue v i) = v `hasValue` i +addFD (OSame a b) = a `same` b +addFD (ODiff a b) = a `different` b +addFD (OLess a b) = a .<. b +addFD (OAdd a b c) = addSum a b c +addFD (OSub a b c) = addSub a b c +addFD (OMult a b c) = addMult a b c +addFD (OAbs a b) = addAbs a b + +fd_domain :: FDVar -> OvertonFD [Int] +fd_domain v = do d <- lookup v + return $ elems d + +fd_objective :: OvertonFD FDVar +fd_objective = + do s <- get + return $ objective s + +-------------------------------------------------------------------------------- + +-- The FD monad +newtype OvertonFD a = OvertonFD { 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 :: OvertonFD 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 OvertonFD monad +consistentFD :: OvertonFD Bool +consistentFD = return True + +-- Run the FD monad and produce a lazy list of possible solutions. +runFD :: OvertonFD 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 -> OvertonFD 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 -> OvertonFD [FDVar] +newVars n d = replicateM n (newVar d) + +-- Lookup the current domain of a variable. +lookup :: FDVar -> OvertonFD 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 -> OvertonFD Bool +update x i = do + debug (show x ++ " <- " ++ show i) (return ()) + s <- get + let vm = varMap s + let vi = vm ! x + debug ("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 -> OvertonFD Bool -> OvertonFD () +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 -> OvertonFD 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 -> OvertonFD 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 -> OvertonFD Bool +same = addBinaryConstraint $ \x y -> do + debug "inside same" $ return () + xv <- lookup x + yv <- lookup y + debug (show xv ++ " same " ++ show yv) $ return () + 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 -> OvertonFD 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 one variable to have a value less than the value of another +-- variable. +infix 4 .<. +(.<.) :: FDVar -> FDVar -> OvertonFD 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 :: OvertonFD s a -> OvertonFD 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] -> OvertonFD s [Int] +labelling = mapM label where + label var = do + vals <- lookup var + val <- OvertonFD . lift $ elems vals + var `hasValue` val + return val +-} + +dump :: [FDVar] -> OvertonFD [Domain] +dump = mapM lookup + +-- Add constraint (z = x `op` y) for var z +addArithmeticConstraint :: + (Domain -> Domain -> Domain) -> + (Domain -> Domain -> Domain) -> + (Domain -> Domain -> Domain) -> + FDVar -> FDVar -> FDVar -> OvertonFD Bool +addArithmeticConstraint getZDomain getXDomain getYDomain x y z = do + xv <- lookup x + yv <- lookup y + let constraint z x y getDomain = do + xv <- lookup x + yv <- lookup y + zv <- lookup z + let znew = debug "binaryArith:intersection" $ (debug "binaryArith:zv" $ zv) `intersection` (debug "binaryArith:getDomain" $ getDomain xv yv) + debug ("binaryArith:" ++ show z ++ " before: " ++ show zv ++ show "; after: " ++ show znew) (return ()) + if debug "binaryArith:null?" $ not $ Domain.null (debug "binaryArith:null?:znew" $ znew) + then if (znew /= zv) + then debug ("binaryArith:update") $ update z znew + else return True + else return False + let zConstraint = debug "binaryArith: zConstraint" $ constraint z x y getZDomain + xConstraint = debug "binaryArith: xConstraint" $ constraint x z y getXDomain + yConstraint = debug "binaryArith: yConstraint" $ constraint y z x getYDomain + debug ("addBinaryArith: z x") (return ()) + addConstraint z xConstraint + debug ("addBinaryArith: z y") (return ()) + addConstraint z yConstraint + debug ("addBinaryArith: x z") (return ()) + addConstraint x zConstraint + debug ("addBinaryArith: x y") (return ()) + addConstraint x yConstraint + debug ("addBinaryArith: y z") (return ()) + addConstraint y zConstraint + debug ("addBinaryArith: y x") (return ()) + addConstraint y xConstraint + debug ("addBinaryArith: done") (return ()) + return True + +-- Add constraint (z = op x) for var z +addUnaryArithmeticConstraint :: (Domain -> Domain) -> (Domain -> Domain) -> FDVar -> FDVar -> OvertonFD Bool +addUnaryArithmeticConstraint getZDomain getXDomain x z = do + xv <- lookup x + let constraint z x getDomain = do + xv <- lookup x + zv <- lookup z + let znew = zv `intersection` (getDomain xv) + debug ("unaryArith:" ++ 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 getZDomain + xConstraint = constraint x z getXDomain + addConstraint z xConstraint + addConstraint x zConstraint + return True + +addSum = addArithmeticConstraint getDomainPlus getDomainMinus getDomainMinus + +addSub = addArithmeticConstraint getDomainMinus getDomainPlus (flip getDomainMinus) + +addMult = addArithmeticConstraint getDomainMult getDomainDiv getDomainDiv + +addAbs = addUnaryArithmeticConstraint (\x -> mapDomain x (\i -> [abs i])) (\z -> mapDomain z (\i -> [i,-i])) + +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 = (\d -> debug ("multDomain" ++ show d ++ "=" ++ show xs ++ "*" ++ show ys ) d) $ 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]] diff --git a/Control/CP/FD/OvertonFD/Sugar.hs b/Control/CP/FD/OvertonFD/Sugar.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/OvertonFD/Sugar.hs @@ -0,0 +1,116 @@ +{- + - Monadic Constraint Programming + - http://www.cs.kuleuven.be/~toms/Haskell/ + - Tom Schrijvers + -} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} + +module Control.CP.FD.OvertonFD.Sugar ( + newBound, + newBoundBis, + restart, + restartOpt, +) where + +import Control.CP.SearchTree hiding (label) +import Control.CP.Transformers +import Control.CP.ComposableTransformers +import Control.CP.Queue +import Control.CP.Solver +import Control.CP.Debug +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.EnumTerm +import Control.CP.Mixin + +import qualified Control.CP.PriorityQueue as PriorityQueue +import qualified Data.Sequence +import Control.CP.FD.OvertonFD.OvertonFD + +newBound :: NewBound OvertonFD +newBound = do obj <- fd_objective + (val:_) <- fd_domain obj + l <- mark + return ((\tree -> tree `insertTree` (obj @@< val)) :: forall b . Tree OvertonFD b -> Tree OvertonFD b) + +newBoundBis :: NewBound OvertonFD +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 OvertonFD b -> Tree OvertonFD 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 = run $ eval model q (RestartST (map Seal cs) return) + +restartOpt :: (Queue q, CTransformer c, CForSolver c ~ OvertonFD, + Elem q ~ (Label OvertonFD,Tree OvertonFD (CForResult c),CTreeState c)) + => q -> [c] -> Tree OvertonFD (CForResult c) -> (Int,[CForResult c]) +restartOpt q cs model = run $ eval model q (RestartST (map Seal cs) opt) + where opt tree = newBound >>= \f -> return (f tree) + +-------------------------------------------------------------------------------- +-- SYNTACTIC SUGAR +-------------------------------------------------------------------------------- + +in_domain v (l,u) = Add (Dom (Term v) l u) true + +(@@<) :: FDVar -> Int -> Tree OvertonFD () +v @@< i = (compile_constraint $ Less (Term v) (Const $ toInteger i)) /\ return () + +(@@>) :: FDVar -> Int -> Tree OvertonFD () +v @@> i = (compile_constraint $ Less (Const $ toInteger i) (Term v)) /\ return () + +-------------------------------------------------------------------------------- +-- FD SUGAR +-------------------------------------------------------------------------------- + +instance FDSolver OvertonFD where + type FDTerm OvertonFD = FDVar + specific_compile_constraint = convert + +-- convert :: Mixin (FDConstraint OvertonFD -> Tree OvertonFD Bool) +convert s t (Same a (Const i)) = debug "convert (Same a (Const i))" $ do + va <- decompose a + addT $ OHasValue va $ fromInteger i +convert s t (Same (Const i) a) = debug "convert (Same (Const i) a)" $ do + va <- decompose a + addT $ OHasValue va $ fromInteger i +convert s t (Same (Plus a b) c) = debug "convert (Same (Plus a b) c)" $ do + va <- decompose a + vb <- decompose b + vc <- decompose c + addT $ OAdd va vb vc +convert s t (Same (Minus a b) c) = debug "convert (Same (Minus a b) c)" $ do + va <- decompose a + vb <- decompose b + vc <- decompose c + addT $ OSub va vb vc +convert s t (Same (Mult a b) c) = debug "convert (Same (Mult a b) c)" $ do + va <- decompose a + vb <- decompose b + vc <- decompose c + addT $ OMult va vb vc +convert s t (Same (Abs a) c) = debug "convert (Same (Abs a) c)" $ do + va <- decompose a + vc <- decompose c + addT $ OAbs va vc +convert s t (Same a b@(Plus _ _)) = debug "convert (Same a Plus)" $ convert s t $ Same b a +convert s t (Same a b@(Minus _ _)) = debug "convert (Same a Minus)" $ convert s t $ Same b a +convert s t (Same a b@(Mult _ _)) = debug "convert (Same a Mult)" $ convert s t $ Same b a +convert s t (Same a b@(Abs _)) = debug "convert (Same a Abs)" $ convert s t $ Same b a +convert s t (Same a b) = debug "convert (Same a b)" $ do + va <- decompose a + vb <- decompose b + addT $ OSame va vb +convert s t (Diff a b) = debug "convert (Diff a b)" $ do + va <- decompose a + vb <- decompose b + addT $ ODiff va vb +convert s t (Less a b) = debug "convert (Less a b)" $ do + va <- decompose a + vb <- decompose b + addT $ OLess va vb +convert s t x = debug "convert _" $ s x diff --git a/Control/CP/FD/Solvers.hs b/Control/CP/FD/Solvers.hs new file mode 100644 --- /dev/null +++ b/Control/CP/FD/Solvers.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE CPP #-} + +module Control.CP.FD.Solvers where + +import qualified Control.CP.PriorityQueue as PriorityQueue +import qualified Data.Sequence + +import Control.CP.ComposableTransformers +import Control.CP.SearchTree +import Control.CP.FD.FD +import Control.CP.FD.OvertonFD.Sugar +import Control.CP.FD.OvertonFD.OvertonFD +import Control.CP.FD.Gecode.CodegenSolver + +#ifdef RGECODE +import Control.CP.FD.Gecode.RuntimeSolver +#endif + +-------------------------------------------------------------------------------- +-- FORCE SOLVERS +-------------------------------------------------------------------------------- + +as_overtonfd :: Tree (FDWrapper OvertonFD) a -> Tree (FDWrapper OvertonFD) a +as_overtonfd = id + +as_gecode_codegen :: Tree (FDWrapper CodegenSolver) a -> Tree CodegenSolver a +as_gecode_codegen = unwrap + +#ifdef RGECODE +as_gecode_runtime :: Tree (FDWrapper RuntimeSolver) a -> Tree (FDWrapper RuntimeSolver) a +as_gecode_runtime = id + +as_gecode_search :: Tree (FDWrapper SearchSolver) a -> Tree (FDWrapper SearchSolver) a +as_gecode_search = id +#endif + +------------------------------------------------------------------------------ +-- SEARCH STRATEGIES +------------------------------------------------------------------------------ + +dfs = [] +bfs = Data.Sequence.empty +pfs :: Ord a => PriorityQueue.PriorityQueue a (a,b,c) +pfs = PriorityQueue.empty + +nb :: Int -> CNodeBoundedST s a +nb = CNBST +db :: Int -> CDepthBoundedST s a +db = CDBST +bb :: NewBound s -> CBranchBoundST s a +bb = CBBST +fs :: CFirstSolutionST s a +fs = CFSST +it :: CIdentityCST s a +it = CIST +ra :: Int -> CRandomST s a +ra = CRST +ld :: Int -> CLimitedDiscrepancyST s a +ld = CLDST + diff --git a/Control/CP/Herbrand/Herbrand.hs b/Control/CP/Herbrand/Herbrand.hs --- a/Control/CP/Herbrand/Herbrand.hs +++ b/Control/CP/Herbrand/Herbrand.hs @@ -1,13 +1,25 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE PatternGuards #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PatternGuards #-} -- |This module provides a Herbrand solver. -- -- The type of terms is parameterized by the "HTerm" type class. -module Control.CP.Herbrand.Herbrand where +module Control.CP.Herbrand.Herbrand ( + HTerm(..), + Herbrand(..), + failure, + success, + unify, + shallow_normalize, + registerAction, + HState, + Unify, + initState, + addH, + newvarH +) where import Control.Monad.State.Lazy import Control.Applicative @@ -80,7 +92,8 @@ instance HTerm t => Term (Herbrand t) t where newvar = newvarH - + type Help (Herbrand t) t = () + help _ _ = () initState :: HTerm t => HState t m initState = HState varSupply Data.Map.empty diff --git a/Control/CP/Herbrand/HerbrandT.hs b/Control/CP/Herbrand/HerbrandT.hs --- a/Control/CP/Herbrand/HerbrandT.hs +++ b/Control/CP/Herbrand/HerbrandT.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} @@ -49,6 +48,10 @@ instance (HTerm t, Solver s) => Term (HerbrandT t s) (L t) where newvar = newvarH >>= return . L + type Help (HerbrandT t s) (L t) = () + help _ _ = () instance (HTerm t, Solver s, Term s st) => Term (HerbrandT t s) (R st) where newvar = lift newvar >>= return . R + type Help (HerbrandT t s) (R st) = () + help _ _ = () diff --git a/Control/CP/Herbrand/Prolog.hs b/Control/CP/Herbrand/Prolog.hs --- a/Control/CP/Herbrand/Prolog.hs +++ b/Control/CP/Herbrand/Prolog.hs @@ -30,6 +30,8 @@ instance Term Prolog PrologTerm where newvar = Prolog $ newvar + type Help Prolog PrologTerm = () + help _ _ = () data PConstraint = PrologTerm := PrologTerm | NotFunctor PrologTerm String diff --git a/Control/CP/Herbrand/PrologTerm.hs b/Control/CP/Herbrand/PrologTerm.hs --- a/Control/CP/Herbrand/PrologTerm.hs +++ b/Control/CP/Herbrand/PrologTerm.hs @@ -1,9 +1,8 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -module Control.CP.Herbrand.PrologTerm where +module Control.CP.Herbrand.PrologTerm ( + PrologTerm(..) +) where import Data.List (intersperse) diff --git a/Control/CP/Mixin.hs b/Control/CP/Mixin.hs new file mode 100644 --- /dev/null +++ b/Control/CP/Mixin.hs @@ -0,0 +1,24 @@ +module Control.CP.Mixin ( + Mixin, + (<@>), + mixin, + mixinConst, + mixinId +) where + +type Mixin a = a -> a -> a + +infixl 5 <@> +(<@>) :: Mixin a -> Mixin a -> Mixin a +(f1 <@> f2) s t = f1 (f2 s t) t + +mixin :: Mixin a -> a +mixin f = let + x = f (error "super called in top-level mixin") x + in x + +mixinConst :: a -> a -> a -> a +mixinConst _ _ c = c + +mixinId :: Mixin a +mixinId s _ = s diff --git a/Control/CP/Queue.hs b/Control/CP/Queue.hs --- a/Control/CP/Queue.hs +++ b/Control/CP/Queue.hs @@ -9,7 +9,14 @@ - Tom Schrijvers -} -module Control.CP.Queue where +module Control.CP.Queue ( + Queue, + Elem, + emptyQ, + isEmptyQ, + popQ, + pushQ +) where import qualified Data.Sequence import qualified Control.CP.PriorityQueue as PriorityQueue @@ -32,7 +39,9 @@ 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) +-- popQ (Data.Sequence.viewl -> x Data.Sequence.:< xs) = (x,xs) + popQ l = case Data.Sequence.viewl l of + x Data.Sequence.:< xs -> (x,xs) pushQ = flip (Data.Sequence.|>) instance Ord a => Queue (PriorityQueue.PriorityQueue a (a,b,c)) where diff --git a/Control/CP/SearchTree.hs b/Control/CP/SearchTree.hs --- a/Control/CP/SearchTree.hs +++ b/Control/CP/SearchTree.hs @@ -1,4 +1,3 @@ -{-# OPTIONS_GHC -fglasgow-exts #-} {- - The Tree data type, a generic modelling language for constraint solvers. - @@ -6,10 +5,38 @@ - http://www.cs.kuleuven.be/~toms/Haskell/ - Tom Schrijvers -} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleContexts #-} -module Control.CP.SearchTree where +module Control.CP.SearchTree ( + Tree(..), + transformTree, + bindTree, + insertTree, + (\/), + (/\), + true, + disj, + conj, + disj2, + prim, + addC, + addT, + exist, + forall, + addTo, + false, + exists, + label, + indent, + showTree, + MonadTree, + untree +) where import Control.CP.Solver +import Control.CP.Mixin import Control.Monad import Control.Monad.Reader @@ -18,6 +45,7 @@ import Data.Monoid + ------------------------------------------------------------------------------- ----------------------------------- Tree -------------------------------------- ------------------------------------------------------------------------------- @@ -30,13 +58,14 @@ NewVar :: Term s t => (t -> Tree s a) -> Tree s a -- add a new variable to a tree Label :: s (Tree s a) -> 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 " +transformTree :: Solver s => Mixin (Tree s a -> Tree s a) +transformTree _ _ Fail = Fail +transformTree _ _ (Return x) = Return x +transformTree _ t (Try x y) = Try (t x) (t y) +transformTree _ t (Add c x) = Add c (t x) +transformTree _ t (NewVar f) = NewVar (\x -> t $ f x) +transformTree _ t (Label m) = Label $ m >>= return . t +-- transformTree s _ x = s x instance Solver s => Functor (Tree s) where fmap = liftM @@ -51,15 +80,14 @@ (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) +(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) +(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 @@ -85,10 +113,10 @@ - 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) + - 5) NewVar i f >>= return + - == NewVar i (\v -> f v >>= return) (bind def) + - == NewVar i (\v -> f v) ((co)-induction?) + - == NewVar i f (eta reduction) - 6) Label sm >>= return - == Label (sm >>= \m -> return (m >>= return)) (bind def) - == Label (sm >>= \m -> return m) (co-induction) @@ -112,12 +140,12 @@ - == 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) + - 4) (NewVar i m >>= f) >>= g + - == NewVar i (\v -> m v >>= f) >>= g (bind def) + - == NewVar i (\w -> (\v -> m v >>= f) w >>= g) (bind def) + - == NewVar i (\w -> (m w >>= f) >>= g) (beta reduction) + - == NewVar i (\w -> m w >>= (\x -> f x >>= g)) (co-induction) + - == NewVar i 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)) @@ -164,37 +192,89 @@ true = return () disj :: MonadTree tree => [tree a] -> tree a -disj = foldr (\/) false +disj [] = false +disj a = foldr1 (\/) a conj :: MonadTree tree => [tree ()] -> tree () -conj = foldr (/\) true +conj [] = true +conj a = foldr1 (/\) a -disj2 :: Solver s => [Tree s a] -> Tree s a +disj2 :: MonadTree tree => [tree a] -> tree 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) - + in (disj2 xs) \/ (disj2 ys) + +prim :: MonadTree tree => TreeSolver tree a -> tree a +prim action = label (action >>= return . return) + +addC :: MonadTree tree => Constraint (TreeSolver tree) -> tree () +addC c = c `addTo` true + +addT :: MonadTree tree => Constraint (TreeSolver tree) -> tree Bool +addT c = c `addTo` (return True) + exist :: (MonadTree tree, Term (TreeSolver tree) t) => Int -> ([t] -> tree a) -> tree a exist n ftree = f n [] - where f 0 acc = ftree acc + where f 0 acc = ftree $ reverse acc f n acc = exists $ \v -> f (n-1) (v:acc) -forall :: (Solver s, Term s t) => [t] -> (t -> Tree s ()) -> Tree s () +forall :: (MonadTree tree, Term (TreeSolver tree) t) => [t] -> (t -> tree ()) -> tree () forall list ftree = conj $ map ftree list - -prim :: MonadTree tree => TreeSolver tree a -> tree a -prim action = label (action >>= return . return) -add :: MonadTree tree => Constraint (TreeSolver tree) -> tree () -add c = c `addTo` true +-- Shortcut the search procedure for a Tree that does not contain Try nodes. +-- create a solver monad that returns the result of the Tree, or a specified +-- value upon failure +untree :: Solver s => v -> Tree s v -> s v +untree _ (Return x) = return x +untree _ (Try _ _) = error "convertion of Try nodes to solver is not supported" +untree e (Fail) = return e +untree e (Label s) = s >>= untree e +untree e (Add c t) = (add c) >>= (\x -> if x then untree e t else return e) +untree e (NewVar f) = do + v <- newvar + untree e (f v) -------------------------------------------------------------------------------- ---------------------------- Monad Transformer Instances ----------------------- -------------------------------------------------------------------------------- +-- | show +indent :: Int -> String +indent l = replicate (2*l) ' ' + +showTree :: (Show (Constraint s), Show a, Solver s) => Int -> Tree s a -> s String +showTree l Fail = return $ indent l ++ "Fail\n" +showTree l (Return x) = return $ indent l ++ "Return [" ++ (show x) ++ "]\n" +showTree l (Try a b) = do + m <- mark + s1 <- showTree (l+1) a + goto m + s2 <- showTree (l+1) b + return $ indent l ++ "Try\n" ++ s1 ++ s2 +showTree l (Add c t) = do + s <- showTree (l+1) t + return $ indent l ++ "Add (" ++ (show c) ++ ")\n" ++ s +showTree l (NewVar f) = do + n <- newvar + s <- showTree (l+1) (f n) + return $ indent l ++ "NewVar\n" ++ s +showTree l (Label a) = do + r <- a + s <- showTree (l+1) r + return $ indent l ++ "Label\n" ++ s + +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 " + +---------------------------------------------------------------------- +-- Monad Transformer Instances +---------------------------------------------------------------------- + instance MonadTree t => MonadTree (ReaderT env t) where type TreeSolver (ReaderT env t) = TreeSolver t addTo constraint tree = ReaderT $ \env -> addTo constraint (runReaderT tree env) @@ -202,7 +282,6 @@ l \/ r = ReaderT $ \env -> runReaderT l env \/ runReaderT r env exists f = ReaderT $ \env -> exists (\var -> runReaderT (f var) env) label p = ReaderT $ \env -> label (p >>= \m -> return $ runReaderT m env) - instance (Monoid w, MonadTree t) => MonadTree (WriterT w t) where type TreeSolver (WriterT w t) = TreeSolver t diff --git a/Control/CP/Solver.hs b/Control/CP/Solver.hs --- a/Control/CP/Solver.hs +++ b/Control/CP/Solver.hs @@ -1,4 +1,3 @@ -{-# OPTIONS_GHC -fglasgow-exts #-} {- - The Solver class, a generic interface for constraint solvers. - @@ -6,8 +5,25 @@ - http://www.cs.kuleuven.be/~toms/Haskell/ - Tom Schrijvers -} -module Control.CP.Solver where +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} + +module Control.CP.Solver ( + Solver, + Constraint, + Label, + add, + run, + mark, + goto, + Term, + newvar, + Help, + help +) where + import Control.Monad.Writer import Data.Monoid @@ -17,7 +33,7 @@ -- | the labels type Label solver :: * -- | add a constraint to the current state, and - -- return whethe the resulting state is consistent + -- return whether the resulting state is consistent add :: Constraint solver -> solver Bool -- | run a computation run :: solver a -> a @@ -26,10 +42,13 @@ -- | go to the state with given label goto :: Label solver -> solver () -class Solver solver => Term solver term where +class (Solver solver) => Term solver term where -- | produce a fresh constraint variable newvar :: solver term - + + type Help solver term + help :: solver () -> term -> Help solver term + -- | WriterT decoration of a solver -- useful for producing statistics during solving instance (Monoid w, Solver s) => Solver (WriterT w s) where @@ -42,3 +61,6 @@ instance (Monoid w, Term s t) => Term (WriterT w s) t where newvar = lift newvar + type Help (WriterT w s) t = () + help _ _ = () + diff --git a/Control/CP/Transformers.hs b/Control/CP/Transformers.hs --- a/Control/CP/Transformers.hs +++ b/Control/CP/Transformers.hs @@ -6,11 +6,19 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Rank2Types #-} -module Control.CP.Transformers where +module Control.CP.Transformers ( + eval, + eval', + continue, + NodeBoundedST, + DepthBoundedST, + Transformer(..), +) where import Control.CP.Solver import Control.CP.SearchTree import Control.CP.Queue +import Control.CP.Debug -------------------------------------------------------------------------------- -- EVALUATION @@ -19,8 +27,9 @@ 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 tree q t = debug "eval" $ + 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 @@ -28,7 +37,7 @@ eval' i (Add c k) wl t es ts = do b <- Control.CP.Solver.add 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 <- newvar +eval' i (NewVar f) wl t es ts = do v <- newvar eval' (i+1) (f v) wl t es ts eval' i (Try l r) wl t es ts = do now <- mark diff --git a/examples/AllInterval.hs b/examples/AllInterval.hs new file mode 100644 --- /dev/null +++ b/examples/AllInterval.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE OverlappingInstances #-} + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_single model + +model n = exist n $ \list -> do + allin list (0,n-1) + let dlist = zipWith (\a b -> abs $ a-b) (take (n-1) list) (tail list) + allin dlist (1,n-1) + allDiff list + allDiff dlist + (list!!0) @< (list!!1) + (dlist!!0) @> (dlist!!(n-2)) + return list diff --git a/examples/Alpha.hs b/examples/Alpha.hs new file mode 100644 --- /dev/null +++ b/examples/Alpha.hs @@ -0,0 +1,61 @@ +-- -------------------------------------------------------------------------- +-- Benchmark (Finite Domain) INRIA Rocquencourt - ChLoE Project -- +-- -- +-- Name : alpha.pl -- +-- Title : alphacipher -- +-- Original Source: Daniel Diaz - INRIA France -- +-- Date : January 1993 -- +-- Adapted for MCP: Tom Schrijvers -- +-- -- +-- This problem comes from the news group rec.puzzle. -- +-- The numbers 1 - 26 have been randomly assigned to the letters of the -- +-- alphabet. The numbers beside each word are the total of the values -- +-- assigned to the letters in the word. e.g for LYRE L,Y,R,E might equal -- +-- 5,9,20 and 13 respectively or any other combination that add up to 47. -- +-- Find the value of each letter under the equations: -- +-- -- +-- BALLET 45 GLEE 66 POLKA 59 SONG 61 -- +-- CELLO 43 JAZZ 58 QUARTET 50 SOPRANO 82 -- +-- CONCERT 74 LYRE 47 SAXOPHONE 134 THEME 72 -- +-- FLUTE 30 OBOE 53 SCALE 51 VIOLIN 100 -- +-- FUGUE 50 OPERA 65 SOLO 37 WALTZ 34 -- +-- -- +-- Solution: -- +-- [A, B,C, D, E,F, G, H, I, J, K,L,M, N, O, P,Q, R, S,T,U, V,W, X, Y, Z] -- +-- [5,13,9,16,20,4,24,21,25,17,23,2,8,12,10,19,7,11,15,3,1,26,6,22,14,18] -- +-- -------------------------------------------------------------------------- + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_void model + +model :: FDSolver solver => Tree (FDWrapper solver) [FDExpr solver] +model = + exist 26 $ + \list@[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z] -> + allin list (1,26) /\ + allDiff list /\ + b + a + l + l + e + t @= 45 /\ + c + e + l + l + o @= 43 /\ + c + o + n + c + e + r + t @= 74 /\ + f + l + u + t + e @= 30 /\ + f + u + g + u + e @= 50 /\ + g + l + e + e @= 66 /\ + j + a + z + z @= 58 /\ + l + y + r + e @= 47 /\ + o + b + o + e @= 53 /\ + o + p + e + r + a @= 65 /\ + p + o + l + k + a @= 59 /\ + q + u + a + r + t + e + t @= 50 /\ + s + a + x + o + p + h + o + n + e @= 134 /\ + s + c + a + l + e @= 51 /\ + s + o + l + o @= 37 /\ + s + o + n + g @= 61 /\ + s + o + p + r + a + n + o @= 82 /\ + t + h + e + m + e @= 72 /\ + v + i + o + l + i + n @= 100 /\ + w + a + l + t + z @= 34 /\ + return list diff --git a/examples/Grocery.hs b/examples/Grocery.hs new file mode 100644 --- /dev/null +++ b/examples/Grocery.hs @@ -0,0 +1,21 @@ +-- A kid goes into a grocery store and buys four items. The cashier charges $7.11. +-- The kid pays and is about to leave when the cashier calls the kid back, and says +-- "Hold on, I multiplied the four items instead of adding them; I'll try again... +-- Gosh, with adding them the price still comes to $7.11"! What were the prices of +-- the four items? + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_void model + +model :: FDModel +model = + exist 4 $ \list@[a,b,c,d] -> + list `allin` (0,711) /\ + a + b + c + d @= 711 /\ + (a * b) * (c * d) @= 711*100*100*100 /\ + sorted list /\ + return list diff --git a/examples/MagicSquare.hs b/examples/MagicSquare.hs new file mode 100644 --- /dev/null +++ b/examples/MagicSquare.hs @@ -0,0 +1,31 @@ +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree +import Data.List (transpose) + +main = example_main_single model + +cutAt p l = case (splitAt p l) of + (l,[]) -> [l] + (b,r) -> b:(cutAt p r) +mexist r c = exist (r*c) $ \list -> return $ cutAt c list +lsum v l = (foldl1 (+) l) @= v +diag bc ic m = map (\x -> (m!!x)!!(bc+ic*x)) [0..(length m)-1] + +interleave [] ys = ys +interleave (x:xs) ys = x : (interleave ys xs) + +model n = do + let nn = n*n + let s = nn*(nn+1) `div` (2*n) + let sums = lsum $ cte s + m <- mexist n n + allin (concat m) (1,nn) + conj $ interleave (map sums m) (map sums $ transpose m) + sums $ diag 0 1 m + sums $ diag (n-1) (-1) m + allDiff $ concat m + (m!!0)!!0 @> (m!!0)!!(n-1) + (m!!0)!!0 @> (m!!(n-1))!!0 + return $ concat m diff --git a/examples/Olympic.hs b/examples/Olympic.hs new file mode 100644 --- /dev/null +++ b/examples/Olympic.hs @@ -0,0 +1,51 @@ +{- +% File : olympic.pl +% Author : Neng-Fa ZHOU +% Date : 1993 +% Purpose: solve a puzzle taken from Olympic Arithmetic Contest +/*********************************************************************** + Given ten variables with the following configuration: + + X7 X8 X9 X10 + + X4 X5 X6 + + X2 X1 + + X1 + + We already know that X1 is equal to 3 and want to assign each variable + with a different integer from {1,2,...,10} such that for any three + variables + Xi Xj + + Xk + the following constraint is satisfied: + + |Xi-Xj| = Xk +***********************************************************************/ +-} + + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_void model + +model :: FDSolver solver => Tree (FDWrapper solver) [Expr (FDTerm solver)] +model = + exist 10 $ \list@[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] + -> list `allin` (1,10) /\ + allDiff list /\ + x1 @= 3 /\ + minus x2 x3 x1 /\ + minus x4 x5 x2 /\ + minus x5 x6 x3 /\ + minus x7 x8 x4 /\ + minus x8 x9 x5 /\ + minus x9 x10 x6 /\ + return list + +minus x1 x2 x3 = (abs (x1-x2)) @= x3 diff --git a/examples/Partition.hs b/examples/Partition.hs new file mode 100644 --- /dev/null +++ b/examples/Partition.hs @@ -0,0 +1,73 @@ +-- -------------------------------------------------------------------------- +-- Benchmark (Finite Domain) -- +-- -- +-- Name : partit.pl -- +-- Title : integer partitionning -- +-- Original Source: Daniel Diaz - INRIA France -- +-- Adapted by : Daniel Diaz for GNU Prolog -- +-- Date : September 1993 (modified March 1997) -- +-- -- +-- Partition numbers 1,2,...,N into two groups A and B such that: -- +-- a) A and B have the same length, -- +-- b) sum of numbers in A = sum of numbers in B, -- +-- c) sum of squares of numbers in A = sum of squares of numbers in B. -- +-- -- +-- This problem admits a solution if N is a multiple of 8. -- +-- -- +-- Note: finding a partition of 1,2...,N into 2 groups A and B such that: -- +-- -- +-- Sum (k^p) = Sum l^p -- +-- k in A l in B -- +-- -- +-- admits a solution if N mod 2^(p+1) = 0 (N is a multiple of 2^(p+1)). -- +-- Condition a) is a special case where p=0, b) where p=1 and c) where p=2.-- +-- -- +-- Two redundant constraints are used: -- +-- -- +-- - in order to avoid duplicate solutions (permutations) we impose -- +-- A1 + exist n $ \list2 -> + allin list1 (1,2*n) /\ + allin list2 (1,2*n) /\ + (let list = list1 ++ list2 + in ascending list1 /\ + ascending list2 /\ + head list1 @< head list2 /\ + allDiff list /\ + csum list1 @= csum list2 /\ + csum (square list1) @= csum (square list2) /\ + csum list1 @= (cte $ hs (2*n)) /\ + csum list2 @= (cte $ hs (2*n)) /\ + csum (square list1) @= (cte $ hss (2*n)) /\ + csum (square list2) @= (cte $ hss (2*n)) /\ + return list + ) + +ascending list = sSorted list + +hs, hss :: Int -> Int +hs n = (n * (n + 1)) `div` 4 +hss n = (n * (n + 1) * (2 * n +1)) `div` 12 + +csum l = foldl1 (+) l + +square l = map (\x -> x * x) l diff --git a/examples/Queens.hs b/examples/Queens.hs new file mode 100644 --- /dev/null +++ b/examples/Queens.hs @@ -0,0 +1,20 @@ +{- + - Monadic Constraint Programming + - http://www.cs.kuleuven.be/~toms/Haskell/ + - Tom Schrijvers & Pieter Wuille + -} + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_single nqueens + +nqueens n = + exist n $ \q -> q `allin` (1,n) /\ conj [ + q!!i @/= q!!j /\ + (q!!i) @+ i @/= (q!!j) @+ j /\ + (q!!i) @- i @/= (q!!j) @- j + | i <- [0..n-1], j <- [0..n-1], i > j + ] /\ return q diff --git a/examples/Ring.hs b/examples/Ring.hs new file mode 100644 --- /dev/null +++ b/examples/Ring.hs @@ -0,0 +1,30 @@ +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +import List (tails) +import Data.Map (toList) + +main = example_main_single model + +-- generate a disjunction producing a list of variables, consisting of alr +-- prefixed by up to maxlen new variables +varexist :: FDSolver solver => Int -> [FDExpr solver] -> Tree (FDWrapper solver) [FDExpr solver] +varexist maxlen alr = + if maxlen==0 + then return alr + else return alr \/ (exists $ \x -> varexist (maxlen-1) (x:alr)) + +-- constr list i = (if (i < (length list)-2) then v2 @= v0 * v1 - i else true) /\ v0 @: (-10,10) +constr list i = 2*v1 @= 2*v2 - v0 /\ + v0 @: (-10,10) + where v0 = list !! i + v1 = list !! ((i+1) `mod` (length list)) + v2 = list !! ((i+2) `mod` (length list)) + +model :: FDSolver solver => Int -> Tree (FDWrapper solver) [FDExpr solver] +model n = exists $ \x -> + do list <- varexist n [x] + conj $ [ constr list i | i <- [0..(length list)-1] ] + return list diff --git a/examples/StressDomain.hs b/examples/StressDomain.hs new file mode 100644 --- /dev/null +++ b/examples/StressDomain.hs @@ -0,0 +1,23 @@ +import List (transpose) + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_single model + +cutAt p l = case (splitAt p l) of + (l,[]) -> [l] + (b,r) -> b:(cutAt p r) +mexist r c = exist (r*c) $ \list -> return $ cutAt c list +lsum v l = (foldl1 (+) l) @= v +diag bc ic m = map (\x -> (m!!x)!!(bc+ic*x)) [0..(length m)-1] + +model :: FDSolver solver => Int -> Tree (FDWrapper solver) [FDExpr solver] +model n = exist 5 $ \l -> do + allin l (0,5*n) + let forvar v = conj $ map (\p -> conj $ map (\j -> v @/= 5*j+p) [0..(cte (5*n))]) [0,2,4] + conj $ map forvar $ reverse l + conj $ map (\j -> conj $ map (\v -> v @>= cte (5*j) /\ v @<= cte (5*(j+5*(n `div` 2)))) $ reverse l) [0..5*(n `div` 2)] + return l diff --git a/examples/TryDemo.hs b/examples/TryDemo.hs new file mode 100644 --- /dev/null +++ b/examples/TryDemo.hs @@ -0,0 +1,19 @@ +{- + - Monadic Constraint Programming + - http://www.cs.kuleuven.be/~toms/Haskell/ + - Tom Schrijvers & Pieter Wuille + -} + +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_void model + +model :: FDSolver solver => Tree (FDWrapper solver) [FDExpr solver] +model = exist 2 $ \[a,b] -> a @: (1,5) /\ + b @: (0,4) /\ + a - b @= 1 /\ + (a @= 2 \/ a @= 3 \/ a @= 4) /\ + return [a,b] diff --git a/examples/Zebra.hs b/examples/Zebra.hs new file mode 100644 --- /dev/null +++ b/examples/Zebra.hs @@ -0,0 +1,39 @@ +import Control.CP.FD.Example.Example +import Control.CP.FD.FD +import Control.CP.FD.Expr +import Control.CP.SearchTree + +main = example_main_void model + +model :: FDSolver solver => Tree (FDWrapper solver) [FDExpr solver] +model = + exist 5 $ \ns@[n1,n2,n3,n4,n5] -> + exist 5 $ \cs@[c1,c2,c3,c4,c5] -> + exist 5 $ \ps@[p1,p2,p3,p4,p5] -> + exist 5 $ \as@[a1,a2,a3,a4,a5] -> + exist 5 $ \ds@[d1,d2,d3,d4,d5] -> + let vars = ns ++ cs ++ ps ++ as ++ ds in + vars `allin` (1,5) /\ + allDiff ns /\ + allDiff cs /\ + allDiff ps /\ + allDiff as /\ + allDiff ds /\ + n1 @= c2 /\ + n2 @= a1 /\ + n3 @= p1 /\ + n4 @= d3 /\ + n5 @= 1 /\ + d5 @= 3 /\ + p3 @= d1 /\ + c1 @= d4 /\ + p5 @= a4 /\ + p2 @= c3 /\ + c1 @= c5+1 /\ + plusorminus a3 p4 1 /\ + plusorminus a5 p2 1 /\ + plusorminus n5 c4 1 /\ + return vars + +plusorminus x y c = + x @= y+c \/ x @= y-c diff --git a/lib/gecodeglue.cpp b/lib/gecodeglue.cpp new file mode 100644 --- /dev/null +++ b/lib/gecodeglue.cpp @@ -0,0 +1,380 @@ +#define _interface_cpp_ + +#include +#include + +#include "gecode/kernel.hh" +#include "gecode/support.hh" +#include "gecode/int.hh" +#include "gecode/search.hh" + +#include "gecodeglue.h" + +using namespace std; +using namespace Gecode; + +int static nModels=0; +int static nOrigModels=0; + +class HaskellModel : public Space { +protected: + vector boolVars; + vector intVars; + IntConLevel icl; +#ifndef NDEBUG + int level; + int origNum,num; +#endif +private: + static IntRelType mapGoperator(goperator_t op, bool revert=false) { + switch(op) { + case GOPERATOR_OEQUAL: return IRT_EQ; + case GOPERATOR_ODIFF: return IRT_NQ; + case GOPERATOR_OLESS: return revert ? IRT_GR : IRT_LE; + } +#ifndef NDEBUG + cerr << "(unknown goperator " << op << "\n"; +#endif + assert(0); + } + +public: + HaskellModel() : boolVars(), intVars(), icl(ICL_DEF) +#ifndef NDEBUG + , level(0), origNum(++nOrigModels), num(++nModels) +#endif + { +#ifndef NDEBUG + identify(); cerr << "newmodel\n"; +#endif + } + ~HaskellModel() { +#ifndef NDEBUG + identify(); cerr << "delmodel\n"; +#endif + } + HaskellModel(bool share, HaskellModel &model) : Space(share,model), boolVars(model.boolVars.size()), intVars(model.intVars.size()), icl(model.icl) +#ifndef NDEBUG + , level(model.level+1), origNum(model.origNum), num(++nModels) +#endif + { +#ifndef NDEBUG + identify(); cerr << "newmodel from [" << model.origNum << ":" << model.num << "]\n"; +#endif + for (int i=0; i=0 && var=0 && var=0 && var=0 && var=0 && var1=0 && var2=0 && var1=0 && var2=0 && var1=0 && var2=0 && var2=0 && var1=0 && var1=0 && var2=0 && varr=0 && var1=0 && var2=0 && varr=0 && var1=0 && var2=0 && varr=0 && var=0 && varr=0 && var=0 && id=0 && id=0 && id=0 && id=0 && idclone(true)); } +extern "C" HaskellModel *gecode_model_copy_reentrant(HaskellModel *model) { return (HaskellModel*)(model->clone(false)); } +extern "C" void gecode_model_fail(HaskellModel *model) { model->fail(); } +extern "C" void gecode_model_destroy(HaskellModel *model) { delete model; } +extern "C" int gecode_int_rel(HaskellModel *model, int v1, goperator_t op, int v2) { model->postIntRel(v1,op,v2); return !model->failed(); } +extern "C" int gecode_int_rel_cf(HaskellModel *model, int v1, goperator_t op, int v2) { model->postIntRelCf(v1,op,v2); return !model->failed(); } +extern "C" int gecode_int_rel_cs(HaskellModel *model, int v1, goperator_t op, int v2) { model->postIntRelCs(v1,op,v2); return !model->failed(); } +extern "C" int gecode_int_newvar(HaskellModel *model) { return model->addIntVar(-1000000000,1000000000); } +extern "C" int gecode_int_value(HaskellModel *model, int v, int val) { model->postIntValue(v,val); return !model->failed(); } +extern "C" int gecode_int_mult(HaskellModel *model, int v1, int v2, int vr) { model->postIntMult(v1,v2,vr); return !model->failed(); } +extern "C" int gecode_int_div(HaskellModel *model, int v1, int v2, int vr) { model->postIntDiv(v1,v2,vr); return !model->failed(); } +extern "C" int gecode_int_mod(HaskellModel *model, int v1, int v2, int vr) { model->postIntMod(v1,v2,vr); return !model->failed(); } +extern "C" int gecode_int_abs(HaskellModel *model, int v, int vr) { model->postIntAbs(v,vr); return !model->failed(); } +extern "C" int gecode_int_dom(HaskellModel *model, int v, int low, int high) { model->postIntDom(v,low,high); return !model->failed(); } +extern "C" int gecode_int_linear(HaskellModel *model, int num, int *vars, int *coef, goperator_t op, int val) { model->postIntLinear(num,vars,coef,op,val); return !model->failed(); } +extern "C" int gecode_int_alldiff(HaskellModel *model, int num, int *vars) { model->postIntAlldiff(num,vars); return !model->failed(); } +extern "C" int gecode_int_sorted(HaskellModel *model, int num, int *vars, int strict) { model->postIntSorted(num,vars,strict); return !model->failed(); } +extern "C" void gecode_int_branch(HaskellModel *model, int num, int *vars) { model->postIntBranching(num,vars); } +extern "C" void gecode_int_info(HaskellModel *model, int var, int *min, int *max, int *med, int *size, int *val) { model->getIntInfo(var,min,max,med,size,val); } +extern "C" int gecode_bool_newvar(HaskellModel *model) { return model->addBoolVar(0,1); } +extern "C" void gecode_bool_branch(HaskellModel *model, int num, int *vars) { model->postBoolBranching(num,vars); } + +extern "C" DFS *gecode_search_create(HaskellModel *model) { + DFS *srch=new DFS(model); +#ifndef NDEBUG + model->identify(); cerr << "search " << srch << " created\n"; +#endif + return srch; +} + +extern "C" void gecode_search_destroy(DFS *search) { +#ifndef NDEBUG + cerr << "[search " << search << "] destroyed\n"; +#endif + delete search; +} + +extern "C" HaskellModel *gecode_search_next(DFS *search) { +#ifndef NDEBUG + cerr << "[search " << search << "] requesting next\n"; +#endif + HaskellModel *res=search->next(); +#ifndef NDEBUG + cerr << "[search " << search << "] requested next (" << res << ")\n"; +#endif + return res; +} diff --git a/monadiccp.cabal b/monadiccp.cabal --- a/monadiccp.cabal +++ b/monadiccp.cabal @@ -1,15 +1,41 @@ -Name: monadiccp -Version: 0.5.2 -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: 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: Constraint Programming -Homepage: http://www.cs.kuleuven.be/~toms/Haskell/ -bug-reports: http://trac.haskell.org/monadiccp/ +Name: monadiccp +Version: 0.6 +Description: Monadic Constraint Programming framework +License: BSD3 +License-file: LICENSE +Author: Tom Schrijvers, Pieter Wuille +Maintainer: tom.schrijvers@cs.kuleuven.be +Build-Type: Simple +Category: control +Synopsis: Constraint Programming +Homepage: http://www.cs.kuleuven.be/~toms/Haskell/ +Bug-reports: http://trac.haskell.org/monadiccp/ +Cabal-Version: >=1.6 +Extra-Source-Files: examples/*.hs + +-- examples/Alpha.hs examples/Grocery.hs examples/MagicSquare.hs examples/Olympic.hs examples/Partition.hs examples/Queens.hs examples/Ring.hs examples/StressDomain.hs examples/TryDemo.hs examples/Zebra.hs + +Flag RuntimeGecode + Description: Include the RuntimeSolver and SearchSolver for Gecode. Requires a working Gecode 3.1 installation. + Default: False + +Flag Debug + Description: Generate debug output + Default: False + +library + Build-Depends: base >= 2 && < 4, containers, mtl, haskell98, random + Exposed-Modules: Control.CP.SearchTree Control.CP.Transformers Control.CP.FD.Gecode.Common Control.CP.FD.Gecode.Translate Control.CP.FD.Gecode.CodegenSolver Control.CP.FD.OvertonFD.Sugar Control.CP.FD.OvertonFD.OvertonFD Control.CP.FD.Solvers Control.CP.FD.FD Control.CP.FD.Example.Example Control.CP.FD.Expr Control.CP.Solver Control.CP.ComposableTransformers Control.CP.EnumTerm Control.CP.PriorityQueue Control.CP.Mixin Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog Control.CP.Herbrand.Herbrand Control.CP.Herbrand.HerbrandT Control.CP.Queue + Other-Modules: Control.CP.Debug Control.CP.FD.OvertonFD.Domain + Include-Dirs: lib + if flag(Debug) + CPP-Options: -DDEBUG + CC-Options: "-O1" "-ggdb3" + else + CC-Options: "-O3" "-g0" "-DNDEBUG" + if flag(RuntimeGecode) + C-Sources: lib/gecodeglue.cpp + Extra-Libraries: gecodesupport gecodeset gecodeint gecodekernel gecodesearch + Exposed-Modules: Control.CP.FD.Gecode.RuntimeSolver + Other-Modules: Control.CP.FD.Gecode.Interface + CPP-Options: -DRGECODE