------------------------------------------------------------------------------
--- 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.
---
--- @author Michael Hanus
--- @version December 2018
------------------------------------------------------------------------------

module CLP.FD
  ( FDConstr, FDExpr, FDRel(..), Option(..), fd
  , allDifferent, domain, sum, scalarProduct, count
  , (=#), (/=#), (<#), (<=#), (>#), (>=#)
  , true, (/\), andC, allC
  , solveFD, solveFDAll, solveFDOne
  ) where

import qualified CLPFD as C
import Control.Findall ( allValues, someValue )

infixl 7 *#
infixl 6 +#, -#
infix  4 =#, /=#, <#, <=#, >#, >=#
infixr 3 /\

------------------------------------------------------------------------------
--- Operations to construct basic constraints.

--- Returns infinite list of FDVars with a given domain.
--- @param min - minimum value for all variables in xs
--- @param max - maximum value for all variables in xs
domain :: Int -> Int -> [FDExpr]
domain min max = genFDVars min max
 where
  genFDVars :: Int -> Int -> [FDExpr]
  genFDVars l u = FDVar l u _ : genFDVars l u

instance Num FDExpr where
  x + y = x +# y
  x - y = x -# y
  x * y = x *# y

  abs _ = error "abs undefined for FD constraints"

  signum _ = error "signum undefined for FD constraints"

  fromInt x = fd x

--- Represent an integer value as an FD expression.
fd :: Int -> FDExpr
fd v = FDInt v

--- 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

--- Conjunction of FD constraints.
(/\) :: FDConstr -> FDConstr -> FDConstr
c1 /\ c2 = FDAnd c1 c2

--- Conjunction of a list of FD constraints.
andC :: [FDConstr] -> FDConstr
andC = foldr (/\) true

--- Maps a constraint abstraction to a list of FD constraints and joins them.
allC :: (a -> FDConstr) -> [a] -> FDConstr
allC c = andC . map c

---------------------------------------------------------------------------
-- Complex constraints.

--- 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

--- "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

---------------------------------------------------------------------------
--- This datatype defines options to control the instantiation of
--- FD variables in the solver ('solveFD').
---
--- @cons LeftMost - The leftmost variable is selected for instantiation (default)
--- @cons FirstFail - The leftmost variable with the smallest domain is selected
---                   (also known as first-fail principle)
--- @cons FirstFailConstrained - The leftmost variable with the smallest domain
---                              and the most constraints on it is selected.
--- @cons Min - The leftmost variable with the smalled lower bound is selected.
--- @cons Max - The leftmost variable with the greatest upper bound is selected.
--- @cons Step - Make a binary choice between `x=#b` and
---              `x/=#b` for the selected variable
---              `x` where `b` is the lower or
---              upper bound of `x` (default).
--- @cons Enum - Make a multiple choice for the selected variable for all the values
---              in its domain.
--- @cons Bisect - Make a binary choice between `x<=#m` and
---                `x>#m` for the selected variable
---                `x` where `m` is the midpoint
---                of the domain `x`
---                (also known as domain splitting).
--- @cons Up - The domain is explored for instantiation in ascending order (default).
--- @cons Down - The domain is explored for instantiation in descending order.
--- @cons All - Enumerate all solutions by backtracking (default).
--- @cons Minimize v - Find a solution that minimizes the domain variable v
---                    (using a branch-and-bound algorithm).
--- @cons Maximize v - Find a solution that maximizes the domain variable v
---                    (using a branch-and-bound algorithm).
--- @cons Assumptions x - The variable x is unified with the number of choices
---                       made by the selected enumeration strategy when
---                       a solution is found.
--- @cons RandomVariable x - Select a random variable for instantiation
---                          where `x` is a seed value for the random numbers
---                          (only supported by SWI-Prolog).
--- @cons RandomValue x - Label variables with random integer values
---                       where `x` is a seed value for the random numbers
---                       (only supported by SWI-Prolog).


data Option = LeftMost
            | FirstFail
            | FirstFailConstrained
            | Min
            | Max
            | Step
            | Enum
            | Bisect
            | Up
            | Down
            | All
            | Minimize Int
            | Maximize Int
            | Assumptions Int
            | RandomVariable Int
            | RandomValue Int

instance Show Option where
  show _ = error "TODO: Show CLP.FD.Option"

------------------------------------------------------------------------
-- Abstract types to represent FD constraints as data.

-- Abstract type for FD expressions:
data FDExpr = FDVar Int Int Int -- variable with domain and value
            | FDInt Int
            | FDBinExp FDOp FDExpr FDExpr

instance Show FDExpr where
  show _ = error "TODO: Show CLP.FD.FDExpr"

data FDOp = Plus | Minus | Times

-- Abstract type for FD constraints:
data FDConstr = FDTrue
  | FDRelCon  FDRel FDExpr FDExpr
  | FDAnd     FDConstr FDConstr
  | FDAllDiff [FDExpr]
  | FDSum     [FDExpr]          FDRel FDExpr
  | FDScalar  [FDExpr] [FDExpr] FDRel FDExpr
  | FDCount   FDExpr   [FDExpr] FDRel FDExpr

------------------------------------------------------------------------
-- The solver is implemented by a transformation into the old CLPFD solver:


--- Computes (non-deterministically) a solution for the FD variables (second
--- argument) w.r.t. constraint (third argument), where
--- the values in the solution correspond to the list of FD variables.
--- The first argument contains options to control the labeling/instantiation
--- of FD variables.
solveFD :: [Option] -> [FDExpr] -> FDConstr -> [Int]
solveFD options cvars constr =
  let domconstr = all fdvar2domain (cvars ++ allFDVars constr)
      tconstr = trC constr
      allvars = map getFDVal cvars
      labelvars = C.labeling (map trO options) allvars
   in (domconstr & tconstr & labelvars) &> allvars
 where
  fdvar2domain e = case e of
    FDVar l u v -> C.domain [v] l u
    _           -> True

--- Computes all solutions for the FD variables (second
--- argument) w.r.t. constraint (third argument), where
--- the values in each solution correspond to the list of FD variables.
--- The first argument contains options to control the labeling/instantiation
--- of FD variables.
solveFDAll :: [Option] -> [FDExpr] -> FDConstr -> [[Int]]
solveFDAll options cvars constr = allValues (solveFD options cvars constr)

--- Computes a single solution for the FD variables (second
--- argument) w.r.t. constraint (third argument), where
--- the values in the solution correspond to the list of FD variables.
--- The first argument contains options to control the labeling/instantiation
--- of FD variables.
solveFDOne :: [Option] -> [FDExpr] -> FDConstr -> [Int]
solveFDOne options cvars constr = someValue (solveFD options cvars constr)

-- 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)
 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 (multi-set) of all variables occurring in a constraint:
allFDVars :: FDConstr -> [FDExpr]
allFDVars FDTrue = []
allFDVars (FDRelCon _ fde1 fde2)     = allEFDVars fde1 ++ allEFDVars fde2
allFDVars (FDAnd      c1 c2)         = allFDVars c1 ++ allFDVars c2
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])

-- 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

trC :: FDConstr -> Bool
trC FDTrue = True
trC (FDRelCon rel fde1 fde2) = (trFDRel rel) (trE fde1) (trE fde2)
trC (FDAnd fde1 fde2) = trC fde1 & trC fde2
trC (FDAllDiff fdvars) = C.allDifferent (map getFDVal fdvars)
trC (FDSum fdvars relop fdv) =
  C.sum (map getFDVal fdvars)
        (trFDRel relop) --(\e1 e2 -> trC (rel (FDInt e1) (FDInt e2)))
        (getFDVal fdv)
trC (FDScalar cs fdvars relop fdv) =
  C.scalarProduct (map getFDVal cs) (map getFDVal fdvars) (trFDRel relop)
                  (getFDVal fdv)
trC (FDCount fdv fdvars relop c) =
  C.count (getFDVal fdv) (map getFDVal fdvars) (trFDRel relop) (getFDVal c)

trE :: FDExpr -> Int
trE (FDVar _ _ v) = v
trE (FDInt i) = i
trE (FDBinExp rel fde1 fde2) = (trFDOp rel) (trE fde1) (trE fde2)

trFDRel :: FDRel -> Int -> Int -> Bool
trFDRel Equ = (C.=#)
trFDRel Neq = (C./=#)
trFDRel Lt  = (C.<#)
trFDRel Leq = (C.<=#)
trFDRel Gt  = (C.>#)
trFDRel Geq = (C.>=#)

trFDOp :: FDOp -> Int -> Int -> Int
trFDOp Plus  = (C.+#)
trFDOp Minus = (C.-#)
trFDOp Times = (C.*#)

trO :: Option -> C.LabelingOption
trO option = case option of
  LeftMost             -> C.LeftMost
  FirstFail            -> C.FirstFail
  FirstFailConstrained -> C.FirstFailConstrained
  Min                  -> C.Min
  Max                  -> C.Max
  Step                 -> C.Step
  Enum                 -> C.Enum                
  Bisect               -> C.Bisect              
  Up                   -> C.Up          
  Down                 -> C.Down                
  All                  -> C.All         
  Minimize n           -> C.Minimize n  
  Maximize n           -> C.Maximize n  
  Assumptions n        -> C.Assumptions n       
  RandomVariable n     -> C.RandomVariable n
  RandomValue n        -> C.RandomValue n

------------------------------------------------------------------------