sbv-6.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.Tools.ExpectedValue

Contents

Description

Computing the expected value of a symbolic variable

Synopsis

Computing expected values

expectedValue :: Outputtable a => Symbolic a -> IO [Double] Source #

Given a symbolic computation that produces a value, compute the expected value that value would take if this computation is run with its free variables drawn from uniform distributions of its respective values, satisfying the given constraints specified by constrain and pConstrain calls. This is equivalent to calling expectedValueWith the following parameters: verbose, warm-up round count of 10000, no maximum iteration count, and with convergence margin 0.0001.

expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double] Source #

Generalized version of expectedValue, allowing the user to specify the warm-up count and the convergence factor. Maximum iteration count can also be specified, at which point convergence won't be sought. The boolean controls verbosity.