----------------------------------------------------------------------------- -- | -- 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 = do x <- sInteger "x" y <- sReal "y" z <- sReal "z" maximize "one-x" $ 1 - x constrain $ y .> 0 .&& z .> 5 minimize "min_y" $ 2+y+z minimize "min_z" z