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

    -- | Optimization goals where min/max values might require assignments
    -- to values that are infinite (integer case), or infinite/epsion (real case).
    -- This simple example demostrates 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 + (3.0 * epsilon) :: Real
    --   min_z = 5.0 + (2.0 * epsilon) :: Real
    -- Objective "min_y": Optimal in an extension field:
    --   one-x =                    oo :: Integer
    --   min_y = 7.0 + (3.0 * epsilon) :: Real
    --   min_z = 5.0 + (2.0 * epsilon) :: Real
    -- Objective "min_z": Optimal in an extension field:
    --   one-x =                    oo :: Integer
    --   min_y = 7.0 + (3.0 * epsilon) :: Real
    --   min_z = 5.0 + (2.0 * epsilon) :: Real
    problem :: Goal
    problem :: Goal
    problem = do SInteger
    x <- String -> Symbolic SInteger
    sInteger "x"
                 SReal
    y <- String -> Symbolic SReal
    sReal "y"
                 SReal
    z <- String -> Symbolic SReal
    sReal "z"

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

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

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