sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Optimization.ExtField

Description

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

Synopsis

- problem :: ConstraintSet

# Documentation

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

problem :: ConstraintSet Source #

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