Documentation.SBV.Examples.Optimization.ExtField

Demonstrates the extension field (oo/epsilon) optimization results.

Documentation

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

problem :: Goal

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