    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Optimization.VM
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Solves a VM allocation problem using optimization features
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Optimization.VM where

    import Data.SBV

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | Computer allocation problem:
    --
    --   - We have three virtual machines (VMs) which require 100, 50 and 15 GB hard disk respectively.
    --
    --   - There are three servers with capabilities 100, 75 and 200 GB in that order.
    --
    --   - Find out a way to place VMs into servers in order to
    --
    --        - Minimize the number of servers used
    --
    --        - Minimize the operation cost (the servers have fixed daily costs 10, 5 and 20 USD respectively.)
    --
    -- We have:
    --
    -- >>> optimize Lexicographic allocate
    -- Optimal model:
    --   x11         = False :: Bool
    --   x12         = False :: Bool
    --   x13         =  True :: Bool
    --   x21         = False :: Bool
    --   x22         = False :: Bool
    --   x23         =  True :: Bool
    --   x31         = False :: Bool
    --   x32         = False :: Bool
    --   x33         =  True :: Bool
    --   noOfServers =     1 :: Integer
    --   cost        =    20 :: Integer
    --
    -- That is, we should put all the jobs on the third server, for a total cost of 20.
    allocate :: ConstraintSet
    allocate :: ConstraintSet
    allocate = do
        -- xij means VM i is running on server j
        x1 :: [SBool]
    x1@[SBool
    x11, SBool
    x12, SBool
    x13] <- [String] -> Symbolic [SBool]
    sBools [String
    "x11", String
    "x12", String
    "x13"]
        x2 :: [SBool]
    x2@[SBool
    x21, SBool
    x22, SBool
    x23] <- [String] -> Symbolic [SBool]
    sBools [String
    "x21", String
    "x22", String
    "x23"]
        x3 :: [SBool]
    x3@[SBool
    x31, SBool
    x32, SBool
    x33] <- [String] -> Symbolic [SBool]
    sBools [String
    "x31", String
    "x32", String
    "x33"]

        -- Each job runs on exactly one server
        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> SBool
    pbStronglyMutexed [SBool]
    x1
        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> SBool
    pbStronglyMutexed [SBool]
    x2
        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> SBool
    pbStronglyMutexed [SBool]
    x3

        let need :: [SBool] -> SInteger
            need :: [SBool] -> SInteger
    need [SBool]
    rs = [SInteger] -> SInteger
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
    forall a b. (a -> b) -> a -> b
    $ (SBool -> SInteger -> SInteger)
    -> [SBool] -> [SInteger] -> [SInteger]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\SBool
    r SInteger
    c -> SBool -> SInteger -> SInteger -> SInteger
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    r SInteger
    c SInteger
    0) [SBool]
    rs [SInteger
    100, SInteger
    50, SInteger
    15]

        -- The capacity on each server is respected
        let capacity1 :: SInteger
    capacity1 = [SBool] -> SInteger
    need [SBool
    x11, SBool
    x21, SBool
    x31]
            capacity2 :: SInteger
    capacity2 = [SBool] -> SInteger
    need [SBool
    x12, SBool
    x22, SBool
    x32]
            capacity3 :: SInteger
    capacity3 = [SBool] -> SInteger
    need [SBool
    x13, SBool
    x23, SBool
    x33]

        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SInteger
    capacity1 SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SInteger
    100
        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SInteger
    capacity2 SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<=  SInteger
    75
        SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SInteger
    capacity3 SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SInteger
    200

        -- compute #of servers running:
        let y1 :: SBool
    y1 = [SBool] -> SBool
    sOr [SBool
    x11, SBool
    x21, SBool
    x31]
            y2 :: SBool
    y2 = [SBool] -> SBool
    sOr [SBool
    x12, SBool
    x22, SBool
    x32]
            y3 :: SBool
    y3 = [SBool] -> SBool
    sOr [SBool
    x13, SBool
    x23, SBool
    x33]

            b2n :: SBool -> a
    b2n SBool
    b = SBool -> a -> a -> a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    b a
    1 a
    0

        let noOfServers :: SInteger
    noOfServers = [SInteger] -> SInteger
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
    forall a b. (a -> b) -> a -> b
    $ (SBool -> SInteger) -> [SBool] -> [SInteger]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SInteger
    forall {a}. (Mergeable a, Num a) => SBool -> a
    b2n [SBool
    y1, SBool
    y2, SBool
    y3]

        -- minimize # of servers
        String -> SInteger -> ConstraintSet
    forall a. Metric a => String -> SBV a -> ConstraintSet
    minimize String
    "noOfServers" (SInteger
    noOfServers :: SInteger)

        -- cost on each server
        let cost1 :: SInteger
    cost1 = SBool -> SInteger -> SInteger -> SInteger
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    y1 SInteger
    10 SInteger
    0
            cost2 :: SInteger
    cost2 = SBool -> SInteger -> SInteger -> SInteger
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    y2  SInteger
    5 SInteger
    0
            cost3 :: SInteger
    cost3 = SBool -> SInteger -> SInteger -> SInteger
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    y3 SInteger
    20 SInteger
    0

        -- minimize the total cost
        String -> SInteger -> ConstraintSet
    forall a. Metric a => String -> SBV a -> ConstraintSet
    minimize String
    "cost" (SInteger
    cost1 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    cost2 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    cost3 :: SInteger)