------------------------------------------------------------------------------ --- Library for finite domain constraint solving. --- --- An FD problem is specified as an expression of type `FDConstr` --- using the constraints and expressions offered in this library. --- FD variables are created by the operation `domain`. --- An FD problem is solved by calling `solveFD` with labeling options, --- the FD variables whose values should be included in the output, --- and a constraint. Hence, the typical program structure to solve --- an FD problem is as follows: --- --- main :: [Int] --- main = --- let fdvars = take n (domain u o) --- fdmodel = {description of FD problem} --- in solveFD {options} fdvars fdmodel --- --- where `n` are the number of variables and `[u..o]` is the --- range of their possible values. --- --- Note that this library defines the operation to describe an FD problem. --- The actual `solveFD` operations are defined in the solver libraries --- which also exports this library. --- --- @author Michael Hanus, Tom Hueser --- @version March 2016 ------------------------------------------------------------------------------ module XFD.FD where import List (nubBy) import qualified Integer as I (abs) infixl 7 *# infixl 6 +#, -# infix 4 =#, /=#, <#, <=#, >#, >=# infixr 3 /\ infixr 2 \/ -------------------------------------------------------------------------------- -- Operations to construct basic constraints. --- Returns an infinite list of named FD variables with given domain --- @param prefix - prefix to use for generated names --- @param lo - minimum value for all variables in xs --- @param up - maximum value for all variables in xs domainWPrefix :: String -> Int -> Int -> [FDExpr] domainWPrefix prf lo up = genFDVars (nameList prefix 1) lo up where prefix :: String prefix = prf ++ (num lo) ++ "_" ++ (num up) ++ "_" num :: Int -> String num i = if i < 0 then "-" ++ (show (- i)) else show i nameList :: String -> Int -> [String] nameList pr i = (pr ++ (show i)) : nameList pr (i+1) genFDVars :: [String] -> Int -> Int -> [FDExpr] genFDVars (n:ns) l u = FDVar n l u _ : genFDVars ns l u genFDVars [] _ _ = [] -- can never choose this rule --- Returns infinite list of named FD variables with given domain and default --- prefix `"fdv_"` --- @param lo - minimum value for all variables in xs --- @param up - maximum value for all variables in xs domain :: Int -> Int -> [FDExpr] domain = domainWPrefix "fdv_" --- Ints as FDExpr fd :: Int -> FDExpr fd x = FDInt x --- Negated FD constraint notC :: FDConstr -> FDConstr notC c = FDNot c --- Addition of FD expressions. (+#) :: FDExpr -> FDExpr -> FDExpr x +# y = FDBinExp Plus x y --- Subtraction of FD expressions. (-#) :: FDExpr -> FDExpr -> FDExpr x -# y = FDBinExp Minus x y --- Multiplication of FD expressions. (*#) :: FDExpr -> FDExpr -> FDExpr x *# y = FDBinExp Times x y --- Equality of FD expressions. (=#) :: FDExpr -> FDExpr -> FDConstr x =# y = FDRelCon Equ x y --- Disequality of FD expressions. (/=#) :: FDExpr -> FDExpr -> FDConstr x /=# y = FDRelCon Neq x y --- "Less than" constraint on FD expressions. (<#) :: FDExpr -> FDExpr -> FDConstr x <# y = FDRelCon Lt x y --- "Less than or equal" constraint on FD expressions. (<=#) :: FDExpr -> FDExpr -> FDConstr x <=# y = FDRelCon Leq x y --- "Greater than" constraint on FD expressions. (>#) :: FDExpr -> FDExpr -> FDConstr x ># y = FDRelCon Gt x y --- "Greater than or equal" constraint on FD expressions. (>=#) :: FDExpr -> FDExpr -> FDConstr x >=# y = FDRelCon Geq x y --- The always satisfied FD constraint. true :: FDConstr true = FDTrue --- The always unsatisfied constraint false :: FDConstr false = FDFalse --- Conjunction of FD constraints. (/\) :: FDConstr -> FDConstr -> FDConstr c1 /\ c2 = FDAnd c1 c2 (\/) :: FDConstr -> FDConstr -> FDConstr c1 \/ c2 = FDOr c1 c2 --- Conjunction of a list of FD constraints. andC :: [FDConstr] -> FDConstr andC = foldr (/\) true --- Disnjunction of a list of FD constraints. orC :: [FDConstr] -> FDConstr orC = foldr (\/) false --- Maps a constraint abstraction to a list of FD constraints and joins them. allC :: (a -> FDConstr) -> [a] -> FDConstr allC c = andC . map c --- "All different" constraint on FD variables. --- @param xs - list of FD variables --- @return satisfied if the FD variables in the argument list xs --- have pairwise different values. allDifferent :: [FDExpr] -> FDConstr allDifferent vs = FDAllDiff vs --- Relates the sum of FD variables with some integer of FD variable. sum :: [FDExpr] -> FDRel -> FDExpr -> FDConstr sum vs rel v = FDSum vs rel v --- `(scalarProduct cs vs relop v)` is satisfied if `(sum (cs*vs) relop v)` --- is satisfied. --- The first argument must be a list of integers. The other arguments are as --- in 'sum'. scalarProduct :: [FDExpr] -> [FDExpr] -> FDRel -> FDExpr -> FDConstr scalarProduct cs vs rel v = FDScalar cs vs rel v --- `(count v vs relop c)` is satisfied if `(n relop c)`, --- where `n` is the number of elements in the --- list of FD variables `vs` that are equal to `v`, is satisfied. --- The first argument must be an integer. The other arguments are as --- in 'sum'. count :: FDExpr -> [FDExpr] -> FDRel -> FDExpr -> FDConstr count v vs rel c = FDCount v vs rel c --- Absolute value of expression. abs :: FDExpr -> FDExpr abs e = FDAbs e -------------------------------------------------------------------------------- -- Abstract types to represent FD constraints as data. -- Abstract type for FD expressions: data FDExpr = FDVar String Int Int Int | FDInt Int | FDBinExp FDOp FDExpr FDExpr | FDAbs FDExpr data FDOp = Plus | Minus | Times --- Possible relations between FD values. --- @cons Equ - Equal --- @cons Neq - Not equal --- @cons Lt - Less than --- @cons Leq - Less than or equal --- @cons Gt - Greater than --- @cons Geq - Greater than or equal data FDRel = Equ | Neq | Lt | Leq | Gt | Geq -- Abstract type for FD constraints: data FDConstr = FDTrue | FDFalse | FDRelCon FDRel FDExpr FDExpr | FDAnd FDConstr FDConstr | FDOr FDConstr FDConstr | FDNot FDConstr | FDAllDiff [FDExpr] | FDSum [FDExpr] FDRel FDExpr | FDScalar [FDExpr] [FDExpr] FDRel FDExpr | FDCount FDExpr [FDExpr] FDRel FDExpr -------------------------------------------------------------------------------- --- Get the name of a FDVar. getFDVarName :: FDExpr -> String getFDVarName var = case var of FDVar n _ _ _ -> n _ -> error "non FDVar has no name" --- Get value (possibly an unbound variable) of an FD expression. getFDVal :: FDExpr -> Int getFDVal var = case var of FDVar _ _ _ v -> v FDInt i -> i FDBinExp fdop fde1 fde2 -> (arithOp fdop) (valOf fde1) (valOf fde2) FDAbs e -> getFDVal e where valOf e = case e of FDInt i -> i FDBinExp op e1 e2 -> (arithOp op) (valOf e1) (valOf e2) _ -> error $ "FD variable or value expected but FD expression found:\n"++ show e arithOp Plus = (+) arithOp Minus = (-) arithOp Times = (*) --- Compute set of all variables occurring in a constraint. allFDVars :: FDConstr -> [FDExpr] allFDVars = (nubBy fdVarEq) . allFDVars' -- compute (multi-set) of all variables occurring in a constraint: allFDVars' :: FDConstr -> [FDExpr] allFDVars' FDTrue = [] allFDVars' FDFalse = [] allFDVars' (FDRelCon _ fde1 fde2) = allEFDVars fde1 ++ allEFDVars fde2 allFDVars' (FDAnd c1 c2) = allFDVars' c1 ++ allFDVars' c2 allFDVars' (FDOr c1 c2) = allFDVars' c1 ++ allFDVars' c2 allFDVars' (FDNot c) = allFDVars' c allFDVars' (FDAllDiff fdvars) = filterVars fdvars allFDVars' (FDSum fdvars _ fdv) = filterVars (fdvars ++ [fdv]) allFDVars' (FDScalar cs fdvars _ fdv) = filterVars (cs ++ fdvars ++ [fdv]) allFDVars' (FDCount fdv fdvars _ c) = filterVars (fdvars ++ [fdv,c]) --- Compute a set of all variables occuring in a list of expressions filterFDVars :: [FDExpr] -> [FDExpr] filterFDVars = (nubBy fdVarEq) . filterVars -- eq relation on FDVars: fdVarEq :: FDExpr -> FDExpr -> Bool fdVarEq v1 v2 = case (v1, v2) of ((FDVar n1 _ _ _), (FDVar n2 _ _ _)) -> n1 == n2 _ -> False -- filter variables in a list of FD expressions filterVars :: [FDExpr] -> [FDExpr] filterVars = concatMap allEFDVars allEFDVars :: FDExpr -> [FDExpr] allEFDVars e = case e of FDVar _ _ _ _ -> [e] FDInt _ -> [] FDBinExp _ e1 e2 -> allEFDVars e1 ++ allEFDVars e2 FDAbs ex -> allEFDVars ex