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

-- | 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 :: Goal
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 -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
pbStronglyMutexed [SBool]
x1
    SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
pbStronglyMutexed [SBool]
x2
    SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
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 (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 -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SInteger
capacity1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
100
    SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SInteger
capacity2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=  SInteger
75
    SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
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 (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 -> Goal
forall a. Metric a => String -> SBV a -> Goal
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 -> Goal
forall a. Metric a => String -> SBV a -> Goal
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)