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

    module Documentation.SBV.Examples.Optimization.VM where

    import Data.SBV

    -- | The allocation problem. Inspired by: <http://rise4fun.com/Z3/tutorialcontent/optimization#h25>
    --
    --   - 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 :: Goal
    allocate = do
        -- xij means VM i is running on server j
        x1@[x11, x12, x13] <- sBools ["x11", "x12", "x13"]
        x2@[x21, x22, x23] <- sBools ["x21", "x22", "x23"]
        x3@[x31, x32, x33] <- sBools ["x31", "x32", "x33"]

        -- Each job runs on exactly one server
        constrain $ pbStronglyMutexed x1
        constrain $ pbStronglyMutexed x2
        constrain $ pbStronglyMutexed x3

        let need :: [SBool] -> SInteger
            need rs = sum $ zipWith (\r c -> ite r c 0) rs [100, 50, 15]

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

        constrain $ capacity1 .<= 100
        constrain $ capacity2 .<=  75
        constrain $ capacity3 .<= 200

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

            b2n b = ite b 1 0

        let noOfServers = sum $ map b2n [y1, y2, y3]

        -- minimize # of servers
        minimize "noOfServers" (noOfServers :: SInteger)

        -- cost on each server
        let cost1 = ite y1 10 0
            cost2 = ite y2  5 0
            cost3 = ite y3 20 0

        -- minimize the total cost
        minimize "cost" (cost1 + cost2 + cost3 :: SInteger)