-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Optimization.ExtField
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates the extension field (@oo@/@epsilon@) optimization results.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Optimization.ExtField where

import Data.SBV

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

-- | Optimization goals where min/max values might require assignments
-- to values that are infinite (integer case), or infinite/epsilon (real case).
-- This simple example demonstrates how SBV can be used to extract such values.
--
-- We have:
--
-- >>> optimize Independent problem
-- Objective "one-x": Optimal in an extension field:
--   one-x =  oo :: Integer
--   min_y = 7.0 :: Real
--   min_z = 5.0 :: Real
-- Objective "min_y": Optimal in an extension field:
--   one-x =  oo :: Integer
--   min_y = 7.0 :: Real
--   min_z = 5.0 :: Real
-- Objective "min_z": Optimal in an extension field:
--   one-x =  oo :: Integer
--   min_y = 7.0 :: Real
--   min_z = 5.0 :: Real
problem :: Goal
problem :: Goal
problem = do SBV Integer
x <- String -> Symbolic (SBV Integer)
sInteger String
"x"
             SReal
y <- String -> Symbolic SReal
sReal String
"y"
             SReal
z <- String -> Symbolic SReal
sReal String
"z"

             forall a. Metric a => String -> SBV a -> Goal
maximize String
"one-x" forall a b. (a -> b) -> a -> b
$ SBV Integer
1 forall a. Num a => a -> a -> a
- SBV Integer
x

             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
y forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
0 SBool -> SBool -> SBool
.&& SReal
z forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
5
             forall a. Metric a => String -> SBV a -> Goal
minimize String
"min_y" forall a b. (a -> b) -> a -> b
$ SReal
2forall a. Num a => a -> a -> a
+SReal
yforall a. Num a => a -> a -> a
+SReal
z

             forall a. Metric a => String -> SBV a -> Goal
minimize String
"min_z" SReal
z