    -----------------------------------------------------------------------------
    -- |
    -- 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 :: ConstraintSet
    problem :: ConstraintSet
    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"

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

                 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
    $ SReal
    y SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SReal
    0 SBool -> SBool -> SBool
    .&& SReal
    z SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SReal
    5
                 String -> SReal -> ConstraintSet
    forall a. Metric a => String -> SBV a -> ConstraintSet
    minimize String
    "min_y" (SReal -> ConstraintSet) -> SReal -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SReal
    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 -> ConstraintSet
    forall a. Metric a => String -> SBV a -> ConstraintSet
    minimize String
    "min_z" SReal
    z