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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Optimization.ExtField

Description

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

Synopsis

Documentation

problem :: Goal Source #

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 + (2.0 * epsilon) :: Real
  min_z =         5.0 + epsilon :: Real
Objective "min_y": Optimal in an extension field:
  one-x =                    oo :: Integer
  min_y = 7.0 + (2.0 * epsilon) :: Real
  min_z =         5.0 + epsilon :: Real
Objective "min_z": Optimal in an extension field:
  one-x =                    oo :: Integer
  min_y = 7.0 + (2.0 * epsilon) :: Real
  min_z =         5.0 + epsilon :: Real