-----------------------------------------------------------------------------
-- |
-- 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/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 + (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 String
"x"
             SReal
y <- String -> Symbolic SReal
sReal String
"y"
             SReal
z <- String -> Symbolic SReal
sReal String
"z"

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